# Re: [isabelle] Recdef or Inductive

Temesghen,
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
consts
Calculate :: "Term => nat"
primrec
"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.
Best,
Tjark
[1] http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf

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