Re: [isabelle] Recdef or Inductive


On Monday 03 July 2006 16:10, Temesghen Kahsai wrote:
> I would like to define function by induction "Calculate" ,that takes
> a Term (that could be a Name, Variable or a Pair) and return a Nat.
> Ex. Calculate of Name is 0
>         Calculate of Var is 0
>         Calculate of Pair(m,n) is Calculate (m) + Calculate (n)
> Somthing similar to the Fibonacci function. Should I use Recdef or
> Inductive? if I have to use Recdef  how I should map the Term (like:
> measure function λn. n in Fibonacci)?
> Thanks for any advice

your example is simple enough to be defined with "primrec".  Here's how:

  datatype Term = Name
                | Var
                | Pair Term Term

    Calculate :: "Term => nat"

    "Calculate Name = 0"
    "Calculate Var = 0"
    "Calculate (Pair t1 t2) = Calculate t1 + Calculate t2"

If you want to define a more complicated function using "recdef", you will 
need to provide an appropriate measure function of type "Term => nat" (or, 
less conveniently, a termination set of type "(Term \<times> Term) set").  
Note that the datatype package already creates a default "size" function for 
each datatype.  Use

  thm "Term.size"

to view the size function's definition for your Term datatype.  See Sections 
2.4.3 and 3.5 of the Isabelle/HOL Tutorial [1] for further details.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.