--- a/CookBook/FirstSteps.thy Wed Oct 01 15:40:20 2008 -0400
+++ b/CookBook/FirstSteps.thy Wed Oct 01 20:09:45 2008 -0400
@@ -64,6 +64,8 @@
then Isabelle's undo operation has no effect on the definition of
@{ML "foo"}.
+ (FIXME: add comment about including whole ML-files)
+
During developments you might find it necessary to quickly inspect some data
in your code. This can be done in a ``quick-and-dirty'' fashion using
the function @{ML "warning"}. For example
@@ -75,8 +77,8 @@
text {*
will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
- PolyML provides a convenient, though quick-and-dirty, method for converting
- arbitrary values into strings, for example:
+ PolyML provides a convenient, though again ``quick-and-dirty'', method for
+ converting arbitrary values into strings, for example:
*}
ML {*
@@ -88,8 +90,8 @@
a function.
*}
-text {* (FIXME: add comment about including ML-files) *}
-
+text {* (FIXME: add here or in the appendix a comment about tracing) *}
+text {* (FIXME: maybe a comment about redirecting the trace information) *}
section {* Antiquotations *}
@@ -106,7 +108,7 @@
text {*
where @{text "@{theory}"} is an antiquotation that is substituted with the
current theory (remember that we assumed we are inside the theory CookBook).
- The name of this theory can be extrated using the function @{ML "Context.theory_name"}.
+ The name of this theory can be extracted using the function @{ML "Context.theory_name"}.
So the code above returns the string @{ML "\"CookBook\""}.
Note, however, that antiquotations are statically scoped, that is the value is
@@ -135,7 +137,7 @@
text {*
In the course of this introduction, we will learn more about
- these antoquotations: they greatly simplify Isabelle programming since one
+ these antiquotations: they greatly simplify Isabelle programming since one
can directly access all kinds of logical elements from ML.
*}
@@ -151,8 +153,8 @@
text {*
This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
- representation of this term. This internal represenation corresponds to the
- datatype defined in @{ML_file "Pure/term.ML"}.
+ representation of this term. This internal representation corresponds to the
+ datatype @{ML_text "term"}.
The internal representation of terms uses the usual de-Bruijn index mechanism where bound
variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
@@ -161,14 +163,16 @@
kept at abstractions for printing purposes, and so should be treated only as comments.
\begin{readmore}
- Terms are described in detail in \ichcite{ch:logic}. Their
+ Terms are described in detail in \isccite{sec:terms}. Their
definition and many useful operations can be found in @{ML_file "Pure/term.ML"}.
\end{readmore}
- Sometimes the internal representation can be surprisingly different
+ Sometimes the internal representation of terms can be surprisingly different
from what you see at the user level, because the layers of
parsing/type checking/pretty printing can be quite elaborate.
+*}
+text {*
\begin{exercise}
Look at the internal term representation of the following terms, and
find out why they are represented like this.
@@ -181,43 +185,45 @@
Hint: The third term is already quite big, and the pretty printer
may omit parts of it by default. If you want to see all of it, you
- can use @{ML "print_depth 50"} to set the limit to a value high enough.
+ can use the following ML funtion to set the limit to a value high
+ enough:
\end{exercise}
+*}
+ML {* print_depth 50 *}
- The anti-quotation @{text "@prop"} constructs terms of proposition type,
- inserting the invisible @{text "Trueprop"} coercion when necessary.
+text {*
+
+ The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
+ inserting the invisible @{text "Trueprop"} coercions whenever necessary.
Consider for example
*}
-ML {* @{term "P x"} *}
+ML {* @{term "P x"} ; @{prop "P x"} *}
-ML {* @{prop "P x"} *}
-
-text {* and *}
+text {* which needs the coercion and *}
-ML {* @{term "P x \<Longrightarrow> Q x"} *}
+ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
-ML {* @{prop "P x \<Longrightarrow> Q x"} *}
+text {* which does not. *}
-section {* Construting Terms Manually *}
+section {* Constructing Terms Manually *}
text {*
While antiquotations are very convenient for constructing terms, they can
- only construct fixed terms. However, one often needs to construct terms dynamially.
- For example in order to write the function that returns the implication
- @{term "\<And>x. P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments, one can
- only write
+ only construct fixed terms. Unfortunately, one often needs to construct terms
+ dynamically. For example, a function that returns the implication
+ @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as input terms
+ can only be written as
*}
ML {*
- fun make_PQ_imp P Q =
+ fun make_imp P Q =
let
- val nat = HOLogic.natT
- val x = Free ("x", nat)
+ val x = @{term "x::nat"}
in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
HOLogic.mk_Trueprop (Q $ x)))
end
@@ -226,45 +232,52 @@
text {*
The reason is that one cannot pass the arguments @{term P} and @{term Q} into
- an antiquotation.
+ an antiquotation, like
+*}
+
+ML {*
+ fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"}
*}
text {*
- The internal names of constants like @{term "zero"} or @{text "+"} are
- often more complex than one first expects. Here, the extra prefixes
- @{text zero_class} and @{text plus_class} are present because the
- constants are defined within a type class. Guessing such internal
- names can be extremely hard, which is why the system provides
- another antiquotation: @{ML "@{const_name plus}"} gives just this
- name. For example
+ To see the difference apply @{text "@{term S}"} and
+ @{text "@{term T}"} to the functions.
+
+
+ One tricky point in constructing terms by hand is to obtain the fully qualified
+ names for constants. For example the names for @{text "zero"} or @{text "+"} are
+ more complex than one first expects, namely @{ML_text "HOL.zero_class.zero"}
+ and @{ML_text "HOL.plus_class.plus"}. The extra prefixes @{ML_text zero_class}
+ and @{ML_text plus_class} are present because these constants are defined
+ within type classes; the prefix @{text "HOL"} indicates in which theory they are
+ defined. Guessing such internal names can sometimes be quite hard. Therefore
+ Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} does the expansion
+ automatically, for example:
*}
-ML {* @{const_name plus} *}
-
-text {* produes the fully qualyfied name of the constant plus. *}
-
-
-
+ML {* @{const_name HOL.zero}; @{const_name plus} *}
text {*
- There are many funtions in @{ML_file "Pure/logic.ML"} and
+ \begin{readmore}
+ There are many functions in @{ML_file "Pure/logic.ML"} and
@{ML_file "HOL/hologic.ML"} that make such manual constructions of terms
- easier. Have a look ther and try to solve the following exercises:
+ easier.\end{readmore}
+
+ Have a look at these files and try to solve the following two exercises:
*}
text {*
- \begin{exercise}
+ \begin{exercise}\label{fun:revsum}
Write a function @{ML_text "rev_sum : term -> term"} that takes a
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
- associates to the left. Try your function on some examples, and see if
- the result typechecks.
+ associates to the left. Try your function on some examples.
\end{exercise}
*}
@@ -298,10 +311,12 @@
section {* Type checking *}
text {*
+
+ (FIXME: Should we say something about types?)
+
We can freely construct and manipulate terms, since they are just
arbitrary unchecked trees. However, we eventually want to see if a
- term is wellformed, or type checks, relative to a theory.
-
+ term is well-formed, or type checks, relative to a theory.
Type checking is done via the function @{ML cterm_of}, which turns
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
Unlike @{ML_type term}s, which are just trees, @{ML_type
@@ -327,37 +342,38 @@
end
*}
+text {*
+
+ \begin{exercise}
+ Check that the function defined in Exercise~\ref{fun:revsum} returns a
+ result that type checks.
+ \end{exercise}
+
+*}
+
section {* Theorems *}
text {*
Just like @{ML_type cterm}s, theorems (of type @{ML_type thm}) are
abstract objects that can only be built by going through the kernel
- interfaces, which means that all your proofs will be checked. The
- basic rules of the Isabelle/Pure logical framework are defined in
- @{ML_file "Pure/thm.ML"}.
+ interfaces, which means that all your proofs will be checked.
- Using these rules, which are just ML functions, you can do simple
- natural deduction proofs on the ML level. For example, the statement
+ To see theorems in ``action'', let us give a proof for the following statement
*}
lemma
assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
and assm\<^isub>2: "P t"
- shows "Q t"
- (*<*)oops(*>*)
+ shows "Q t" (*<*)oops(*>*)
text {*
- can be proved in ML like
- this\footnote{Note that @{text "|>"} is just reverse
+ on the ML level:\footnote{Note that @{text "|>"} is just reverse
application. This combinator, and several variants are defined in
- @{ML_file "Pure/General/basics.ML"}}:
+ @{ML_file "Pure/General/basics.ML"}.}
*}
-
-
ML {*
-
let
val thy = @{theory}
@@ -375,13 +391,15 @@
|> implies_intr assm2
|> implies_intr assm1
end
-
*}
text {*
- For how the functions @{text "assume"}, @{text "forall_elim"} and so on work
- see \ichcite{sec:thms}. (FIXME correct name)
+ \begin{readmore}
+ For how the functions @{text "assume"}, @{text "forall_elim"} etc work
+ see \isccite{sec:thms}. The basic functions for theorems are defined in
+ @{ML_file "Pure/thm.ML"}.
+ \end{readmore}
*}
@@ -389,20 +407,26 @@
section {* Tactical Reasoning *}
text {*
- The goal-oriented tactical style is similar to the @{text apply}
- style at the user level. Reasoning is centered around a \emph{goal},
- which is modified in a sequence of proof steps until it is solved.
+ The goal-oriented tactical style reasoning of the ML level is similar
+ to the @{text apply}-style at the user level, i.e.~the reasoning is centred
+ around a \emph{goal}, which is modified in a sequence of proof steps
+ until it is solved.
A goal (or goal state) is a special @{ML_type thm}, which by
convention is an implication of the form:
@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
- Since the formula @{term C} could potentially be an implication, there is a
+ where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals.
+
+ Since the goal @{term C} can potentially be an implication, there is a
@{text "#"} wrapped around it, which prevents that premises are
misinterpreted as open subgoals. The protection @{text "# :: prop \<Rightarrow>
prop"} is just the identity function and used as a syntactic marker.
- For more on this goals see \ichcite{sec:tactical-goals}. (FIXME name)
+
+ \begin{readmore}
+ For more on goals see \isccite{sec:tactical-goals}.
+ \end{readmore}
Tactics are functions that map a goal state to a (lazy)
sequence of successor states, hence the type of a tactic is
@@ -410,18 +434,18 @@
\begin{readmore}
See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy
- sequences. However one rarly onstructs sequences manually, but uses
- the predefined tactic combinators (tacticals) instead
- (see @{ML_file "Pure/tctical.ML"}).
+ sequences. However in day-to-day Isabelle programming, one rarely
+ constructs sequences explicitly, but uses the predefined tactic
+ combinators (tacticals) instead (see @{ML_file "Pure/tctical.ML"}).
+ (FIXME: Pointer to the old reference manual)
\end{readmore}
- Note, however, that tactics are expected to behave nicely and leave
- the final conclusion @{term C} intact (that is only work on the @{text "A\<^isub>i"}
- representing the subgoals to be proved) with the exception of possibly
- instantiating schematic variables.
+ While tatics can operate on the subgoals (the @{text "A\<^isub>i"} above), they
+ are expected to leave the conclusion @{term C} intact, with the
+ exception of possibly instantiating schematic variables.
- To see how tactics work, let us transcribe a simple apply-style proof from the
- tutorial \cite{isa-tutorial} into ML:
+ To see how tactics work, let us transcribe a simple @{text apply}-style
+ proof from the tutorial \cite{isa-tutorial} into ML:
*}
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"
@@ -437,9 +461,9 @@
To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt params assms goal tac"}
sets up a goal state for proving @{text goal} under the assumptions @{text assms} with
- additional variables @{text params} (the variables that are generalised once the
- goal is proved); @{text "tac"} is a function that returns a tactic (FIXME see non-existing
- explanation in the imp-manual).
+ the variables @{text params} that will be generalised once the
+ goal is proved; @{text "tac"} is a function that returns a tactic having some funny
+ input parameters (FIXME by possibly having an explanation in the implementation-manual).
*}