--- a/CookBook/FirstSteps.thy	Thu Feb 26 14:20:52 2009 +0000
+++ b/CookBook/FirstSteps.thy	Fri Feb 27 13:02:19 2009 +0000
@@ -894,8 +894,7 @@
   theorem is proven. In particular, it is not possible to find out
   what are all theorems that have a given attribute in common, unless of course
   the function behind the attribute stores the theorems in a retrivable 
-  datastructure. This can be easily done by the recipe described in 
-  \ref{rec:named}. 
+  datastructure. 
 
   If you want to print out all currently known attributes a theorem 
   can have, you can use the function:
@@ -927,8 +926,7 @@
 
 setup {*
   Attrib.add_attributes 
-    [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")]
-*}
+    [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
 
 text {*
   The attribute does not expect any further arguments (unlike @{text "[OF
@@ -949,28 +947,186 @@
   @{text "> "}~@{thm test[my_sym]}
   \end{isabelle}
 
+  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
+  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.
 *}
 
+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 function @{ML Thm.declaration_attribute} expects us to 
+  provide two functions that add and delete theorems from this list. At
+  the moment we use the two functions:
+*}
+
+ML{*fun my_thms_add thm ctxt =
+  (my_thms := Thm.add_thm thm (!my_thms); ctxt)
+
+fun my_thms_del thm ctxt =
+  (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
+
 text {*
-What are: 
+  These functions take a theorem and a context and, for what we are explaining
+  here it is sufficient to 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).
 
 
-@{text "declaration_attribute"}
+  We can turn both functions into attributes using
+*}
+
+ML{*val my_add = Thm.declaration_attribute my_thms_add
+val my_del = Thm.declaration_attribute my_thms_del *}
+
+text {* 
+  and set up the attributes as follows
+*}
+
+setup {*
+  Attrib.add_attributes 
+    [("my_thms", Attrib.add_del_args my_add my_del, 
+        "maintaining a list of my_thms")] *}
+
+text {*
+  Now if you prove the lemma attaching 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.
+
+  @{ML_response_fake [display,gray]
+  "!my_thms" "[\"True\"]"}
+
+  We can also add theorems using the command \isacommand{declare}
+*}
+
+declare test[my_thms] trueI_2[my_thms add]
+
+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.
+
+  @{ML_response_fake [display,gray]
+  "!my_thms"
+  "[\"True\", \"Suc (Suc 0) = 2\"]"}
+
+  The theorem @{thm [source] trueI_2} only appears once, since the 
+  function @{ML Thm.add_thm} tests for duplicates, before extending
+  the list. Deletion from the list works as follows:
+*}
+
+declare test[my_thms del]
+
+text {* After this, the theorem list is: 
+
+  @{ML_response_fake [display,gray]
+  "!my_thms"
+  "[\"True\"]"}
+
+  We used in this example two functions declared as @{ML Thm.declaration_attribute}, 
+  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 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}:
+*}
 
-@{text "theory_attributes"}
+ML {*structure Data = GenericDataFun
+ (type T = thm list
+  val empty = []
+  val extend = I
+  fun merge _ = Thm.merge_thms) *}
+
+text {*
+  To use this data slot, we only have to change the functions @{ML my_thms_add} and
+  @{ML my_thms_del} to:
+*}
+
+ML{*val thm_add = Data.map o Thm.add_thm
+val thm_del = Data.map o Thm.del_thm*}
+
+text {*
+  where @{ML Data.map} updates the data appropriately in the context. 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"); *}
+
+text {*
+  and set up the @{ML_struct FooRules} with the command
+*}
+
+setup {* 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.
 
-@{text "proof_attributes"}
+  Furthermore, the facts are made available on the user level under the dynamic 
+  fact name @{text foo}. For example we 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"} an 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"} and also
+  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
+  data.
+  \end{readmore}
+
+  What are: 
+
+  @{text "theory_attributes"}
+  @{text "proof_attributes"}
 
 
   \begin{readmore}
   FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
   \end{readmore}
-
-
 *}
 
 
-section {* Theories and Local Theories *}
+section {* Theories, Contexts and Local Theories *}
 
 text {*
   (FIXME: expand)

--- a/CookBook/Intro.thy	Thu Feb 26 14:20:52 2009 +0000
+++ b/CookBook/Intro.thy	Fri Feb 27 13:02:19 2009 +0000
@@ -132,7 +132,7 @@
   about parsing.
 
   \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' 
-  chapter and also contributed recipe \ref{rec:named}.
+  chapter and also contributed the material on @{text NamedThmsFun}.
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining

--- a/CookBook/ROOT.ML	Thu Feb 26 14:20:52 2009 +0000
+++ b/CookBook/ROOT.ML	Fri Feb 27 13:02:19 2009 +0000
@@ -15,7 +15,6 @@
 use_thy "Package/Ind_Code";
 
 use_thy "Appendix";
-use_thy "Recipes/NamedThms";
 use_thy "Recipes/Antiquotes";
 use_thy "Recipes/TimeLimit";
 use_thy "Recipes/Config";

--- a/CookBook/Recipes/NamedThms.thy	Thu Feb 26 14:20:52 2009 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-theory NamedThms
-imports "../Base"
-begin
-
-section {* Accumulate a List of Theorems under a Name\label{rec:named} *} 
-
-
-text {*
-  {\bf Problem:} 
-  Your tool @{text foo} works with special rules, called @{text foo}-rules.
-  Users should be able to declare @{text foo}-rules in the theory,
-  which are then used in a method.\smallskip
-
-  {\bf Solution:} This can be achieved using named theorem lists.\smallskip
-
-  Named theorem lists can be set up using the code
-
-  *}
-
-ML{*structure FooRules = NamedThmsFun (
-  val name = "foo" 
-  val description = "Rules for foo"); *}
-
-text {*
-  and the command
-*}
-
-setup {* FooRules.setup *}
-
-text {*
-  This code declares a context data slot where the theorems are stored,
-  an attribute @{text foo} (with the usual @{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 we 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"} an 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"} and also
-  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
-  data.
-  \end{readmore}
- *}
-
-text {*
-  (FIXME: maybe add a comment about the case when the theorems 
-  to be added need to satisfy certain properties)
-
-*}
-
-
-end
-  
-
-
-

--- a/CookBook/Solutions.thy	Thu Feb 26 14:20:52 2009 +0000
+++ b/CookBook/Solutions.thy	Fri Feb 27 13:02:19 2009 +0000
@@ -1,5 +1,6 @@
 theory Solutions
 imports Base
+uses "infix_conv.ML"
 begin
 
 chapter {* Solutions to Most Exercises *}
@@ -90,9 +91,50 @@
   
   \begin{minipage}{\textwidth}
   @{subgoals [display]}
-  \end{minipage}
+  \end{minipage}\bigskip
+*}(*<*)oops(*>*)
+
+text {* \solution{ex:addconversion} *}
+
+text {*
+  (FIXME This solution works but is awkward.)
+*}
+
+ML{*fun add_conv ctxt ctrm =
+  (case Thm.term_of ctrm of
+     @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ => 
+         (let
+            val eq1 = Conv.binop_conv (add_conv ctxt) ctrm;
+            val ctrm' = Thm.rhs_of eq1;
+            val trm' = Thm.term_of ctrm';
+            val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm'
+          in
+             Thm.transitive eq1 eq2
+          end)       
+    | _ $ _ => Conv.combination_conv 
+                 (add_conv ctxt) (add_conv ctxt) ctrm
+    | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
+    | _ => Conv.all_conv ctrm)
+
+val add_tac = CSUBGOAL (fn (goal, i) =>
+  let
+    val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
+  in
+    CONVERSION
+      (Conv.params_conv ~1 (fn ctxt =>
+        (Conv.prems_conv ~1 (add_conv ctxt) then_conv
+          Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i
+  end)*}
+
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+  apply(tactic {* add_tac 1 *})?
+txt {* 
+  where the simproc produces the goal state
+  
+  \begin{minipage}{\textwidth}
+  @{subgoals [display]}
+  \end{minipage}\bigskip
 *}(*<*)oops(*>*)
 
 
-
 end
\ No newline at end of file

--- a/CookBook/Tactical.thy	Thu Feb 26 14:20:52 2009 +0000
+++ b/CookBook/Tactical.thy	Fri Feb 27 13:02:19 2009 +0000
@@ -662,17 +662,20 @@
   also described in \isccite{sec:results}. 
   \end{readmore}
 
-  A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. 
-  It allows you to inspect a given  subgoal. With this you can implement 
-  a tactic that applies a rule according to the topmost logic connective in the 
-  subgoal (to illustrate this we only analyse a few connectives). The code
-  of the tactic is as follows.\label{tac:selecttac}
+  Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
+  and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
+  presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
+  cterm}). With this you can implement a tactic that applies a rule according
+  to the topmost logic connective in the subgoal (to illustrate this we only
+  analyse a few connectives). The code of the tactic is as
+  follows.\label{tac:selecttac}
+
 *}
 
-ML %linenosgray{*fun select_tac (t,i) =
+ML %linenosgray{*fun select_tac (t, i) =
   case t of
-     @{term "Trueprop"} $ t' => select_tac (t',i)
-   | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)
+     @{term "Trueprop"} $ t' => select_tac (t', i)
+   | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
    | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
    | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
    | @{term "Not"} $ _ => rtac @{thm notI} i
@@ -727,8 +730,7 @@
   the first goal. To do this can result in quite messy code. In contrast, 
   the ``reverse application'' is easy to implement.
 
-  The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes
-  a @{ML_type cterm} instead of a @{ML_type term}.  Of course, this example is
+  Of course, this example is
   contrived: there are much simpler methods available in Isabelle for
   implementing a proof procedure analysing a goal according to its topmost
   connective. These simpler methods use tactic combinators, which we will
@@ -1013,7 +1015,7 @@
 
 *}
 
-section {* Rewriting and Simplifier Tactics *}
+section {* Simplifier Tactics *}
 
 text {*
   @{ML rewrite_goals_tac}
@@ -1458,7 +1460,7 @@
 
   Here the conversion of @{thm [source] true_conj1} only applies
   in the first case, but fails in the second. The whole conversion
-  does not fail, however, because the combinator @{ML else_conv} will then 
+  does not fail, however, because the combinator @{ML Conv.else_conv} will then 
   try out @{ML Conv.all_conv}, which always succeeds.
 
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
@@ -1600,8 +1602,8 @@
   in
     CONVERSION 
       (Conv.params_conv ~1 (fn ctxt =>
-        (Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv
-          Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i
+        (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
+          Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i
   end)*}
 
 text {* 
@@ -1629,15 +1631,23 @@
   and simprocs; the advantage of conversions, however, is that you never have
   to worry about non-termination.
 
+  \begin{exercise}\label{ex:addconversion}
+  Write a tactic that is based on conversions which does the same as the simproc in
+  exercise \ref{ex:addsimproc}, that is replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} 
+  by their result. You can make the same assumptions as in \ref{ex:addsimproc}.
+  \end{exercise}
+
   \begin{readmore}
   See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. 
   Further conversions are defined in  @{ML_file "Pure/thm.ML"},
   @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
   \end{readmore}
+
 *}
 
 
 
+
 section {* Structured Proofs *}
 
 text {* TBD *}

Binary file cookbook.pdf has changed