1 theory General

     2 imports Base FirstSteps

     3 begin

     4 

     5 chapter {* General Infrastructure *}

     6 

     7 section {* Terms and Types *}

     8 

     9 text {*

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

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

    12 

    13   @{ML_response [display,gray] 

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

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

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

    17 

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

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

    20 *}  

    21 

    22 ML_val %linenosgray{*datatype term =

    23   Const of string * typ 

    24 | Free of string * typ 

    25 | Var of indexname * typ 

    26 | Bound of int 

    27 | Abs of string * typ * term 

    28 | $ of term * term *}

    29 

    30 text {*

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

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

    33   for representing bound variables.  For

    34   example in

    35 

    36   @{ML_response_fake [display, gray]

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

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

    39 

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

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

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

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

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

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

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

    47   term-constructor @{ML $}.

    48 

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

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

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

    52   leading question mark). Consider the following two examples

    53   

    54   @{ML_response_fake [display, gray]

    55 "let

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

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

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

    59 in

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

    61   |> tracing

    62 end"

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

    64 

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

    66   mentioned earlier, you cannot construct schematic variables using the

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

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

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

    70   similar distinction between free and schematic variables holds for types

    71   (see below).

    72 

    73   \begin{readmore}

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

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

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

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

    78   \end{readmore}

    79   

    80   Constructing terms via antiquotations has the advantage that only typable

    81   terms can be constructed. For example

    82 

    83   @{ML_response_fake_both [display,gray]

    84   "@{term \"x x\"}"

    85   "Type unification failed: Occurs check!"}

    86 

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

    88 

    89   @{ML_response_fake [display,gray] 

    90 "let

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

    92 in 

    93   tracing (string_of_term @{context} omega)

    94 end"

    95   "x x"}

    96 

    97   with the raw ML-constructors.

    98   

    99   Sometimes the internal representation of terms can be surprisingly different

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

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

   102 

   103   \begin{exercise}

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

   105   find out why they are represented like this:

   106 

   107   \begin{itemize}

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

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

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

   111   \end{itemize}

   112 

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

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

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

   116   value:

   117 

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

   119   \end{exercise}

   120 

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

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

   123   Consider for example the pairs

   124 

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

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

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

   128  

   129   where a coercion is inserted in the second component and 

   130 

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

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

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

   134 

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

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

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

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

   139 

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

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

   142 

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

   144 

   145   The corresponding datatype is

   146 *}

   147   

   148 ML_val{*datatype typ =

   149   Type  of string * typ list 

   150 | TFree of string * sort 

   151 | TVar  of indexname * sort *}

   152 

   153 text {*

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

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

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

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

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

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

   160   Here is a contrived example:

   161 

   162   @{ML_response [display, gray]

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

   164   "true"}

   165 

   166   \begin{readmore}

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

   168   definition and many useful operations are implemented 

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

   170   \end{readmore}

   171 *}

   172 

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

   174 

   175 text {*

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

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

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

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

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

   181 

   182 *}

   183 

   184 ML{*fun make_imp P Q =

   185 let

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

   187 in 

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

   189 end *}

   190 

   191 text {*

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

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

   194   the following does \emph{not} work.

   195 *}

   196 

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

   198 

   199 text {*

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

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

   202   the given arguments

   203 

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

   205 "Const \<dots> $ 

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

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

   208 

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

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

   211 

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

   213 "Const \<dots> $ 

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

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

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

   217 

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

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

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

   221   list applied to the term. For example

   222 

   223 @{ML_response_fake [display,gray]

   224 "let

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

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

   227 in

   228   list_comb (trm, args)

   229 end"

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

   231 

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

   233   in a term. For example

   234 

   235   @{ML_response_fake [display,gray]

   236 "let

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

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

   239 in

   240   lambda x_nat trm

   241 end"

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

   243 

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

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

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

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

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

   249   as in

   250 

   251   @{ML_response_fake [display,gray]

   252 "let

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

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

   255 in

   256   lambda x_int trm

   257 end"

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

   259 

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

   261   This is a fundamental principle

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

   263   have different type.

   264 

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

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

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

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

   269 

   270   @{ML_response_fake [display,gray]

   271 "let

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

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

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

   275 in

   276   subst_free [sub1, sub2] trm

   277 end"

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

   279 

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

   281   However it takes alpha-equivalence into account:

   282 

   283   @{ML_response_fake [display, gray]

   284 "let

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

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

   287 in

   288   subst_free [sub] trm

   289 end"

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

   291 

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

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

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

   295 *}

   296 

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

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

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

   300 

   301 text {*

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

   303   the body of the universal quantifications. For example

   304 

   305   @{ML_response_fake [display, gray]

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

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

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

   309 

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

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

   312   Bound}s with the stripped off variables.

   313 

   314   @{ML_response_fake [display, gray, linenos]

   315   "let

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

   317 in 

   318   subst_bounds (rev vrs, trm) 

   319   |> string_of_term @{context}

   320   |> tracing

   321 end"

   322   "x = y"}

   323 

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

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

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

   327   and so on. 

   328 

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

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

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

   332   arguments. For example

   333 

   334 @{ML_response_fake [gray,display]

   335 "let

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

   337 in

   338   string_of_term @{context} eq

   339   |> tracing

   340 end"

   341   "True = False"}

   342 *}

   343 

   344 text {*

   345   \begin{readmore}

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

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

   348   constructions of terms and types easier.

   349   \end{readmore}

   350 

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

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

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

   354   @{text is_true} as follows

   355 *}

   356 

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

   358   | is_true _ = false*}

   359 

   360 text {*

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

   362   the function 

   363 *}

   364 

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

   366   | is_all _ = false*}

   367 

   368 text {* 

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

   370 

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

   372 

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

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

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

   376   for this function is

   377 *}

   378 

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

   380   | is_all _ = false*}

   381 

   382 text {* 

   383   because now

   384 

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

   386 

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

   388   second any term).

   389 

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

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

   392 *}

   393 

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

   395   | is_nil _ = false *}

   396 

   397 text {* 

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

   399 

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

   401 

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

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

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

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

   406 

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

   408 

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

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

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

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

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

   414 

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

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

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

   418 

   419   While you could use the complete name, for example 

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

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

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

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

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

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

   426   matching against constants that have a polymorphic type should 

   427   be written as follows.

   428 *}

   429 

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

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

   432   | is_nil_or_all _ = false *}

   433 

   434 text {*

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

   436   For example

   437 

   438   @{ML_response [display,gray]

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

   440 

   441   (FIXME: Explain the following better.)

   442 

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

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

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

   446 

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

   448 

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

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

   451   strips off all qualifiers.

   452 

   453   \begin{readmore}

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

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

   456   \end{readmore}

   457 

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

   459   situations where you need to construct types manually, especially  

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

   461   type is as follows:

   462 

   463 *} 

   464 

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

   466 

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

   468 

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

   470 

   471 text {*

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

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

   474 *}

   475 

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

   477 

   478 text {*

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

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

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

   482 *}

   483 

   484 ML{*fun nat_to_int ty =

   485   (case ty of

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

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

   488    | _ => ty)*}

   489 

   490 text {*

   491   Here is an example:

   492 

   493 @{ML_response_fake [display,gray] 

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

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

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

   497 

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

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

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

   501   One would expect that such functions

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

   503 

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

   505 

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

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

   508   call them as follows

   509 

   510   @{ML_response [gray,display]

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

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

   513 

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

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

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

   517 

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

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

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

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

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

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

   524   \end{exercise}

   525 

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

   527   Write a function which takes two terms representing natural numbers

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

   529   number representing their sum.

   530   \end{exercise}

   531 

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

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

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

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

   536   

   537   \begin{center}

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

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

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

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

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

   543   \end{tabular}

   544   \end{center}

   545 

   546   For n=3 this function returns the term

   547 

   548   \begin{center}

   549   \begin{tabular}{l}

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

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

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

   553   \end{tabular}

   554   \end{center}

   555 

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

   557   for constructing the terms for the logical connectives. 

   558   \end{exercise}

   559 *}

   560 

   561 

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

   563 

   564 text {* 

   565   

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

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

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

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

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

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

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

   573   be constructed via ``official interfaces''.

   574 

   575 

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

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

   578   For example you can write:

   579 

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

   581 

   582   This can also be written with an antiquotation:

   583 

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

   585 

   586   Attempting to obtain the certified term for

   587 

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

   589 

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

   591   example that type-checks is:

   592 

   593 @{ML_response_fake [display,gray] 

   594 "let

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

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

   597 in

   598   cterm_of @{theory} 

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

   600 end" "0 + 0"}

   601 

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

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

   604   the ML-level as follows:

   605 

   606   @{ML_response_fake [display,gray]

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

   608   "nat \<Rightarrow> bool"}

   609 

   610   or with the antiquotation:

   611 

   612   @{ML_response_fake [display,gray]

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

   614   "nat \<Rightarrow> bool"}

   615 

   616   \begin{readmore}

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

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

   619   \end{readmore}

   620 

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

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

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

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

   625   type of a term. Consider for example:

   626 

   627   @{ML_response [display,gray] 

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

   629 

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

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

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

   633 

   634   @{ML_response_fake [display,gray] 

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

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

   637 

   638   Since the complete traversal might sometimes be too costly and

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

   640   also returns the type of a term.

   641 

   642   @{ML_response [display,gray] 

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

   644 

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

   646   can see this in the following example

   647 

   648    @{ML_response [display,gray] 

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

   650 

   651   where no error is detected.

   652 

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

   654   complete typing annotations, especially in cases where the typing 

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

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

   657   complete type. An example is as follows:

   658 

   659   @{ML_response_fake [display,gray] 

   660 "let

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

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

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

   664 in   

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

   666 end"

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

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

   669 

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

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

   672 

   673   \begin{readmore}

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

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

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

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

   678   \end{readmore}

   679 

   680   (FIXME: say something about sorts)

   681 

   682   \begin{exercise}

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

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

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

   686   as input.

   687   \end{exercise}

   688 *}

   689 

   690 

   691 section {* Theorems *}

   692 

   693 text {*

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

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

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

   697   \cite{GordonMilnerWadsworth79}.

   698 

   699 

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

   701   statement:

   702 *}

   703 

   704   lemma 

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

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

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

   708 

   709 text {*

   710   The corresponding ML-code is as follows:

   711 

   712 @{ML_response_fake [display,gray]

   713 "let

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

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

   716 

   717   val Pt_implies_Qt = 

   718         assume assm1

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

   720   

   721   val Qt = implies_elim Pt_implies_Qt (assume assm2);

   722 in

   723   Qt 

   724   |> implies_intr assm2

   725   |> implies_intr assm1

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

   727 

   728   This code-snippet constructs the following proof:

   729 

   730   \[

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

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

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

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

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

   736                  &

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

   738           }

   739        }

   740     }

   741   \]

   742 

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

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

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

   746 

   747   \begin{readmore}

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

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

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

   751   \end{readmore}

   752 

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

   754 

   755   (FIXME: @{ML_ind prove in Goal})

   756 

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

   758   next section)

   759 

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

   761 *}

   762 

   763 ML {*

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

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

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

   767 

   768 fun style_parm_premise i ctxt t =

   769   let val prems = Logic.strip_imp_prems t in

   770     if i <= length prems

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

   772          in subst_bounds(map Free params, t) end

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

   774       " in propositon: " ^ string_of_term ctxt t)

   775   end;

   776 *}

   777 

   778 ML {*

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

   780 *}

   781 

   782 setup %gray {*

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

   784   TermStyle.add_style "no_all_prem2" (style_parm_premise 2)

   785 *}

   786 

   787 lemma 

   788   shows "A \<Longrightarrow> B"

   789   and   "C \<Longrightarrow> D"

   790 oops

   791 

   792 

   793 section {* Setups (TBD) *}

   794 

   795 text {*

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

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

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

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

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

   801   

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

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

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

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

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

   807 *}  

   808 

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

   810 

   811 text {*

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

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

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

   815 

   816   \begin{isabelle}

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

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

   819   \end{isabelle}

   820 

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

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

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

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

   825 *}

   826 

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

   828 

   829 text {* 

   830   Now 

   831   

   832   \begin{isabelle}

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

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

   835   \end{isabelle}

   836 

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

   838 

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

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

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

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

   843   the current simpset.

   844 *}

   845 

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

   847 

   848 text {*

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

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

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

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

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

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

   855   data structure. 

   856 

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

   858   you can use the Isabelle command

   859 

   860   \begin{isabelle}

   861   \isacommand{print\_attributes}\\

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

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

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

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

   866   \end{isabelle}

   867   

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

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

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

   871   the theorem to the current simpset).

   872 

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

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

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

   876   this attribute is

   877 *}

   878 

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

   880 

   881 text {* 

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

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

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

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

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

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

   888 

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

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

   891 *}

   892 

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

   894   "applying the sym rule"

   895 

   896 text {*

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

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

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

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

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

   902 *} 

   903 

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

   905 

   906 text {*

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

   908   can see this, if you query the lemma: 

   909 

   910   \begin{isabelle}

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

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

   913   \end{isabelle}

   914 

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

   916 

   917   \begin{isabelle}

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

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

   920   \end{isabelle}

   921 

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

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

   924   attribute as follows:

   925 *}

   926 

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

   928   "applying the sym rule" *}

   929 

   930 text {*

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

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

   933 

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

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

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

   937   after another). The code for this attribute is

   938 *}

   939 

   940 ML{*fun MY_THEN thms = 

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

   942 

   943 text {* 

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

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

   946   theorems. 

   947 *}

   948 

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

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

   951 

   952 text {* 

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

   954   meta-equation:

   955 

   956   \begin{isabelle}

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

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

   959   \end{isabelle}

   960 

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

   962 

   963   \begin{isabelle}

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

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

   966   \end{isabelle}

   967 

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

   969   

   970   \begin{isabelle}

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

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

   973   \end{isabelle}

   974   

   975   However, here also a weakness of the concept

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

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

   978 

   979   \begin{isabelle}

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

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

   982   \end{isabelle}

   983 

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

   985   does not resolve with meta-equations. 

   986 

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

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

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

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

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

   992   of theorems.

   993 *}

   994 

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

   996 

   997 text {* 

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

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

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

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

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

  1003   data properly without using references.

  1004  

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

  1006   For this we use the two functions:

  1007 *}

  1008 

  1009 ML{*fun my_thm_add thm ctxt =

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

  1011 

  1012 fun my_thm_del thm ctxt =

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

  1014 

  1015 text {*

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

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

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

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

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

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

  1022   their proved propositions modulo alpha-equivalence).

  1023 

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

  1025   attributes with the code

  1026 *}

  1027 

  1028 ML{*val my_add = Thm.declaration_attribute my_thm_add

  1029 val my_del = Thm.declaration_attribute my_thm_del *}

  1030 

  1031 text {* 

  1032   and set up the attributes as follows

  1033 *}

  1034 

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

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

  1037 

  1038 text {*

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

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

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

  1042 *}

  1043 

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

  1045 

  1046 text {*

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

  1048 

  1049   @{ML_response_fake [display,gray]

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

  1051 

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

  1053 *}

  1054 

  1055 declare test[my_thms] trueI_2[my_thms add] 

  1056 

  1057 text {*

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

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

  1060   theorem list to be updated as:

  1061 

  1062   @{ML_response_fake [display,gray]

  1063   "!my_thms"

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

  1065 

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

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

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

  1069 *}

  1070 

  1071 declare test[my_thms del]

  1072 

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

  1074 

  1075   @{ML_response_fake [display,gray]

  1076   "!my_thms"

  1077   "[\"True\"]"}

  1078 

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

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

  1081   the arguments accordingly. 

  1082 

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

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

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

  1086   @{text GenericDataFun}:

  1087 *}

  1088 

  1089 ML{*structure MyThmsData = GenericDataFun

  1090  (type T = thm list

  1091   val empty = []

  1092   val extend = I

  1093   fun merge _ = Thm.merge_thms) *}

  1094 

  1095 text {*

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

  1097   to where data slots are explained properly.}

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

  1099   @{ML my_thm_del} to:

  1100 *}

  1101 

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

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

  1104 

  1105 text {*

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

  1107   corresponding theorem attributes are

  1108 *}

  1109 

  1110 ML{*val my_add = Thm.declaration_attribute my_thm_add

  1111 val my_del = Thm.declaration_attribute my_thm_del *}

  1112 

  1113 text {*

  1114   and the setup is as follows

  1115 *}

  1116 

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

  1118   "properly maintaining a list of my_thms"

  1119 

  1120 text {*

  1121   Initially, the data slot is empty 

  1122 

  1123   @{ML_response_fake [display,gray]

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

  1125   "[]"}

  1126 

  1127   but if you prove

  1128 *}

  1129 

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

  1131 

  1132 text {*

  1133   then the lemma is recorded. 

  1134 

  1135   @{ML_response_fake [display,gray]