10   build on top of this trusted core.

    10   build on top of this trusted core. The central data structures involved

    11   in this core are certified terms and types as well as theorems.

    18   One way to construct Isabelle terms, is by using the antiquotation 

    19   In Isabelle there are certified terms (respectively types) and uncertified

    19   \mbox{@{text "@{term \<dots>}"}}. For example

    20   terms. The latter are called just terms. One way to construct them is by 

    21   using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example

   449   (FIXME: Explain the following better.)

   451   \footnote{\bf FIXME: Explain the following better; maybe put in a separate

   452   section and link with the comment in the antiquotation section.}

   540   \begin{exercise}\footnote{Personal communication of

   543   \begin{exercise}\label{ex:debruijn}

   541   de Bruijn to Dyckhoff.}\label{ex:debruijn}

   544   Implement the function, which we below name deBruijn\footnote{According to 

   542   Implement the function, which we below name deBruijn, that depends on a natural

   545   personal communication of de Bruijn to Dyckhoff.}, that depends on a natural

   554   For n=3 this function returns the term

   557   This function returns for n=3 the term

   688   (FIXME: say something about sorts)

   691   \footnote{\bf FIXME: say something about sorts.}

   693   exercise given in \ref{ch:solutions} when they receive an ill-typed term

   696   exercise given in Appendix \ref{ch:solutions} when they receive an 

   694   as input.

   697   ill-typed term as input.

   985   arbitrary functions, they do not in general commute. If you try

   988   arbitrary functions, they do not commute in general. If you try

   995   The purpose of @{ML_ind  rule_attribute in Thm} is to directly manipulate theorems.

   998   The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate

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

   999   theorems.  Another usage of theorem attributes is to add and delete theorems

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

  1000   from stored data.  For example the theorem attribute @{text "[simp]"} adds

   998   current simpset. For these applications, you can use @{ML_ind  declaration_attribute in Thm}. 

  1001   or deletes a theorem from the current simpset. For these applications, you

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

  1002   can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,

  1000   of theorems.

  1003   let us introduce a theorem list.

  1001 *}

  1004 *}

  1002 

  1005 

  1003 ML{*val my_thms = Unsynchronized.ref ([] : thm list)*}

  1006 ML{*structure MyThms = Named_Thms

  1007   (val name = "attr_thms" 

  1008    val description = "Theorems for an Attribute") *}

  1006   The purpose of this reference is to store a list of theorems.

  1011   We are going to modify this list by adding and deleting theorems.

  1007   We are going to modify it by adding and deleting theorems.

  1012   For this we use the two functions @{ML MyThms.add_thm} and

  1008   However, a word of warning: such references must not 

  1013   @{ML MyThms.del_thm}. You can turn them into attributes 

  1009   be used in any code that is meant to be more than just for testing purposes! 

  1014   with the code

  1010   Here it is only used to illustrate matters. We will show later how to store 

  1015 *}

  1011   data properly without using references.

  1016 

  1012  

  1017 ML{*val my_add = Thm.declaration_attribute MyThms.add_thm

  1013   We need to provide two functions that add and delete theorems from this list. 

  1018 val my_del = Thm.declaration_attribute MyThms.del_thm *}

  1014   For this we use the two functions:

  1015 *}

  1016 

  1017 ML{*fun my_thm_add thm ctxt =

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

  1019 

  1020 fun my_thm_del thm ctxt =

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

  1022 

  1023 text {*

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

  1025   here it is sufficient that they just return the context unchanged. They change

  1026   however the reference @{ML my_thms}, whereby the function 

  1027   @{ML_ind  add_thm in Thm} adds a theorem if it is not already included in 

  1028   the list, and @{ML_ind  del_thm in Thm} deletes one (both functions use the 

  1029   predicate @{ML_ind  eq_thm_prop in Thm}, which compares theorems according to 

  1030   their proved propositions modulo alpha-equivalence).

  1031 

  1032   You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into 

  1033   attributes with the code

  1034 *}

  1035 

  1036 ML{*val my_add = Thm.declaration_attribute my_thm_add

  1037 val my_del = Thm.declaration_attribute my_thm_del *}

  1044   "maintaining a list of my_thms - rough test only!" 

  1025   "maintaining a list of my_thms" 

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

  1039   "MyThms.get @{context}" 

  1040   "[\"True\"]"}

  1063 declare test[my_thms] trueI_2[my_thms add] 

  1045 declare test[my_thms] trueI_2[my_thms add]

  1071   "!my_thms"

  1053   "MyThms.get @{context}"

  1084   "!my_thms"

  1066   "MyThms.get @{context}"

  1087   We used in this example two functions declared as @{ML_ind  declaration_attribute in Thm}, 

  1069   We used in this example two functions declared as @{ML_ind

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

  1070   declaration_attribute in Thm}, but there can be any number of them. We just

  1089   the arguments accordingly. 

  1071   have to change the parser for reading the arguments accordingly.

  1090 

  1072 

  1091   However, as said at the beginning of this example, using references for storing theorems is

  1073   \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}

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

  1093   start a ``data slot'', below called @{text MyThmsData}, generated by the functor 

  1094   @{text GenericDataFun}:

  1095 *}

  1096 

  1097 ML{*structure MyThmsData = GenericDataFun

  1098  (type T = thm list

  1099   val empty = []

  1100   val extend = I

  1101   fun merge _ = Thm.merge_thms) *}

  1102 

  1103 text {*

  1104   The type @{text "T"} of this data slot is @{ML_type "thm list"}.\footnote{FIXME: give a pointer

  1105   to where data slots are explained properly.}

  1106   To use this data slot, you only have to change @{ML my_thm_add} and

  1107   @{ML my_thm_del} to:

  1108 *}

  1109 

  1110 ML{*val my_thm_add = MyThmsData.map o Thm.add_thm

  1111 val my_thm_del = MyThmsData.map o Thm.del_thm*}

  1112 

  1113 text {*

  1114   where @{ML MyThmsData.map} updates the data appropriately. The

  1115   corresponding theorem attributes are

  1116 *}

  1117 

  1118 ML{*val my_add = Thm.declaration_attribute my_thm_add

  1119 val my_del = Thm.declaration_attribute my_thm_del *}

  1120 

  1121 text {*

  1122   and the setup is as follows

  1123 *}

  1124 

  1125 attribute_setup %gray my_thms2 = {* Attrib.add_del my_add my_del *} 

  1126   "properly maintaining a list of my_thms"

  1127 

  1128 text {*

  1129   Initially, the data slot is empty 

  1130 

  1131   @{ML_response_fake [display,gray]

  1132   "MyThmsData.get (Context.Proof @{context})"

  1133   "[]"}

  1134 

  1135   but if you prove

  1136 *}

  1137 

  1138 lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp

  1139 

  1140 text {*

  1141   then the lemma is recorded. 

  1142 

  1143   @{ML_response_fake [display,gray]

  1144   "MyThmsData.get (Context.Proof @{context})"

  1145   "[\"3 = Suc (Suc (Suc 0))\"]"}

  1146 

  1147   With theorem attribute @{text my_thms2} you can also nicely see why it 

  1148   is important to 

  1149   store data in a ``data slot'' and \emph{not} in a reference. Backtrack

  1150   to the point just before the lemma @{thm [source] three} was proved and 

  1151   check the the content of @{ML_struct MyThmsData}: it should be empty. 

  1152   The addition has been properly retracted. Now consider the proof:

  1153 *}

  1154 

  1155 lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp

  1156 

  1157 text {*

  1158   Checking the content of @{ML my_thms} gives

  1159 

  1160   @{ML_response_fake [display,gray]

  1161   "!my_thms"

  1162   "[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}

  1163 

  1164   as expected, but if you backtrack before the lemma @{thm [source] four}, the

  1165   content of @{ML my_thms} is unchanged. The backtracking mechanism

  1166   of Isabelle is completely oblivious about what to do with references, but

  1167   properly treats ``data slots''!

  1168 

  1169   Since storing theorems in a list is such a common task, there is the special

  1170   functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain

  1171   a named theorem list, you just declare

  1172 *}

  1173 

  1174 ML{*structure FooRules = Named_Thms

  1175  (val name = "foo" 

  1176   val description = "Rules for foo") *}

  1177 

  1178 text {*

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

  1180 *}

  1181 

  1182 setup %gray {* FooRules.setup *}

  1183 

  1184 text {*

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

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

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

  1188   modify the theorems.

  1189 

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

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

  1192   @{text foo} by:

  1193 *}

  1194 

  1195 lemma rule1[foo]: "A" sorry

  1196 lemma rule2[foo]: "B" sorry

  1197 lemma rule3[foo]: "C" sorry

  1198 

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

  1200 

  1201 declare rule1[foo del]

  1202 

  1203 text {* and query the remaining ones with:

  1204 

  1205   \begin{isabelle}

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

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

  1208   @{text "> ?B"}

  1209   \end{isabelle}

  1210 

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

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

  1213 

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

  1215 

  1216   \begin{readmore}

  1217   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.

  1218   \end{readmore}

  1219 

  1220   (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)

  1221