Email Gateway (Aug 18 2022 at 10:52): Email Gateway (Aug 18 2022 at 10:52):From: Tobias Nipkow <nipkow@in.tum.de>
The `value' command that John Matthews mentioned has been available
since the 2005 version.
Tobias
Simone Cavalheiro schrieb:
Email Gateway (Aug 18 2022 at 10:52):From: Simon Meier <simon.meier@inf.ethz.ch>
Hi Simone,
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
Email Gateway (Aug 18 2022 at 10:57):From: Simone Cavalheiro <simone.cavalheiro@gmail.com>
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
Email Gateway (Aug 18 2022 at 10:57):From: Brian Huffman <brianh@cs.pdx.edu>
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"
Last updated: May 03 2024 at 12:27 UTC