# Re: [isabelle] beginner doubt: how can I evaluate a function?

Hi Simone,

I have just started using and learning Isabelle and
I am trying to evaluate basic functions as, for example, "rev [1::nat, 2 ,
3]". I have done it using
ML code (command ML), but I would like to define my own functions inside a
theory and evaluate them (just to test) before proving some property.
How it can be done inside a theory?

`I assume you are using Isabelle 2005 together with ProofGeneral. Thus
``you are writting an ISAR theory. If you look at the List theory in
`
$ISABELLE_HOME/src/HOL/List.thy

`you will see that the function "rev", which you want to evaluate, is
``defined as:
`
consts
rev :: "'a list => 'a list"
primrec
"rev([]) = []"
"rev(x#xs) = rev(xs) @ [x]"

`This first extends the signature of the List theory with the constant
``"rev" and then defines it as a primitive recursive function. The primrec
``command automatically proves and registers the appropriate
``simplification rules. You can check them by entering:
`
thm rev.simps
The simplifier can then be used to "evaluate" a function as in:
lemma rev_example: "rev [1, 2, 3] = [3, 2,1]"
apply(simp)
done

`The idea behind the ML{* ... *} command is to give users the possibility
``to communicate directly with the ML system on top of which Isabelle is
``built. You will not need it, unless you want to extend Isabelle with
``specialized tactics or you need to peek at Isabelles internal details.
`

`I guess you can find most of the answers to your questions also in the
``tutorial on Isabelle/HOL at
``http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf
`
Have fun,
Simon

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