[isabelle] Recdef or Inductive



Hi all

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

-T



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