--- a/CookBook/FirstSteps.thy Sat Nov 01 15:20:36 2008 +0100
+++ b/CookBook/FirstSteps.thy Mon Nov 24 02:51:08 2008 +0100
@@ -28,7 +28,7 @@
text {*
The easiest and quickest way to include code in a theory is
- by using the \isacommand{ML} command. For example\smallskip
+ by using the \isacommand{ML}-command. For example\smallskip
\isa{\isacommand{ML}
\isacharverbatimopen\isanewline
@@ -36,11 +36,11 @@
\isacharverbatimclose\isanewline
@{ML_text "> 7"}\smallskip}
- Expressions inside \isacommand{ML} commands are immediately evaluated,
+ Expressions inside \isacommand{ML}-commands are immediately evaluated,
like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of
- your Isabelle environment. The code inside the \isacommand{ML} command
+ your Isabelle environment. The code inside the \isacommand{ML}-command
can also contain value and function bindings, and even those can be
- undone when the proof script is retracted. From now on we will drop the
+ undone when the proof script is retracted. In what follows we will drop the
\isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
we show code and its response.
@@ -81,10 +81,10 @@
a function.
The funtion @{ML "warning"} should only be used for testing purposes, because any
- output this funtion generates will be overwritten, as soon as an error is
+ output this funtion generates will be overwritten as soon as an error is
raised. Therefore for printing anything more serious and elaborate, the
function @{ML tracing} should be used. This function writes all output into
- a separate tracing buffer.
+ a separate tracing buffer. For example
@{ML [display] "tracing \"foo\""}
@@ -119,18 +119,19 @@
section {* Antiquotations *}
text {*
- The main advantage of embedding all code
- in a theory is that the code can contain references to entities defined
- on the logical level of Isabelle. This is done using antiquotations.
- For example, one can print out the name of
- the current theory by typing
+ The main advantage of embedding all code in a theory is that the code can
+ contain references to entities defined on the logical level of Isabelle (by
+ this we mean definitions, theorems, terms and so on). This is done using
+ antiquotations. For example, one can print out the name of the current
+ theory by typing
+
@{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"}
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 extracted using the function
- @{ML "Context.theory_name"}.
+ current theory (remember that we assumed we are inside the theory
+ @{ML_text FirstSteps}). The name of this theory can be extracted using
+ the function @{ML "Context.theory_name"}.
Note, however, that antiquotations are statically scoped, that is the value is
determined at ``compile-time'', not ``run-time''. For example the function
@@ -155,7 +156,7 @@
@{ML [display] "@{thm allI}"}
@{ML [display] "@{simpset}"}
- While antiquotations have many applications, they were originally introduced to
+ While antiquotations nowadays have many applications, they were originally introduced to
avoid explicit bindings for theorems such as
*}
@@ -164,19 +165,21 @@
*}
text {*
- These bindings were difficult to maintain and also could be accidentally overwritten
- by the user. This usually broke definitional packages. Antiquotations solve this
- problem, since they are ``linked'' statically at compile time. In the course of this
- introduction, we will learn more about these antiquotations: they greatly simplify
- Isabelle programming since one can directly access all kinds of logical elements
- from ML.
+ These bindings were difficult to maintain and also could be accidentally
+ overwritten by the user. This usually broke definitional
+ packages. Antiquotations solve this problem, since they are ``linked''
+ statically at compile-time. However, that also sometimes limits there
+ applicability. In the course of this introduction, we will learn more about
+ these antiquotations: they greatly simplify Isabelle programming since one
+ can directly access all kinds of logical elements from ML.
+
*}
section {* Terms and Types *}
text {*
- One way to construct terms of Isabelle on the ML level is by using the antiquotation
- \mbox{@{text "@{term \<dots>}"}}:
+ One way to construct terms of Isabelle on the ML-level is by using the antiquotation
+ \mbox{@{text "@{term \<dots>}"}}. For example
@{ML_response [display] "@{term \"(a::nat) + b = c\"}"
"Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
@@ -292,18 +295,33 @@
which theory they are defined. Guessing such internal names can sometimes be quite hard.
Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the
expansion automatically, for example:
-*}
-
-text {*
+
+ @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"}
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
- (FIXME: how to construct types manually)
+ Similarly, types can be constructed for example as follows:
+
+*}
+
+ML {*
+fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2])
+*}
+
+text {*
+ which can be equally written as
+*}
+
+ML {*
+fun make_fun_type tau1 tau2 = tau1 --> tau2
+*}
+
+text {*
\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.\end{readmore}
+ and types easier.\end{readmore}
Have a look at these files and try to solve the following two exercises:
@@ -327,14 +345,14 @@
*}
-section {* Type Checking *}
+section {* Type-Checking *}
text {*
We can freely construct and manipulate terms, since they are just
arbitrary unchecked trees. However, we eventually want to see if a
term is well-formed, or type checks, relative to a theory.
- Type checking is done via the function @{ML cterm_of}, which turns
+ 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
"cterm"}s are abstract objects that are guaranteed to be
@@ -386,7 +404,7 @@
shows "Q t" (*<*)oops(*>*)
text {*
- on the ML level:\footnote{Note that @{text "|>"} is reverse
+ on the ML-level:\footnote{Note that @{text "|>"} is reverse
application. This combinator, and several variants are defined in
@{ML_file "Pure/General/basics.ML"}.}
@@ -395,7 +413,7 @@
val thy = @{theory}
val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
- val assm2 = cterm_of thy @{prop \"((P::nat\<Rightarrow>bool) t)\"}
+ val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}
val Pt_implies_Qt =
assume assm1
@@ -447,14 +465,13 @@
@{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> #(C)"}
- where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open subgoals.
+ 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.
- (FIXME: maybe show how this is printed on the screen)
-
\begin{readmore}
For more on goals see \isccite{sec:tactical-goals}.
\end{readmore}
@@ -476,7 +493,7 @@
exception of possibly instantiating schematic variables.
To see how tactics work, let us transcribe a simple @{text apply}-style
- proof from the tutorial \cite{isa-tutorial} into ML:
+ proof from the tutorial~\cite{isa-tutorial} into ML:
*}
lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P"