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.