
diff -r c0cae24b9d46 -r 5dffcab68680 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/General.thy	Sat Oct 03 19:10:23 2009 +0200
@@ -7,7 +7,8 @@
 text {*
   Isabelle is build around a few central ideas. One is the LCF-approach to
   theorem proving where there is a small trusted core and everything else is
-  build on top of this trusted core.
+  build on top of this trusted core. The central data structures involved
+  in this core are certified terms and types as well as theorems.
 
 *}
 
@@ -15,8 +16,9 @@
 section {* Terms and Types *}
 
 text {*
-  One way to construct Isabelle terms, is by using the antiquotation 
-  \mbox{@{text "@{term \<dots>}"}}. For example
+  In Isabelle there are certified terms (respectively types) and uncertified
+  terms. The latter are called just terms. One way to construct them is by 
+  using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
 
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
@@ -446,7 +448,8 @@
   @{ML_response [display,gray]
   "@{type_name \"list\"}" "\"List.list\""}
 
-  (FIXME: Explain the following better.)
+  \footnote{\bf FIXME: Explain the following better; maybe put in a separate
+  section and link with the comment in the antiquotation section.}
 
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML_ind  "Sign.extern_const"} or
@@ -537,9 +540,9 @@
   number representing their sum.
   \end{exercise}
 
-  \begin{exercise}\footnote{Personal communication of
-  de Bruijn to Dyckhoff.}\label{ex:debruijn}
-  Implement the function, which we below name deBruijn, that depends on a natural
+  \begin{exercise}\label{ex:debruijn}
+  Implement the function, which we below name deBruijn\footnote{According to 
+  personal communication of de Bruijn to Dyckhoff.}, that depends on a natural
   number n$>$0 and constructs terms of the form:
   
   \begin{center}
@@ -551,7 +554,7 @@
   \end{tabular}
   \end{center}
 
-  For n=3 this function returns the term
+  This function returns for n=3 the term
 
   \begin{center}
   \begin{tabular}{l}
@@ -685,13 +688,13 @@
   @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
 
-  (FIXME: say something about sorts)
+  \footnote{\bf FIXME: say something about sorts.}
 
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
   result that type-checks. See what happens to the  solutions of this 
-  exercise given in \ref{ch:solutions} when they receive an ill-typed term
-  as input.
+  exercise given in Appendix \ref{ch:solutions} when they receive an 
+  ill-typed term as input.
   \end{exercise}
 *}
 
@@ -982,7 +985,7 @@
   
   However, here also a weakness of the concept
   of theorem attributes shows through: since theorem attributes can be
-  arbitrary functions, they do not in general commute. If you try
+  arbitrary functions, they do not commute in general. If you try
 
   \begin{isabelle}
   \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
@@ -992,56 +995,34 @@
   you get an exception indicating that the theorem @{thm [source] sym}
   does not resolve with meta-equations. 
 
-  The purpose of @{ML_ind  rule_attribute in Thm} is to directly manipulate theorems.
-  Another usage of theorem attributes is to add and delete theorems from stored data.
-  For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
-  current simpset. For these applications, you can use @{ML_ind  declaration_attribute in Thm}. 
-  To illustrate this function, let us introduce a reference containing a list
-  of theorems.
-*}
-
-ML{*val my_thms = Unsynchronized.ref ([] : thm list)*}
-
-text {* 
-  The purpose of this reference is to store a list of theorems.
-  We are going to modify it by adding and deleting theorems.
-  However, a word of warning: such references must not 
-  be used in any code that is meant to be more than just for testing purposes! 
-  Here it is only used to illustrate matters. We will show later how to store 
-  data properly without using references.
- 
-  We need to provide two functions that add and delete theorems from this list. 
-  For this we use the two functions:
+  The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate
+  theorems.  Another usage of theorem attributes is to add and delete theorems
+  from stored data.  For example the theorem attribute @{text "[simp]"} adds
+  or deletes a theorem from the current simpset. For these applications, you
+  can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,
+  let us introduce a theorem list.
 *}
 
