Augusto Ribeiro wrote:
> I'm trying to prove a simple property over a function. This is the
function:
> - val half = Define `half(x) = if x = 0 then 0 else if x = 1 then 0 else
> 1 + half(x - 2)`
> - g `x >= half x`
> - e (RW_TAC arith_ss [half_def]);
> And I'm trying to prove this goal with the rewrite tactic. The
> problem is this tactic leads to infinite rewrites. Is there any
> other way to do it or is it impossible to do rewrites in recursive
> functions with "if then else" expression. Thank you for the
> attention and help.
As Konrad said, you can't prove this goal only with rewriting, you'll
need to do an induction.
However, I thought I would add that if you want to rewrite safely in
the presence of if-then-else expressions, you can make the simplifier
never look at the branches of an if-then-else with a congruence rule.
Do
val ccong = prove(
``(p = p') ==> ((if p then q else r) = (if p' then q else r))``,
SIMP_TAC (srw_ss()) []);
You can then use the Cong function to add this congruence rule to the
simplifier.
For example,
- SIMP_CONV (srw_ss()) [Cong ccong, half_def] ``half 10``;
> val it = |- half 10 = 5 : thm
If you now want to see how annoying proof with HOL can be, try to
prove
half (x + 4) = half x + 2
This doesn't need an induction.
Michael.
-------------------------------------------------------------------------
This SF.net email is sponsored by the 2008 JavaOne(SM) Conference
Register now and save $200. Hurry, offer ends at 11:59 p.m.,
Monday, April 7! Use priority code J8TLD2.
http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
