--- a/ProgTutorial/FirstSteps.thy Tue Oct 13 22:57:25 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Wed Oct 14 02:32:53 2009 +0200
@@ -17,7 +17,7 @@
{\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
@@ -214,7 +214,7 @@
*)
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
@@ -1045,11 +1045,11 @@
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
@@ -1059,13 +1059,13 @@
"WrongRefData.get @{theory}"
"ref [1]"}
- So far everything is as expected. But, the trouble starts if we attempt
- to backtrack to ``before'' the \isacommand{setup}-command. There, we
- would expect that the list is empty again. But since it is stored in
- a reference, Isabelle has no control over it. So it is not
- empty, but still @{ML "ref [1]" in Unsynchronized}. Adding to the trouble,
- if we execute the \isacommand{setup}-command again, we do not obtain
- @{ML "ref [1]" in Unsynchronized}, but
+ So far everything is as expected. But, the trouble starts if we attempt to
+ 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 a
+ reference, Isabelle has no control over it. So it is not empty, but still
+ @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
+ \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
+ Unsynchronized}, but
@{ML_response_fake [display,gray]
"WrongRefData.get @{theory}"
@@ -1080,7 +1080,7 @@
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}
@@ -1114,16 +1114,16 @@
@{ML_response_fake [display,gray]
"let
- val ctxt = @{context}
- val ctxt' = ctxt |> update @{term \"False\"}
- |> update @{term \"True \<and> True\"}
- val ctxt'' = ctxt |> update @{term \"1::nat\"}
- val ctxt''' = ctxt'' |> update @{term \"2::nat\"}
+ val ctxt0 = @{context}
+ val ctxt1 = ctxt0 |> update @{term \"False\"}
+ |> update @{term \"True \<and> True\"}
+ val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
+ val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
in
- print ctxt;
- print ctxt';
- print ctxt'';
- print ctxt'''
+ print ctxt0;
+ print ctxt1;
+ print ctxt2;
+ print ctxt3
end"
"Empty!
True \<and> True, False
@@ -1138,8 +1138,7 @@
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
- conflict with the statements below.}
+ indefinitely.
For convenience there is an abstract layer, the type @{ML_type Context.generic},
for theories and proof contexts. This type is defined as follows
@@ -1199,18 +1198,24 @@
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})
-*}
+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\"]"}
+ @{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
@@ -1251,24 +1256,25 @@
"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}
- or @{ML_ind put_thy in Config}. For example
+ from the ML-level with the functions @{ML_ind put in Config}
+ 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
@@ -1287,9 +1293,13 @@
contains mechanisms for storing arbitrary data in theory and proof
contexts.
- This chapter also mentions two coding conventions: namely printing
- entities belonging together as one string, and not using references
- in any Isabelle code.
+ \begin{conventions}
+ \begin{itemize}
+ \item Print messages that belong together as a single string.
+ \item Do not use references in any Isabelle code.
+ \end{itemize}
+ \end{conventions}
+
*}