# Re: [isabelle] Recdef or Inductive

-------- Original-Nachricht --------
Datum: Mon, 3 Jul 2006 16:10:43 +0200
Von: Temesghen Kahsai <lememta at gmail.com>
An: isabelle-users at cl.cam.ac.uk
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. s.th 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: http://www.gmx.net/de/go/smartsurfer

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