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
