--- 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)