Hi Augusto:
1. One way to control rewriting is to attach a tag to the
rewrite rule that will set a limit on how many times it is
expanded.
RW_TAC arith_ss [Once half]
2. You will need to use induction to prove your goal. You can
use math. induction via
Induct
but you will then need to do some case-splitting. For this
proof it is simpler to use the induction coming from the
definition of "half"
val half_ind = fetch "-" "half_ind";
g `!x. x >= half x`;
e (recInduct half_ind);
e (REPEAT STRIP_TAC);
e (RW_TAC arith_ss [Once half]);
Cheers,
Konrad.
On Apr 7, 2008, at 3:57 AM, Augusto Ribeiro wrote:
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
-------------------------------------------------------------------------
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
