diff -r cb39c41548bd -r 7e0bf13bf743 CookBook/FirstSteps.thy --- 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)