I am trying to define three mutually recursive functions.
I initially defined them using the following approach
Define
`( =
if then else
)
/\
( =
if then else
)
/\
( =
if then else
)
`;
I defined what I need for num; however, I need to have it defined for
rational (it will be good if I can define it for real).
I was not able to accomplish this even for int.
Following is an example of an error that I got:
Define
`H x:int = if x <= 0 then 0 else
x + H (x - 1)`;
Exception raised at TotalDefn.Define:
roughly between line 14, character 2 and line 15, character 17:
at TotalDefn.primDefine:
Unable to prove totality!
Use "Defn.Hol_defn" to make the definition,
and "Defn.tgoal <defn>" to set up the termination proof.
! Uncaught exception:
! HOL_ERR
I then tried using inductive approach with a base and step. Small
examples work for num, but, I also have problem in making it works for
other than num.
Is it possible to explixitely define the type of the variable using
this approach for a recursive function (how can this be done to the
second H function below).
- Define `
(H 0 = 0) /\
(H (SUC x) = (1+ (H x)))
`;
Definition has been stored under "H_def".
> val it = |- (H 0 = 0) /\ !x. H (SUC x) = 1 + H x : thm
-
- Define `
(H 0 = 0) /\
(H (x + 1) = (1+ (H x)))
`;
Exception raised at TotalDefn.Define:
between line 6, character 8 and line 7, character 31:
at Defn.mk_defn:
at Functional.mk_case:
Some patterns are not constructors or variables but contain free variables
! Uncaught exception:
! HOL_ERR
- load "ratTheory";
> val it = () : unit
- Define `
(H 0 = 0) /\
(H (x + 1/2) = (1+ (H x)))
`;
<<HOL message: more than one resolution of overloading was possible>>
Exception raised at TotalDefn.Define:
between line 16, character 8 and line 17, character 33:
at Defn.mk_defn:
at Functional.mk_case:
Some patterns are not constructors or variables but contain free variables
! Uncaught exception:
! HOL_ERR
Walid
-------------------------------------------------------------------------
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
