--- a/CookBook/FirstSteps.thy Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/FirstSteps.thy Sat Feb 07 12:05:02 2009 +0000
@@ -37,17 +37,18 @@
\end{graybox}
\end{isabelle}
- Like normal Isabelle proof scripts,
- \isacommand{ML}-commands can be evaluated 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, and even those can be
- undone when the proof script is retracted. As mentioned earlier, we will
- drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
- scaffolding whenever we show code.
+ Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
+ evaluated 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, and even those can be undone when the proof
+ script is retracted. As mentioned earlier, we will drop the
+ \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
+ show code. The lines prefixed with @{text ">"} are not part of the
+ code, rather they indicate what the response is when the code is evaluated.
- Once a portion of code is relatively stable, one usually wants to
- export it to a separate ML-file. Such files can then be included in a
- theory by using the \isacommand{uses}-command in the header of the theory, like:
+ Once a portion of code is relatively stable, you usually want to export it
+ to a separate ML-file. Such files can then be included in a theory by using
+ the \isacommand{uses}-command in the header of the theory, like:
\begin{center}
\begin{tabular}{@ {}l}
@@ -115,6 +116,8 @@
@{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
+ See leter on in Section~\ref{sec:printing} for information about printing
+ out data of type @{ML_type term}, @{ML_type cterm} and @{ML_type thm}.
*}
@@ -277,13 +280,12 @@
text {*
While antiquotations are very convenient for constructing terms, they can
- only construct fixed terms (remember they are ``linked'' at
- compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external}
- for a function that pattern-matches over terms and where the patterns are
- constructed using antiquotations. However, 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 type @{term
- "\<tau>"} as arguments can only be written as:
+ only construct fixed terms (remember they are ``linked'' at compile-time).
+ However, you often need 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 type @{term "\<tau>"} as arguments can only be
+ written as:
+
*}
ML{*fun make_imp P Q tau =
@@ -294,7 +296,7 @@
end *}
text {*
- The reason is that one cannot pass the arguments @{term P}, @{term Q} and
+ The reason is that you cannot pass the arguments @{term P}, @{term Q} and
@{term "tau"} into an antiquotation. For example the following does \emph{not} work:
*}
@@ -303,7 +305,7 @@
text {*
To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
to both functions. With @{ML make_imp} we obtain the intended term involving
- @{term "S"}, @{text "T"} and @{text "@{typ nat}"}
+ the given arguments
@{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}"
"Const \<dots> $
@@ -342,8 +344,8 @@
(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
- Similarly, one can construct types manually. For example the function returning
- a function type is as follows:
+ Similarly, you occasionally need to construct types manually. For example
+ the function returning a function type is as follows:
*}
@@ -357,7 +359,7 @@
\begin{readmore}
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
- @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms
+ @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
and types easier.\end{readmore}
Have a look at these files and try to solve the following two exercises:
@@ -403,8 +405,8 @@
text {*
- We can freely construct and manipulate terms, since they are just
- arbitrary unchecked trees. However, we eventually want to see if a
+ You can freely construct and manipulate terms, since they are just
+ arbitrary unchecked trees. However, you 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 converts
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
@@ -415,11 +417,11 @@
Type-checking is always relative to a theory context. For now we use
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
- For example we can write
+ For example you can write:
@{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
- This can also be wirtten with an antiquotation
+ This can also be wirtten with an antiquotation:
@{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
@@ -428,8 +430,7 @@
@{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
yields an error (since the term is not typable). A slightly more elaborate
- example that type-checks is
-
+ example that type-checks is:
@{ML_response_fake [display,gray]
"let
@@ -503,6 +504,9 @@
}
\]
+ However, while we obtained a theorem as result, this theorem is not
+ yet stored in Isabelle's theorem database. So it cannot be referenced later
+ on. How to store theorems will be explained in the next section.
\begin{readmore}
For the functions @{text "assume"}, @{text "forall_elim"} etc
@@ -519,8 +523,8 @@
section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
text {*
- You will occationally feel the need to inspect terms, cterms or theorems during
- development. Isabelle contains elaborate pretty-printing functions for that, but
+ During development, you will occationally feel the need to inspect terms, cterms
+ or theorems. Isabelle contains elaborate pretty-printing functions for that, but
for quick-and-dirty solutions they are way too unwieldy. A simple way to transform
a term into a string is to use the function @{ML Syntax.string_of_term}.
@@ -542,12 +546,12 @@
Syntax.string_of_term ctxt (term_of t)*}
text {*
- If there are more than one @{ML_type cterm} to be printed, you can use the function
- @{ML commas} to conveniently separate them.
+ If there are more than one @{ML_type cterm}s to be printed, you can use the
+ function @{ML commas} to separate them.
*}
ML{*fun str_of_cterms ctxt ts =
- commas (map (str_of_cterm ctxt) ts)*}
+ commas (map (str_of_cterm ctxt) ts)*}
text {*
The easiest way to get the string of a theorem is to transform it
@@ -722,7 +726,7 @@
The combinators @{ML "|>>"} and @{ML "||>"} are defined for
functions manipulating pairs. The first applies the function to
- the first component of the pair, defined as:
+ the first component of the pair, defined as
*}
ML{*fun (x, y) |>> f = (f x, y)*}