834 section {* Terms and Types *}

   835 

   836 text {*

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

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

   839 

   840   @{ML_response [display,gray] 

   841 "@{term \"(a::nat) + b = c\"}" 

   842 "Const (\"op =\", \<dots>) $ 

   843   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

   844 

   845   will show the term @{term "(a::nat) + b = c"}, but printed using the internal

   846   representation corresponding to the datatype @{ML_type  "term"} defined as follows: 

   847 *}  

   848 

   849 ML_val %linenosgray{*datatype term =

   850   Const of string * typ 

   851 | Free of string * typ 

   852 | Var of indexname * typ 

   853 | Bound of int 

   854 | Abs of string * typ * term 

   855 | $ of term * term *}

   856 

   857 text {*

   858   This datatype implements lambda-terms typed in Church-style.

   859   As can be seen in Line 5, terms use the usual de Bruijn index mechanism

   860   for representing bound variables.  For

   861   example in

   862 

   863   @{ML_response_fake [display, gray]

   864   "@{term \"\<lambda>x y. x y\"}"

   865   "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}

   866 

   867   the indices refer to the number of Abstractions (@{ML Abs}) that we need to

   868   skip until we hit the @{ML Abs} that binds the corresponding

   869   variable. Constructing a term with dangling de Bruijn indices is possible,

   870   but will be flagged as ill-formed when you try to typecheck or certify it

   871   (see Section~\ref{sec:typechecking}). Note that the names of bound variables

   872   are kept at abstractions for printing purposes, and so should be treated

   873   only as ``comments''.  Application in Isabelle is realised with the

   874   term-constructor @{ML $}.

   875 

   876   Isabelle makes a distinction between \emph{free} variables (term-constructor

   877   @{ML Free} and written on the user level in blue colour) and

   878   \emph{schematic} variables (term-constructor @{ML Var} and written with a

   879   leading question mark). Consider the following two examples

   880   

   881   @{ML_response_fake [display, gray]

   882 "let

   883   val v1 = Var ((\"x\", 3), @{typ bool})

   884   val v2 = Var ((\"x1\", 3), @{typ bool})

   885   val v3 = Free (\"x\", @{typ bool})

   886 in

   887   string_of_terms @{context} [v1, v2, v3]

   888   |> tracing

   889 end"

   890 "?x3, ?x1.3, x"}

   891 

   892   When constructing terms, you are usually concerned with free variables (as

   893   mentioned earlier, you cannot construct schematic variables using the

   894   antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,

   895   however, observe the distinction. The reason is that only schematic

   896   varaibles can be instantiated with terms when a theorem is applied. A

   897   similar distinction between free and schematic variables holds for types

   898   (see below).

   899 

   900   \begin{readmore}

   901   Terms and types are described in detail in \isccite{sec:terms}. Their

   902   definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.

   903   For constructing terms involving HOL constants, many helper functions are defined

   904   in @{ML_file "HOL/Tools/hologic.ML"}.

   905   \end{readmore}

   906   

   907   Constructing terms via antiquotations has the advantage that only typable

   908   terms can be constructed. For example

   909 

   910   @{ML_response_fake_both [display,gray]

   911   "@{term \"x x\"}"

   912   "Type unification failed: Occurs check!"}

   913 

   914   raises a typing error, while it perfectly ok to construct the term

   915 

   916   @{ML_response_fake [display,gray] 

   917 "let

   918   val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})

   919 in 

   920   tracing (string_of_term @{context} omega)

   921 end"

   922   "x x"}

   923 

   924   with the raw ML-constructors.

   925   

   926   Sometimes the internal representation of terms can be surprisingly different

   927   from what you see at the user-level, because the layers of

   928   parsing/type-checking/pretty printing can be quite elaborate. 

   929 

   930   \begin{exercise}

   931   Look at the internal term representation of the following terms, and

   932   find out why they are represented like this:

   933 

   934   \begin{itemize}

   935   \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}  

   936   \item @{term "\<lambda>(x,y). P y x"}  

   937   \item @{term "{ [x::int] | x. x \<le> -2 }"}  

   938   \end{itemize}

   939 

   940   Hint: The third term is already quite big, and the pretty printer

   941   may omit parts of it by default. If you want to see all of it, you

   942   can use the following ML-function to set the printing depth to a higher 

   943   value:

   944 

   945   @{ML [display,gray] "print_depth 50"}

   946   \end{exercise}

   947 

   948   The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 

   949   usually invisible @{text "Trueprop"}-coercions whenever necessary. 

   950   Consider for example the pairs

   951 

   952 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 

   953 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),

   954  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}

   955  

   956   where a coercion is inserted in the second component and 

   957 

   958   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 

   959   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, 

   960  Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}

   961 

   962   where it is not (since it is already constructed by a meta-implication). 

   963   The purpose of the @{text "Trueprop"}-coercion is to embed formulae of

   964   an object logic, for example HOL, into the meta-logic of Isabelle. It

   965   is needed whenever a term is constructed that will be proved as a theorem. 

   966 

   967   As already seen above, types can be constructed using the antiquotation 

   968   @{text "@{typ \<dots>}"}. For example:

   969 

   970   @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}

   971 

   972   The corresponding datatype is

   973 *}

   974   

   975 ML_val{*datatype typ =

   976   Type  of string * typ list 

   977 | TFree of string * sort 

   978 | TVar  of indexname * sort *}

   979 

   980 text {*

   981   Like with terms, there is the distinction between free type

   982   variables (term-constructor @{ML "TFree"} and schematic

   983   type variables (term-constructor @{ML "TVar"}). A type constant,

   984   like @{typ "int"} or @{typ bool}, are types with an empty list

   985   of argument types. However, it is a bit difficult to show an

   986   example, because Isabelle always pretty-prints types (unlike terms).

   987   Here is a contrived example:

   988 

   989   @{ML_response [display, gray]

   990   "if Type (\"bool\", []) = @{typ \"bool\"} then true else false"

   991   "true"}

   992 

   993   \begin{readmore}

   994   Types are described in detail in \isccite{sec:types}. Their

   995   definition and many useful operations are implemented 

   996   in @{ML_file "Pure/type.ML"}.

   997   \end{readmore}

   998 *}

   999 

  1000 section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 

  1001 

  1002 text {*

  1003   While antiquotations are very convenient for constructing terms, they can

  1004   only construct fixed terms (remember they are ``linked'' at compile-time).

  1005   However, you often need to construct terms dynamically. For example, a

  1006   function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking

  1007   @{term P} and @{term Q} as arguments can only be written as:

  1008 

  1009 *}

  1010 

  1011 ML{*fun make_imp P Q =

  1012 let

  1013   val x = Free ("x", @{typ nat})

  1014 in 

  1015   Logic.all x (Logic.mk_implies (P $ x, Q $ x))

  1016 end *}

  1017 

  1018 text {*

  1019   The reason is that you cannot pass the arguments @{term P} and @{term Q} 

  1020   into an antiquotation.\footnote{At least not at the moment.} For example 

  1021   the following does \emph{not} work.

  1022 *}

  1023 

  1024 ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}

  1025 

  1026 text {*

  1027   To see this, apply @{text "@{term S}"} and @{text "@{term T}"} 

  1028   to both functions. With @{ML make_imp} you obtain the intended term involving 

  1029   the given arguments

  1030 

  1031   @{ML_response [display,gray] "make_imp @{term S} @{term T}" 

  1032 "Const \<dots> $ 

  1033   Abs (\"x\", Type (\"nat\",[]),

  1034     Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}

  1035 

  1036   whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 

  1037   and @{text "Q"} from the antiquotation.

  1038 

  1039   @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" 

  1040 "Const \<dots> $ 

  1041   Abs (\"x\", \<dots>,

  1042     Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 

  1043                 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}

  1044 

  1045   There are a number of handy functions that are frequently used for 

  1046   constructing terms. One is the function @{ML_ind  list_comb}, which takes a term

  1047   and a list of terms as arguments, and produces as output the term

  1048   list applied to the term. For example

  1049 

  1050 @{ML_response_fake [display,gray]

  1051 "let

  1052   val trm = @{term \"P::nat\"}

  1053   val args = [@{term \"True\"}, @{term \"False\"}]

  1054 in

  1055   list_comb (trm, args)

  1056 end"

  1057 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}

  1058 

  1059   Another handy function is @{ML_ind  lambda}, which abstracts a variable 

  1060   in a term. For example

  1061 

  1062   @{ML_response_fake [display,gray]

  1063 "let

  1064   val x_nat = @{term \"x::nat\"}

  1065   val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}

  1066 in

  1067   lambda x_nat trm

  1068 end"

  1069   "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}

  1070 

  1071   In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 

  1072   and an abstraction. It also records the type of the abstracted

  1073   variable and for printing purposes also its name.  Note that because of the

  1074   typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}

  1075   is of the same type as the abstracted variable. If it is of different type,

  1076   as in

  1077 

  1078   @{ML_response_fake [display,gray]

  1079 "let

  1080   val x_int = @{term \"x::int\"}

  1081   val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}

  1082 in

  1083   lambda x_int trm

  1084 end"

  1085   "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}

  1086 

  1087   then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 

  1088   This is a fundamental principle

  1089   of Church-style typing, where variables with the same name still differ, if they 

  1090   have different type.

  1091 

  1092   There is also the function @{ML_ind  subst_free} with which terms can be

  1093   replaced by other terms. For example below, we will replace in @{term

  1094   "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by

  1095   @{term y}, and @{term x} by @{term True}.

  1096 

  1097   @{ML_response_fake [display,gray]

  1098 "let

  1099   val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})

  1100   val sub2 = (@{term \"x::nat\"}, @{term \"True\"})

  1101   val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}

  1102 in

  1103   subst_free [sub1, sub2] trm

  1104 end"

  1105   "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}

  1106 

  1107   As can be seen, @{ML subst_free} does not take typability into account.

  1108   However it takes alpha-equivalence into account:

  1109 

  1110   @{ML_response_fake [display, gray]

  1111 "let

  1112   val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})

  1113   val trm = @{term \"(\<lambda>x::nat. x)\"}

  1114 in

  1115   subst_free [sub] trm

  1116 end"

  1117   "Free (\"x\", \"nat\")"}

  1118 

  1119   Similarly the function @{ML_ind  subst_bounds}, replaces lose bound 

  1120   variables with terms. To see how this function works, let us implement a

  1121   function that strips off the outermost quantifiers in a term.

  1122 *}

  1123 

  1124 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =

  1125          strip_alls t |>> cons (Free (n, T))

  1126   | strip_alls t = ([], t) *}

  1127 

  1128 text {*

  1129   The function returns a pair consisting of the stripped off variables and

  1130   the body of the universal quantifications. For example

  1131 

  1132   @{ML_response_fake [display, gray]

  1133   "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"

  1134 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],

  1135   Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}

  1136 

  1137   After calling @{ML strip_alls}, you obtain a term with lose bound variables. With

  1138   the function @{ML subst_bounds}, you can replace these lose @{ML_ind 

  1139   Bound}s with the stripped off variables.

  1140 

  1141   @{ML_response_fake [display, gray, linenos]

  1142   "let

  1143   val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}

  1144 in 

  1145   subst_bounds (rev vrs, trm) 

  1146   |> string_of_term @{context}

  1147   |> tracing

  1148 end"

  1149   "x = y"}

  1150 

  1151   Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls}

  1152   returned. The reason is that the head of the list the function @{ML subst_bounds}

  1153   takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}

  1154   and so on. 

  1155 

  1156   There are many convenient functions that construct specific HOL-terms. For

  1157   example @{ML_ind  mk_eq in HOLogic} constructs an equality out of two terms.

  1158   The types needed in this equality are calculated from the type of the

  1159   arguments. For example

  1160 

  1161 @{ML_response_fake [gray,display]

  1162 "let

  1163   val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})

  1164 in

  1165   string_of_term @{context} eq

  1166   |> tracing

  1167 end"

  1168   "True = False"}

  1169 *}

  1170 

  1171 text {*

  1172   \begin{readmore}

  1173   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file

  1174   "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual

  1175   constructions of terms and types easier.

  1176   \end{readmore}

  1177 

  1178   When constructing terms manually, there are a few subtle issues with

  1179   constants. They usually crop up when pattern matching terms or types, or

  1180   when constructing them. While it is perfectly ok to write the function

  1181   @{text is_true} as follows

  1182 *}

  1183 

  1184 ML{*fun is_true @{term True} = true

  1185   | is_true _ = false*}

  1186 

  1187 text {*

  1188   this does not work for picking out @{text "\<forall>"}-quantified terms. Because

  1189   the function 

  1190 *}

  1191 

  1192 ML{*fun is_all (@{term All} $ _) = true

  1193   | is_all _ = false*}

  1194 

  1195 text {* 

  1196   will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: 

  1197 

  1198   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}

  1199 

  1200   The problem is that the @{text "@term"}-antiquotation in the pattern 

  1201   fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 

  1202   an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 

  1203   for this function is

  1204 *}

  1205 

  1206 ML{*fun is_all (Const ("All", _) $ _) = true

  1207   | is_all _ = false*}

  1208 

  1209 text {* 

  1210   because now

  1211 

  1212 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}

  1213 

  1214   matches correctly (the first wildcard in the pattern matches any type and the

  1215   second any term).

  1216 

  1217   However there is still a problem: consider the similar function that

  1218   attempts to pick out @{text "Nil"}-terms:

  1219 *}

  1220 

  1221 ML{*fun is_nil (Const ("Nil", _)) = true

  1222   | is_nil _ = false *}

  1223 

  1224 text {* 

  1225   Unfortunately, also this function does \emph{not} work as expected, since

  1226 

  1227   @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}

  1228 

  1229   The problem is that on the ML-level the name of a constant is more

  1230   subtle than you might expect. The function @{ML is_all} worked correctly,

  1231   because @{term "All"} is such a fundamental constant, which can be referenced

  1232   by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at

  1233 

  1234   @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}

  1235 

  1236   the name of the constant @{text "Nil"} depends on the theory in which the

  1237   term constructor is defined (@{text "List"}) and also in which datatype

  1238   (@{text "list"}). Even worse, some constants have a name involving

  1239   type-classes. Consider for example the constants for @{term "zero"} and

  1240   \mbox{@{text "(op *)"}}:

  1241 

  1242   @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 

  1243  "(Const (\"HOL.zero_class.zero\", \<dots>), 

  1244  Const (\"HOL.times_class.times\", \<dots>))"}

  1245 

  1246   While you could use the complete name, for example 

  1247   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or

  1248   matching against @{text "Nil"}, this would make the code rather brittle. 

  1249   The reason is that the theory and the name of the datatype can easily change. 

  1250   To make the code more robust, it is better to use the antiquotation 

  1251   @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 

  1252   variable parts of the constant's name. Therefore a function for 

  1253   matching against constants that have a polymorphic type should 

  1254   be written as follows.

  1255 *}

  1256 

  1257 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true

  1258   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true

  1259   | is_nil_or_all _ = false *}

  1260 

  1261 text {*

  1262   The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.

  1263   For example

  1264 

  1265   @{ML_response [display,gray]

  1266   "@{type_name \"list\"}" "\"List.list\""}

  1267 

  1268   (FIXME: Explain the following better.)

  1269 

  1270   Occasionally you have to calculate what the ``base'' name of a given

  1271   constant is. For this you can use the function @{ML_ind  "Sign.extern_const"} or

  1272   @{ML_ind  Long_Name.base_name}. For example:

  1273 

  1274   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}

  1275 

  1276   The difference between both functions is that @{ML extern_const in Sign} returns

  1277   the smallest name that is still unique, whereas @{ML base_name in Long_Name} always

  1278   strips off all qualifiers.

  1279 

  1280   \begin{readmore}

  1281   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

  1282   functions about signatures in @{ML_file "Pure/sign.ML"}.

  1283   \end{readmore}

  1284 

  1285   Although types of terms can often be inferred, there are many

  1286   situations where you need to construct types manually, especially  

  1287   when defining constants. For example the function returning a function 

  1288   type is as follows:

  1289 

  1290 *} 

  1291 

  1292 ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}

  1293 

  1294 text {* This can be equally written with the combinator @{ML_ind  "-->"} as: *}

  1295 

  1296 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}

  1297 

  1298 text {*

  1299   If you want to construct a function type with more than one argument

  1300   type, then you can use @{ML_ind  "--->"}.

  1301 *}

  1302 

  1303 ML{*fun make_fun_types tys ty = tys ---> ty *}

  1304 

  1305 text {*

  1306   A handy function for manipulating terms is @{ML_ind  map_types}: it takes a 

  1307   function and applies it to every type in a term. You can, for example,

  1308   change every @{typ nat} in a term into an @{typ int} using the function:

  1309 *}

  1310 

  1311 ML{*fun nat_to_int ty =

  1312   (case ty of

  1313      @{typ nat} => @{typ int}

  1314    | Type (s, tys) => Type (s, map nat_to_int tys)

  1315    | _ => ty)*}

  1316 

  1317 text {*

  1318   Here is an example:

  1319 

  1320 @{ML_response_fake [display,gray] 

  1321 "map_types nat_to_int @{term \"a = (1::nat)\"}" 

  1322 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")

  1323            $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}

  1324 

  1325   If you want to obtain the list of free type-variables of a term, you

  1326   can use the function @{ML_ind  add_tfrees in Term} 

  1327   (similarly @{ML_ind  add_tvars in Term} for the schematic type-variables). 

  1328   One would expect that such functions

  1329   take a term as input and return a list of types. But their type is actually 

  1330 

  1331   @{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}

  1332 

  1333   that is they take, besides a term, also a list of type-variables as input. 

  1334   So in order to obtain the list of type-variables of a term you have to 

  1335   call them as follows

  1336 

  1337   @{ML_response [gray,display]

  1338   "Term.add_tfrees @{term \"(a, b)\"} []"

  1339   "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}

  1340 

  1341   The reason for this definition is that @{ML add_tfrees in Term} can

  1342   be easily folded over a list of terms. Similarly for all functions

  1343   named @{text "add_*"} in @{ML_file "Pure/term.ML"}.

  1344 

  1345   \begin{exercise}\label{fun:revsum}

  1346   Write a function @{text "rev_sum : term -> term"} that takes a

  1347   term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)

  1348   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume

  1349   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 

  1350   associates to the left. Try your function on some examples. 

  1351   \end{exercise}

  1352 

  1353   \begin{exercise}\label{fun:makesum}

  1354   Write a function which takes two terms representing natural numbers

  1355   in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the

  1356   number representing their sum.

  1357   \end{exercise}

  1358 

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

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

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

  1362   number n$>$0 and constructs terms of the form:

  1363   

  1364   \begin{center}

  1365   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

  1366   {\it rhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n.  P\,i}\\

  1367   {\it lhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i = P (i + 1 mod n)}

  1368                         $\longrightarrow$ {\it rhs n}\\

  1369   {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\

  1370   \end{tabular}

  1371   \end{center}

  1372 

  1373   For n=3 this function returns the term

  1374 

  1375   \begin{center}

  1376   \begin{tabular}{l}

  1377   (P 1 = P 2 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\

  1378   (P 2 = P 3 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\ 

  1379   (P 3 = P 1 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3

  1380   \end{tabular}

  1381   \end{center}

  1382 

  1383   Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}

  1384   for constructing the terms for the logical connectives. 

  1385   \end{exercise}

  1386 *}

  1387 

  1388 

  1389 section {* Type-Checking\label{sec:typechecking} *}

  1390 

  1391 text {* 

  1392   

  1393   You can freely construct and manipulate @{ML_type "term"}s and @{ML_type

  1394   typ}es, since they are just arbitrary unchecked trees. However, you

  1395   eventually want to see if a term is well-formed, or type-checks, relative to

  1396   a theory.  Type-checking is done via the function @{ML_ind  cterm_of}, which

  1397   converts a @{ML_type  term} into a @{ML_type  cterm}, a \emph{certified}

  1398   term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are

  1399   abstract objects that are guaranteed to be type-correct, and they can only

  1400   be constructed via ``official interfaces''.

  1401 

  1402 

  1403   Type-checking is always relative to a theory context. For now we use

  1404   the @{ML "@{theory}"} antiquotation to get hold of the current theory.

  1405   For example you can write:

  1406 

  1407   @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"}

  1408 

  1409   This can also be written with an antiquotation:

  1410 

  1411   @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}

  1412 

  1413   Attempting to obtain the certified term for

  1414 

  1415   @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}

  1416 

  1417   yields an error (since the term is not typable). A slightly more elaborate

  1418   example that type-checks is:

  1419 

  1420 @{ML_response_fake [display,gray] 

  1421 "let

  1422   val natT = @{typ \"nat\"}

  1423   val zero = @{term \"0::nat\"}

  1424 in

  1425   cterm_of @{theory} 

  1426       (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)

  1427 end" "0 + 0"}

  1428 

  1429   In Isabelle not just terms need to be certified, but also types. For example, 

  1430   you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 

  1431   the ML-level as follows:

  1432 

  1433   @{ML_response_fake [display,gray]

  1434   "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"

  1435   "nat \<Rightarrow> bool"}

  1436 

  1437   or with the antiquotation:

  1438 

  1439   @{ML_response_fake [display,gray]

  1440   "@{ctyp \"nat \<Rightarrow> bool\"}"

  1441   "nat \<Rightarrow> bool"}

  1442 

  1443   \begin{readmore}

  1444   For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 

  1445   the file @{ML_file "Pure/thm.ML"}.

  1446   \end{readmore}

  1447 

  1448   Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 

  1449   enough typing information (constants, free variables and abstractions all have typing 

  1450   information) so that it is always clear what the type of a term is. 

  1451   Given a well-typed term, the function @{ML_ind  type_of} returns the 

  1452   type of a term. Consider for example:

  1453 

  1454   @{ML_response [display,gray] 

  1455   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}

  1456 

  1457   To calculate the type, this function traverses the whole term and will

  1458   detect any typing inconsistency. For example changing the type of the variable 

  1459   @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 

  1460 

  1461   @{ML_response_fake [display,gray] 

  1462   "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 

  1463   "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}

  1464 

  1465   Since the complete traversal might sometimes be too costly and

  1466   not necessary, there is the function @{ML_ind  fastype_of}, which 

  1467   also returns the type of a term.

  1468 

  1469   @{ML_response [display,gray] 

  1470   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}

  1471 

  1472   However, efficiency is gained on the expense of skipping some tests. You 

  1473   can see this in the following example

  1474 

  1475    @{ML_response [display,gray] 

  1476   "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}

  1477 

  1478   where no error is detected.

  1479 

  1480   Sometimes it is a bit inconvenient to construct a term with 

  1481   complete typing annotations, especially in cases where the typing 

  1482   information is redundant. A short-cut is to use the ``place-holder'' 

  1483   type @{ML_ind  dummyT} and then let type-inference figure out the 

  1484   complete type. An example is as follows:

  1485 

  1486   @{ML_response_fake [display,gray] 

  1487 "let

  1488   val c = Const (@{const_name \"plus\"}, dummyT) 

  1489   val o = @{term \"1::nat\"} 

  1490   val v = Free (\"x\", dummyT)

  1491 in   

  1492   Syntax.check_term @{context} (c $ o $ v)

  1493 end"

  1494 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $

  1495   Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}

  1496 

  1497   Instead of giving explicitly the type for the constant @{text "plus"} and the free 

  1498   variable @{text "x"}, type-inference fills in the missing information.

  1499 

  1500   \begin{readmore}

  1501   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,

  1502   checking and pretty-printing of terms are defined. Functions related to

  1503   type-inference are implemented in @{ML_file "Pure/type.ML"} and 

  1504   @{ML_file "Pure/type_infer.ML"}. 

  1505   \end{readmore}

  1506 

  1507   (FIXME: say something about sorts)

  1508 

  1509   \begin{exercise}

  1510   Check that the function defined in Exercise~\ref{fun:revsum} returns a

  1511   result that type-checks. See what happens to the  solutions of this 

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

  1513   as input.

  1514   \end{exercise}

  1515 *}

  1516 

  1517 

  1518 section {* Theorems *}

  1519 

  1520 text {*

  1521   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 

  1522   that can only be built by going through interfaces. As a consequence, every proof 

  1523   in Isabelle is correct by construction. This follows the tradition of the LCF approach

  1524   \cite{GordonMilnerWadsworth79}.

  1525 

  1526 

  1527   To see theorems in ``action'', let us give a proof on the ML-level for the following 

  1528   statement:

  1529 *}

  1530 

  1531   lemma 

  1532    assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 

  1533    and     assm\<^isub>2: "P t"

  1534    shows "Q t" (*<*)oops(*>*) 

  1535 

  1536 text {*

  1537   The corresponding ML-code is as follows:

  1538 

  1539 @{ML_response_fake [display,gray]

  1540 "let

  1541   val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}

  1542   val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}

  1543 

  1544   val Pt_implies_Qt = 

  1545         assume assm1

  1546         |> forall_elim @{cterm \"t::nat\"};

  1547   

  1548   val Qt = implies_elim Pt_implies_Qt (assume assm2);

  1549 in

  1550   Qt 

  1551   |> implies_intr assm2

  1552   |> implies_intr assm1

  1553 end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}

  1554 

  1555   This code-snippet constructs the following proof:

  1556 

  1557   \[

  1558   \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}

  1559     {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}

  1560        {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}

  1561           {\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}

  1562                  {\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}

  1563                  &

  1564            \infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}

  1565           }

  1566        }

  1567     }

  1568   \]

  1569 

  1570   However, while we obtained a theorem as result, this theorem is not

  1571   yet stored in Isabelle's theorem database. So it cannot be referenced later

  1572   on. How to store theorems will be explained in Section~\ref{sec:storing}.

  1573 

  1574   \begin{readmore}

  1575   For the functions @{text "assume"}, @{text "forall_elim"} etc 

  1576   see \isccite{sec:thms}. The basic functions for theorems are defined in

  1577   @{ML_file "Pure/thm.ML"}. 

  1578   \end{readmore}

  1579 

  1580   (FIXME: handy functions working on theorems, like @{ML_ind  rulify in ObjectLogic} and so on) 

  1581 

  1582   (FIXME: how to add case-names to goal states - maybe in the 

  1583   next section)

  1584 

  1585   (FIXME: example for how to add theorem styles)

  1586 *}

  1587 

  1588 ML {*

  1589 fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) =

  1590       strip_assums_all ((a, T)::params, t)

  1591   | strip_assums_all (params, B) = (params, B)

  1592 

  1593 fun style_parm_premise i ctxt t =

  1594   let val prems = Logic.strip_imp_prems t in

  1595     if i <= length prems

  1596     then let val (params,t) = strip_assums_all([], nth prems (i - 1))

  1597          in subst_bounds(map Free params, t) end

  1598     else error ("Not enough premises for prem" ^ string_of_int i ^

  1599       " in propositon: " ^ string_of_term ctxt t)

  1600   end;

  1601 *}

  1602 

  1603 ML {*

  1604 strip_assums_all ([], @{term "\<And>x y. A x y"})

  1605 *}

  1606 

  1607 setup %gray {*

  1608   TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>

  1609   TermStyle.add_style "no_all_prem2" (style_parm_premise 2)

  1610 *}

  1611 

  1612 

  1613 section {* Setups (TBD) *}

  1614 

  1615 text {*

  1616   In the previous section we used \isacommand{setup} in order to make

  1617   a theorem attribute known to Isabelle. What happens behind the scenes

  1618   is that \isacommand{setup} expects a function of type 

  1619   @{ML_type "theory -> theory"}: the input theory is the current theory and the 

  1620   output the theory where the theory attribute has been stored.

  1621   

  1622   This is a fundamental principle in Isabelle. A similar situation occurs 

  1623   for example with declaring constants. The function that declares a 

  1624   constant on the ML-level is @{ML_ind  add_consts_i in Sign}. 

  1625   If you write\footnote{Recall that ML-code  needs to be 

  1626   enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 

  1627 *}  

  1628 

  1629 ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}

  1630 

  1631 text {*

  1632   for declaring the constant @{text "BAR"} with type @{typ nat} and 

  1633   run the code, then you indeed obtain a theory as result. But if you 

  1634   query the constant on the Isabelle level using the command \isacommand{term}

  1635 

  1636   \begin{isabelle}

  1637   \isacommand{term}~@{text [quotes] "BAR"}\\

  1638   @{text "> \"BAR\" :: \"'a\""}

  1639   \end{isabelle}

  1640 

  1641   you do not obtain a constant of type @{typ nat}, but a free variable (printed in 

  1642   blue) of polymorphic type. The problem is that the ML-expression above did 

  1643   not register the declaration with the current theory. This is what the command

  1644   \isacommand{setup} is for. The constant is properly declared with

  1645 *}

  1646 

  1647 setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}

  1648 

  1649 text {* 

  1650   Now 

  1651   

  1652   \begin{isabelle}

  1653   \isacommand{term}~@{text [quotes] "BAR"}\\

  1654   @{text "> \"BAR\" :: \"nat\""}

  1655   \end{isabelle}

  1656 

  1657   returns a (black) constant with the type @{typ nat}.

  1658 

  1659   A similar command is \isacommand{local\_setup}, which expects a function

  1660   of type @{ML_type "local_theory -> local_theory"}. Later on we will also

  1661   use the commands \isacommand{method\_setup} for installing methods in the

  1662   current theory and \isacommand{simproc\_setup} for adding new simprocs to

  1663   the current simpset.

  1664 *}

  1665 

  1666 section {* Theorem Attributes\label{sec:attributes} *}

  1667 

  1668 text {*

  1669   Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text

  1670   "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags

  1671   annotated to theorems, but functions that do further processing once a

  1672   theorem is proved. In particular, it is not possible to find out

  1673   what are all theorems that have a given attribute in common, unless of course

  1674   the function behind the attribute stores the theorems in a retrievable 

  1675   data structure. 

  1676 

  1677   If you want to print out all currently known attributes a theorem can have, 

  1678   you can use the Isabelle command

  1679 

  1680   \begin{isabelle}

  1681   \isacommand{print\_attributes}\\

  1682   @{text "> COMP:  direct composition with rules (no lifting)"}\\

  1683   @{text "> HOL.dest:  declaration of Classical destruction rule"}\\

  1684   @{text "> HOL.elim:  declaration of Classical elimination rule"}\\

  1685   @{text "> \<dots>"}

  1686   \end{isabelle}

  1687   

  1688   The theorem attributes fall roughly into two categories: the first category manipulates

  1689   the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second

  1690   stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds

  1691   the theorem to the current simpset).

  1692 

  1693   To explain how to write your own attribute, let us start with an extremely simple 

  1694   version of the attribute @{text "[symmetric]"}. The purpose of this attribute is

  1695   to produce the ``symmetric'' version of an equation. The main function behind 

  1696   this attribute is

  1697 *}

  1698 

  1699 ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}

  1700 

  1701 text {* 

  1702   where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 

  1703   context (which we ignore in the code above) and a theorem (@{text thm}), and 

  1704   returns another theorem (namely @{text thm} resolved with the theorem 

  1705   @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind "RS"} 

  1706   is explained in Section~\ref{sec:simpletacs}). The function 

  1707   @{ML rule_attribute in Thm} then returns  an attribute.

  1708 

  1709   Before we can use the attribute, we need to set it up. This can be done

  1710   using the Isabelle command \isacommand{attribute\_setup} as follows:

  1711 *}

  1712 

  1713 attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *} 

  1714   "applying the sym rule"

  1715 

  1716 text {*

  1717   Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser

  1718   for the theorem attribute. Since the attribute does not expect any further 

  1719   arguments (unlike @{text "[THEN \<dots>]"}, for example), we use the parser @{ML

  1720   Scan.succeed}. Later on we will also consider attributes taking further

  1721   arguments. An example for the attribute @{text "[my_sym]"} is the proof

  1722 *} 

  1723 

  1724 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp

  1725 

  1726 text {*

  1727   which stores the theorem @{thm test} under the name @{thm [source] test}. You

  1728   can see this, if you query the lemma: 

  1729 

  1730   \begin{isabelle}

  1731   \isacommand{thm}~@{text "test"}\\

  1732   @{text "> "}~@{thm test}

  1733   \end{isabelle}

  1734 

  1735   We can also use the attribute when referring to this theorem:

  1736 

  1737   \begin{isabelle}

  1738   \isacommand{thm}~@{text "test[my_sym]"}\\

  1739   @{text "> "}~@{thm test[my_sym]}

  1740   \end{isabelle}

  1741 

  1742   An alternative for setting up an attribute is the function @{ML_ind  setup in Attrib}.

  1743   So instead of using \isacommand{attribute\_setup}, you can also set up the

  1744   attribute as follows:

  1745 *}

  1746 

  1747 ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)

  1748   "applying the sym rule" *}

  1749 

  1750 text {*

  1751   This gives a function from @{ML_type "Context.theory -> Context.theory"}, which

  1752   can be used for example with \isacommand{setup}.

  1753 

  1754   As an example of a slightly more complicated theorem attribute, we implement 

  1755   our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems

  1756   as argument and resolve the proved theorem with this list (one theorem 

  1757   after another). The code for this attribute is

  1758 *}

  1759 

  1760 ML{*fun MY_THEN thms = 

  1761   Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}

  1762 

  1763 text {* 

  1764   where @{ML swap} swaps the components of a pair. The setup of this theorem

  1765   attribute uses the parser @{ML thms in Attrib}, which parses a list of

  1766   theorems. 

  1767 *}

  1768 

  1769 attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} 

  1770   "resolving the list of theorems with the proved theorem"

  1771 

  1772 text {* 

  1773   You can, for example, use this theorem attribute to turn an equation into a 

  1774   meta-equation:

  1775 

  1776   \begin{isabelle}

  1777   \isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\

  1778   @{text "> "}~@{thm test[MY_THEN eq_reflection]}

  1779   \end{isabelle}

  1780 

  1781   If you need the symmetric version as a meta-equation, you can write

  1782 

  1783   \begin{isabelle}

  1784   \isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\

  1785   @{text "> "}~@{thm test[MY_THEN sym eq_reflection]}

  1786   \end{isabelle}

  1787 

  1788   It is also possible to combine different theorem attributes, as in:

  1789   

  1790   \begin{isabelle}

  1791   \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\

  1792   @{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}

  1793   \end{isabelle}

  1794   

  1795   However, here also a weakness of the concept

  1796   of theorem attributes shows through: since theorem attributes can be

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

  1798 

  1799   \begin{isabelle}

  1800   \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\

  1801   @{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}

  1802   \end{isabelle}

  1803 

  1804   you get an exception indicating that the theorem @{thm [source] sym}

  1805   does not resolve with meta-equations. 

  1806 

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

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

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

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

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

  1812   of theorems.

  1813 *}

  1814 

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

  1816 

  1817 text {* 

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

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

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

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

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

  1823   data properly without using references.

  1824  

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

  1826   For this we use the two functions:

  1827 *}

  1828 

  1829 ML{*fun my_thm_add thm ctxt =

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

  1831 

  1832 fun my_thm_del thm ctxt =

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

  1834 

  1835 text {*

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

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

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

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

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

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

  1842   their proved propositions modulo alpha-equivalence).

  1843 

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

  1845   attributes with the code

  1846 *}

  1847 

  1848 ML{*val my_add = Thm.declaration_attribute my_thm_add

  1849 val my_del = Thm.declaration_attribute my_thm_del *}

  1850 

  1851 text {* 

  1852   and set up the attributes as follows

  1853 *}

  1854 

  1855 attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} 

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

  1857 

  1858 text {*

  1859   The parser @{ML_ind  add_del in Attrib} is a predefined parser for 

  1860   adding and deleting lemmas. Now if you prove the next lemma 

  1861   and attach to it the attribute @{text "[my_thms]"}

  1862 *}

  1863 

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

  1865 

  1866 text {*

  1867   then you can see it is added to the initially empty list.

  1868 

  1869   @{ML_response_fake [display,gray]

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

  1871 

  1872   You can also add theorems using the command \isacommand{declare}.

  1873 *}

  1874 

  1875 declare test[my_thms] trueI_2[my_thms add] 

  1876 

  1877 text {*

  1878   With this attribute, the @{text "add"} operation is the default and does 

  1879   not need to be explicitly given. These three declarations will cause the 

  1880   theorem list to be updated as:

  1881 

  1882   @{ML_response_fake [display,gray]

  1883   "!my_thms"

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

  1885 

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

  1887   function @{ML_ind  add_thm in Thm} tests for duplicates, before extending

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

  1889 *}

  1890 

  1891 declare test[my_thms del]

  1892 

  1893 text {* After this, the theorem list is again: 

  1894 

  1895   @{ML_response_fake [display,gray]

  1896   "!my_thms"

  1897   "[\"True\"]"}

  1898 

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

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

  1901   the arguments accordingly. 

  1902 

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

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

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

  1906   @{text GenericDataFun}:

  1907 *}

  1908 

  1909 ML{*structure MyThmsData = GenericDataFun

  1910  (type T = thm list

  1911   val empty = []

  1912   val extend = I

  1913   fun merge _ = Thm.merge_thms) *}

  1914 

  1915 text {*

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

  1917   to where data slots are explained properly.}

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

  1919   @{ML my_thm_del} to:

  1920 *}

  1921 

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

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

  1924 

  1925 text {*

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

  1927   corresponding theorem attributes are

  1928 *}

  1929 

  1930 ML{*val my_add = Thm.declaration_attribute my_thm_add

  1931 val my_del = Thm.declaration_attribute my_thm_del *}

  1932 

  1933 text {*

  1934   and the setup is as follows

  1935 *}

  1936 

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

  1938   "properly maintaining a list of my_thms"

  1939 

  1940 text {*

  1941   Initially, the data slot is empty 

  1942 

  1943   @{ML_response_fake [display,gray]

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

  1945   "[]"}

  1946 

  1947   but if you prove

  1948 *}

  1949 

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

  1951 

  1952 text {*

  1953   then the lemma is recorded. 

  1954 

  1955   @{ML_response_fake [display,gray]

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

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

  1958 

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

  1960   is important to 

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

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

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