Looks like prove_general_recursive_function_exists has me on the path to
solving this problem, so no need to reply now. Thanks
-Jesse
________________________________
From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] On Behalf Of Bingham,
Jesse D
Sent: Tuesday, July 22, 2008 12:55 AM
To: [email protected]
Subject: [Hol-info] recursive defs in HOL light
How does one do general recursive definitions in HOL light,
analogously to how HOL4 allows the user to supply a measure function to
prove termination? HOL light has new_recursive_definition, but this
seems to require the recursion to follow the structure of a recursive
data type. Here's an example where this is not the case:
define `f n = n-1`;;
(* this fails, i guess because the recursion doesn't follow
exactly how num is typedef'd *)
new_recursive_definition num_RECURSION `(g 0 = 0) /\ (g (SUC n)
= 42 + g (f n))`;;
Thanks
-Jesse
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