-ML{*fun my_thm_add thm ctxt =
-  (my_thms := Thm.add_thm thm (!my_thms); ctxt)
-
-fun my_thm_del thm ctxt =
-  (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
+ML{*structure MyThms = Named_Thms
+  (val name = "attr_thms" 
+   val description = "Theorems for an Attribute") *}
 
-text {*
-  These functions take a theorem and a context and, for what we are explaining
-  here it is sufficient that they just return the context unchanged. They change
-  however the reference @{ML my_thms}, whereby the function 
-  @{ML_ind  add_thm in Thm} adds a theorem if it is not already included in 
-  the list, and @{ML_ind  del_thm in Thm} deletes one (both functions use the 
-  predicate @{ML_ind  eq_thm_prop in Thm}, which compares theorems according to 
-  their proved propositions modulo alpha-equivalence).
-
-  You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into 
-  attributes with the code
+text {* 
+  We are going to modify this list by adding and deleting theorems.
+  For this we use the two functions @{ML MyThms.add_thm} and
+  @{ML MyThms.del_thm}. You can turn them into attributes 
+  with the code
 *}
 
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
+ML{*val my_add = Thm.declaration_attribute MyThms.add_thm
+val my_del = Thm.declaration_attribute MyThms.del_thm *}
 
 text {* 
   and set up the attributes as follows
 *}
 
 attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} 
-  "maintaining a list of my_thms - rough test only!" 
+  "maintaining a list of my_thms" 
 
 text {*
   The parser @{ML_ind  add_del in Attrib} is a predefined parser for 
@@ -1055,12 +1036,13 @@
   then you can see it is added to the initially empty list.
 
   @{ML_response_fake [display,gray]
-  "!my_thms" "[\"True\"]"}
+  "MyThms.get @{context}" 
+  "[\"True\"]"}
 
   You can also add theorems using the command \isacommand{declare}.
 *}
 
-declare test[my_thms] trueI_2[my_thms add] 
+declare test[my_thms] trueI_2[my_thms add]
 
 text {*
   With this attribute, the @{text "add"} operation is the default and does 
@@ -1068,7 +1050,7 @@
   theorem list to be updated as:
 
   @{ML_response_fake [display,gray]
-  "!my_thms"
+  "MyThms.get @{context}"
   "[\"True\", \"Suc (Suc 0) = 2\"]"}
 
   The theorem @{thm [source] trueI_2} only appears once, since the 
@@ -1081,144 +1063,14 @@
 text {* After this, the theorem list is again: 
 
   @{ML_response_fake [display,gray]
-  "!my_thms"
+  "MyThms.get @{context}"
   "[\"True\"]"}
 
-  We used in this example two functions declared as @{ML_ind  declaration_attribute in Thm}, 
-  but there can be any number of them. We just have to change the parser for reading
-  the arguments accordingly. 
-
-  However, as said at the beginning of this example, using references for storing theorems is
-  \emph{not} the received way of doing such things. The received way is to 
-  start a ``data slot'', below called @{text MyThmsData}, generated by the functor 
-  @{text GenericDataFun}:
-*}
-
-ML{*structure MyThmsData = GenericDataFun
- (type T = thm list
-  val empty = []
-  val extend = I
-  fun merge _ = Thm.merge_thms) *}
-
-text {*
-  The type @{text "T"} of this data slot is @{ML_type "thm list"}.\footnote{FIXME: give a pointer
-  to where data slots are explained properly.}
-  To use this data slot, you only have to change @{ML my_thm_add} and
-  @{ML my_thm_del} to:
-*}
-
-ML{*val my_thm_add = MyThmsData.map o Thm.add_thm
-val my_thm_del = MyThmsData.map o Thm.del_thm*}
-
-text {*
-  where @{ML MyThmsData.map} updates the data appropriately. The
-  corresponding theorem attributes are
-*}
-
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
-
-text {*
-  and the setup is as follows
-*}
-
-attribute_setup %gray my_thms2 = {* Attrib.add_del my_add my_del *} 
-  "properly maintaining a list of my_thms"
-
-text {*
-  Initially, the data slot is empty 
-
-  @{ML_response_fake [display,gray]
-  "MyThmsData.get (Context.Proof @{context})"
-  "[]"}
-
-  but if you prove
-*}
-
-lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
-
-text {*
-  then the lemma is recorded. 
-
-  @{ML_response_fake [display,gray]
-  "MyThmsData.get (Context.Proof @{context})"
-  "[\"3 = Suc (Suc (Suc 0))\"]"}
-
-  With theorem attribute @{text my_thms2} you can also nicely see why it 
-  is important to 
-  store data in a ``data slot'' and \emph{not} in a reference. Backtrack
-  to the point just before the lemma @{thm [source] three} was proved and 
-  check the the content of @{ML_struct MyThmsData}: it should be empty. 
-  The addition has been properly retracted. Now consider the proof:
-*}
+  We used in this example two functions declared as @{ML_ind
+  declaration_attribute in Thm}, but there can be any number of them. We just
+  have to change the parser for reading the arguments accordingly.
 
-lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
-
-text {*
-  Checking the content of @{ML my_thms} gives
-
-  @{ML_response_fake [display,gray]
-  "!my_thms"
-  "[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
-
-  as expected, but if you backtrack before the lemma @{thm [source] four}, the
-  content of @{ML my_thms} is unchanged. The backtracking mechanism
-  of Isabelle is completely oblivious about what to do with references, but
-  properly treats ``data slots''!
-
-  Since storing theorems in a list is such a common task, there is the special
-  functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain
-  a named theorem list, you just declare
-*}
-
-ML{*structure FooRules = Named_Thms
- (val name = "foo" 
-  val description = "Rules for foo") *}
-
-text {*
-  and set up the @{ML_struct FooRules} with the command
-*}
-
-setup %gray {* FooRules.setup *}
-
-text {*
-  This code declares a data slot 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 the rules marked with @{text "foo"} can be retrieved
-  using the function @{ML FooRules.get}:
-
-  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
-
-  \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
-  \end{readmore}
-
-  (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
-
+  \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}
 
   \begin{readmore}
   FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in 




