Email Gateway (Aug 17 2022 at 14:49): Email Gateway (Aug 17 2022 at 14:49):From: Peter Lammich <Views@gmx.de>
-------- Original-Nachricht --------
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"
Email Gateway (Aug 18 2022 at 09:30):From: Temesghen Kahsai <lememta@gmail.com>
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
Email Gateway (Aug 18 2022 at 09:32):From: Tjark Weber <tjark.weber@gmx.de>
Temesghen,
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
Last updated: May 03 2024 at 12:27 UTC