--- a/CookBook/FirstSteps.thy Mon Jan 26 12:29:43 2009 +0000
+++ b/CookBook/FirstSteps.thy Mon Jan 26 16:09:02 2009 +0000
@@ -112,7 +112,7 @@
Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
will cause that all tracing information is printed into the file @{text "foo.bar"}.
- Error messages can be printed using the function @{ML error} as in
+ Error messages can be printed using the function @{ML error}, as in
@{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
@@ -138,7 +138,7 @@
@{text FirstSteps}). The name of this theory can be extracted with
the function @{ML "Context.theory_name"}.
- Note, however, that antiquotations are statically scoped, that is the value is
+ Note, however, that antiquotations are statically scoped, that is their value is
determined at ``compile-time'', not ``run-time''. For example the function
*}
@@ -154,7 +154,7 @@
some data structure and return it. Instead, it is literally
replaced with the value representing the theory name.
- In a similar way you can use antiquotations to refer to theorems:
+ In a similar way you can use antiquotations to refer to proved theorems:
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
@@ -167,15 +167,17 @@
map #name (Net.entries rules)
end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
- The code above extracts the theorem names that are stored in the current simpset.
- We refer to the simpset with the antiquotation @{text "@{simpset}"}.
- The function @{ML rep_ss in MetaSimplifier} returns a record
- containing all information about the simpset. The rules of a simpset are stored
- in a \emph{discrimination net} (a datastructure for fast indexing). From this net
- we can extract the entries using the function @{ML Net.entries}.
+ The code about simpsets extracts the theorem names that are stored in the
+ current simpset. We get hold of the current simpset with the antiquotation
+ @{text "@{simpset}"}. The function @{ML rep_ss in MetaSimplifier} returns a record
+ containing all information about the simpset. The rules of a simpset are
+ stored in a \emph{discrimination net} (a datastructure for fast
+ indexing). From this net we can extract the entries using the function @{ML
+ Net.entries}.
+
\begin{readmore}
- The infrastructure for simpsets is contained in @{ML_file "Pure/meta_simplifier.ML"}
+ The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
in @{ML_file "Pure/net.ML"}.
\end{readmore}
@@ -275,13 +277,14 @@
section {* Constructing Terms and Types Manually *}
text {*
-
- While antiquotations are very convenient for constructing terms,
- they can only construct fixed terms (remember they are ``linked'' at compile-time).
- 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
+ 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 pattern are
+ constructed from 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
*}
ML{*fun make_imp P Q tau =
@@ -310,7 +313,7 @@
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $
(Free (\"T\",\<dots>) $ \<dots>))"}
- Whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
+ whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
and @{text "Q"} from the antiquotation.
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}"
@@ -319,6 +322,8 @@
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
+ (FIXME: expand the following point)
+
One tricky point in constructing terms by hand is to obtain the fully
qualified name for constants. For example the names for @{text "zero"} and
@{text "+"} are more complex than one first expects, namely
@@ -390,7 +395,7 @@
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
- type-correct, and they can only be constructed via the ``official
+ type-correct, and they can only be constructed via ``official
interfaces''.
Type-checking is always relative to a theory context. For now we use
@@ -399,7 +404,7 @@
@{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}
- or use the antiquotation
+ This can also be wirtten with an antiquotation
@{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
@@ -505,10 +510,10 @@
section {* Combinators\label{sec:combinators} *}
text {*
- Perhaps one of the most puzzling aspects for a beginner when reading
- existing Isabelle code is the liberal use of combinators. At first they
+ Perhaps one of the most puzzling aspect for a beginner when reading
+ existing Isabelle code special purpose combinators. At first they
seem to obstruct the comprehension of the code, but after getting familiar
- with them they actually ease the reading and also the programming.
+ with them they actually ease the understanding and also the programming.
\begin{readmore}
The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
@@ -520,20 +525,21 @@
ML{*fun I x = x*}
-text {* Another frequently used combinator is @{ML K} *}
+text {* Another combinator is @{ML K}, defined as *}
ML{*fun K x = fn _ => x*}
text {*
- which ``wraps'' a function around the argument @{text "x"}. This function
- ignores its argument.
+ It ``wraps'' a function around the argument @{text "x"}. However, this
+ function ignores its argument.
- The next combinator is reverse application defined as
+ The next combinator is reverse application, @{ML "(op |>)"}, defined as
*}
ML{*fun x |> f = f x*}
-text {* The purpose of this combinator is to implement functions in a
+text {* While just syntactic sugar for the usual function application,
+ the purpose of this combinator is to implement functions in a
``waterfall fashion''. Consider for example the function *}
ML %linenumbers{*fun inc_by_five x =
@@ -547,7 +553,7 @@
the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
the first component of the pair (Line 4) and finally incrementing the first
component by 4 (Line 5). This kind of cascading manipulations of values is quite
- common when extending theories (for example by adding a definition, followed by
+ common when dealing with theories (for example by adding a definition, followed by
lemmas and so on). Writing the function @{ML inc_by_five} using the reverse
application is much clearer than writing
*}
@@ -559,7 +565,7 @@
ML{*fun inc_by_five x =
((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
-text {* and much more economical than *}
+text {* and typographically more economical than *}
ML{*fun inc_by_five x =
let val y1 = x + 1
@@ -569,8 +575,10 @@
in y4 end*}
text {*
+ (FIXME: give a real world example involving theories)
+
Similarly, the combinator @{ML "(op #>)"} is the reverse function
- composition. It allows us to define functions as follows
+ composition. It can be used to define functions as follows
*}
ML{*val inc_by_six =
@@ -589,8 +597,8 @@
The remaining combinators add convenience for the ``waterfall method''
of writing functions. The combinator @{ML tap} allows one to get
- hold of a intermediate result for some side-calculations. For
- example the function *}
+ hold of an intermediate result (to do some side-calculations for instance).
+ The function *}
ML{*fun inc_by_three x =
x |> (fn x => x + 1)
@@ -598,14 +606,15 @@
|> (fn x => x + 2)*}
text {* increments the argument first by one and then by two. In the middle,
- however, it prints the ``plus-one'' intermediate result inside the
- tracing buffer.
+ however, it uses @{ML tap} for printing the ``plus-one'' intermediate
+ result inside the tracing buffer.
The combinator @{ML "(op `)"} is similar, but applies a function to the value
- and returns the result together with the original value as pair. For example
- the following function takes @{text x} then increments @{text x} and returns
- the pair @{ML "(x + 1,x)" for x}. It then increments the right-hand component
- of the pair.
+ and returns the result together with the original value (as pair). For example
+ the following function takes @{text x} as argument, and then first
+ increments @{text x}, but also keeps @{text x}. The intermediate result is
+ therefore the pair @{ML "(x + 1,x)" for x}. The function then increments the
+ right-hand component of the pair.
*}
ML{*fun inc_as_pair x =
@@ -615,16 +624,19 @@
text {*
The combinators @{ML "(op |>>)"} and @{ML "(op ||>)"} are defined for
functions manipulating pairs. The first applies the function to
- the first component of the pair:
+ the first component of the pair, defined as:
*}
ML{*fun (x, y) |>> f = (f x, y)*}
text {*
- and the second combinator to the second component:
+ and the second combinator to the second component, defined as
*}
ML{*fun (x, y) ||> f = (x, f y)*}
+text {*
+ (FIXME: find a good exercise for combinators)
+*}
end
\ No newline at end of file
--- a/CookBook/Intro.thy Mon Jan 26 12:29:43 2009 +0000
+++ b/CookBook/Intro.thy Mon Jan 26 16:09:02 2009 +0000
@@ -12,7 +12,7 @@
provided in the Cookbook is as far as possible checked against recent
versions of Isabelle. If something does not work, then please let us
know. If you have comments or like to add to the Cookbook,
- feel free--you are very welcome!
+ feel free---you are most welcome!
*}
section {* Intended Audience and Prior Knowledge *}
@@ -62,11 +62,11 @@
*}
-section {* Conventions in the Cookbook *}
+section {* Typographic Conventions *}
text {*
- All ML-code in this Cookbook is shown in highlighed displays, like the following
+ All ML-code in this Cookbook is typeset in highlighed boxes, like the following
ML-expression.
\begin{isabelle}
@@ -78,25 +78,28 @@
\end{graybox}
\end{isabelle}
- This corresponds to how code can be processed inside the interactive
- environment of Isabelle. However, for better readability we will drop
- the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
+ This corresponds to how code can be processed inside the interactive
+ environment of Isabelle. It is therefore easy to experiment with the code
+ (which by the way is highly recommended). However, for better readability we
+ will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
\isacharverbatimclose} and just write
+
@{ML [display,gray] "3 + 4"}
- for the code above. Whenever appropriate we also show the response of the code
- when evaluated. The response is prefixed with a @{text [quotes] ">"}" like
+ for the code above. Whenever appropriate we also show the response the code
+ generates when evaluated. This response is prefixed with a
+ @{text [quotes] ">"} like
@{ML_response [display,gray] "3 + 4" "7"}
- Isabelle commands are written in bold, for example \isacommand{lemma},
+ The usual Isabelle commands are written in bold, for example \isacommand{lemma},
\isacommand{foobar} and so on. We use @{text "$"} to indicate that
a command needs to be run on the Unix-command line, for example
@{text [display] "$ ls -la"}
- Pointers to further information and Isabelle files are highlighted
+ Pointers to further information and Isabelle files are given
as follows:
\begin{readmore}