isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:c0cae24b9d46
+:5dffcab68680
 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.
 *}
-section {* Debugging and Printing\label{sec:printing} *}
+section {* Printing and Debugging\label{sec:printing} *}
 text {*
 During development you might find it necessary to inspect some data in your
 code. This can be done in a ``quick-and-dirty'' fashion using the function
 @{ML_ind  "writeln"}. For example
 Most often you want to inspect data of Isabelle's most 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 structure @{ML_struct
+function @{ML_ind  string_of_term in Syntax} in the structure @{ML_struct
 Syntax}, which we bind for more convenience to the toplevel.
 *}
 ML{*val string_of_term = Syntax.string_of_term*}
 When using combinators for writing functions in waterfall fashion, it is
 sometimes necessary to do some ``plumbing'' in order to fit functions
 together. We have already seen such plumbing in the function @{ML
 apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
 list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
-plumbing is also needed in situations where a functions operate over lists,
+plumbing is also needed in situations where a function operate over lists,
 but one calculates only with a single element. An example is the function
 @{ML_ind  check_terms in Syntax}, whose purpose is to type-check a list
 of terms.
 @{ML_response_fake [display, gray]
 end"
 "m + n, m * n, m - n"}
 *}
 text {*
-In this example we obtain three terms in which @{text m} and @{text n} are of
+In this example we obtain three terms whose variables @{text m} and @{text
-type @{typ "nat"}. If you have only a single term, then @{ML
+n} are of type @{typ "nat"}. If you have only a single term, then @{ML
 check_terms in Syntax} needs plumbing. This can be done with the function
 @{ML singleton}.\footnote{There is already a function @{ML check_term in
 Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
 and @{ML check_terms in Syntax}.} For example
 current theory (remember that we assumed we are inside the theory
 @{text FirstSteps}). The name of this theory can be extracted using
 the function @{ML_ind  theory_name in Context}.
 Note, however, that antiquotations are statically linked, that is their value is
-determined at ``compile-time'', not ``run-time''. For example the function
+determined at ``compile-time'', not at ``run-time''. For example the function
 *}
 ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 text {*
 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
 The point of these antiquotations is that referring to theorems in this way
 makes your code independent from what theorems the user might have stored
 under this name (this becomes especially important when you deal with
-theorem lists; see Section \ref{sec:attributes}).
+theorem lists; see Section \ref{sec:storing}).
 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.
 *}
 An example where a qualified name is needed is the function
 @{ML_ind  define in LocalTheory}.  This function is used below to define
 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
 *}
 local_setup %gray {*
 LocalTheory.define Thm.internalK
 ((@{binding "TrueConj"}, NoSyn),
 (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
 \begin{isabelle}
 \isacommand{thm}~@{text "TrueConj_def"}\\
 @{text "> "}~@{thm TrueConj_def}
 \end{isabelle}
+\begin{readmore}
+The basic operations on bindings are implemented in
+@{ML_file "Pure/General/binding.ML"}.
+\end{readmore}
 \footnote{\bf FIXME give a better example why bindings are important; maybe
 give a pointer to \isacommand{local\_setup}; if not, then explain
 why @{ML snd} is needed.}
+\footnote{\bf FIXME: There should probably a separate section on binding, long-names
+and sign.}
 It is also possible to define your own antiquotations. But you should
 exercise care when introducing new ones, as they can also make your code
 also difficult to read. In the next chapter we will see how the (build in)
 antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
 @{ML_response_fake [display,gray]
 "WrongRefData.get @{theory}"
 "ref []"}
-For updating the reference we use the following function.
+For updating the reference we use the following function
 *}
 ML{*fun ref_update n = WrongRefData.map
 (fn r => let val _ = r := n::(!r) in r end)*}
 text {*
+which takes an integer and adds it to the content of the reference.
 As above we update the reference with the command
 \isacommand{setup}.
 *}
 setup %gray{* ref_update 1 *}
 "WrongRefData.get @{theory}"
 "ref [1, 1]"}
 Now imagine how often you go backwards and forwards in your proof scripts.
 By using references in Isabelle code, you are bound to cause all
-hell to break lose. Therefore observe the coding convention:
+hell to break loose. Therefore observe the coding convention:
 Do not use references for storing data!
 \begin{readmore}
 The functors for data storage are defined in @{ML_file "Pure/context.ML"}.
 Isabelle contains implementations of several container data structures,
 including association lists in @{ML_file "Pure/General/alist.ML"},
 directed graphs in @{ML_file "Pure/General/graph.ML"}. and
 tables and symtables in @{ML_file "Pure/General/table.ML"}.
-\end{readmore}
-A special instance of the data storage mechanism described above are
-configuration values. They are used to enable users to configure tools
-without having to resort to the ML-level (and also to avoid
-references). Assume you want the user to control three values, say @{text
-bval} containing a boolean, @{text ival} containing an integer and @{text
-sval} containing a string. These values can be declared by
-*}
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
-val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
-text {*
-where each value needs to be given a default. To enable these values, they need to
-be set up with
-*}
-setup %gray {*
-setup_bval #>
-setup_ival
-*}
-text {*
-The user can now manipulate the values from the user-level of Isabelle
-with the command
-*}
-declare [[bval = true, ival = 3]]
-text {*
-On the ML-level these values can be retrieved using the
-function @{ML Config.get}.
-@{ML_response [display,gray] "Config.get @{context} bval" "true"}
-\begin{readmore}
-For more information about configuration values see
-@{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
 \end{readmore}
 Storing data in a proof context is done in a similar fashion. The
 corresponding functor is @{ML_funct_ind ProofDataFun}. With the
 following code we can store a list of terms in a proof context.
 Isabelle code, although the ``context flow'' is usually only linear.
 Note also that the calculation above has no effect on the underlying
 theory. Once we throw away the contexts, we have no access to their
 associated data. This is different to theories, where the command
 \isacommand{setup} registers the data with the current and future
-theories, and therefore can access the data potentially indefinitely.
+theories, and therefore can access the data potentially
-*}
+indefinitely.\footnote{\bf FIXME: check this; it seems that is in
+conflict with the statements below.}
+\footnote{\bf FIXME: Say something about generic contexts.}
+There are two special instances of the data storage mechanism described
+above. The first instance are named theorem lists. Since storing theorems in a list
+is such a common task, there is the special functor @{ML_funct_ind Named_Thms}.
+To obtain a named theorem list, you just declare
+*}
+ML{*structure FooRules = Named_Thms
+(val name = "foo"
+val description = "Theorems for foo") *}
+text {*
+and set up the @{ML_struct FooRules} with the command
+*}
+setup %gray {* FooRules.setup *}
+text {*
+This code declares a data container where the theorems are stored,
+an attribute @{text foo} (with the @{text add} and @{text del} options
+for adding and deleting theorems) and an internal ML-interface to retrieve and
+modify the theorems.
+Furthermore, the facts are made available on the user-level under the dynamic
+fact name @{text foo}. For example you can declare three lemmas to be of the kind
+@{text foo} by:
+*}
+lemma rule1[foo]: "A" sorry
+lemma rule2[foo]: "B" sorry
+lemma rule3[foo]: "C" sorry
+text {* and undeclare the first one by: *}
+declare rule1[foo del]
+text {* and query the remaining ones with:
+\begin{isabelle}
+\isacommand{thm}~@{text "foo"}\\
+@{text "> ?C"}\\
+@{text "> ?B"}
+\end{isabelle}
+On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}:
+*}
+setup %gray {*
+Context.theory_map (FooRules.add_thm @{thm TrueI})
+*}
+text {*
+The rules in the list can be retrieved using the function
+@{ML FooRules.get}:
+@{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"True\", \"?C\",\"?B\"]"}
+\begin{readmore}
+For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+\end{readmore}
+The second special instance of the data storage mechanism are configuration
+values. They are used to enable users to configure tools without having to
+resort to the ML-level (and also to avoid references). Assume you want the
+user to control three values, say @{text bval} containing a boolean, @{text
+ival} containing an integer and @{text sval} containing a string. These
+values can be declared by
+*}
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
+val (ival, setup_ival) = Attrib.config_int "ival" 0
+val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
+text {*
+where each value needs to be given a default. To enable these values, they need to
+be set up with
+*}
+setup %gray {*
+setup_bval #>
+setup_ival
+*}
+text {*
+The user can now manipulate the values from the user-level of Isabelle
+with the command
+*}
+declare [[bval = true, ival = 3]]
+text {*
+On the ML-level these values can be retrieved using the
+function @{ML Config.get}.
+@{ML_response [display,gray] "Config.get @{context} bval" "true"}
+\begin{readmore}
+For more information about configuration values see
+@{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
+\end{readmore}
+*}
 (**************************************************)
 (* bak                                            *)
 (**************************************************)

changeset 329	5dffcab68680
parent 328	c0cae24b9d46
child 330	7718da58d9c0