1052   theories).  On the other hand, data such as facts change inside a proof and

  1052   theories).  On the other hand, data such as facts change inside a proof and

  1053   are only relevant to the proof at hand. Therefore such data needs to be 

  1053   are only relevant to the proof at hand. Therefore such data needs to be 

  1054   maintained inside a proof context, which represents ``local'' data.

  1054   maintained inside a proof context, which represents ``local'' data.

  1055 

  1055 

  1056   For theories and proof contexts there are, respectively, the functors 

  1056   For theories and proof contexts there are, respectively, the functors 

  1058   with the data storage. Below we show how to implement a table in which you

  1058   with the data storage. Below we show how to implement a table in which you

  1059   can store theorems and look them up according to a string key. The

  1059   can store theorems and look them up according to a string key. The

  1060   intention in this example is to be able to look up introduction rules for logical

  1060   intention in this example is to be able to look up introduction rules for logical

  1061   connectives. Such a table might be useful in an automatic proof procedure

  1061   connectives. Such a table might be useful in an automatic proof procedure

  1062   and therefore it makes sense to store this data inside a theory.  

  1062   and therefore it makes sense to store this data inside a theory.  

  1064   The code for the table is:

  1064   The code for the table is:

  1065 *}

  1065 *}

  1066 

  1066 

  1068   (type T = thm Symtab.table

  1068   (type T = thm Symtab.table

  1069    val empty = Symtab.empty

  1069    val empty = Symtab.empty

  1071    val extend = I

  1070    val extend = I

  1073 

  1072 

  1074 text {*

  1073 text {*

  1075   In order to store data in a theory, we have to specify the type of the data

  1074   In order to store data in a theory, we have to specify the type of the data

  1076   (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"},

  1075   (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"},

  1077   which stands for a table in which @{ML_type string}s can be looked up

  1076   which stands for a table in which @{ML_type string}s can be looked up

  1078   producing an associated @{ML_type thm}. We also have to specify four

  1077   producing an associated @{ML_type thm}. We also have to specify four

  1079   functions to use this functor: namely how to initialise the data storage

  1078   functions to use this functor: namely how to initialise the data storage

  1082   operations performed on theories and we just give some sensible 

  1081   operations performed on theories and we just give some sensible 

  1083   defaults.\footnote{\bf FIXME: Say more about the

  1082   defaults.\footnote{\bf FIXME: Say more about the

  1084   assumptions of these operations.} The result structure @{ML_text Data}

  1083   assumptions of these operations.} The result structure @{ML_text Data}

  1085   contains functions for accessing the table (@{ML Data.get}) and for updating

  1084   contains functions for accessing the table (@{ML Data.get}) and for updating

  1088   auxiliary functions, which help us with accessing the table.

  1087   auxiliary functions, which help us with accessing the table.

  1089 *}

  1088 *}

  1090 

  1089 

  1091 ML{*val lookup = Symtab.lookup o Data.get

  1090 ML{*val lookup = Symtab.lookup o Data.get

  1092 fun update k v = Data.map (Symtab.update (k, v))*}

  1091 fun update k v = Data.map (Symtab.update (k, v))*}

  1131   defeat its undo-mechanism. To see the latter, consider the 

  1130   defeat its undo-mechanism. To see the latter, consider the 

  1132   following data container where we maintain a reference to a list of 

  1131   following data container where we maintain a reference to a list of 

  1133   integers.

  1132   integers.

  1134 *}

  1133 *}

  1135 

  1134 

  1137   (type T = (int list) Unsynchronized.ref

  1136   (type T = (int list) Unsynchronized.ref

  1138    val empty = Unsynchronized.ref []

  1137    val empty = Unsynchronized.ref []

  1140    val extend = I

  1138    val extend = I

  1142 

  1140 

  1143 text {*

  1141 text {*

  1144   We initialise the reference with the empty list. Consequently a first 

  1142   We initialise the reference with the empty list. Consequently a first 

  1145   lookup produces @{ML "ref []" in Unsynchronized}.

  1143   lookup produces @{ML "ref []" in Unsynchronized}.

  1146 

  1144 

  1194   directed graphs in @{ML_file "Pure/General/graph.ML"}, and 

  1192   directed graphs in @{ML_file "Pure/General/graph.ML"}, and 

  1195   tables and symtables in @{ML_file "Pure/General/table.ML"}.

  1193   tables and symtables in @{ML_file "Pure/General/table.ML"}.

  1196   \end{readmore}

  1194   \end{readmore}

  1197 

  1195 

  1198   Storing data in a proof context is done in a similar fashion. As mentioned

  1196   Storing data in a proof context is done in a similar fashion. As mentioned

  1200   following code we can store a list of terms in a proof context.

  1198   following code we can store a list of terms in a proof context.

  1201 *}

  1199 *}

  1202 

  1200 

  1204   (type T = term list

  1202   (type T = term list

  1205    fun init _ = [])*}

  1203    fun init _ = [])*}

  1206 

  1204 

  1207 text {*

  1205 text {*

  1208   The function we have to specify has to produce a list once a context 

  1206   The function we have to specify has to produce a list once a context