isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:95e9c4556221
+:8fda6b452f28
 text {*
 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\""}
 *}
 where @{text "@{theory}"} is an antiquotation that is substituted with the
 current theory (remember that we assumed we are inside the theory
 @{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
 *}
 ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is
 \emph{not} replaced with code that will look up the current theory in
 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"}
 or simpsets:
 val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
 in
 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.
+The code about simpsets extracts the theorem names that are stored in the
-We refer to the simpset with the antiquotation @{text "@{simpset}"}.
+current simpset.  We get hold of the current simpset with the antiquotation
-The function @{ML rep_ss in MetaSimplifier} returns a record
+@{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
+containing all information about the simpset. The rules of a simpset are
-in a \emph{discrimination net} (a datastructure for fast indexing). From this net
+stored in a \emph{discrimination net} (a datastructure for fast
-we can extract the entries using the function @{ML Net.entries}.
+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}
 While antiquotations have many applications, they were originally introduced in order
 section {* Constructing Terms and Types Manually *}
 text {*
+While antiquotations are very convenient for constructing terms, they can
-While antiquotations are very convenient for constructing terms,
+only construct fixed terms (remember they are ``linked'' at
-they can only construct fixed terms (remember they are ``linked'' at compile-time).
+compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external}
-However, one often needs to construct terms
+for a function that pattern-matches over terms and where the pattern are
-dynamically. For example, a function that returns the implication
+constructed from antiquotations.  However, one often needs to construct
-@{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"}
+terms dynamically. For example, a function that returns the implication
-as arguments can only be written as
+@{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 =
 let
 val x = Free ("x",tau)
 "Const \<dots> $
 Abs (\"x\", Type (\"nat\",[]),
 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}"
 "Const \<dots> $
 Abs (\"x\", \<dots>,
 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
 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.
 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
 the @{ML "@{theory}"} antiquotation to get hold of the current theory.
 For example we can write
 @{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"}
 Attempting to obtain the certified term for
 *}
 section {* Combinators\label{sec:combinators} *}
 text {*
-Perhaps one of the most puzzling aspects for a beginner when reading
+Perhaps one of the most puzzling aspect for a beginner when reading
-existing Isabelle code is the liberal use of combinators. At first they
+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"}
 and @{ML_file "Pure/General/basics.ML"}.
 \end{readmore}
 The simplest combinator is @{ML I} which is just the identity function.
 *}
 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
+It ``wraps'' a function around the argument @{text "x"}. However, this
-ignores its argument.
+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 =
 x |> (fn x => x + 1)
 |> (fn x => (x, x))
 text {*
 which increments the argument @{text x} by 5. It does this by first incrementing
 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
 *}
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 text {* or *}
 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
 val y2 = (y1, y1)
 val y3 = fst y2
 val y4 = y3 + 4
 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 =
 (fn x => x + 1)
 #> (fn x => x + 2)
 as expected.
 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
+hold of an intermediate result (to do some side-calculations for instance).
-example the function *}
+The function *}
 ML{*fun inc_by_three x =
 x |> (fn x => x + 1)
 |> tap (fn x => tracing (makestring x))
 |> (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
+however, it uses @{ML tap} for printing the ``plus-one'' intermediate
-tracing buffer.
+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
+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 following function takes @{text x} as argument, and then first
-the pair @{ML "(x + 1,x)" for x}. It then increments the right-hand component
+increments @{text x}, but also keeps @{text x}. The intermediate result is
-of the pair.
+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 =
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))*}
 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

changeset 81	8fda6b452f28
parent 78	ef778679d3e0
child 82	6dfe6975bda0