isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:0fea8b7a14a1
+:01e71cddf6a3
 text {*
 \begin{flushright}
 {\em
 ``We will most likely never realize the full importance of painting the Tower,\\
 that it is the essential element in the conservation of metal works and the\\
-more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex]
+more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
 Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been
 re-painted 18 times since its initial construction, an average of once every
 seven years. It takes more than a year for a team of 25 painters to paint the tower
 from top to bottom.}
 \end{flushright}
 ML {* Toplevel.program (fn () => innocent ()) *}
 *)
 text {*
-Most often you want to inspect data of Isabelle's most basic data
+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
 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
+As done above, we update the reference with the command
 \isacommand{setup}.
 *}
-setup %gray{* ref_update 1 *}
+setup %gray {* ref_update 1 *}
 text {*
 A lookup in the current theory gives then the expected list
 @{ML "ref [1]" in Unsynchronized}.
 @{ML_response_fake [display,gray]
 "WrongRefData.get @{theory}"
 "ref [1]"}
-So far everything is as expected. But, the trouble starts if we attempt
+So far everything is as expected. But, the trouble starts if we attempt to
-to backtrack to ``before'' the \isacommand{setup}-command. There, we
+backtrack to the point ``before'' the \isacommand{setup}-command. There, we
-would expect that the list is empty again. But since it is stored in
+would expect that the list is empty again. But since it is stored in a
-a reference, Isabelle has no control over it. So it is not
+reference, Isabelle has no control over it. So it is not empty, but still
-empty, but still @{ML "ref [1]" in Unsynchronized}. Adding to the trouble,
+@{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
-if we execute the \isacommand{setup}-command again, we do not obtain
+\isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
-@{ML "ref [1]" in Unsynchronized}, but
+Unsynchronized}, but
 @{ML_response_fake [display,gray]
 "WrongRefData.get @{theory}"
 "ref [1, 1]"}
 \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
+directed graphs in @{ML_file "Pure/General/graph.ML"}, and
 tables and symtables in @{ML_file "Pure/General/table.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
 Next we start with the context generated by the antiquotation
 @{text "@{context}"} and update it in various ways.
 @{ML_response_fake [display,gray]
 "let
-val ctxt    = @{context}
+val ctxt0 = @{context}
-val ctxt'   = ctxt   |> update @{term \"False\"}
+val ctxt1 = ctxt0 |> update @{term \"False\"}
 |> update @{term \"True \<and> True\"}
-val ctxt''  = ctxt   |> update @{term \"1::nat\"}
+val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
-val ctxt''' = ctxt'' |> update @{term \"2::nat\"}
+val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
 in
-print ctxt;
+print ctxt0;
-print ctxt';
+print ctxt1;
-print ctxt'';
+print ctxt2;
-print ctxt'''
+print ctxt3
 end"
 "Empty!
 True \<and> True, False
 1
 2, 1"}
 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 one can access the data potentially
-indefinitely.\footnote{\bf FIXME: check this; it seems that is in
+indefinitely.
-conflict with the statements below.}
 For convenience there is an abstract layer, the type @{ML_type Context.generic},
 for theories and proof contexts. This type is defined as follows
 *}
 \end{isabelle}
 On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}:
 *}
-setup %gray {*
+setup %gray {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *}
-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\"]"}
+@{ML_response_fake [display,gray]
+"FooRules.get @{context}"
+"[\"True\", \"?C\",\"?B\"]"}
+Note that this function takes a proof context as argument. This might be
+confusing, since the theorem list is stored as theory data. The proof context
+however conatains the information about the current theory and so the function
+can access the theorem list in the theory via the context.
 \begin{readmore}
-For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+For more information about named theorem lists 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
 @{ML_response [display,gray]
 "Config.get @{context} bval"
 "true"}
-or from a theory using the function @{ML_ind get_thy in Config}
+or directly from a theory using the function @{ML_ind get_thy in Config}
 @{ML_response [display,gray]
 "Config.get_thy @{theory} bval"
 "true"}
 It is also possible to manipulate the configuration values
-from the ML-level with the function @{ML_ind put in Config}
+from the ML-level with the functions @{ML_ind put in Config}
-or @{ML_ind put_thy in Config}. For example
+and @{ML_ind put_thy in Config}. For example
 @{ML_response [display,gray]
 "let
 val ctxt = @{context}
 val ctxt' = Config.put sval \"foo\" ctxt
+val ctxt'' = Config.put sval \"bar\" ctxt'
 in
-(Config.get ctxt sval, Config.get ctxt' sval)
+(Config.get ctxt sval, Config.get ctxt' sval, Config.get ctxt'' sval)
 end"
-"(\"some string\", \"foo\")"}
+"(\"some string\", \"foo\", \"bar\")"}
 \begin{readmore}
 For more information about configuration values see
 the files @{ML_file "Pure/Isar/attrib.ML"} and
 @{ML_file "Pure/config.ML"}.
 and @{ML_type thm}. The section on ML-antiquotations shows how to refer
 statically to entities from the logic level of Isabelle. Isabelle also
 contains mechanisms for storing arbitrary data in theory and proof
 contexts.
-This chapter also mentions two coding conventions: namely printing
+\begin{conventions}
-entities belonging together as one string, and not using references
+\begin{itemize}
-in any Isabelle code.
+\item Print messages that belong together as a single string.
+\item Do not use references in any Isabelle code.
+\end{itemize}
+\end{conventions}
 *}
 (**************************************************)
 (* bak                                            *)

changeset 347	01e71cddf6a3
parent 346	0fea8b7a14a1
child 350	364fffa80794