isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:bdd82350cf22
+:258ce361ba1b
 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
+show code. The lines prefixed with @{text [quotes] ">"} 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, 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:
 @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
 will print out @{text [quotes] "any string"} inside the response buffer
 of Isabelle.  This function expects a string as argument. If you develop under PolyML,
 then there is a convenient, though again ``quick-and-dirty'', method for
-converting values into strings, namely using the function @{ML makestring}:
+converting values into strings, namely the function @{ML makestring}:
 @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
 However @{ML makestring} only works if the type of what is converted is monomorphic
 and not a function.
 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 It is also possible to redirect the ``channel'' where the string @{text "foo"} is
 printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive
-amounts of trace output. This redirection can be achieved using the code
+amounts of trace output. This redirection can be achieved with the code:
 *}
 ML{*val strip_specials =
 let
 fun strip ("\^A" :: _ :: cs) = strip cs
 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"}.
-You can print out error messages with the function @{ML error}, as in:
+You can print out error messages with the function @{ML error}; for example:
 @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
 Section~\ref{sec:printing} will give more information about printing
-the main datas tructures of Isabelle, namely @{ML_type term}, @{ML_type cterm}
+the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm}
 and @{ML_type thm}.
 *}
 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:
+and simpsets:
 @{ML_response_fake [display,gray]
 "let
 val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset}
 in
 Write a function which takes two terms representing natural numbers
 in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
 number representing their sum.
 \end{exercise}
-(FIXME: maybe should go)
+A handy function for manipulating terms is @{ML map_types}: it takes a
+function and applies it to every type in the term. You can, for example,
+change every @{typ nat} into an @{typ int} using the function
 *}
 ML{*fun nat_to_int t =
 (case t of
 @{typ nat} => @{typ int}
 | Type (s, ts) => Type (s, map nat_to_int ts)
 | _ => t)*}
 text {*
+an then apply it as follows:
 @{ML_response_fake [display,gray]
 "map_types nat_to_int @{term \"a = (1::nat)\"}"
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
 the @{ML "@{theory}"} antiquotation to get hold of the current theory.
 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 written with an antiquotation:
 @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
 Attempting to obtain the certified term for
 section {* Theorems *}
 text {*
 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
 that can only be built by going through interfaces. As a consequence, every proof
-in Isabelle is correct by construction (FIXME reference LCF-philosophy)
+in Isabelle is correct by construction.
+(FIXME reference LCF-philosophy)
 To see theorems in ``action'', let us give a proof on the ML-level for the following
 statement:
 *}
 section {* Theorem Attributes *}
 section {* Printing Terms and Theorems\label{sec:printing} *}
 text {*
-During development, you often want to inspect terms, cterms
+During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm}
-or theorems. Isabelle contains elaborate pretty-printing functions for printing them,
+or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
 but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
 a term into a string is to use the function @{ML Syntax.string_of_term}.
 @{ML_response_fake [display,gray]
 "Syntax.string_of_term @{context} @{term \"1::nat\"}"
 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 This produces a string with some printing directions encoded in it. The string
-can be properly printed by using @{ML warning} foe example.
+can be properly printed by using the function @{ML warning}.
 @{ML_response_fake [display,gray]
 "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 This combinator is defined as
 *}
 ML{*fun (x, y) |-> f = f x y*}
-text {* and can be used to write the following version of the @{text double} function *}
+text {* and can be used to write the following roundabout version
+of the @{text double} function
+*}
 ML{*fun double x =
 x |>  (fn x => (x, x))
 |-> (fn x => fn y => x + y)*}

changeset 107	258ce361ba1b
parent 104	5dcad9348e4d
child 108	8bea3f74889d