--- 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