isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:28a49fe024c9
+:304426a9aecf
 \isacommand{oops}
 \end{isabelle}
 \end{quote}
 However, both commands will only play minor roles in this tutorial (we will
-always arrange that the ML-code is defined outside of proofs).
+always arrange that the ML-code is defined outside proofs).
 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 somewhere inside a
 theory by using the command \isacommand{use}. For example
 *}
 section {* Printing and Debugging\label{sec:printing} *}
 text {*
-During development you might find it necessary to inspect some data in your
+During development you might find it necessary to inspect data in your
 code. This can be done in a ``quick-and-dirty'' fashion using the function
 @{ML_ind writeln in Output}. For example
 @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}
 output into a separate tracing buffer. For example:
 @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}
 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
+"foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from
 choking on massive amounts of trace output. This redirection can be achieved
 with the code:
 *}
 ML{*val strip_specials =
 Most often you want to inspect data of Isabelle's basic data
 structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
 thm}. Isabelle contains elaborate pretty-printing functions for printing
 them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
 are a bit unwieldy. One way to transform a term into a string is to use the
-function @{ML_ind  string_of_term in Syntax} in the structure @{ML_struct
+function @{ML_ind  string_of_term in Syntax} from the structure @{ML_struct
 Syntax}. For more convenience, we bind this function to the toplevel.
 *}
 ML{*val string_of_term = Syntax.string_of_term*}
 ML{*fun string_of_terms ctxt ts =
 commas (map (string_of_term ctxt) ts)*}
 text {*
-You can also print out term together with type information.
+You can also print out terms together with typing information.
-This can be achieved by setting the reference @{ML_ind show_types in Syntax}
+For this you need to set the reference @{ML_ind show_types in Syntax}
 to @{ML true}.
 *}
 ML{*show_types := true*}
 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
 "(1::nat, x::'a)"}
 where @{text 1} and @{text x} are displayed with their inferred type.
 Even more type information can be printed by setting
-@{ML_ind show_all_types in Syntax} to @{ML true}. We obtain then
+the reference @{ML_ind show_all_types in Syntax} to @{ML true}.
+We obtain then
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
 text {*
 @{ML_response_fake [display, gray]
 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
 "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
+where @{term Pair} is the term-constructor for products.
 Other references that influence printing are @{ML_ind show_brackets in Syntax}
 and @{ML_ind show_sorts in Syntax}.
 *}
 (*<*)ML %linenos {*show_types := false; show_all_types := false*}
 (*>*)
 fun string_of_thm_no_vars ctxt thm =
 string_of_term ctxt (prop_of (no_vars ctxt thm))*}
 text {*
-Theorem @{thm [source] conjI} is now printed as follows:
+With this function, theorem @{thm [source] conjI} is now printed as follows:
 @{ML_response_fake [display, gray]
 "tracing (string_of_thm_no_vars @{context} @{thm conjI})"
 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}.
 The references that change the printing information are declared in
 @{ML_file "Pure/Syntax/printer.ML"}.
 \end{readmore}
-Note that when printing out several ``parcels'' of information that
+Note that for printing out several ``parcels'' of information that
 semantically belong together, like a warning message consisting of
 a term and its type, you should try to keep this information together in a
 single string. Therefore do \emph{not} print out information as
 @{ML_response_fake [display,gray]
 "tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
 "First half,
 and second half."}
 To ease this kind of string manipulations, there are a number
-of library functions. For example,  the function @{ML_ind cat_lines in Library}
+of library functions in Isabelle. For example,  the function
-concatenates a list of strings and inserts newlines.
+@{ML_ind cat_lines in Library} concatenates a list of strings
+and inserts newlines in between each element.
 @{ML_response [display, gray]
 "cat_lines [\"foo\", \"bar\"]"
 "\"foo\\nbar\""}
-Section \ref{sec:pretty} will also explain the infrastructure of Isabelle
+Section \ref{sec:pretty} will also explain the infrastructure that Isabelle
-that helps with more elaborate pretty printing.
+provides for more elaborate pretty printing.
 \begin{readmore}
 Most of the basic string functions of Isabelle are defined in
 @{ML_file "Pure/library.ML"}.
 \end{readmore}
 avoiding the given @{text f}; the list of name-type pairs is turned into a
 list of variable terms in Line 6, which in the last line is applied by the
 function @{ML_ind list_comb in Term} to the term. In this last step we have
 to use the function @{ML_ind curry in Library}, because @{ML list_comb}
 expects the function and the variables list as a pair.
 Functions like @{ML apply_fresh_args} are often needed when constructing
 terms with fresh variables. The
 infrastructure helps tremendously to avoid any name clashes. Consider for
 example:
 The combinator @{ML_ind "#>" in Basics} is the reverse function composition.
 It can be used to define the following function
 *}
 ML{*val inc_by_six =
-(fn x => x + 1)
+(fn x => x + 1) #>
-#> (fn x => x + 2)
+(fn x => x + 2) #>
-#> (fn x => x + 3)*}
+(fn x => x + 3)*}
 text {*
 which is the function composed of first the increment-by-one function and then
 increment-by-two, followed by increment-by-three. Again, the reverse function
 composition allows you to read the code top-down.

changeset 374	304426a9aecf
parent 373	28a49fe024c9
child 375	92f7328dc5cc