Re: [isabelle] Recdef or Inductive

-------- Original-Nachricht --------
Datum: Mon, 3 Jul 2006 16:10:43 +0200
Von: Temesghen Kahsai <lememta at>
An: isabelle-users at
Betreff: [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

if the type of the argument is given constructor based, i.e. like
datatype C = Name X | Var Y | Pair C C
then you should use a primrec - definition, this will define the measure-function for you :)

primrec Calculate
  "Calculate (Name n) = 0"
  "Calculate (Var n) = 0"
  "Calculate (Pair a b) = Calculate a + Calculate b"


Der GMX SmartSurfer hilft bis zu 70% Ihrer Onlinekosten zu sparen!
Ideal für Modem und ISDN:

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