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

On Wednesday 03 October 2007, Simone Cavalheiro wrote:
> 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?
>
> Sorry for the basic question.
> Simone
You can evaluate terms using Isabelle's simplifier, as long as all of the
relevant defining equations are declared [simp] (which they usually are, if
the functions have been defined with primrec, recdef, or the function
package).
Try something like this:
lemma "rev [1::nat,2,3] = ?x"
by simp
Isabelle then responds with:
lemma rev [1, 2, 3] = [3, 2, Suc 0]
The "?x" on the right-hand side of the lemma is a "schematic" variable, which
means that Isabelle is free to instantiate it to anything it wants. Behind
the scenes, when the simplifier is given the subgoal "rev [1::nat,2,3] = ?x"
it first simplifies the left-hand side as much as possible, resulting in "[3,
2, Suc 0] = ?x". Then it instantiates "?x" to "[3, 2, Suc 0]" and proves the
result using the reflexivity rule.
Alternatively, the current developer version of Isabelle has a "value" command
that performs evaluation.
value "rev [1::nat,2,3]"
Isabelle then responds with:
"[Suc (Suc (Suc 0)), Suc (Suc 0), Suc 0]"
:: "nat list"
- Brian

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