Dear All,
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.
Cheers,
Augusto
-------------------------------------------------------------------------
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
