isabelle-cookbook: comparison ProgTutorial/First

equal deleted inserted replaced

-:0fb910f62bf9
+:141751cab5b2
 @{text "\<verbclose>"}\isanewline
 @{text "> 7"}\smallskip
 \end{graybox}
 \end{isabelle}
 If you work with ProofGeneral then like normal Isabelle scripts
-\isacommand{ML}-commands can be evaluated by
+\isacommand{ML}-commands can be evaluated by using the advance and
-using the advance and undo buttons of your Isabelle environment. The code
+undo buttons of your Isabelle environment.  If you work with the
-inside the \isacommand{ML}-command can also contain value and function
+Jedit GUI, then you just have to hover the cursor over the code
-bindings, for example
+and you see the evaluated result in the ``Output'' window.
-*}
+As mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
-ML %gray {*
-val r = Unsynchronized.ref 0
-fun f n = n + 1
-*}
-text {*
-and even those can be undone when the proof script is retracted.  As
-mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
 "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we 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.  There are also
 the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including
 ML-code. The first evaluates the given code, but any effect on the theory,
 code. This can be done in a ``quick-and-dirty'' fashion using the function
 @{ML_ind writeln in Output}. For example
 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
-will print out @{text [quotes] "any string"} inside the response buffer of
+will print out @{text [quotes] "any string"} inside the response buffer.
-Isabelle.  This function expects a string as argument. If you develop under
+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 the antiquotation
 @{text "@{make_string}"}:
 @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""}
 At command \"ML\"."}
 This function raises the exception @{text ERROR}, which will then
 be displayed by the infrastructure. Note that this exception is meant
 for ``user-level'' error messages seen by the ``end-user''.
 For messages where you want to indicate a genuine program error, then
-use the exception @{text Fail}. Here the infrastructure indicates that this
+use the exception @{text Fail}.
-is a low-level exception, and also prints the source position of the ML
-raise statement.
 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,
 which we will explain in more detail in Section \ref{sec:pretty}. For now
 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]
-"writeln \"First half,\";
+"pwriteln (Pretty.str \"First half,\");
-writeln \"and second half.\""
+pwriteln (Pretty.str \"and second half.\")"
 "First half,
 and second half."}
 but as a single string with appropriate formatting. For example
 @{ML_response_fake [display,gray]
-"writeln (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
+"pwriteln (Pretty.str (\"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]
-"writeln (cat_lines [\"foo\", \"bar\"])"
+"pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"
 "foo
 bar"}
 Section \ref{sec:pretty} will explain the infrastructure that Isabelle
 provides for more elaborate pretty printing.
 then increment-by-two, followed by increment-by-three. Again, the reverse
 function composition allows you to read the code top-down. This combinator
 is often used for setup functions inside the
 \isacommand{setup}-command. These functions have to be of type @{ML_type
 "theory -> theory"}. More than one such setup function can be composed with
-@{ML "#>"}.\footnote{give example}
+@{ML "#>"}.\footnote{TBD: give example}
 The remaining combinators we describe in this section add convenience for the
 ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
 Basics} allows you to get hold of an intermediate result (to do some
 side-calculations or print out an intermediate result, for instance). The function
 *}
 ML %linenosgray{*fun inc_by_three x =
 x |> (fn x => x + 1)
-|> tap (fn x => writeln (@{make_string} x))
+|> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
 |> (fn x => x + 2)*}
 text {*
 increments the argument first by @{text "1"} and then by @{text "2"}. In the
 middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
 "(?P \<and> ?Q) = (?Q \<and> ?P)
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
 The thm-antiquotations can also be used for manipulating theorems. For
-example, if you need the version of te theorem @{thm [source] refl} that
+example, if you need the version of the theorem @{thm [source] refl} that
 has a meta-equality instead of an equality, you can write
 @{ML_response_fake [display,gray]
 "@{thm refl[THEN eq_reflection]}"
 "?x \<equiv> ?x"}
 |> ML_Syntax.atomic
 in
 ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
 end*}
+text {*
+To use it you also have to install it using \isacommand{setup} like so
+*}
 setup{* term_pat_setup *}
 text {*
 The parser in Line 2 provides us with a context and a string; this string is
 transformed into a term using the function @{ML_ind read_term_pattern in
 @{ML_response_fake [display,gray]
 "@{term_pat \"Suc (?x::nat)\"}"
 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 which shows the internal representation of the term @{text "Suc ?x"}. Similarly
-we can write an antiquotation for type patterns.
+we can write an antiquotation for type patterns. Its code is
 *}
 ML{*val type_pat_setup =
 let
 val parser = Args.context -- Scan.lift Args.name_source
 |> ML_Syntax.atomic
 in
 ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
 end*}
+text {*
+which can be installed with
+*}
 setup{* type_pat_setup *}
 text {*
+However, a word of warning is in order: Introducing new antiquotations
+should be done only after careful deliberations. They can make your
+code harder to read, than making it easier.
 \begin{readmore}
 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
 for most antiquotations. Most of the basic operations on ML-syntax are implemented
 in @{ML_file "Pure/ML/ml_syntax.ML"}.
 \end{readmore}
 In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is
 in contrast to datatypes, which only allow injection and projection of data for
 some \emph{fixed} collection of types. In light of the conventional wisdom cited
 above it is important to keep in mind that the universal type does not
 destroy type-safety of ML: storing and accessing the data can only be done
-in a type-safe manner.
+in a type-safe manner...though run-time checks are needed for that.
 \begin{readmore}
 In Isabelle the universal type is implemented as the type @{ML_type
 Universal.universal} in the file
 @{ML_file "Pure/ML-Systems/universal.ML"}.
 then store them in a @{ML_type "Universal.universal list"} as follows:
 *}
 ML{*val foo_list =
 let
-val thirteen  = inject_int 13
+val thirteen = inject_int 13
 val truth_val = inject_bool true
 in
 [thirteen, truth_val]
 end*}
 @{ML_response_fake [display,gray]
 "WrongRefData.get @{theory}"
 "ref [1, 1]"}
-Now imagine how often you go backwards and forwards in your proof scripts.
+Now imagine how often you go backwards and forwards in your proof
+scripts.\footnote{The same problem can be triggered in the Jedit GUI by
+making the parser to go over and over again over the \isacommand{setup} command.}
 By using references in Isabelle code, you are bound to cause all
 hell to break loose. Therefore observe the coding convention:
 Do not use references for storing data!
 \begin{readmore}
 ML{*fun update trm = Data.map (fn trms => trm::trms)
 fun print ctxt =
 case (Data.get ctxt) of
-[] => writeln "Empty!"
+[] => pwriteln (Pretty.str "Empty!")
 | trms => pwriteln (pretty_terms ctxt trms)*}
 text {*
 Next we start with the context generated by the antiquotation
 @{text "@{context}"} and update it in various ways.
 end"
 "(\"some string\", \"foo\", \"bar\")"}
 A concrete example for a configuration value is
 @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
-in the simplifier. This can be used as in the following proof
+in the simplifier. This can be used for example in the following proof
 *}
 lemma
 shows "(False \<or> True) \<and> True"
 proof (rule conjI)

changeset 477	141751cab5b2
parent 476	0fb910f62bf9
parent 474	683fb6e468b1
child 478	dfbd535cd1fd