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.
Not so annoying: the following works.
RW_TAC arith_ss [Ntimes half 2]
Konrad.
On Apr 7, 2008, at 8:01 PM, Michael Norrish wrote:
val half = Define `half(x) = if x = 0 then 0 else if x = 1 then 0
else
1 + half(x - 2)`
-------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
