--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 12:13:33 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 18:17:24 2009 +0100
@@ -180,7 +180,7 @@
   into a @{ML_type cterm} using the function @{ML crep_thm}. 
 *}
 
-ML{*fun str_of_thm_raw ctxt thm =
+ML{*fun str_of_thm ctxt thm =
   str_of_cterm ctxt (#prop (crep_thm thm))*}
 
 text {*
@@ -188,7 +188,7 @@
   @{text "?Q"} and so on. 
 
   @{ML_response_fake [display, gray]
-  "warning (str_of_thm_raw @{context} @{thm conjI})"
+  "warning (str_of_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
   In order to improve the readability of theorems we convert
@@ -203,15 +203,15 @@
   thm'
 end
 
-fun str_of_thm ctxt thm =
+fun str_of_thm_no_vars ctxt thm =
   str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
 
 text {* 
-  Theorem @{thm [source] conjI} looks now as follows
+  Theorem @{thm [source] conjI} looks now as follows:
 
   @{ML_response_fake [display, gray]
-  "warning (str_of_thm_raw @{context} @{thm conjI})"
-  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+  "warning (str_of_thm_no_vars @{context} @{thm conjI})"
+  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
   
   Again the function @{ML commas} helps with printing more than one theorem. 
 *}
@@ -219,8 +219,8 @@
 ML{*fun str_of_thms ctxt thms =  
   commas (map (str_of_thm ctxt) thms)
 
-fun str_of_thms_raw ctxt thms =  
-  commas (map (str_of_thm_raw ctxt) thms)*}
+fun str_of_thms_no_vars ctxt thms =  
+  commas (map (str_of_thm_no_vars ctxt) thms) *}
 
 section {* Combinators\label{sec:combinators} *}
 
@@ -305,9 +305,9 @@
       |> (curry list_comb) f *}
 
 text {*
-  This code extracts the argument types of a given function and then generates 
+  This code extracts the argument types of a given function @{text "f"} and then generates 
   for each argument type a distinct variable; finally it applies the generated 
-  variables to the function. For example
+  variables to the function. For example:
 
   @{ML_response_fake [display,gray]
 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} 
@@ -323,8 +323,8 @@
   function @{ML variant_frees in Variable} generates for each @{text "z"} a
   unique name avoiding the given @{text f}; the list of name-type pairs is turned
   into a list of variable terms in Line 6, which in the last line is applied
-  by the function @{ML list_comb} to the function. We have to use the
-  function @{ML curry}, because @{ML list_comb} expects the function and the
+  by the function @{ML list_comb} to the function. In this last step we have to 
+  use the function @{ML curry}, because @{ML list_comb} expects the function and the
   variables list as a pair.
   
   The combinator @{ML "#>"} is the reverse function composition. It can be
@@ -525,7 +525,8 @@
   @{text "> "}@{thm TrueConj_def}
   \end{isabelle}
 
-  (FIXME give a better example why bindings are important)
+  (FIXME give a better example why bindings are important; maybe
+  give a pointer to \isacommand{local\_setup})
 
   While antiquotations have many applications, they were originally introduced in order 
   to avoid explicit bindings for theorems such as:
@@ -578,7 +579,7 @@
   "@{term \"(x::nat) x\"}"
   "Type unification failed \<dots>"}
 
-  raises a typing error, while it perfectly ok to construct
+  raises a typing error, while it perfectly ok to construct the term
   
   @{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"}
 
@@ -659,7 +660,7 @@
 ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
 
 text {*
-  To see this apply @{text "@{term S}"} and @{text "@{term T}"} 
+  To see this, apply @{text "@{term S}"} and @{text "@{term T}"} 
   to both functions. With @{ML make_imp} you obtain the intended term involving 
   the given arguments
 
@@ -679,7 +680,7 @@
 
   There are a number of handy functions that are frequently used for 
   constructing terms. One is the function @{ML list_comb}, which takes 
-  a term and a list of terms as argument, and produces as output the term
+  a term and a list of terms as arguments, and produces as output the term
   list applied to the term. For example
 
 @{ML_response_fake [display,gray]
@@ -693,7 +694,7 @@
   "lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}"
   "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
-  In the example @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}), 
+  In the example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}), 
   and an abstraction. It also records the type of the abstracted
   variable and for printing purposes also its name.  Note that because of the
   typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
@@ -710,8 +711,9 @@
   have different type.
 
   There is also the function @{ML subst_free} with which terms can 
-  be replaced by other terms. For example below we replace in  @{term "f 0 x"} 
-  the subterm @{term "f 0"} by @{term y} and @{term x} by @{term True}.
+  be replaced by other terms. For example below, we will replace in  
+  @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0 x"} 
+  the subterm @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0"} by @{term y}, and @{term x} by @{term True}.
 
   @{ML_response_fake [display,gray]
 "subst_free [(@{term \"(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0\"}, @{term \"y::nat\<Rightarrow>nat\"}),
@@ -1066,7 +1068,8 @@
   @{ML_file "Pure/thm.ML"}. 
   \end{readmore}
 
-  (FIXME: how to add case-names to goal states - maybe in the next section)
+  (FIXME: handy functions working on theorems; how to add case-names to goal 
+  states - maybe in the next section)
 *}
 
 section {* Theorem Attributes *}
@@ -1145,16 +1148,17 @@
   \end{isabelle}
 
   As an example of a slightly more complicated theorem attribute, we implement 
-  our version of @{text "[THEN \<dots>]"}. This attribute takes a list of theorems
-  as argument and resolves the proved theorem with this list (one theorem 
-  after another). The code for this attribute is:
+  our 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
 *}
 
 ML{*fun MY_THEN thms = 
   Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
 
 text {* 
-  where @{ML swap} swaps the components of a pair. The setup of this theorem
+  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
   attribute uses the parser @{ML Attrib.thms}, which parses a list of
   theorems. 
 *}
@@ -1178,7 +1182,7 @@
   @{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
   \end{isabelle}
 
-  Of course, it is also possible to combine different theorem attributes, as in:
+  It is also possible to combine different theorem attributes, as in:
   
   \begin{isabelle}
   \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
@@ -1186,7 +1190,7 @@
   \end{isabelle}
   
   However, here also a weakness of the concept
-  of theorem attributes show through: since theorem attributes can be an
+  of theorem attributes shows through: since theorem attributes can be
   arbitrary functions, they do not in general commute. If you try
 
   \begin{isabelle}
@@ -1198,8 +1202,8 @@
   does not resolve with meta-equations. 
 
   The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
-  Another usage of attributes is to add and delete theorems from stored data.
-  For example the attribute @{text "[simp]"} adds or deletes a theorem from the
+  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 Thm.declaration_attribute}. 
   To illustrate this function, let us introduce a reference containing a list
   of theorems.
@@ -1229,12 +1233,13 @@
   here it is sufficient that they just return the context unchanged. They change
   however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
   adds a theorem if it is not already included in the list, and @{ML
-  Thm.del_thm} deletes one. Both functions use the predicate @{ML
-  Thm.eq_thm_prop} which compares theorems according to their proved
-  propositions (modulo alpha-equivalence).
+  Thm.del_thm} deletes one (both functions use the predicate @{ML
+  Thm.eq_thm_prop}, which compares theorems according to their proved
+  propositions modulo alpha-equivalence).
 
 
-  You can turn both functions into attributes using
+  You can turn functions @{ML my_thms_add} and @{ML my_thms_del} into 
+  attributes with the code
 *}
 
 ML{*val my_add = Thm.declaration_attribute my_thms_add
@@ -1248,13 +1253,16 @@
   "maintaining a list of my_thms" 
 
 text {*
-  Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
+  The parser @{ML Attrib.add_del} is a predefined parser for 
+  adding and deleting lemmas. Now if you prove the next lemma 
+  and attach the attribute 
+  @{text "[my_thms]"}
 *}
 
 lemma trueI_2[my_thms]: "True" by simp
 
 text {*
-  then you can see the lemma is added to the initially empty list.
+  then you can see it is added to the initially empty list.
 
   @{ML_response_fake [display,gray]
   "!my_thms" "[\"True\"]"}
@@ -1266,8 +1274,8 @@
 
 text {*
   The @{text "add"} is the default operation and does not need
-  to be given. This declaration will cause the theorem list to be 
-  updated as follows.
+  to be explicitly given. These two declarations will cause the 
+  theorem list to be updated as:
 
   @{ML_response_fake [display,gray]
   "!my_thms"
@@ -1292,7 +1300,8 @@
 
   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'' in a context by using the functor @{text GenericDataFun}:
+  start a ``data slot'', below called @{text MyThmsData}, by using the functor 
+  @{text GenericDataFun}:
 *}
 
 ML {*structure MyThmsData = GenericDataFun
@@ -1310,40 +1319,67 @@
 val thm_del = MyThmsData.map o Thm.del_thm*}
 
 text {*
-  where @{ML MyThmsData.map} updates the data appropriately in the context. The
-  theorem addtributes are
+  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 *}
 
 text {*
-  ad the setup is as follows
+  and the setup is as follows
 *}
 
 attribute_setup %gray my_thms2 = {* Attrib.add_del add del *} 
   "properly maintaining a list of my_thms"
 
-ML {* MyThmsData.get (Context.Proof @{context}) *}
-
-lemma [my_thms2]: "2 = Suc (Suc 0)" by simp
+text {*
+  Initially, the data slot is empty
 
-ML {* MyThmsData.get (Context.Proof @{context}) *}
+  @{ML_response_fake [display,gray]
+  "MyThmsData.get (Context.Proof @{context})"
+  "[]"}
 
-ML {* !my_thms *}
+  but if you prove
+*}
+
+lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
 
 text {*
-  (FIXME: explain problem with backtracking)
+  the lemma is now included
+
+  @{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 
+  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:
+*}
+
+lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
 
-  Since storing
-  theorems in a special list is such a common task, there is the functor @{text NamedThmsFun},
-  which does most of the work for you. To obtain such a named theorem lists, you just
-  declare 
+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 we 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!
+
+  Since storing theorems in a special list is such a common task, there is the
+  functor @{text NamedThmsFun}, which does most of the work for you. To obtain
+  such a named theorem lists, you just declare
 *}
 
 ML{*structure FooRules = NamedThmsFun 
  (val name = "foo" 
-  val description = "Rules for foo"); *}
+  val description = "Rules for foo") *}
 
 text {*
   and set up the @{ML_struct FooRules} with the command

--- a/ProgTutorial/Intro.thy	Mon Mar 23 12:13:33 2009 +0100
+++ b/ProgTutorial/Intro.thy	Mon Mar 23 18:17:24 2009 +0100
@@ -144,6 +144,9 @@
 
   \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 
   chapter and also contributed the material on @{text NamedThmsFun}.
+
+  \item {\bf Christian Sternagel} proof read the tutorial and made 
+  comments. 
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining

--- a/ProgTutorial/Package/Ind_Code.thy	Mon Mar 23 12:13:33 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Mar 23 18:17:24 2009 +0100
@@ -97,7 +97,7 @@
   val arg =  ((@{binding "MyTrue"}, NoSyn), @{term True})
   val (def, lthy') = make_defs arg lthy 
 in
-  warning (str_of_thm lthy' def); lthy'
+  warning (str_of_thm_no_vars lthy' def); lthy'
 end *}
 
 text {*
@@ -218,7 +218,7 @@
   val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
 in
-  warning (str_of_thms lthy' defs); lthy'
+  warning (str_of_thms_no_vars lthy' defs); lthy'
 end *}
 
 text {*
@@ -413,7 +413,7 @@
   val intro = 
     prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys)
 in
-  warning (str_of_thm_raw lthy intro); lthy
+  warning (str_of_thm lthy intro); lthy
 end *} 
 
 text {*
@@ -477,7 +477,7 @@
   val tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   val ind_thms = inductions rules defs preds tyss lthy
 in
-  warning (str_of_thms_raw lthy ind_thms); lthy
+  warning (str_of_thms lthy ind_thms); lthy
 end *}
 
 
@@ -530,7 +530,7 @@
   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
-  warning (str_of_thm @{context} new_thm)
+  warning (str_of_thm_no_vars @{context} new_thm)
 end"
   "P a b c"}
 
@@ -538,7 +538,7 @@
   For example 
 
   @{ML_response_fake [display, gray]
-"warning (str_of_thm @{context} 
+"warning (str_of_thm_no_vars @{context} 
             (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
   "C"}
 *}
@@ -571,7 +571,7 @@
 ML {*
 fun chop_print_tac2 ctxt prems =
 let
-  val _ = warning (commas (map (str_of_thm ctxt) prems))
+  val _ = warning (commas (map (str_of_thm_no_vars ctxt) prems))
 in
    all_tac
 end

--- a/ProgTutorial/Parsing.thy	Mon Mar 23 12:13:33 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Mon Mar 23 18:17:24 2009 +0100
@@ -1051,7 +1051,7 @@
 *}
 
 (*<*)
-
+(* THIS IS AN OLD VERSION OF THE PARSING CHAPTER BY JEREMY DAWSON *)
 chapter {* Parsing *}
 
 text {*

--- a/ProgTutorial/Tactical.thy	Mon Mar 23 12:13:33 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Mon Mar 23 18:17:24 2009 +0100
@@ -209,7 +209,7 @@
 
 ML{*fun my_print_tac ctxt thm =
 let
-  val _ = warning (str_of_thm ctxt thm)
+  val _ = warning (str_of_thm_no_vars ctxt thm)
 in 
   Seq.single thm
 end*}
@@ -325,7 +325,7 @@
 
 *}
 
-section {* Simple Tactics *}
+section {* Simple Tactics\label{sec:simpletacs} *}
 
 text {*
   Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful 
@@ -546,7 +546,7 @@
   val str_of_params = str_of_cterms context params
   val str_of_asms = str_of_cterms context asms
   val str_of_concl = str_of_cterm context concl
-  val str_of_prems = str_of_thms context prems   
+  val str_of_prems = str_of_thms_no_vars context prems   
   val str_of_schms = str_of_cterms context (snd schematics)    
  
   val _ = (warning ("params: " ^ str_of_params);
@@ -1143,7 +1143,7 @@
   val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
-      "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+      "  " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm)
   fun name_ctrm (nm, ctrm) =
       "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
 

Binary file progtutorial.pdf has changed