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.