Hi Walid,
You will need to manually prove that your functions terminate. To do
this, you will need to use entry-points like Hol_defn and WF_REL_TAC.
For example, your H function over the integers can be shown to work as
follows:
open bossLib integerTheory
val H_defn = Hol_defn "H"
`H (x:int) = if x <= 0 then 0 else x + H(x - 1)`
val (H_def, H_ind) = Defn.tprove(H_defn,
WF_REL_TAC `measure (Num o ABS)` THEN
Q.X_GEN_TAC `i` THEN
Q.SPEC_THEN `i` STRIP_ASSUME_TAC INT_NUM_CASES THEN
SRW_TAC [][] THEN
FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [INT_SUB, INT_ABS_NUM]);
val _ = save_thm("H_def", H_def)
I'm afraid the automatic support for definitions such as these is not
well developed at all. The essence of what needs to happen is clear:
you show termination by demonstrating that there is a well-founded
relation between successive arguments to the functions. Often, as
here, it is easy to map the function arguments back into the natural
numbers.
Michael
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
