
diff -r 096776f180fc -r d3cd633e8240 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Tue Mar 24 09:34:03 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Tue Mar 24 12:09:38 2009 +0100
@@ -132,15 +132,17 @@
 *}
 
 (*
-ML {* set Toplevel.debug *}
+ML {* reset Toplevel.debug *}
+
+ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
 
-ML {*
-fun dodgy_fun () = (raise (ERROR "bar"); 1) 
-*}
+ML {* fun innocent () = dodgy_fun () *}
+ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}
+ML {* exception_trace (fn () => innocent ()) *}
 
-ML {* fun f1 () = dodgy_fun () *}
+ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}
 
-ML {* f1 () *}
+ML {* Toplevel.program (fn () => innocent ()) *}
 *)
 
 text {*
@@ -207,7 +209,7 @@
   str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
 
 text {* 
-  Theorem @{thm [source] conjI} looks now as follows:
+  Theorem @{thm [source] conjI} is now printed as follows:
 
   @{ML_response_fake [display, gray]
   "warning (str_of_thm_no_vars @{context} @{thm conjI})"
@@ -520,7 +522,6 @@
     ((@{binding "TrueConj"}, NoSyn), 
      (Attrib.empty_binding, @{term "True \<and> True"})) *}
 
-<<<<<<< local
 text {* 
   Now querying the definition you obtain:
 
@@ -560,7 +561,7 @@
 "Const (\"op =\", \<dots>) $ 
   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
-  will show the term @{term "(a::nat) + b = c"}, but printed using an internal
+  will show the term @{term "(a::nat) + b = c"}, but printed using the internal
   representation corresponding to the data type @{ML_type "term"}.
   
   This internal representation uses the usual de Bruijn index mechanism---where
@@ -937,6 +938,12 @@
   "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
   "nat \<Rightarrow> bool"}
 
+  or with the antiquotation:
+
+  @{ML_response_fake [display,gray]
+  "@{ctyp \"nat \<Rightarrow> bool\"}"
+  "nat \<Rightarrow> bool"}
+
   \begin{readmore}
   For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
   the file @{ML_file "Pure/thm.ML"}.
@@ -1072,8 +1079,10 @@
   @{ML_file "Pure/thm.ML"}. 
   \end{readmore}
 
-  (FIXME: handy functions working on theorems; how to add case-names to goal 
-  states - maybe in the next section)
+  (FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on) 
+
+  (FIXME how to add case-names to goal states - maybe in the 
+  next section)
 *}
 
 section {* Theorem Attributes *}
@@ -1099,8 +1108,8 @@
   \end{isabelle}
   
   The theorem attributes fall roughly into two categories: the first category manipulates
-  the proved theorem (like @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
-  stores the proved theorem somewhere as data (like @{text "[simp]"}, which adds
+  the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
+  stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds
   the theorem to the current simpset).
 
   To explain how to write your own attribute, let us start with an extremely simple 
@@ -1114,8 +1123,10 @@
 text {* 
   where the function @{ML "Thm.rule_attribute"} expects a function taking a 
   context (which we ignore in the code above) and a theorem (@{text thm}), and 
-  returns another theorem (namely @{text thm} resolved with the lemma 
-  @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 
+  returns another theorem (namely @{text thm} resolved with the theorem 
+  @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained
+  later on in Section~\ref{sec:simpletacs}.} The function 
+  @{ML "Thm.rule_attribute"} then returns 
   an attribute.
 
   Before we can use the attribute, we need to set it up. This can be done
@@ -1126,11 +1137,11 @@
   "applying the sym rule"
 
 text {*
-  The attribute does not expect any further arguments (unlike @{text "[THEN
-  \<dots>]"}, for example). Therefore
-  we use the parser @{ML Scan.succeed}. Later on we will also consider
-  attributes taking further arguments. An example for the attribute @{text
-  "[my_sym]"} is the proof
+  Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
+  for the theorem attribute. Since the attribute does not expect any further 
+  arguments (unlike @{text "[THEN \<dots>]"}, for example), we use the parser @{ML
+  Scan.succeed}. Later on we will also consider attributes taking further
+  arguments. An example for the attribute @{text "[my_sym]"} is the proof
 *} 
 
 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
@@ -1152,7 +1163,7 @@
   \end{isabelle}
 
   As an example of a slightly more complicated theorem attribute, we implement 
-  our version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
+  our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
   as argument and resolve the proved theorem with this list (one theorem 
   after another). The code for this attribute is
 *}
@@ -1161,8 +1172,7 @@
   Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
 
 text {* 
-  where @{ML swap} swaps the components of a pair (@{ML RS} is explained
-  later on in Section~\ref{sec:simpletacs}). The setup of this theorem
+  where @{ML swap} swaps the components of a pair. The setup of this theorem
   attribute uses the parser @{ML Attrib.thms}, which parses a list of
   theorems. 
 *}
@@ -1216,20 +1226,20 @@
 ML{*val my_thms = ref ([] : thm list)*}
 
 text {* 
-  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.
+  The purpose of this reference is that we are going to add and delete theorems
+  to the referenced list. 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.
  
-  The function @{ML Thm.declaration_attribute} expects us to 
-  provide two functions that add and delete theorems from this list. 
+  We need to provide two functions that add and delete theorems from this list. 
   For this we use the two functions:
 *}
 
-ML{*fun my_thms_add thm ctxt =
+ML{*fun my_thm_add thm ctxt =
   (my_thms := Thm.add_thm thm (!my_thms); ctxt)
 
-fun my_thms_del thm ctxt =
+fun my_thm_del thm ctxt =
   (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
 
 text {*
@@ -1242,25 +1252,24 @@
   propositions modulo alpha-equivalence).
 
 
-  You can turn functions @{ML my_thms_add} and @{ML my_thms_del} into 
+  You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into 
   attributes with the code
 *}
 
-ML{*val my_add = Thm.declaration_attribute my_thms_add
-val my_del = Thm.declaration_attribute my_thms_del *}
+ML{*val my_add = Thm.declaration_attribute my_thm_add
+val my_del = Thm.declaration_attribute my_thm_del *}
 
 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" 
+  "maintaining a list of my_thms - rough test only!" 
 
 text {*
-  The parser @{ML Attrib.add_del} is a predefined parser for 
+  The parser @{ML Attrib.add_del} is a pre-defined parser for 
   adding and deleting lemmas. Now if you prove the next lemma 
-  and attach the attribute 
-  @{text "[my_thms]"}
+  and attach to it the attribute @{text "[my_thms]"}
 *}
 
 lemma trueI_2[my_thms]: "True" by simp
@@ -1274,11 +1283,11 @@
   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 {*
-  The @{text "add"} is the default operation and does not need
-  to be explicitly given. These two declarations will cause the 
+  With this attribute, the @{text "add"} operation is the default and does 
+  not need to be explicitly given. These three declarations will cause the 
   theorem list to be updated as:
 
   @{ML_response_fake [display,gray]
@@ -1304,7 +1313,7 @@
 
   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}, by using the functor 
+  start a ``data slot'', below called @{text MyThmsData}, generated by the functor 
   @{text GenericDataFun}:
 *}
 
@@ -1315,30 +1324,32 @@
   fun merge _ = Thm.merge_thms) *}
 
 text {*
-  To use this data slot, you only have to change @{ML my_thms_add} and
-  @{ML my_thms_del} to:
+  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 thm_add = MyThmsData.map o Thm.add_thm
-val thm_del = MyThmsData.map o Thm.del_thm*}
+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 addtributes are
 *}
 
-ML{*val add = Thm.declaration_attribute thm_add
-val del = Thm.declaration_attribute thm_del *}
+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 add del *} 
+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
+  Initially, the data slot is empty 
 
   @{ML_response_fake [display,gray]
   "MyThmsData.get (Context.Proof @{context})"
@@ -1350,17 +1361,18 @@
 lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
 
 text {*
-  the lemma is now included
+  then the lemma is recorded. 
 
   @{ML_response_fake [display,gray]
   "MyThmsData.get (Context.Proof @{context})"
   "[\"3 = Suc (Suc (Suc 0))\"]"}
 
-  With @{text my_thms2} you can also nicely see why it is important to 
+  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} is proved and 
-  check the the content of @{ML_struct "MyThmsData"}: it is now again 
-  empty. The addition has been properly retracted. Now consider the proof:
+  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:
 *}
 
 lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
@@ -1372,13 +1384,14 @@
   "!my_thms"
   "[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
 
-  as expected, but if we backtrack before the lemma @{thm [source] four}, the
+  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!
+  of Isabelle is completely oblivious about what to do with references, but
+  properly treats ``data slots''!
 
-  Since storing theorems in a special list is such a common task, there is the
+  Since storing theorems in a list is such a common task, there is the special
   functor @{text NamedThmsFun}, which does most of the work for you. To obtain
-  such a named theorem lists, you just declare
+  a named theorem lists, you just declare
 *}
 
 ML{*structure FooRules = NamedThmsFun 
@@ -1433,7 +1446,9 @@
 
 
   \begin{readmore}
-  FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
+  FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in 
+  @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
+  parsing.
   \end{readmore}
 *}
 




