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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info