isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:b83c75d051b7
+:a0b280dd4bc7
 \isacommand{begin}\\
 \ldots
 \end{tabular}
 \end{quote}
-Note that no parentheses are given this time. Note also that the included
+Note that no parentheses are given in this case. Note also that the included
 ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
 is unable to record all file dependencies, which is a nuisance if you have
 to track down errors.
 *}
 %Fail, although there is some special treatment when Toplevel.debug is
 %enabled.
 Most often you want to inspect data of Isabelle's basic data structures,
 namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
-and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions
+and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
-for printing them (see Section \ref{sec:pretty}), but for quick-and-dirty
+which we will explain in more detail in Section \ref{sec:pretty}. For now
-solutions they are a bit unwieldy. One way to transform a term into a string
+we just use the functions @{ML_ind writeln in Pretty}  from the structure
-is to use the function @{ML_ind string_of_term in Syntax} from the structure
+@{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
-@{ML_struct Syntax}. For more convenience, we bind this function to the
+@{ML_struct Syntax}. For more convenience, we bind them to the toplevel.
-toplevel.
 *}
 ML{*val string_of_term = Syntax.string_of_term*}
+ML{*val pretty_term = Syntax.pretty_term*}
-text {*
+ML{*val pwriteln = Pretty.writeln*}
-It can now be used as follows
+text {*
+They can now be used as follows
 @{ML_response_fake [display,gray]
-"string_of_term @{context} @{term \"1::nat\"}"
+"pwriteln (pretty_term @{context} @{term \"1::nat\"})"
-"\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
-We obtain a string corrsponding to the term @{term [show_types] "1::nat"} with some
-additional information encoded in it. The string can be properly printed by
-using either the function @{ML  writeln} or @{ML  tracing}:
-@{ML_response_fake [display,gray]
-"writeln (string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
-or
+If there is more than one term to be printed, you can use the
+function @{ML_ind enum in Pretty} to separate them.
-@{ML_response_fake [display,gray]
-"tracing (string_of_term @{context} @{term \"1::nat\"})"
-"\"1\""}
-If there are more than one term to be printed, you can use the
-function @{ML_ind commas in Library} to separate them.
 *}
 ML{*fun string_of_terms ctxt ts =
 commas (map (string_of_term ctxt) ts)*}
+ML{*fun pretty_terms ctxt ts =
-text {*
+Pretty.enum "," "" "" (map (pretty_term ctxt) ts)*}
-You can also print out terms together with typing information.
+text {*
+You can also print out terms together with their typing information.
 For this you need to set the reference @{ML_ind show_types in Syntax}
 to @{ML true}.
 *}
 ML{*show_types := true*}
 text {*
-Now @{ML string_of_term} prints out
+Now @{ML pretty_term} prints out
 @{ML_response_fake [display, gray]
-"tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+"pwriteln (pretty_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
 the reference @{ML_ind show_all_types in Syntax} to @{ML true}.
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
 text {*
 @{ML_response_fake [display, gray]
-"tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+"pwriteln (pretty_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 of terms are
 @{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}.
 *}
 (*<*)ML %linenos {*show_types := false; show_all_types := false*}
 (*>*)
 text {*
-A @{ML_type cterm} can be transformed into a string by the following function.
+A @{ML_type cterm} can be printed with the following function.
 *}
 ML{*fun string_of_cterm ctxt ct =
 string_of_term ctxt (term_of ct)*}
+ML{*fun pretty_cterm ctxt ct =
-text {*
+pretty_term ctxt (term_of ct)*}
-In this example the function @{ML_ind term_of in Thm} extracts the @{ML_type
-term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be
+text {*
-printed with @{ML commas}.
+Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
+term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can be
+printed again with @{ML enum in Pretty}.
 *}
 ML{*fun string_of_cterms ctxt cts =
 commas (map (string_of_cterm ctxt) cts)*}
+ML{*fun pretty_cterms ctxt cts =
+Pretty.enum "," "" "" (map (pretty_cterm ctxt) cts)*}
 text {*
 The easiest way to get the string of a theorem is to transform it
 into a @{ML_type term} using the function @{ML_ind prop_of in Thm}.
 *}
-ML{*fun string_of_thm ctxt thm =
+ML{*fun pretty_thm ctxt thm =
-string_of_term ctxt (prop_of thm)*}
+pretty_term ctxt (prop_of thm)*}
 text {*
 Theorems include schematic variables, such as @{text "?P"},
 @{text "?Q"} and so on. They are needed in Isabelle in order to able to
 instantiate theorems when they are applied. For example the theorem
 @{thm [source] conjI} shown below can be used for any (typable)
 instantiation of @{text "?P"} and @{text "?Q"}.
 @{ML_response_fake [display, gray]
-"tracing (string_of_thm @{context} @{thm conjI})"
+"pwriteln (pretty_thm @{context} @{thm conjI})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 However, in order to improve the readability when printing theorems, we
 convert these schematic variables into free variables using the function
 @{ML_ind  import in Variable}. This is similar to statements like @{text
 val ((_, [thm']), _) = Variable.import true [thm] ctxt
 in
 thm'
 end
-fun string_of_thm_no_vars ctxt thm =
+fun pretty_thm_no_vars ctxt thm =
-string_of_term ctxt (prop_of (no_vars ctxt thm))*}
+pretty_term ctxt (prop_of (no_vars ctxt thm))*}
 text {*
 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})"
+"pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
 Again the function @{ML commas} helps with printing more than one theorem.
 *}
-ML{*fun string_of_thms ctxt thms =
+ML{*fun pretty_thms ctxt thms =
-commas (map (string_of_thm ctxt) thms)
+Pretty.enum "," "" "" (map (pretty_thm ctxt) thms)
-fun string_of_thms_no_vars ctxt thms =
+fun pretty_thms_no_vars ctxt thms =
-commas (map (string_of_thm_no_vars ctxt) thms) *}
+Pretty.enum "," "" "" (map (pretty_thm_no_vars ctxt) thms)*}
 text {*
 The printing functions for types are
 *}
-ML{*fun string_of_typ ctxt ty = Syntax.string_of_typ ctxt ty
+ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
-fun string_of_typs ctxt tys = commas (map (string_of_typ ctxt) tys)*}
+fun pretty_typs ctxt tys = Pretty.commas (map (pretty_typ ctxt) tys)*}
 text {*
 respectively ctypes
 *}
-ML{*fun string_of_ctyp ctxt cty = string_of_typ ctxt (typ_of cty)
+ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
-fun string_of_ctyps ctxt ctys = commas (map (string_of_ctyp ctxt) ctys)*}
+fun pretty_ctyps ctxt ctys = Pretty.commas (map (pretty_ctyp ctxt) ctys)*}
 text {*
 \begin{readmore}
 The simple conversion functions from Isabelle's main datatypes to
 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}.
 together, like a warning message consisting of a term and its type, you
 should try to print these parcels together in a single string. Therefore do
 \emph{not} print out information as
 @{ML_response_fake [display,gray]
-"tracing \"First half,\";
+"writeln \"First half,\";
-tracing \"and second half.\""
+writeln \"and second half.\""
 "First half,
 and second half."}
 but as a single string with appropriate formatting. For example
 @{ML_response_fake [display,gray]
-"tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
+"writeln (\"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 in Isabelle. For example,  the function
 @{ML_ind cat_lines in Library} concatenates a list of strings
 and inserts newlines in between each element.
 @{ML_response_fake [display, gray]
-"tracing (cat_lines [\"foo\", \"bar\"])"
+"writeln (cat_lines [\"foo\", \"bar\"])"
 "foo
 bar"}
 Section \ref{sec:pretty} will explain the infrastructure that Isabelle
 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}
 *}
 section {* Combinators\label{sec:combinators} *}
 and the second is a proof. For example
 *}
 ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
+ML {*
+pretty_thms_no_vars
+*}
 text {*
 The result can be printed out as follows.
 @{ML_response_fake [gray,display]
-"foo_thm |> string_of_thms_no_vars @{context}
+"foo_thm |> pretty_thms_no_vars @{context}
-|> tracing"
+|> pwriteln"
 "True, False \<Longrightarrow> P"}
 You can also refer to the current simpset via an antiquotation. To illustrate
 this we implement the function that extracts the theorem names stored in a
 simpset.

changeset 440	a0b280dd4bc7
parent 423	0a25b35178c3