897   datastructure. This can be easily done by the recipe described in 

   897   datastructure. 

   898   \ref{rec:named}. 

   930     [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")]

   929     [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}

   931 *}

   952 *}

   950   The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.

   953 

   951   Another usage of attributes is to add and delete theorems from stored data.

   954 text {*

   952   For example the attribute @{text "[simp]"} adds or deletes a theorem from the

   955 What are: 

   953   current simpset. For these applications, you can use @{ML Thm.declaration_attribute}. 

   956 

   954   To illustrate this function, let us introduce a reference containing a list

   957 

   955   of theorems.

   958 @{text "declaration_attribute"}

   956 *}

   959 

   957 

   960 @{text "theory_attributes"}

   958 ML{*val my_thms = ref ([]:thm list)*}

   961 

   959 

   962 @{text "proof_attributes"}

   960 text {* 

   961   A word of warning: such references must not be used in any code that

   962   is meant to be more than just for testing purposes! Here it is only used 

   963   to illustrate matters. We will show later how to store data properly without 

   964   using references. The function @{ML Thm.declaration_attribute} expects us to 

   965   provide two functions that add and delete theorems from this list. At

   966   the moment we use the two functions:

   967 *}

   968 

   969 ML{*fun my_thms_add thm ctxt =

   970   (my_thms := Thm.add_thm thm (!my_thms); ctxt)

   971 

   972 fun my_thms_del thm ctxt =

   973   (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}

   974 

   975 text {*

   976   These functions take a theorem and a context and, for what we are explaining

   977   here it is sufficient to just return the context unchanged. They change

   978   however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}

   979   adds a theorem if it is not already included in the list, and @{ML

   980   Thm.del_thm} deletes one. Both functions use the predicate @{ML

   981   Thm.eq_thm_prop} which compares theorems according to their proved

   982   propositions (modulo alpha-equivalence).

   983 

   984 

   985   We can turn both functions into attributes using

   986 *}

   987 

   988 ML{*val my_add = Thm.declaration_attribute my_thms_add

   989 val my_del = Thm.declaration_attribute my_thms_del *}

   990 

   991 text {* 

   992   and set up the attributes as follows

   993 *}

   994 

   995 setup {*

   996   Attrib.add_attributes 

   997     [("my_thms", Attrib.add_del_args my_add my_del, 

   998         "maintaining a list of my_thms")] *}

   999 

  1000 text {*

  1001   Now if you prove the lemma attaching the attribute @{text "[my_thms]"}

  1002 *}

  1003 

  1004 lemma trueI_2[my_thms]: "True" by simp

  1005 

  1006 text {*

  1007   then you can see the lemma is added to the initially empty list.

  1008 

  1009   @{ML_response_fake [display,gray]

  1010   "!my_thms" "[\"True\"]"}

  1011 

  1012   We can also add theorems using the command \isacommand{declare}

  1013 *}

  1014 

  1015 declare test[my_thms] trueI_2[my_thms add]

  1016 

  1017 text {*

  1018   The @{text "add"} is the default operation and does not need

  1019   to be given. This declaration will cause the theorem list to be 

  1020   updated as follows.

  1021 

  1022   @{ML_response_fake [display,gray]

  1023   "!my_thms"

  1024   "[\"True\", \"Suc (Suc 0) = 2\"]"}

  1025 

  1026   The theorem @{thm [source] trueI_2} only appears once, since the 

  1027   function @{ML Thm.add_thm} tests for duplicates, before extending

  1028   the list. Deletion from the list works as follows:

  1029 *}

  1030 

  1031 declare test[my_thms del]

  1032 

  1033 text {* After this, the theorem list is: 

  1034 

  1035   @{ML_response_fake [display,gray]

  1036   "!my_thms"

  1037   "[\"True\"]"}

  1038 

  1039   We used in this example two functions declared as @{ML Thm.declaration_attribute}, 

  1040   but there can be any number of them. We just have to change the parser for reading

  1041   the arguments accordingly. 

  1042 

  1043   However, as said at the beginning using references for storing theorems is

  1044   \emph{not} the received way of doing such things. The received way is to 

  1045   start a ``data slot'' in a context by using the functor @{text GenericDataFun}:

  1046 *}

  1047 

  1048 ML {*structure Data = GenericDataFun

  1049  (type T = thm list

  1050   val empty = []

  1051   val extend = I

  1052   fun merge _ = Thm.merge_thms) *}

  1053 

  1054 text {*

  1055   To use this data slot, we only have to change the functions @{ML my_thms_add} and

  1056   @{ML my_thms_del} to:

  1057 *}

  1058 

  1059 ML{*val thm_add = Data.map o Thm.add_thm

  1060 val thm_del = Data.map o Thm.del_thm*}

  1061 

  1062 text {*

  1063   where @{ML Data.map} updates the data appropriately in the context. Since storing

  1064   theorems in a special list is such a common task, there is the functor @{text NamedThmsFun},

  1065   which does most of the work for you. To obtain such a named theorem lists, you just

  1066   declare 

  1067 *}

  1068 

  1069 ML{*structure FooRules = NamedThmsFun 

  1070  (val name = "foo" 

  1071   val description = "Rules for foo"); *}

  1072 

  1073 text {*

  1074   and set up the @{ML_struct FooRules} with the command

  1075 *}

  1076 

  1077 setup {* FooRules.setup *}

  1078 

  1079 text {*

  1080   This code declares a data slot where the theorems are stored,

  1081   an attribute @{text foo} (with the @{text add} and @{text del} options

  1082   for adding and deleting theorems) and an internal ML interface to retrieve and 

  1083   modify the theorems.

  1084 

  1085   Furthermore, the facts are made available on the user level under the dynamic 

  1086   fact name @{text foo}. For example we can declare three lemmas to be of the kind

  1087   @{text foo} by:

  1088 *}

  1089 

  1090 lemma rule1[foo]: "A" sorry

  1091 lemma rule2[foo]: "B" sorry

  1092 lemma rule3[foo]: "C" sorry

  1093 

  1094 text {* and undeclare the first one by: *}

  1095 

  1096 declare rule1[foo del]

  1097 

  1098 text {* and query the remaining ones with:

  1099 

  1100   \begin{isabelle}

  1101   \isacommand{thm}~@{text "foo"}\\

  1102   @{text "> ?C"}\\

  1103   @{text "> ?B"}

  1104   \end{isabelle}

  1105 

  1106   On the ML-level the rules marked with @{text "foo"} an be retrieved

  1107   using the function @{ML FooRules.get}:

  1108 

  1109   @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}

  1110 

  1111   \begin{readmore}

  1112   For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also

  1113   the recipe in Section~\ref{recipe:storingdata} about storing arbitrary

  1114   data.

  1115   \end{readmore}

  1116 

  1117   What are: 

  1118 

  1119   @{text "theory_attributes"}

  1120   @{text "proof_attributes"}

   968 

  1126 *}

   969 

  1127 

   970 *}

  1128 

   971 

  1129 section {* Theories, Contexts and Local Theories *}

   972 

   973 section {* Theories and Local Theories *}