--- a/CookBook/FirstSteps.thy Wed Oct 29 21:51:25 2008 +0100
+++ b/CookBook/FirstSteps.thy Thu Oct 30 13:36:51 2008 +0100
@@ -24,6 +24,8 @@
section {* Including ML-Code *}
+
+
text {*
The easiest and quickest way to include code in a theory is
by using the \isacommand{ML} command. For example\smallskip
@@ -37,18 +39,8 @@
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
- can also contain value and function bindings. However on such \isacommand{ML}
- commands the undo operation behaves slightly counter-intuitive, because
- if you define\smallskip
-
-\isa{\isacommand{ML}
-\isacharverbatimopen\isanewline
-\hspace{5mm}@{ML_text "val foo = true"}\isanewline
-\isacharverbatimclose\isanewline
-@{ML_text "> true"}\smallskip}
-
- then Isabelle's undo operation has no effect on the definition of
- @{ML_text "foo"}. Note that from now on we will drop the
+ 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
\isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
we show code and its response.
@@ -78,7 +70,7 @@
@{ML [display] "warning \"any string\""}
- will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle.
+ will print out @{ML_text [quotes] "any string"} inside the response buffer of Isabelle.
If you develop under PolyML, then there is a convenient, though again
``quick-and-dirty'', method for converting values into strings,
for example:
@@ -101,7 +93,7 @@
amounts of trace output. This rediretion can be achieved using the code
*}
-ML {*
+ML{*
val strip_specials =
let
fun strip ("\^A" :: _ :: cs) = strip cs
@@ -113,7 +105,7 @@
Output.tracing_fn := (fn s =>
(TextIO.output (stream, (strip_specials s));
TextIO.output (stream, "\n");
- TextIO.flushOut stream));
+ TextIO.flushOut stream));
*}
text {*
@@ -163,8 +155,8 @@
@{ML [display] "@{thm allI}"}
@{ML [display] "@{simpset}"}
- While antiquotations have many uses, they were introduced to avoid explicit
- bindings for theorems such as
+ While antiquotations have many applications, they were originally introduced to
+ avoid explicit bindings for theorems such as
*}
ML {*
@@ -172,14 +164,12 @@
*}
text {*
- These bindings were difficult to maintain and also could be overwritten
- by bindings introduced by the user. This had the potential to break
- definitional packages. This additional layer of maintenance complexity
- can be avoided by using antiquotations, 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. 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 *}
@@ -208,10 +198,8 @@
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.
-*}
+ 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.
@@ -246,24 +234,14 @@
which does not.
Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
-
- *}
-
-
-text {*
@{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
- (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the
- internal representation. Is there a reason for this, that needs to be explained
- here?)
-
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
definition and many useful operations can be found in @{ML_file "Pure/type.ML"}.
\end{readmore}
-
- *}
+*}
section {* Constructing Terms and Types Manually *}
@@ -271,7 +249,7 @@
text {*
While antiquotations are very convenient for constructing terms and types,
- they can only construct fixed terms. Unfortunately, one often needs to construct them
+ they can only construct fixed terms. Unfortunately, one often needs to construct terms
dynamically. For example, a function that returns the implication
@{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
as arguments can only be written as
@@ -289,7 +267,8 @@
text {*
The reason is that one cannot pass the arguments @{term P}, @{term Q} and
- @{term "tau"} into an antiquotation. For example the following does not work.
+ @{term "tau"} into an antiquotation. For example the following does not work as
+ expected.
*}
ML {*
@@ -350,6 +329,8 @@
section {* Type Checking *}
+ML {* cterm_of @{theory} @{term "a + b = c"} *}
+
text {*
We can freely construct and manipulate terms, since they are just
@@ -364,11 +345,15 @@
Type checking is always relative to a theory context. For now we can use
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
- For example we can write:
+ For example we can write
+
+ @{ML_response_fake [display] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
+
+ or use the antiquotation
@{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
- and
+ A slightly more elaborate example is
@{ML_response_fake [display]
"let