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

Reply via email to