1 theory FirstSteps

     2 imports Base

     3 begin

     4 

     5 chapter {* First Steps *}

     6 

     7 text {*

     8 

     9   Isabelle programming is done in ML.  Just like lemmas and proofs, ML-code

    10   in Isabelle is part of a theory. If you want to follow the code given in

    11   this chapter, we assume you are working inside the theory starting with

    12 

    13   \begin{center}

    14   \begin{tabular}{@ {}l}

    15   \isacommand{theory} FirstSteps\\

    16   \isacommand{imports} Main\\

    17   \isacommand{begin}\\

    18   \ldots

    19   \end{tabular}

    20   \end{center}

    21 

    22   We also generally assume you are working with HOL. The given examples might

    23   need to be adapted slightly if you work in a different logic.

    24 *}

    25 

    26 section {* Including ML-Code *}

    27 

    28 

    29 

    30 text {*

    31   The easiest and quickest way to include code in a theory is

    32   by using the \isacommand{ML}-command. For example:

    33 

    34 \begin{isabelle}

    35 \begin{graybox}

    36 \isacommand{ML}~@{text "\<verbopen>"}\isanewline

    37 \hspace{5mm}@{ML "3 + 4"}\isanewline

    38 @{text "\<verbclose>"}\isanewline

    39 @{text "> 7"}\smallskip

    40 \end{graybox}

    41 \end{isabelle}

    42 

    43   Like normal Isabelle proof scripts, \isacommand{ML}-commands can be

    44   evaluated by using the advance and undo buttons of your Isabelle

    45   environment. The code inside the \isacommand{ML}-command can also contain

    46   value and function bindings, and even those can be undone when the proof

    47   script is retracted. As mentioned in the Introduction, we will drop the

    48   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we

    49   show code. The lines prefixed with @{text [quotes] ">"} are not part of the

    50   code, rather they indicate what the response is when the code is evaluated.

    51 

    52   Once a portion of code is relatively stable, you usually want to export it

    53   to a separate ML-file. Such files can then be included in a theory by using

    54   the \isacommand{uses}-command in the header of the theory, like:

    55 

    56   \begin{center}

    57   \begin{tabular}{@ {}l}

    58   \isacommand{theory} FirstSteps\\

    59   \isacommand{imports} Main\\

    60   \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\

    61   \isacommand{begin}\\

    62   \ldots

    63   \end{tabular}

    64   \end{center}

    65   

    66 *}

    67 

    68 section {* Debugging and Printing\label{sec:printing} *}

    69 

    70 text {*

    71 

    72   During development you might find it necessary to inspect some data

    73   in your code. This can be done in a ``quick-and-dirty'' fashion using 

    74   the function @{ML "warning"}. For example 

    75 

    76   @{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}

    77 

    78   will print out @{text [quotes] "any string"} inside the response buffer

    79   of Isabelle.  This function expects a string as argument. If you develop under PolyML,

    80   then there is a convenient, though again ``quick-and-dirty'', method for

    81   converting values into strings, namely the function @{ML makestring}:

    82 

    83   @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} 

    84 

    85   However @{ML makestring} only works if the type of what is converted is monomorphic 

    86   and not a function.

    87 

    88   The function @{ML "warning"} should only be used for testing purposes, because any

    89   output this function generates will be overwritten as soon as an error is

    90   raised. For printing anything more serious and elaborate, the

    91   function @{ML tracing} is more appropriate. This function writes all output into

    92   a separate tracing buffer. For example:

    93 

    94   @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}

    95 

    96   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 

    97   printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive 

    98   amounts of trace output. This redirection can be achieved with the code:

    99 *}

   100 

   101 ML{*val strip_specials =

   102 let

   103   fun strip ("\^A" :: _ :: cs) = strip cs

   104     | strip (c :: cs) = c :: strip cs

   105     | strip [] = [];

   106 in implode o strip o explode end;

   107 

   108 fun redirect_tracing stream =

   109  Output.tracing_fn := (fn s =>

   110     (TextIO.output (stream, (strip_specials s));

   111      TextIO.output (stream, "\n");

   112      TextIO.flushOut stream)) *}

   113 

   114 text {*

   115   Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 

   116   will cause that all tracing information is printed into the file @{text "foo.bar"}.

   117 

   118   You can print out error messages with the function @{ML error}; for example:

   119 

   120 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 

   121 "Exception- ERROR \"foo\" raised

   122 At command \"ML\"."}

   123 

   124   Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} 

   125   or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, 

   126   but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform 

   127   a term into a string is to use the function @{ML Syntax.string_of_term}.

   128 

   129   @{ML_response_fake [display,gray]

   130   "Syntax.string_of_term @{context} @{term \"1::nat\"}"

   131   "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}

   132 

   133   This produces a string with some additional information encoded in it. The string

   134   can be properly printed by using the function @{ML warning}.

   135 

   136   @{ML_response_fake [display,gray]

   137   "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"

   138   "\"1\""}

   139 

   140   A @{ML_type cterm} can be transformed into a string by the following function.

   141 *}

   142 

   143 ML{*fun str_of_cterm ctxt t =  

   144    Syntax.string_of_term ctxt (term_of t)*}

   145 

   146 text {*

   147   In this example the function @{ML term_of} extracts the @{ML_type term} from

   148   a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be

   149   printed, you can use the function @{ML commas} to separate them.

   150 *} 

   151 

   152 ML{*fun str_of_cterms ctxt ts =  

   153    commas (map (str_of_cterm ctxt) ts)*}

   154 

   155 text {*

   156   The easiest way to get the string of a theorem is to transform it

   157   into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems

   158   also include schematic variables, such as @{text "?P"}, @{text "?Q"}

   159   and so on. In order to improve the readability of theorems we convert

   160   these schematic variables into free variables using the 

   161   function @{ML Variable.import_thms}.

   162 *}

   163 

   164 ML{*fun no_vars ctxt thm =

   165 let 

   166   val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt

   167 in

   168   thm'

   169 end

   170 

   171 fun str_of_thm ctxt thm =

   172   str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}

   173 

   174 text {* 

   175   Again the function @{ML commas} helps with printing more than one theorem. 

   176 *}

   177 

   178 ML{*fun str_of_thms ctxt thms =  

   179   commas (map (str_of_thm ctxt) thms)*}

   180 

   181 text {*

   182 (FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug})

   183 *}

   184 

   185 section {* Combinators\label{sec:combinators} *}

   186 

   187 text {*

   188   For beginners perhaps the most puzzling parts in the existing code of Isabelle are

   189   the combinators. At first they seem to greatly obstruct the

   190   comprehension of the code, but after getting familiar with them, they

   191   actually ease the understanding and also the programming.

   192 

   193   The simplest combinator is @{ML I}, which is just the identity function defined as

   194 *}

   195 

   196 ML{*fun I x = x*}

   197 

   198 text {* Another simple combinator is @{ML K}, defined as *}

   199 

   200 ML{*fun K x = fn _ => x*}

   201 

   202 text {*

   203   @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this 

   204   function ignores its argument. As a result, @{ML K} defines a constant function 

   205   always returning @{text x}.

   206 

   207   The next combinator is reverse application, @{ML "|>"}, defined as: 

   208 *}

   209 

   210 ML{*fun x |> f = f x*}

   211 

   212 text {* While just syntactic sugar for the usual function application,

   213   the purpose of this combinator is to implement functions in a  

   214   ``waterfall fashion''. Consider for example the function *}

   215 

   216 ML %linenosgray{*fun inc_by_five x =

   217   x |> (fn x => x + 1)

   218     |> (fn x => (x, x))

   219     |> fst

   220     |> (fn x => x + 4)*}

   221 

   222 text {*

   223   which increments its argument @{text x} by 5. It does this by first incrementing 

   224   the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 

   225   the first component of the pair (Line 4) and finally incrementing the first 

   226   component by 4 (Line 5). This kind of cascading manipulations of values is quite

   227   common when dealing with theories (for example by adding a definition, followed by

   228   lemmas and so on). The reverse application allows you to read what happens in 

   229   a top-down manner. This kind of coding should also be familiar, 

   230   if you have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using 

   231   the reverse application is much clearer than writing

   232 *}

   233 

   234 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}

   235 

   236 text {* or *}

   237 

   238 ML{*fun inc_by_five x = 

   239        ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}

   240 

   241 text {* and typographically more economical than *}

   242 

   243 ML{*fun inc_by_five x =

   244    let val y1 = x + 1

   245        val y2 = (y1, y1)

   246        val y3 = fst y2

   247        val y4 = y3 + 4

   248    in y4 end*}

   249 

   250 text {* 

   251   Another reason why the let-bindings in the code above are better to be

   252   avoided: it is more than easy to get the intermediate values wrong, not to 

   253   mention the nightmares the maintenance of this code causes!

   254 

   255   In the context of Isabelle, a ``real world'' example for a function written in 

   256   the waterfall fashion might be the following code:

   257 *}

   258 

   259 ML %linenosgray{*fun apply_fresh_args pred ctxt =

   260   pred |> fastype_of

   261        |> binder_types 

   262        |> map (pair "z")

   263        |> Variable.variant_frees ctxt [pred]

   264        |> map Free  

   265        |> (curry list_comb) pred *}

   266 

   267 text {*

   268   This code extracts the argument types of a given

   269   predicate and then generates for each argument type a distinct variable; finally it

   270   applies the generated variables to the predicate. For example

   271 

   272   @{ML_response_fake [display,gray]

   273 "apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context} 

   274  |> Syntax.string_of_term @{context}

   275  |> warning"

   276   "P z za zb"}

   277 

   278   You can read off this behaviour from how @{ML apply_fresh_args} is

   279   coded: in Line 2, the function @{ML fastype_of} calculates the type of the

   280   predicate; @{ML binder_types} in the next line produces the list of argument

   281   types (in the case above the list @{text "[nat, int, unit]"}); Line 4 

   282   pairs up each type with the string  @{text "z"}; the

   283   function @{ML variant_frees in Variable} generates for each @{text "z"} a

   284   unique name avoiding the given @{text pred}; the list of name-type pairs is turned

   285   into a list of variable terms in Line 6, which in the last line is applied

   286   by the function @{ML list_comb} to the predicate. We have to use the

   287   function @{ML curry}, because @{ML list_comb} expects the predicate and the

   288   variables list as a pair.

   289   

   290   The combinator @{ML "#>"} is the reverse function composition. It can be

   291   used to define the following function

   292 *}

   293 

   294 ML{*val inc_by_six = 

   295       (fn x => x + 1)

   296    #> (fn x => x + 2)

   297    #> (fn x => x + 3)*}

   298 

   299 text {* 

   300   which is the function composed of first the increment-by-one function and then

   301   increment-by-two, followed by increment-by-three. Again, the reverse function 

   302   composition allows you to read the code top-down.

   303 

   304   The remaining combinators described in this section add convenience for the

   305   ``waterfall method'' of writing functions. The combinator @{ML tap} allows

   306   you to get hold of an intermediate result (to do some side-calculations for

   307   instance). The function

   308 

   309  *}

   310 

   311 ML %linenosgray{*fun inc_by_three x =

   312      x |> (fn x => x + 1)

   313        |> tap (fn x => tracing (makestring x))

   314        |> (fn x => x + 2)*}

   315 

   316 text {* 

   317   increments the argument first by @{text "1"} and then by @{text "2"}. In the

   318   middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''

   319   intermediate result inside the tracing buffer. The function @{ML tap} can

   320   only be used for side-calculations, because any value that is computed

   321   cannot be merged back into the ``main waterfall''. To do this, you can use

   322   the next combinator.

   323 

   324   The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value

   325   and returns the result together with the value (as a pair). For example

   326   the function 

   327 *}

   328 

   329 ML{*fun inc_as_pair x =

   330      x |> `(fn x => x + 1)

   331        |> (fn (x, y) => (x, y + 1))*}

   332 

   333 text {*

   334   takes @{text x} as argument, and then increments @{text x}, but also keeps

   335   @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"

   336   for x}. After that, the function increments the right-hand component of the

   337   pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.

   338 

   339   The combinators @{ML "|>>"} and @{ML "||>"} are defined for 

   340   functions manipulating pairs. The first applies the function to

   341   the first component of the pair, defined as

   342 *}

   343 

   344 ML{*fun (x, y) |>> f = (f x, y)*}

   345 

   346 text {*

   347   and the second combinator to the second component, defined as

   348 *}

   349 

   350 ML{*fun (x, y) ||> f = (x, f y)*}

   351 

   352 text {*

   353   With the combinator @{ML "|->"} you can re-combine the elements from a pair.

   354   This combinator is defined as

   355 *}

   356 

   357 ML{*fun (x, y) |-> f = f x y*}

   358 

   359 text {* and can be used to write the following roundabout version 

   360   of the @{text double} function: 

   361 *}

   362 

   363 ML{*fun double x =

   364       x |>  (fn x => (x, x))

   365         |-> (fn x => fn y => x + y)*}

   366 

   367 text {*

   368   Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 

   369   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},

   370   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function

   371   composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 

   372   for example, the function @{text double} can also be written as:

   373 *}

   374 

   375 ML{*val double =

   376             (fn x => (x, x))

   377         #-> (fn x => fn y => x + y)*}

   378 

   379 text {*

   380   

   381   (FIXME: find a good exercise for combinators)

   382 

   383   \begin{readmore}

   384   The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}

   385   and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 

   386   contains further information about combinators.

   387   \end{readmore}

   388  

   389 *}

   390 

   391 

   392 section {* Antiquotations *}

   393 

   394 text {*

   395   The main advantage of embedding all code in a theory is that the code can

   396   contain references to entities defined on the logical level of Isabelle. By

   397   this we mean definitions, theorems, terms and so on. This kind of reference is

   398   realised with antiquotations.  For example, one can print out the name of the current

   399   theory by typing

   400 

   401   

   402   @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}

   403  

   404   where @{text "@{theory}"} is an antiquotation that is substituted with the

   405   current theory (remember that we assumed we are inside the theory 

   406   @{text FirstSteps}). The name of this theory can be extracted using

   407   the function @{ML "Context.theory_name"}. 

   408 

   409   Note, however, that antiquotations are statically linked, that is their value is

   410   determined at ``compile-time'', not ``run-time''. For example the function

   411 *}

   412 

   413 ML{*fun not_current_thyname () = Context.theory_name @{theory} *}

   414 

   415 text {*

   416 

   417   does \emph{not} return the name of the current theory, if it is run in a 

   418   different theory. Instead, the code above defines the constant function 

   419   that always returns the string @{text [quotes] "FirstSteps"}, no matter where the

   420   function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 

   421   \emph{not} replaced with code that will look up the current theory in 

   422   some data structure and return it. Instead, it is literally

   423   replaced with the value representing the theory name.

   424 

   425   In a similar way you can use antiquotations to refer to proved theorems: 

   426   @{text "@{thm \<dots>}"} for a single theorem

   427 

   428   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}

   429 

   430   and @{text "@{thms \<dots>}"} for more than one

   431 

   432 @{ML_response_fake [display,gray] "@{thms conj_ac}" 

   433 "(?P \<and> ?Q) = (?Q \<and> ?P)

   434 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)

   435 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  

   436 

   437   You can also refer to the current simpset. To illustrate this we implement the

   438   function that extracts the theorem names stored in a simpset.

   439 *}

   440 

   441 ML{*fun get_thm_names_from_ss simpset =

   442 let

   443   val {simps,...} = MetaSimplifier.dest_ss simpset

   444 in

   445   map #1 simps

   446 end*}

   447 

   448 text {*

   449   The function @{ML dest_ss in MetaSimplifier} returns a record containing all

   450   information stored in the simpset. We are only interested in the names of the

   451   simp-rules. So now you can feed in the current simpset into this function. 

   452   The simpset can be referred to using the antiquotation @{text "@{simpset}"}.

   453 

   454   @{ML_response_fake [display,gray] 

   455   "get_thm_names_from_ss @{simpset}" 

   456   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

   457 

   458   Again, this way or referencing simpsets makes you independent from additions

   459   of lemmas to the simpset by the user that potentially cause loops.

   460 

   461   While antiquotations have many applications, they were originally introduced in order 

   462   to avoid explicit bindings for theorems such as:

   463 *}

   464 

   465 ML{*val allI = thm "allI" *}

   466 

   467 text {*

   468   These bindings are difficult to maintain and also can be accidentally

   469   overwritten by the user. This often broke Isabelle

   470   packages. Antiquotations solve this problem, since they are ``linked''

   471   statically at compile-time.  However, this static linkage also limits their

   472   usefulness in cases where data needs to be build up dynamically. In the

   473   course of this chapter you will learn more about these antiquotations:

   474   they can simplify Isabelle programming since one can directly access all

   475   kinds of logical elements from th ML-level.

   476 *}

   477 

   478 text {*

   479   (FIXME: say something about @{text "@{binding \<dots>}"}

   480 *}

   481 

   482 section {* Terms and Types *}

   483 

   484 text {*

   485   One way to construct terms of Isabelle is by using the antiquotation 

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

   487 

   488   @{ML_response [display,gray] 

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

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

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

   492 

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

   494   representation of this term. This internal representation corresponds to the 

   495   datatype @{ML_type "term"}.

   496   

   497   The internal representation of terms uses the usual de Bruijn index mechanism where bound 

   498   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to

   499   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that

   500   binds the corresponding variable. However, in Isabelle the names of bound variables are 

   501   kept at abstractions for printing purposes, and so should be treated only as ``comments''. 

   502   Application in Isabelle is realised with the term-constructor @{ML $}.

   503 

   504   \begin{readmore}

   505   Terms are described in detail in \isccite{sec:terms}. Their

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

   507   \end{readmore}

   508 

   509   Sometimes the internal representation of terms can be surprisingly different

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

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

   512 

   513   \begin{exercise}

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

   515   find out why they are represented like this:

   516 

   517   \begin{itemize}

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

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

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

   521   \end{itemize}

   522 

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

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

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

   526   value:

   527 

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

   529   \end{exercise}

   530 

   531   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 

   532   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 

   533   Consider for example the pairs

   534 

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

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

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

   538  

   539   where a coercion is inserted in the second component and 

   540 

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

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

   543 

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

   545 

   546   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example:

   547 

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

   549 

   550   \begin{readmore}

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

   552   definition and many useful operations are implemented 

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

   554   \end{readmore}

   555 *}

   556 

   557 

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

   559 

   560 text {*

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

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

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

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

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

   566 

   567 *}

   568 

   569 ML{*fun make_imp P Q =

   570 let

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

   572 in 

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

   574 end *}

   575 

   576 text {*

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

   578   into an antiquotation. For example the following does \emph{not} work.

   579 *}

   580 

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

   582 

   583 text {*

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

   585   to both functions. With @{ML make_imp} we obtain the intended term involving 

   586   the given arguments

   587 

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

   589 "Const \<dots> $ 

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

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

   592 

   593   whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} 

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

   595 

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

   597 "Const \<dots> $ 

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

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

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

   601 

   602   (FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda})

   603 *}

   604 

   605 

   606 text {*

   607   \begin{readmore}

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

   609   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 

   610   and types easier.\end{readmore}

   611 

   612   Have a look at these files and try to solve the following two exercises:

   613 *}

   614 

   615 text {*

   616 

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

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

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

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

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

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

   623   \end{exercise}

   624 

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

   626   Write a function which takes two terms representing natural numbers

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

   628   number representing their sum.

   629   \end{exercise}

   630 

   631   There are a few subtle issues with constants. They usually crop up when

   632   pattern matching terms or types, or when constructing them. While it is perfectly ok

   633   to write the function @{text is_true} as follows

   634 *}

   635 

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

   637   | is_true _ = false*}

   638 

   639 text {*

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

   641   the function 

   642 *}

   643 

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

   645   | is_all _ = false*}

   646 

   647 text {* 

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

   649 

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

   651 

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

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

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

   655   for this function is

   656 *}

   657 

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

   659   | is_all _ = false*}

   660 

   661 text {* 

   662   because now

   663 

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

   665 

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

   667   second any term).

   668 

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

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

   671 *}

   672 

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

   674   | is_nil _ = false *}

   675 

   676 text {* 

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

   678 

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

   680 

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

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

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

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

   685 

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

   687 

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

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

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

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

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

   693 

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

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

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

   697 

   698   While you could use the complete name, for example 

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

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

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

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

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

   704   variable parts of the constant's name. Therefore a functions for 

   705   matching against constants that have a polymorphic type should 

   706   be written as follows.

   707 *}

   708 

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

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

   711   | is_nil_or_all _ = false *}

   712 

   713 text {*

   714   Occasional you have to calculate what the ``base'' name of a given

   715   constant is. For this you can use the function @{ML Sign.extern_const} or

   716   @{ML Long_Name.base_name}. For example:

   717 

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

   719 

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

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

   722   strips off all qualifiers.

   723 

   724   \begin{readmore}

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

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

   727   \end{readmore}

   728 

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

   730   situations where you need to construct types manually, especially  

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

   732   type is as follows:

   733 

   734 *} 

   735 

   736 ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}

   737 

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

   739 

   740 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}

   741 

   742 text {*

   743   A handy function for manipulating terms is @{ML map_types}: it takes a 

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

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

   746 *}

   747 

   748 ML{*fun nat_to_int t =

   749   (case t of

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

   751    | Type (s, ts) => Type (s, map nat_to_int ts)

   752    | _ => t)*}

   753 

   754 text {*

   755   An example as follows:

   756 

   757 @{ML_response_fake [display,gray] 

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

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

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

   761 

   762   (FIXME: readmore about types)

   763 *}

   764 

   765 

   766 section {* Type-Checking *}

   767 

   768 text {* 

   769   

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

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

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

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

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

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

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

   777   be constructed via ``official interfaces''.

   778 

   779 

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

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

   782   For example you can write:

   783 

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

   785 

   786   This can also be written with an antiquotation:

   787 

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

   789 

   790   Attempting to obtain the certified term for

   791 

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

   793 

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

   795   example that type-checks is:

   796 

   797 @{ML_response_fake [display,gray] 

   798 "let

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

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

   801 in

   802   cterm_of @{theory} 

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

   804 end" "0 + 0"}

   805 

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

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

   808   the ML-level as follows:

   809 

   810   @{ML_response_fake [display,gray]

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

   812   "nat \<Rightarrow> bool"}

   813 

   814   \begin{readmore}

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

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

   817   \end{readmore}

   818 

   819   \begin{exercise}

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

   821   result that type-checks.

   822   \end{exercise}

   823 

   824   Remember Isabelle foolows the Church-style typing for terms, i.e.~a term contains 

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

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

   827   Given a well-typed term, the function @{ML type_of} returns the 

   828   type of a term. Consider for example:

   829 

   830   @{ML_response [display,gray] 

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

   832 

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

   834   detect any typing inconsistency. For examle changing the type of the variable 

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

   836 

   837   @{ML_response_fake [display,gray] 

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

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

   840 

   841   Since the complete traversal might sometimes be too costly and

   842   not necessary, there is the function @{ML fastype_of}, which 

   843   also returns the type of a term.

   844 

   845   @{ML_response [display,gray] 

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

   847 

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

   849   can see this in the following example

   850 

   851    @{ML_response [display,gray] 

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

   853 

   854   where no error is detected.

   855 

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

   857   complete typing annotations, especially in cases where the typing 

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

   859   type @{ML "dummyT"} and then let type-inference figure out the 

   860   complete type. An example is as follows:

   861 

   862   @{ML_response_fake [display,gray] 

   863 "let

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

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

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

   867 in   

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

   869 end"

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

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

   872 

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

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

   875 

   876   \begin{readmore}

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

   878   checking and pretty-printing of terms are defined. Fuctions related to the

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

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

   881   \end{readmore}

   882 

   883   (FIXME: say something about sorts)

   884 *}

   885 

   886 

   887 section {* Theorems *}

   888 

   889 text {*

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

   891   that can only be build by going through interfaces. As a consequence, every proof 

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

   893   \cite{GordonMilnerWadsworth79}.

   894 

   895 

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

   897   statement:

   898 *}

   899 

   900   lemma 

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

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

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

   904 

   905 text {*

   906   The corresponding ML-code is as follows:

   907 

   908 @{ML_response_fake [display,gray]

   909 "let

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

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

   912 

   913   val Pt_implies_Qt = 

   914         assume assm1

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

   916   

   917   val Qt = implies_elim Pt_implies_Qt (assume assm2);

   918 in

   919   Qt 

   920   |> implies_intr assm2

   921   |> implies_intr assm1

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

   923 

   924   This code-snippet constructs the following proof:

   925 

   926   \[

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

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

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

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

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

   932                  &

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

   934           }

   935        }

   936     }

   937   \]

   938 

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

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

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

   942 

   943   \begin{readmore}

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

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

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

   947   \end{readmore}

   948 

   949   (FIXME: how to add case-names to goal states - maybe in the next section)

   950 *}

   951 

   952 section {* Theorem Attributes *}

   953 

   954 text {*

   955   Theorem attributes are @{text "[simp]"}, @{text "[OF \<dots>]"}, @{text

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

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

   958   theorem is proven. In particular, it is not possible to find out

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

   960   the function behind the attribute stores the theorems in a retrivable 

   961   datastructure. 

   962 

   963   If you want to print out all currently known attributes a theorem 

   964   can have, you can use the function:

   965 

   966   @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" 

   967 "COMP:  direct composition with rules (no lifting)

   968 HOL.dest:  declaration of Classical destruction rule

   969 HOL.elim:  declaration of Classical elimination rule 

   970 \<dots>"}

   971 

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

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

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

   975   this attribute is

   976 *}

   977 

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

   979 

   980 text {* 

   981   where the function @{ML "Thm.rule_attribute"} expects a function taking a 

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

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

   984   @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 

   985   an attribute.

   986 

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

   988   using the function @{ML Attrib.setup} as follows.

   989 *}

   990 

   991 setup %gray {* Attrib.setup @{binding "my_sym"} 

   992   (Scan.succeed my_symmetric) "applying the sym rule"*}

   993 

   994 text {*

   995   The attribute does not expect any further arguments (unlike @{text "[OF

   996   \<dots>]"}, for example, which can take a list of theorems as argument). Therefore

   997   we use the parser @{ML Scan.succeed}. Later on we will also consider

   998   attributes taking further arguments. An example for the attribute @{text

   999   "[my_sym]"} is the proof

  1000 *} 

  1001 

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

  1003 

  1004 text {*

  1005   which stores the theorem @{thm test} under the name @{thm [source] test}. We 

  1006   can also use the attribute when referring to this theorem.

  1007 

  1008   \begin{isabelle}

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

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

  1011   \end{isabelle}

  1012 

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

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

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

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

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

  1018   of theorems.

  1019 *}

  1020 

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

  1022 

  1023 text {* 

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

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

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

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

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

  1029   For this we use the two functions:

  1030 *}

  1031 

  1032 ML{*fun my_thms_add thm ctxt =

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

  1034 

  1035 fun my_thms_del thm ctxt =

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

  1037 

  1038 text {*

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

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

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

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

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

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

  1045   propositions (modulo alpha-equivalence).

  1046 

  1047 

  1048   You can turn both functions into attributes using

  1049 *}

  1050 

  1051 ML{*val my_add = Thm.declaration_attribute my_thms_add

  1052 val my_del = Thm.declaration_attribute my_thms_del *}

  1053 

  1054 text {* 

  1055   and set up the attributes as follows

  1056 *}

  1057 

  1058 setup %gray {* Attrib.setup @{binding "my_thms"}

  1059   (Attrib.add_del my_add my_del) "maintaining a list of my_thms" *}

  1060 

  1061 text {*

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

  1063 *}

  1064 

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

  1066 

  1067 text {*

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

  1069 

  1070   @{ML_response_fake [display,gray]

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

  1072 

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

  1074 *}

  1075 

  1076 declare test[my_thms] trueI_2[my_thms add]

  1077 

  1078 text {*

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

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

  1081   updated as follows.

  1082 

  1083   @{ML_response_fake [display,gray]

  1084   "!my_thms"

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

  1086 

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

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

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

  1090 *}

  1091 

  1092 declare test[my_thms del]

  1093 

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

  1095 

  1096   @{ML_response_fake [display,gray]

  1097   "!my_thms"

  1098   "[\"True\"]"}

  1099 

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

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

  1102   the arguments accordingly. 

  1103 

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

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

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

  1107 *}

  1108 

  1109 ML {*structure Data = GenericDataFun

  1110  (type T = thm list

  1111   val empty = []

  1112   val extend = I

  1113   fun merge _ = Thm.merge_thms) *}

  1114 

  1115 text {*

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

  1117   @{ML my_thms_del} to:

  1118 *}

  1119 

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

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

  1122 

  1123 text {*

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

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

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

  1127   declare 

  1128 *}

  1129 

  1130 ML{*structure FooRules = NamedThmsFun 

  1131  (val name = "foo" 

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

  1133 

  1134 text {*

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