theory FirstSteps
imports Base
uses "FirstSteps.ML"
begin

chapter {* First Steps *}

text {*
  Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
  Isabelle must be part of a theory. If you want to follow the code given in
  this chapter, we assume you are working inside the theory starting with

  \begin{quote}
  \begin{tabular}{@ {}l}
  \isacommand{theory} FirstSteps\\
  \isacommand{imports} Main\\
  \isacommand{begin}\\
  \ldots
  \end{tabular}
  \end{quote}

  We also generally assume you are working with HOL. The given examples might
  need to be adapted if you work in a different logic.
*}

section {* Including ML-Code *}

text {*
  The easiest and quickest way to include code in a theory is by using the
  \isacommand{ML}-command. For example:

  \begin{isabelle}
  \begin{graybox}
  \isacommand{ML}~@{text "\<verbopen>"}\isanewline
  \hspace{5mm}@{ML "3 + 4"}\isanewline
  @{text "\<verbclose>"}\isanewline
  @{text "> 7"}\smallskip
  \end{graybox}
  \end{isabelle}

  Like normal Isabelle scripts, \isacommand{ML}-commands can be evaluated by
  using the advance and undo buttons of your Isabelle environment. The code
  inside the \isacommand{ML}-command can also contain value and function
  bindings, for example
*}

ML %gray {* 
  val r = ref 0
  fun f n = n + 1 
*}

text {*
  and even those can be undone when the proof script is retracted.  As
  mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
  "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines
  prefixed with @{text [quotes] ">"} are not part of the code, rather they
  indicate what the response is when the code is evaluated.  There are also
  the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including
  ML-code. The first evaluates the given code, but any effect on the theory,
  in which the code is embedded, is suppressed. The second needs to be used if
  ML-code is defined inside a proof. For example

  \begin{quote}
  \begin{isabelle}
  \isacommand{lemma}~@{text "test:"}\isanewline
  \isacommand{shows}~@{text [quotes] "True"}\isanewline
  \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline
  \isacommand{oops}
  \end{isabelle}
  \end{quote}

  However, both commands will only play minor roles in this tutorial (we will
  always arrange that the ML-code is defined outside of proofs, for example).

  Once a portion of code is relatively stable, you usually want to export it
  to a separate ML-file. Such files can then be included somewhere inside a 
  theory by using the command \isacommand{use}. For example

  \begin{quote}
  \begin{tabular}{@ {}l}
  \isacommand{theory} FirstSteps\\
  \isacommand{imports} Main\\
  \isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\
  \isacommand{begin}\\
  \ldots\\
  \isacommand{use}~@{text "\"file_to_be_included.ML\""}\\
  \ldots
  \end{tabular}
  \end{quote}

  The \isacommand{uses}-command in the header of the theory is needed in order 
  to indicate the dependency of the theory on the ML-file. Alternatively, the 
  file can be included by just writing in the header

  \begin{quote}
  \begin{tabular}{@ {}l}
  \isacommand{theory} FirstSteps\\
  \isacommand{imports} Main\\
  \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
  \isacommand{begin}\\
  \ldots
  \end{tabular}
  \end{quote}

  Note that no parentheses are given this time. Note also that the included
  ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
  is unable to record all file dependencies, which is a nuisance if you have
  to track down errors.
*}

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

text {*
  During development you might find it necessary to inspect some data in your
  code. This can be done in a ``quick-and-dirty'' fashion using the function
  @{ML_ind  "writeln"}. For example

  @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}

  will print out @{text [quotes] "any string"} inside the response buffer of
  Isabelle.  This function expects a string as argument. If you develop under
  PolyML, then there is a convenient, though again ``quick-and-dirty'', method
  for converting values into strings, namely the function 
  @{ML_ind  makestring in PolyML}:

  @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} 

  However, @{ML makestring in PolyML} only works if the type of what
  is converted is monomorphic and not a function.

  The function @{ML "writeln"} should only be used for testing purposes,
  because any output this function generates will be overwritten as soon as an
  error is raised. For printing anything more serious and elaborate, the
  function @{ML_ind  tracing} is more appropriate. This function writes all
  output into a separate tracing buffer. For example:

  @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}

  It is also possible to redirect the ``channel'' where the string @{text
  "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from
  choking on massive amounts of trace output. This redirection can be achieved
  with the code:
*}

ML{*val strip_specials =
let
  fun strip ("\^A" :: _ :: cs) = strip cs
    | strip (c :: cs) = c :: strip cs
    | strip [] = [];
in 
  implode o strip o explode 
end

fun redirect_tracing stream =
 Output.tracing_fn := (fn s =>
    (TextIO.output (stream, (strip_specials s));
     TextIO.output (stream, "\n");
     TextIO.flushOut stream)) *}

text {*
  Calling now

  @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"}

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

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

@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
"Exception- ERROR \"foo\" raised
At command \"ML\"."}

  This function raises the exception @{text ERROR}, which will then 
  be displayed by the infrastructure.


  (FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 
  @{ML_ind  profiling in Toplevel}.)
*}

(*
ML {* reset Toplevel.debug *}

ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}

ML {* fun innocent () = dodgy_fun () *}
ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}
ML {* exception_trace (fn () => innocent ()) *}

ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}

ML {* Toplevel.program (fn () => innocent ()) *}
*)

text {*
  Most often you want to inspect data of Isabelle's most basic data
  structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
  thm}. Isabelle contains elaborate pretty-printing functions for printing
  them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
  are a bit unwieldy. One way to transform a term into a string is to use the
  function @{ML_ind  string_of_term in Syntax} in structure @{ML_struct
  Syntax}, which we bind for more convenience to the toplevel.
*}

ML{*val string_of_term = Syntax.string_of_term*}

text {*
  It can now be used as follows

  @{ML_response_fake [display,gray]
  "string_of_term @{context} @{term \"1::nat\"}"
  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} 

  This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
  additional information encoded in it. The string can be properly printed by
  using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:

  @{ML_response_fake [display,gray]
  "writeln (string_of_term @{context} @{term \"1::nat\"})"
  "\"1\""}

  or

  @{ML_response_fake [display,gray]
  "tracing (string_of_term @{context} @{term \"1::nat\"})"
  "\"1\""}

  If there are more than one @{ML_type term}s to be printed, you can use the 
  function @{ML_ind  commas} to separate them.
*} 

ML{*fun string_of_terms ctxt ts =  
  commas (map (string_of_term ctxt) ts)*}

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

ML{*fun string_of_cterm ctxt ct =  
  string_of_term ctxt (term_of ct)*}

text {*
  In this example the function @{ML_ind  term_of} extracts the @{ML_type
  term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be
  printed with @{ML_ind  commas}.
*} 

ML{*fun string_of_cterms ctxt cts =  
  commas (map (string_of_cterm ctxt) cts)*}

text {*
  The easiest way to get the string of a theorem is to transform it
  into a @{ML_type cterm} using the function @{ML_ind  crep_thm}. 
*}

ML{*fun string_of_thm ctxt thm =
  string_of_cterm ctxt (#prop (crep_thm thm))*}

text {*
  Theorems also include schematic variables, such as @{text "?P"}, 
  @{text "?Q"} and so on. They are needed in order to able to
  instantiate theorems when they are applied. For example the theorem 
  @{thm [source] conjI} shown below can be used for any (typable) 
  instantiation of @{text "?P"} and @{text "?Q"} 

  @{ML_response_fake [display, gray]
  "tracing (string_of_thm @{context} @{thm conjI})"
  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}

  However, in order to improve the readability when printing theorems, we
  convert these schematic variables into free variables using the function
  @{ML_ind  import in Variable}. This is similar to statements like @{text
  "conjI[no_vars]"} from Isabelle's user-level.
*}

ML{*fun no_vars ctxt thm =
let 
  val ((_, [thm']), _) = Variable.import true [thm] ctxt
in
  thm'
end

fun string_of_thm_no_vars ctxt thm =
  string_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}

text {* 
  Theorem @{thm [source] conjI} is now printed as follows:

  @{ML_response_fake [display, gray]
  "tracing (string_of_thm_no_vars @{context} @{thm conjI})"
  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
  
  Again the function @{ML commas} helps with printing more than one theorem. 
*}

ML{*fun string_of_thms ctxt thms =  
  commas (map (string_of_thm ctxt) thms)

fun string_of_thms_no_vars ctxt thms =  
  commas (map (string_of_thm_no_vars ctxt) thms) *}

text {*
  Note, that when printing out several parcels of information that
  semantically belong together, like a warning message consisting for example
  of a term and a type, you should try to keep this information together in a
  single string. So do not print out information as

@{ML_response_fake [display,gray]
"tracing \"First half,\"; 
tracing \"and second half.\""
"First half,
and second half."}

  but as a single string with appropriate formatting. For example

@{ML_response_fake [display,gray]
"tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
"First half,
and second half."}
  
  To ease this kind of string manipulations, there are a number
  of library functions. For example,  the function @{ML_ind  cat_lines}
  concatenates a list of strings and inserts newlines. 

  @{ML_response [display, gray]
  "cat_lines [\"foo\", \"bar\"]"
  "\"foo\\nbar\""}

  Section \ref{sec:pretty} will also explain infrastructure that helps 
  with more elaborate pretty printing. 
*}


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

text {*
  For beginners perhaps the most puzzling parts in the existing code of Isabelle are
  the combinators. At first they seem to greatly obstruct the
  comprehension of the code, but after getting familiar with them, they
  actually ease the understanding and also the programming.

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

ML{*fun I x = x*}

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

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

text {*
  @{ML_ind  K} ``wraps'' a function around the argument @{text "x"}. However, this 
  function ignores its argument. As a result, @{ML K} defines a constant function 
  always returning @{text x}.

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

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

text {* While just syntactic sugar for the usual function application,
  the purpose of this combinator is to implement functions in a  
  ``waterfall fashion''. Consider for example the function *}

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

text {*
  which increments its argument @{text x} by 5. It proceeds by first incrementing 
  the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking 
  the first component of the pair (Line 4) and finally incrementing the first 
  component by 4 (Line 5). This kind of cascading manipulations of values is quite
  common when dealing with theories (for example by adding a definition, followed by
  lemmas and so on). The reverse application allows you to read what happens in 
  a top-down manner. This kind of coding should also be familiar, 
  if you have been exposed to Haskell's {\it do}-notation. Writing the function 
  @{ML inc_by_five} using the reverse application is much clearer than writing
*}

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

text {* or *}

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

text {* and typographically more economical than *}

ML{*fun inc_by_five x =
let val y1 = x + 1
    val y2 = (y1, y1)
    val y3 = fst y2
    val y4 = y3 + 4
in y4 end*}

text {* 
  Another reason why the let-bindings in the code above are better to be
  avoided: it is more than easy to get the intermediate values wrong, not to 
  mention the nightmares the maintenance of this code causes!

  In Isabelle, a ``real world'' example for a function written in 
  the waterfall fashion might be the following code:
*}

ML %linenosgray{*fun apply_fresh_args f ctxt =
    f |> fastype_of
      |> binder_types 
      |> map (pair "z")
      |> Variable.variant_frees ctxt [f]
      |> map Free  
      |> curry list_comb f *}

text {*
  This function takes a term and a context as argument. If the term is of function
  type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
  applied to it. For example below variables are applied to the term 
  @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:

  @{ML_response_fake [display,gray]
"let
  val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
  val ctxt = @{context}
in 
  apply_fresh_args t ctxt
   |> string_of_term ctxt
   |> tracing
end" 
  "P z za zb"}

  You can read off this behaviour from how @{ML apply_fresh_args} is
  coded: in Line 2, the function @{ML_ind  fastype_of} calculates the type of the
  term; @{ML_ind  binder_types} in the next line produces the list of argument
  types (in the case above the list @{text "[nat, int, unit]"}); Line 4 
  pairs up each type with the string  @{text "z"}; the
  function @{ML_ind  variant_frees in Variable} generates for each @{text "z"} a
  unique name avoiding the given @{text f}; the list of name-type pairs is turned
  into a list of variable terms in Line 6, which in the last line is applied
  by the function @{ML_ind  list_comb} to the term. In this last step we have to 
  use the function @{ML_ind  curry}, because @{ML_ind  list_comb} expects the 
  function and the variables list as a pair. This kind of functions is often needed when
  constructing terms with fresh variables. The infrastructure helps tremendously 
  to avoid any name clashes. Consider for example: 

   @{ML_response_fake [display,gray]
"let
  val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
  val ctxt = @{context}
in
  apply_fresh_args t ctxt 
   |> string_of_term ctxt
   |> tracing
end"
  "za z zb"}
  
  where the @{text "za"} is correctly avoided.

  The combinator @{ML_ind  "#>"} is the reverse function composition. It can be
  used to define the following function
*}

ML{*val inc_by_six = 
      (fn x => x + 1)
   #> (fn x => x + 2)
   #> (fn x => x + 3)*}

text {* 
  which is the function composed of first the increment-by-one function and then
  increment-by-two, followed by increment-by-three. Again, the reverse function 
  composition allows you to read the code top-down.

  The remaining combinators described in this section add convenience for the
  ``waterfall method'' of writing functions. The combinator @{ML_ind  tap} allows
  you to get hold of an intermediate result (to do some side-calculations for
  instance). The function

 *}

ML %linenosgray{*fun inc_by_three x =
     x |> (fn x => x + 1)
       |> tap (fn x => tracing (PolyML.makestring x))
       |> (fn x => x + 2)*}

text {* 
  increments the argument first by @{text "1"} and then by @{text "2"}. In the
  middle (Line 3), however, it uses @{ML_ind  tap} for printing the ``plus-one''
  intermediate result inside the tracing buffer. The function @{ML_ind  tap} can
  only be used for side-calculations, because any value that is computed
  cannot be merged back into the ``main waterfall''. To do this, you can use
  the next combinator.

  The combinator @{ML_ind  "`"} (a backtick) is similar to @{ML tap}, but applies a
  function to the value and returns the result together with the value (as a
  pair). For example the function 
*}

ML{*fun inc_as_pair x =
     x |> `(fn x => x + 1)
       |> (fn (x, y) => (x, y + 1))*}

text {*
  takes @{text x} as argument, and then increments @{text x}, but also keeps
  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
  for x}. After that, the function increments the right-hand component of the
  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.

  The combinators @{ML_ind  "|>>"} and @{ML_ind  "||>"} are defined for 
  functions manipulating pairs. The first applies the function to
  the first component of the pair, defined as
*}

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

text {*
  and the second combinator to the second component, defined as
*}

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

text {*
  These two functions can, for example, be used to avoid explicit @{text "lets"} for
  intermediate values in functions that return pairs. As an example, suppose you
  want to separate a list of integers into two lists according to a
  treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
  should be separated to @{ML "([1,2,3,4], [6,5])"}.  This function can be
  implemented as
*}

ML{*fun separate i [] = ([], [])
  | separate i (x::xs) =
      let 
        val (los, grs) = separate i xs
      in
        if i <= x then (los, x::grs) else (x::los, grs)
      end*}

text {*
  where however the return value of the recursive call is bound explicitly to
  the pair @{ML "(los, grs)" for los grs}. You can implement this function
  more concisely as
*}

ML{*fun separate i [] = ([], [])
  | separate i (x::xs) =
      if i <= x 
      then separate i xs ||> cons x
      else separate i xs |>> cons x*}

text {*
  avoiding the explicit @{text "let"}. While in this example the gain in
  conciseness is only small, in more complicated situations the benefit of
  avoiding @{text "lets"} can be substantial.

  With the combinator @{ML_ind  "|->"} you can re-combine the elements from a pair.
  This combinator is defined as
*}

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

text {* 
  and can be used to write the following roundabout version 
  of the @{text double} function: 
*}

ML{*fun double x =
      x |>  (fn x => (x, x))
        |-> (fn x => fn y => x + y)*}

text {* 
  The combinator @{ML_ind  ||>>} plays a central rôle whenever your task is to update a 
  theory and the update also produces a side-result (for example a theorem). Functions 
  for such tasks return a pair whose second component is the theory and the fist 
  component is the side-result. Using @{ML_ind  ||>>}, you can do conveniently the update 
  and also accumulate the side-results. Consider the following simple function. 
*}

ML %linenosgray{*fun acc_incs x =
    x |> (fn x => ("", x)) 
      ||>> (fn x => (x, x + 1))
      ||>> (fn x => (x, x + 1))
      ||>> (fn x => (x, x + 1))*}

text {*
  The purpose of Line 2 is to just pair up the argument with a dummy value (since
  @{ML_ind  "||>>"} operates on pairs). Each of the next three lines just increment 
  the value by one, but also nest the intermediate results to the left. For example 

  @{ML_response [display,gray]
  "acc_incs 1"
  "((((\"\", 1), 2), 3), 4)"}

  You can continue this chain with:
  
  @{ML_response [display,gray]
  "acc_incs 1 ||>> (fn x => (x, x + 2))"
  "(((((\"\", 1), 2), 3), 4), 6)"}

  (FIXME: maybe give a ``real world'' example for this combinator)
*}

text {*
  Recall that @{ML_ind  "|>"} is the reverse function application. Recall also that
  the related 
  reverse function composition is @{ML_ind  "#>"}. In fact all the combinators 
  @{ML_ind  "|->"}, @{ML_ind  "|>>"} , @{ML_ind  "||>"} and @{ML_ind  
  "||>>"} described above have related combinators for 
  function composition, namely @{ML_ind  "#->"}, @{ML_ind  "#>>"}, 
  @{ML_ind  "##>"} and @{ML_ind  "##>>"}. 
  Using @{ML_ind  "#->"}, for example, the function @{text double} can also be written as:
*}

ML{*val double =
            (fn x => (x, x))
        #-> (fn x => fn y => x + y)*}


text {* 
  When using combinators for writing functions in waterfall fashion, it is
  sometimes necessary to do some ``plumbing'' in order to fit functions
  together. We have already seen such plumbing in the function @{ML
  apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
  list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such 
  plumbing is also needed in situations where a functions operate over lists, 
  but one calculates only with a single entity. An example is the function 
  @{ML_ind  check_terms in Syntax}, whose purpose is to type-check a list 
  of terms.

  @{ML_response_fake [display, gray]
  "let
  val ctxt = @{context}
in
  map (Syntax.parse_term ctxt) [\"m + n\", \"m - (n::nat)\"] 
  |> Syntax.check_terms ctxt
  |> string_of_terms ctxt
  |> tracing
end"
  "m + n, m - n"}
*}

text {*
  In this example we obtain two terms with appropriate typing. However, if you
  have only a single term, then @{ML check_terms in Syntax} needs to be
  adapted. This can be done with the ``plumbing'' function @{ML
  singleton}.\footnote{There is already a function @{ML check_term in Syntax}
  in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML
  check_terms in Syntax}.} For example

  @{ML_response_fake [display, gray]
  "let 
  val ctxt = @{context}
in
  Syntax.parse_term ctxt \"m - (n::nat)\" 
  |> singleton (Syntax.check_terms ctxt)
  |> string_of_term ctxt
  |> tracing
end"
  "m - n"}
   
  \begin{readmore}
  The most frequently used combinators are defined in the files @{ML_file
  "Pure/library.ML"}
  and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} 
  contains further information about combinators.
  \end{readmore}

  (FIXME: find a good exercise for combinators)

  (FIXME: say something about calling conventions) 
*}


section {* Antiquotations *}

text {*
  The main advantage of embedding all code in a theory is that the code can
  contain references to entities defined on the logical level of Isabelle. By
  this we mean definitions, theorems, terms and so on. This kind of reference is
  realised with antiquotations, sometimes also referred to as ML-antiquotations.  
  For example, one can print out the name of the current
  theory by typing

  
  @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
 
  where @{text "@{theory}"} is an antiquotation that is substituted with the
  current theory (remember that we assumed we are inside the theory 
  @{text FirstSteps}). The name of this theory can be extracted using
  the function @{ML_ind  theory_name in Context}. 

  Note, however, that antiquotations are statically linked, that is their value is
  determined at ``compile-time'', not ``run-time''. For example the function
*}

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

text {*

  does \emph{not} return the name of the current theory, if it is run in a 
  different theory. Instead, the code above defines the constant function 
  that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
  function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
  \emph{not} replaced with code that will look up the current theory in 
  some data structure and return it. Instead, it is literally
  replaced with the value representing the theory name.

  In a similar way you can use antiquotations to refer to proved theorems: 
  @{text "@{thm \<dots>}"} for a single theorem

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

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

@{ML_response_fake [display,gray] "@{thms conj_ac}" 
"(?P \<and> ?Q) = (?Q \<and> ?P)
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  

  The point of these antiquotations is that referring to theorems in this way
  makes your code independent from what theorems the user might have stored
  under this name (this becomes especially important when you deal with
  theorem lists; see Section \ref{sec:attributes}).

  You can also refer to the current simpset via an antiquotation. To illustrate 
  this we implement the function that extracts the theorem names stored in a 
  simpset.
*}

ML{*fun get_thm_names_from_ss simpset =
let
  val {simps,...} = MetaSimplifier.dest_ss simpset
in
  map #1 simps
end*}

text {*
  The function @{ML_ind  dest_ss in MetaSimplifier} returns a record containing all
  information stored in the simpset, but we are only interested in the names of the
  simp-rules. Now you can feed in the current simpset into this function. 
  The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.

  @{ML_response_fake [display,gray] 
  "get_thm_names_from_ss @{simpset}" 
  "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

  Again, this way of referencing simpsets makes you independent from additions
  of lemmas to the simpset by the user that can potentially cause loops in your
  code.

  On the ML-level of Isabelle, you often have to work with qualified names.
  These are strings with some additional information, such as positional
  information and qualifiers. Such qualified names can be generated with the
  antiquotation @{text "@{binding \<dots>}"}. For example

  @{ML_response [display,gray]
  "@{binding \"name\"}"
  "name"}

  An example where a qualified name is needed is the function 
  @{ML_ind  define in LocalTheory}.  This function is used below to define 
  the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
  
local_setup %gray {* 
  snd o LocalTheory.define Thm.internalK 
    ((@{binding "TrueConj"}, NoSyn), 
     (Attrib.empty_binding, @{term "True \<and> True"})) *}

text {* 
  Now querying the definition you obtain:

  \begin{isabelle}
  \isacommand{thm}~@{text "TrueConj_def"}\\
  @{text "> "}~@{thm TrueConj_def}
  \end{isabelle}

  (FIXME give a better example why bindings are important; maybe
  give a pointer to \isacommand{local\_setup}; if not, then explain
  why @{ML snd} is needed)

  It is also possible to define your own antiquotations. But you should
  exercise care when introducing new ones, as they can also make your code
  also difficult to read. In the next section we will see how the (build in)
  antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
  restriction of this antiquotation is that it does not allow you to use
  schematic variables. If you want to have an antiquotation that does not have
  this restriction, you can implement your own using the function @{ML_ind 
  ML_Antiquote.inline}. The code is as follows.
*}

ML %linenosgray{*ML_Antiquote.inline "term_pat"
  (Args.context -- Scan.lift Args.name_source >>
     (fn (ctxt, s) =>
       s |> ProofContext.read_term_pattern ctxt
         |> ML_Syntax.print_term
         |> ML_Syntax.atomic))*}

text {*
  The parser in Line 2 provides us with a context and a string; this string is
  transformed into a term using the function @{ML_ind  read_term_pattern in
  ProofContext} (Line 4); the next two lines print the term so that the
  ML-system can understand them. An example of this antiquotation is as
  follows.

  @{ML_response_fake [display,gray]
  "@{term_pat \"Suc (?x::nat)\"}"
  "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}

  which is the internal representation of the term @{text "Suc ?x"}.

  \begin{readmore}
  The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
  for most antiquotations. 
  \end{readmore}

  Note one source of possible confusion about antiquotations. There are two kinds 
  of them in Isabelle, which have very different purpose and infrastructures. The 
  first kind, described in this section, are \emph{ML-antiquotations}. They are 
  used to refer to entities (like terms, types etc) from Isabelle's logic layer 
  inside ML-code. They are ``linked'' statically at compile-time, which  limits 
  sometimes their usefulness in  cases where, for example, terms needs to be 
  built up dynamically.  

  The other kind of antiquotations are \emph{document} antiquotations. 
  They are used only in the text parts of Isabelle and their purpose is to print 
  logical entities inside \LaTeX-documents. They are part of the user level and
  therefore we are not interested in them in this Tutorial, except in 
  Appendix \ref{rec:docantiquotations} where we show how to implement your 
  own document antiquotations. 
*}

section {* Terms and Types *}

text {*
  One way to construct Isabelle terms, is by using the antiquotation 
  \mbox{@{text "@{term \<dots>}"}}. For example

  @{ML_response [display,gray] 
"@{term \"(a::nat) + b = c\"}" 
"Const (\"op =\", \<dots>) $ 
  (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

  will show the term @{term "(a::nat) + b = c"}, but printed using the internal
  representation corresponding to the datatype @{ML_type  "term"} defined as follows: 
*}  

ML_val %linenosgray{*datatype term =
  Const of string * typ 
| Free of string * typ 
| Var of indexname * typ 
| Bound of int 
| Abs of string * typ * term 
| $ of term * term *}

text {*
  This datatype implements lambda-terms typed in Church-style.
  As can be seen in Line 5, terms use the usual de Bruijn index mechanism
  for representing bound variables.  For
  example in

  @{ML_response_fake [display, gray]
  "@{term \"\<lambda>x y. x y\"}"
  "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}

  the indices refer to the number of Abstractions (@{ML Abs}) that we need to
  skip until we hit the @{ML Abs} that binds the corresponding
  variable. Constructing a term with dangling de Bruijn indices is possible,
  but will be flagged as ill-formed when you try to typecheck or certify it
  (see Section~\ref{sec:typechecking}). Note that the names of bound variables
  are kept at abstractions for printing purposes, and so should be treated
  only as ``comments''.  Application in Isabelle is realised with the
  term-constructor @{ML $}.

  Isabelle makes a distinction between \emph{free} variables (term-constructor
  @{ML Free} and written on the user level in blue colour) and
  \emph{schematic} variables (term-constructor @{ML Var} and written with a
  leading question mark). Consider the following two examples
  
  @{ML_response_fake [display, gray]
"let
  val v1 = Var ((\"x\", 3), @{typ bool})
  val v2 = Var ((\"x1\", 3), @{typ bool})
  val v3 = Free (\"x\", @{typ bool})
in
  string_of_terms @{context} [v1, v2, v3]
  |> tracing
end"
"?x3, ?x1.3, x"}

  When constructing terms, you are usually concerned with free variables (as
  mentioned earlier, you cannot construct schematic variables using the
  antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,
  however, observe the distinction. The reason is that only schematic
  varaibles can be instantiated with terms when a theorem is applied. A
  similar distinction between free and schematic variables holds for types
  (see below).

  \begin{readmore}
  Terms and types are described in detail in \isccite{sec:terms}. Their
  definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
  For constructing terms involving HOL constants, many helper functions are defined
  in @{ML_file "HOL/Tools/hologic.ML"}.
  \end{readmore}
  
  Constructing terms via antiquotations has the advantage that only typable
  terms can be constructed. For example

  @{ML_response_fake_both [display,gray]
  "@{term \"x x\"}"
  "Type unification failed: Occurs check!"}

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

  @{ML_response_fake [display,gray] 
"let
  val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
in 
  tracing (string_of_term @{context} omega)
end"
  "x x"}

  with the raw ML-constructors.
  
  Sometimes the internal representation of terms can be surprisingly different
  from what you see at the user-level, because the layers of
  parsing/type-checking/pretty printing can be quite elaborate. 

  \begin{exercise}
  Look at the internal term representation of the following terms, and
  find out why they are represented like this:

  \begin{itemize}
  \item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}  
  \item @{term "\<lambda>(x,y). P y x"}  
  \item @{term "{ [x::int] | x. x \<le> -2 }"}  
  \end{itemize}

  Hint: The third term is already quite big, and the pretty printer
  may omit parts of it by default. If you want to see all of it, you
  can use the following ML-function to set the printing depth to a higher 
  value:

  @{ML [display,gray] "print_depth 50"}
  \end{exercise}

  The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 
  usually invisible @{text "Trueprop"}-coercions whenever necessary. 
  Consider for example the pairs

@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
 Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
 
  where a coercion is inserted in the second component and 

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

  where it is not (since it is already constructed by a meta-implication). 
  The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
  an object logic, for example HOL, into the meta-logic of Isabelle. It
  is needed whenever a term is constructed that will be proved as a theorem. 

  As already seen above, types can be constructed using the antiquotation 
  @{text "@{typ \<dots>}"}. For example:

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

  The corresponding datatype is
*}
  
ML_val{*datatype typ =
  Type  of string * typ list 
| TFree of string * sort 
| TVar  of indexname * sort *}

text {*
  Like with terms, there is the distinction between free type
  variables (term-constructor @{ML "TFree"} and schematic
  type variables (term-constructor @{ML "TVar"}). A type constant,
  like @{typ "int"} or @{typ bool}, are types with an empty list
  of argument types. However, it is a bit difficult to show an
  example, because Isabelle always pretty-prints types (unlike terms).
  Here is a contrived example:

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

  \begin{readmore}
  Types are described in detail in \isccite{sec:types}. Their
  definition and many useful operations are implemented 
  in @{ML_file "Pure/type.ML"}.
  \end{readmore}
*}

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

text {*
  While antiquotations are very convenient for constructing terms, they can
  only construct fixed terms (remember they are ``linked'' at compile-time).
  However, you often need to construct terms dynamically. For example, a
  function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
  @{term P} and @{term Q} as arguments can only be written as:

*}

ML{*fun make_imp P Q =
let
  val x = Free ("x", @{typ nat})
in 
  Logic.all x (Logic.mk_implies (P $ x, Q $ x))
end *}

text {*
  The reason is that you cannot pass the arguments @{term P} and @{term Q} 
  into an antiquotation.\footnote{At least not at the moment.} For example 
  the following does \emph{not} work.
*}

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

text {*
  To see this, apply @{text "@{term S}"} and @{text "@{term T}"} 
  to both functions. With @{ML make_imp} you obtain the intended term involving 
  the given arguments

  @{ML_response [display,gray] "make_imp @{term S} @{term T}" 
"Const \<dots> $ 
  Abs (\"x\", Type (\"nat\",[]),
    Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}

  whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 
  and @{text "Q"} from the antiquotation.

  @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" 
"Const \<dots> $ 
  Abs (\"x\", \<dots>,
    Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
                (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}

  There are a number of handy functions that are frequently used for 
  constructing terms. One is the function @{ML_ind  list_comb}, which takes a term
  and a list of terms as arguments, and produces as output the term
  list applied to the term. For example

@{ML_response_fake [display,gray]
"let
  val trm = @{term \"P::nat\"}
  val args = [@{term \"True\"}, @{term \"False\"}]
in
  list_comb (trm, args)
end"
"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}

  Another handy function is @{ML_ind  lambda}, which abstracts a variable 
  in a term. For example

  @{ML_response_fake [display,gray]
"let
  val x_nat = @{term \"x::nat\"}
  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
in
  lambda x_nat trm
end"
  "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}

  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
  and an abstraction. It also records the type of the abstracted
  variable and for printing purposes also its name.  Note that because of the
  typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
  is of the same type as the abstracted variable. If it is of different type,
  as in

  @{ML_response_fake [display,gray]
"let
  val x_int = @{term \"x::int\"}
  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
in
  lambda x_int trm
end"
  "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}

  then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 
  This is a fundamental principle
  of Church-style typing, where variables with the same name still differ, if they 
  have different type.

  There is also the function @{ML_ind  subst_free} with which terms can be
  replaced by other terms. For example below, we will replace in @{term
  "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
  @{term y}, and @{term x} by @{term True}.

  @{ML_response_fake [display,gray]
"let
  val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
  val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
  val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
in
  subst_free [sub1, sub2] trm
end"
  "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}

  As can be seen, @{ML subst_free} does not take typability into account.
  However it takes alpha-equivalence into account:

  @{ML_response_fake [display, gray]
"let
  val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
  val trm = @{term \"(\<lambda>x::nat. x)\"}
in
  subst_free [sub] trm
end"
  "Free (\"x\", \"nat\")"}

  Similarly the function @{ML_ind  subst_bounds}, replaces lose bound 
  variables with terms. To see how this function works, let us implement a
  function that strips off the outermost quantifiers in a term.
*}

ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
         strip_alls t |>> cons (Free (n, T))
  | strip_alls t = ([], t) *}

text {*
  The function returns a pair consisting of the stripped off variables and
  the body of the universal quantifications. For example

  @{ML_response_fake [display, gray]
  "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
  Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}

  After calling @{ML strip_alls}, you obtain a term with lose bound variables. With
  the function @{ML subst_bounds}, you can replace these lose @{ML_ind 
  Bound}s with the stripped off variables.

  @{ML_response_fake [display, gray, linenos]
  "let
  val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
in 
  subst_bounds (rev vrs, trm) 
  |> string_of_term @{context}
  |> tracing
end"
  "x = y"}

  Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls}
  returned. The reason is that the head of the list the function @{ML subst_bounds}
  takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}
  and so on. 

  There are many convenient functions that construct specific HOL-terms. For
  example @{ML_ind  mk_eq in HOLogic} constructs an equality out of two terms.
  The types needed in this equality are calculated from the type of the
  arguments. For example

@{ML_response_fake [gray,display]
"let
  val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
in
  string_of_term @{context} eq
  |> tracing
end"
  "True = False"}
*}

text {*
  \begin{readmore}
  There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
  "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual
  constructions of terms and types easier.
  \end{readmore}

  When constructing terms manually, there are a few subtle issues with
  constants. They usually crop up when pattern matching terms or types, or
  when constructing them. While it is perfectly ok to write the function
  @{text is_true} as follows
*}

ML{*fun is_true @{term True} = true
  | is_true _ = false*}

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

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

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

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

  The problem is that the @{text "@term"}-antiquotation in the pattern 
  fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
  an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
  for this function is
*}

ML{*fun is_all (Const ("All", _) $ _) = true
  | is_all _ = false*}

text {* 
  because now

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

  matches correctly (the first wildcard in the pattern matches any type and the
  second any term).

  However there is still a problem: consider the similar function that
  attempts to pick out @{text "Nil"}-terms:
*}

ML{*fun is_nil (Const ("Nil", _)) = true
  | is_nil _ = false *}

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

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

  The problem is that on the ML-level the name of a constant is more
  subtle than you might expect. The function @{ML is_all} worked correctly,
  because @{term "All"} is such a fundamental constant, which can be referenced
  by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at

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

  the name of the constant @{text "Nil"} depends on the theory in which the
  term constructor is defined (@{text "List"}) and also in which datatype
  (@{text "list"}). Even worse, some constants have a name involving
  type-classes. Consider for example the constants for @{term "zero"} and
  \mbox{@{text "(op *)"}}:

  @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})" 
 "(Const (\"HOL.zero_class.zero\", \<dots>), 
 Const (\"HOL.times_class.times\", \<dots>))"}

  While you could use the complete name, for example 
  @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
  matching against @{text "Nil"}, this would make the code rather brittle. 
  The reason is that the theory and the name of the datatype can easily change. 
  To make the code more robust, it is better to use the antiquotation 
  @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
  variable parts of the constant's name. Therefore a function for 
  matching against constants that have a polymorphic type should 
  be written as follows.
*}

ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
  | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
  | is_nil_or_all _ = false *}

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

  @{ML_response [display,gray]
  "@{type_name \"list\"}" "\"List.list\""}

  (FIXME: Explain the following better.)

  Occasionally you have to calculate what the ``base'' name of a given
  constant is. For this you can use the function @{ML_ind  "Sign.extern_const"} or
  @{ML_ind  Long_Name.base_name}. For example:

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

  The difference between both functions is that @{ML extern_const in Sign} returns
  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
  strips off all qualifiers.

  \begin{readmore}
  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
  functions about signatures in @{ML_file "Pure/sign.ML"}.
  \end{readmore}

  Although types of terms can often be inferred, there are many
  situations where you need to construct types manually, especially  
  when defining constants. For example the function returning a function 
  type is as follows:

*} 

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

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

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

text {*
  If you want to construct a function type with more than one argument
  type, then you can use @{ML_ind  "--->"}.
*}

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

text {*
  A handy function for manipulating terms is @{ML_ind  map_types}: it takes a 
  function and applies it to every type in a term. You can, for example,
  change every @{typ nat} in a term into an @{typ int} using the function:
*}

ML{*fun nat_to_int ty =
  (case ty of
     @{typ nat} => @{typ int}
   | Type (s, tys) => Type (s, map nat_to_int tys)
   | _ => ty)*}

text {*
  Here is an example:

@{ML_response_fake [display,gray] 
"map_types nat_to_int @{term \"a = (1::nat)\"}" 
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}

  If you want to obtain the list of free type-variables of a term, you
  can use the function @{ML_ind  add_tfrees in Term} 
  (similarly @{ML_ind  add_tvars in Term} for the schematic type-variables). 
  One would expect that such functions
  take a term as input and return a list of types. But their type is actually 

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

  that is they take, besides a term, also a list of type-variables as input. 
  So in order to obtain the list of type-variables of a term you have to 
  call them as follows

  @{ML_response [gray,display]
  "Term.add_tfrees @{term \"(a, b)\"} []"
  "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}

  The reason for this definition is that @{ML add_tfrees in Term} can
  be easily folded over a list of terms. Similarly for all functions
  named @{text "add_*"} in @{ML_file "Pure/term.ML"}.

  \begin{exercise}\label{fun:revsum}
  Write a function @{text "rev_sum : term -> term"} that takes a
  term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
  and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
  the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
  associates to the left. Try your function on some examples. 
  \end{exercise}

  \begin{exercise}\label{fun:makesum}
  Write a function which takes two terms representing natural numbers
  in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
  number representing their sum.
  \end{exercise}

  \begin{exercise}\footnote{Personal communication of
  de Bruijn to Dyckhoff.}\label{ex:debruijn}
  Implement the function, which we below name deBruijn, that depends on a natural
  number n$>$0 and constructs terms of the form:
  
  \begin{center}
  \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
  {\it rhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n.  P\,i}\\
  {\it lhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i = P (i + 1 mod n)}
                        $\longrightarrow$ {\it rhs n}\\
  {\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\
  \end{tabular}
  \end{center}

  For n=3 this function returns the term

  \begin{center}
  \begin{tabular}{l}
  (P 1 = P 2 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\
  (P 2 = P 3 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\ 
  (P 3 = P 1 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3
  \end{tabular}
  \end{center}

  Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}
  for constructing the terms for the logical connectives. 
  \end{exercise}
*}


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

text {* 
  
  You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
  typ}es, since they are just arbitrary unchecked trees. However, you
  eventually want to see if a term is well-formed, or type-checks, relative to
  a theory.  Type-checking is done via the function @{ML_ind  cterm_of}, which
  converts a @{ML_type  term} into a @{ML_type  cterm}, a \emph{certified}
  term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
  abstract objects that are guaranteed to be type-correct, and they can only
  be constructed via ``official interfaces''.


  Type-checking is always relative to a theory context. For now we use
  the @{ML "@{theory}"} antiquotation to get hold of the current theory.
  For example you can write:

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

  This can also be written with an antiquotation:

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

  Attempting to obtain the certified term for

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

  yields an error (since the term is not typable). A slightly more elaborate
  example that type-checks is:

@{ML_response_fake [display,gray] 
"let
  val natT = @{typ \"nat\"}
  val zero = @{term \"0::nat\"}
in
  cterm_of @{theory} 
      (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
end" "0 + 0"}

  In Isabelle not just terms need to be certified, but also types. For example, 
  you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
  the ML-level as follows:

  @{ML_response_fake [display,gray]
  "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
  "nat \<Rightarrow> bool"}

  or with the antiquotation:

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

  \begin{readmore}
  For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
  the file @{ML_file "Pure/thm.ML"}.
  \end{readmore}

  Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 
  enough typing information (constants, free variables and abstractions all have typing 
  information) so that it is always clear what the type of a term is. 
  Given a well-typed term, the function @{ML_ind  type_of} returns the 
  type of a term. Consider for example:

  @{ML_response [display,gray] 
  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}

  To calculate the type, this function traverses the whole term and will
  detect any typing inconsistency. For example changing the type of the variable 
  @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 

  @{ML_response_fake [display,gray] 
  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 
  "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}

  Since the complete traversal might sometimes be too costly and
  not necessary, there is the function @{ML_ind  fastype_of}, which 
  also returns the type of a term.

  @{ML_response [display,gray] 
  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}

  However, efficiency is gained on the expense of skipping some tests. You 
  can see this in the following example

   @{ML_response [display,gray] 
  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}

  where no error is detected.

  Sometimes it is a bit inconvenient to construct a term with 
  complete typing annotations, especially in cases where the typing 
  information is redundant. A short-cut is to use the ``place-holder'' 
  type @{ML_ind  dummyT} and then let type-inference figure out the 
  complete type. An example is as follows:

  @{ML_response_fake [display,gray] 
"let
  val c = Const (@{const_name \"plus\"}, dummyT) 
  val o = @{term \"1::nat\"} 
  val v = Free (\"x\", dummyT)
in   
  Syntax.check_term @{context} (c $ o $ v)
end"
"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
  Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}

  Instead of giving explicitly the type for the constant @{text "plus"} and the free 
  variable @{text "x"}, type-inference fills in the missing information.

  \begin{readmore}
  See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
  checking and pretty-printing of terms are defined. Functions related to
  type-inference are implemented in @{ML_file "Pure/type.ML"} and 
  @{ML_file "Pure/type_infer.ML"}. 
  \end{readmore}

  (FIXME: say something about sorts)

  \begin{exercise}
  Check that the function defined in Exercise~\ref{fun:revsum} returns a
  result that type-checks. See what happens to the  solutions of this 
  exercise given in \ref{ch:solutions} when they receive an ill-typed term
  as input.
  \end{exercise}
*}


section {* Theorems *}

text {*
  Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
  that can only be built by going through interfaces. As a consequence, every proof 
  in Isabelle is correct by construction. This follows the tradition of the LCF approach
  \cite{GordonMilnerWadsworth79}.


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

  lemma 
   assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
   and     assm\<^isub>2: "P t"
   shows "Q t" (*<*)oops(*>*) 

text {*
  The corresponding ML-code is as follows:

@{ML_response_fake [display,gray]
"let
  val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
  val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}

  val Pt_implies_Qt = 
        assume assm1
        |> forall_elim @{cterm \"t::nat\"};
  
  val Qt = implies_elim Pt_implies_Qt (assume assm2);
in
  Qt 
  |> implies_intr assm2
  |> implies_intr assm1
end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}

  This code-snippet constructs the following proof:

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

  However, while we obtained a theorem as result, this theorem is not
  yet stored in Isabelle's theorem database. So it cannot be referenced later
  on. How to store theorems will be explained in Section~\ref{sec:storing}.

  \begin{readmore}
  For the functions @{text "assume"}, @{text "forall_elim"} etc 
  see \isccite{sec:thms}. The basic functions for theorems are defined in
  @{ML_file "Pure/thm.ML"}. 
  \end{readmore}

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

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

  (FIXME: example for how to add theorem styles)
*}

ML {*
fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) =
      strip_assums_all ((a, T)::params, t)
  | strip_assums_all (params, B) = (params, B)

fun style_parm_premise i ctxt t =
  let val prems = Logic.strip_imp_prems t in
    if i <= length prems
    then let val (params,t) = strip_assums_all([], nth prems (i - 1))
         in subst_bounds(map Free params, t) end
    else error ("Not enough premises for prem" ^ string_of_int i ^
      " in propositon: " ^ string_of_term ctxt t)
  end;
*}

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

setup %gray {*
  TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
  TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
*}


section {* Setups (TBD) *}

text {*
  In the previous section we used \isacommand{setup} in order to make
  a theorem attribute known to Isabelle. What happens behind the scenes
  is that \isacommand{setup} expects a function of type 
  @{ML_type "theory -> theory"}: the input theory is the current theory and the 
  output the theory where the theory attribute has been stored.
  
  This is a fundamental principle in Isabelle. A similar situation occurs 
  for example with declaring constants. The function that declares a 
  constant on the ML-level is @{ML_ind  add_consts_i in Sign}. 
  If you write\footnote{Recall that ML-code  needs to be 
  enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 
*}  

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

text {*
  for declaring the constant @{text "BAR"} with type @{typ nat} and 
  run the code, then you indeed obtain a theory as result. But if you 
  query the constant on the Isabelle level using the command \isacommand{term}

  \begin{isabelle}
  \isacommand{term}~@{text [quotes] "BAR"}\\
  @{text "> \"BAR\" :: \"'a\""}
  \end{isabelle}

  you do not obtain a constant of type @{typ nat}, but a free variable (printed in 
  blue) of polymorphic type. The problem is that the ML-expression above did 
  not register the declaration with the current theory. This is what the command
  \isacommand{setup} is for. The constant is properly declared with
*}

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

text {* 
  Now 
  
  \begin{isabelle}
  \isacommand{term}~@{text [quotes] "BAR"}\\
  @{text "> \"BAR\" :: \"nat\""}
  \end{isabelle}

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

  A similar command is \isacommand{local\_setup}, which expects a function
  of type @{ML_type "local_theory -> local_theory"}. Later on we will also
  use the commands \isacommand{method\_setup} for installing methods in the
  current theory and \isacommand{simproc\_setup} for adding new simprocs to
  the current simpset.
*}

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

text {*
  Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
  "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
  annotated to theorems, but functions that do further processing once a
  theorem is proved. In particular, it is not possible to find out
  what are all theorems that have a given attribute in common, unless of course
  the function behind the attribute stores the theorems in a retrievable 
  data structure. 

  If you want to print out all currently known attributes a theorem can have, 
  you can use the Isabelle command

  \begin{isabelle}
  \isacommand{print\_attributes}\\
  @{text "> COMP:  direct composition with rules (no lifting)"}\\
  @{text "> HOL.dest:  declaration of Classical destruction rule"}\\
  @{text "> HOL.elim:  declaration of Classical elimination rule"}\\
  @{text "> \<dots>"}
  \end{isabelle}
  
  The theorem attributes fall roughly into two categories: the first category manipulates
  the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
  stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds
  the theorem to the current simpset).

  To explain how to write your own attribute, let us start with an extremely simple 
  version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
  to produce the ``symmetric'' version of an equation. The main function behind 
  this attribute is
*}

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

text {* 
  where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 
  context (which we ignore in the code above) and a theorem (@{text thm}), and 
  returns another theorem (namely @{text thm} resolved with the theorem 
  @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind "RS"} 
  is explained in Section~\ref{sec:simpletacs}). The function 
  @{ML rule_attribute in Thm} then returns  an attribute.

  Before we can use the attribute, we need to set it up. This can be done
  using the Isabelle command \isacommand{attribute\_setup} as follows:
*}

attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *} 
  "applying the sym rule"

text {*
  Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
  for the theorem attribute. Since the attribute does not expect any further 
  arguments (unlike @{text "[THEN \<dots>]"}, for example), we use the parser @{ML
  Scan.succeed}. Later on we will also consider attributes taking further
  arguments. An example for the attribute @{text "[my_sym]"} is the proof
*} 

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

text {*
  which stores the theorem @{thm test} under the name @{thm [source] test}. You
  can see this, if you query the lemma: 

  \begin{isabelle}
  \isacommand{thm}~@{text "test"}\\
  @{text "> "}~@{thm test}
  \end{isabelle}

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

  \begin{isabelle}
  \isacommand{thm}~@{text "test[my_sym]"}\\
  @{text "> "}~@{thm test[my_sym]}
  \end{isabelle}

  An alternative for setting up an attribute is the function @{ML_ind  setup in Attrib}.
  So instead of using \isacommand{attribute\_setup}, you can also set up the
  attribute as follows:
*}

ML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
  "applying the sym rule" *}

text {*
  This gives a function from @{ML_type "Context.theory -> Context.theory"}, which
  can be used for example with \isacommand{setup}.

  As an example of a slightly more complicated theorem attribute, we implement 
  our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
  as argument and resolve the proved theorem with this list (one theorem 
  after another). The code for this attribute is
*}

ML{*fun MY_THEN thms = 
  Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}

text {* 
  where @{ML swap} swaps the components of a pair. The setup of this theorem
  attribute uses the parser @{ML thms in Attrib}, which parses a list of
  theorems. 
*}

attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} 
  "resolving the list of theorems with the proved theorem"

text {* 
  You can, for example, use this theorem attribute to turn an equation into a 
  meta-equation:

  \begin{isabelle}
  \isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\
  @{text "> "}~@{thm test[MY_THEN eq_reflection]}
  \end{isabelle}

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

  \begin{isabelle}
  \isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\
  @{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
  \end{isabelle}

  It is also possible to combine different theorem attributes, as in:
  
  \begin{isabelle}
  \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
  @{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
  \end{isabelle}
  
  However, here also a weakness of the concept
  of theorem attributes shows through: since theorem attributes can be
  arbitrary functions, they do not in general commute. If you try

  \begin{isabelle}
  \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
  @{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
  \end{isabelle}

  you get an exception indicating that the theorem @{thm [source] sym}
  does not resolve with meta-equations. 

  The purpose of @{ML_ind  rule_attribute in Thm} is to directly manipulate theorems.
  Another usage of theorem attributes is to add and delete theorems from stored data.
  For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
  current simpset. For these applications, you can use @{ML_ind  declaration_attribute in Thm}. 
  To illustrate this function, let us introduce a reference containing a list
  of theorems.
*}

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

text {* 
  The purpose of this reference is to store a list of theorems.
  We are going to modify it by adding and deleting theorems.
  However, a word of warning: such references must not 
  be used in any code that is meant to be more than just for testing purposes! 
  Here it is only used to illustrate matters. We will show later how to store 
  data properly without using references.
 
  We need to provide two functions that add and delete theorems from this list. 
  For this we use the two functions:
*}

ML{*fun my_thm_add thm ctxt =
  (my_thms := Thm.add_thm thm (!my_thms); ctxt)

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

text {*
  These functions take a theorem and a context and, for what we are explaining
  here it is sufficient that they just return the context unchanged. They change
  however the reference @{ML my_thms}, whereby the function 
  @{ML_ind  add_thm in Thm} adds a theorem if it is not already included in 
  the list, and @{ML_ind  del_thm in Thm} deletes one (both functions use the 
  predicate @{ML_ind  eq_thm_prop in Thm}, which compares theorems according to 
  their proved propositions modulo alpha-equivalence).

  You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into 
  attributes with the code
*}

ML{*val my_add = Thm.declaration_attribute my_thm_add
val my_del = Thm.declaration_attribute my_thm_del *}

text {* 
  and set up the attributes as follows
*}

attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} 
  "maintaining a list of my_thms - rough test only!" 

text {*
  The parser @{ML_ind  add_del in Attrib} is a predefined parser for 
  adding and deleting lemmas. Now if you prove the next lemma 
  and attach to it the attribute @{text "[my_thms]"}
*}

lemma trueI_2[my_thms]: "True" by simp

text {*
  then you can see it is added to the initially empty list.

  @{ML_response_fake [display,gray]
  "!my_thms" "[\"True\"]"}

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

declare test[my_thms] trueI_2[my_thms add] 

text {*
  With this attribute, the @{text "add"} operation is the default and does 
  not need to be explicitly given. These three declarations will cause the 
  theorem list to be updated as:

  @{ML_response_fake [display,gray]
  "!my_thms"
  "[\"True\", \"Suc (Suc 0) = 2\"]"}

  The theorem @{thm [source] trueI_2} only appears once, since the 
  function @{ML_ind  add_thm in Thm} tests for duplicates, before extending
  the list. Deletion from the list works as follows:
*}

declare test[my_thms del]

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

  @{ML_response_fake [display,gray]
  "!my_thms"
  "[\"True\"]"}

  We used in this example two functions declared as @{ML_ind  declaration_attribute in Thm}, 
  but there can be any number of them. We just have to change the parser for reading
  the arguments accordingly. 

  However, as said at the beginning of this example, using references for storing theorems is
  \emph{not} the received way of doing such things. The received way is to 
  start a ``data slot'', below called @{text MyThmsData}, generated by the functor 
  @{text GenericDataFun}:
*}

ML{*structure MyThmsData = GenericDataFun
 (type T = thm list
  val empty = []
  val extend = I
  fun merge _ = Thm.merge_thms) *}

text {*
  The type @{text "T"} of this data slot is @{ML_type "thm list"}.\footnote{FIXME: give a pointer
  to where data slots are explained properly.}
  To use this data slot, you only have to change @{ML my_thm_add} and
  @{ML my_thm_del} to:
*}

ML{*val my_thm_add = MyThmsData.map o Thm.add_thm
val my_thm_del = MyThmsData.map o Thm.del_thm*}

text {*
  where @{ML MyThmsData.map} updates the data appropriately. The
  corresponding theorem attributes are
*}

ML{*val my_add = Thm.declaration_attribute my_thm_add
val my_del = Thm.declaration_attribute my_thm_del *}

text {*
  and the setup is as follows
*}

attribute_setup %gray my_thms2 = {* Attrib.add_del my_add my_del *} 
  "properly maintaining a list of my_thms"

text {*
  Initially, the data slot is empty 

  @{ML_response_fake [display,gray]
  "MyThmsData.get (Context.Proof @{context})"
  "[]"}

  but if you prove
*}

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

text {*
  then the lemma is recorded. 

  @{ML_response_fake [display,gray]
  "MyThmsData.get (Context.Proof @{context})"
  "[\"3 = Suc (Suc (Suc 0))\"]"}

  With theorem attribute @{text my_thms2} you can also nicely see why it 
  is important to 
  store data in a ``data slot'' and \emph{not} in a reference. Backtrack
  to the point just before the lemma @{thm [source] three} was proved and 
  check the the content of @{ML_struct MyThmsData}: it should be empty. 
  The addition has been properly retracted. Now consider the proof:
*}

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

text {*
  Checking the content of @{ML my_thms} gives

  @{ML_response_fake [display,gray]
  "!my_thms"
  "[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}

  as expected, but if you backtrack before the lemma @{thm [source] four}, the
  content of @{ML my_thms} is unchanged. The backtracking mechanism
  of Isabelle is completely oblivious about what to do with references, but
  properly treats ``data slots''!

  Since storing theorems in a list is such a common task, there is the special
  functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain
  a named theorem list, you just declare
*}

ML{*structure FooRules = Named_Thms
 (val name = "foo" 
  val description = "Rules for foo") *}

text {*
  and set up the @{ML_struct FooRules} with the command
*}

setup %gray {* FooRules.setup *}

text {*
  This code declares a data slot where the theorems are stored,
  an attribute @{text foo} (with the @{text add} and @{text del} options
  for adding and deleting theorems) and an internal ML interface to retrieve and 
  modify the theorems.

  Furthermore, the facts are made available on the user-level under the dynamic 
  fact name @{text foo}. For example you can declare three lemmas to be of the kind
  @{text foo} by:
*}

lemma rule1[foo]: "A" sorry
lemma rule2[foo]: "B" sorry
lemma rule3[foo]: "C" sorry

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

declare rule1[foo del]

text {* and query the remaining ones with:

  \begin{isabelle}
  \isacommand{thm}~@{text "foo"}\\
  @{text "> ?C"}\\
  @{text "> ?B"}
  \end{isabelle}

  On the ML-level the rules marked with @{text "foo"} can be retrieved
  using the function @{ML FooRules.get}:

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

  \begin{readmore}
  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
  \end{readmore}

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


  \begin{readmore}
  FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in 
  @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
  parsing.
  \end{readmore}
*}



section {* Theories, Contexts and Local Theories (TBD) *}

text {*
  There are theories, proof contexts and local theories (in this order, if you
  want to order them). 

  In contrast to an ordinary theory, which simply consists of a type
  signature, as well as tables for constants, axioms and theorems, a local
  theory contains additional context information, such as locally fixed
  variables and local assumptions that may be used by the package. The type
  @{ML_type local_theory} is identical to the type of \emph{proof contexts}
  @{ML_type "Proof.context"}, although not every proof context constitutes a
  valid local theory.
*}

(*
ML{*signature UNIVERSAL_TYPE =
sig
  type t

  val embed: unit -> ('a -> t) * (t -> 'a option)
end*}

ML{*structure U:> UNIVERSAL_TYPE =
   struct
      type t = exn

      fun 'a embed () =
         let
            exception E of 'a
            fun project (e: t): 'a option =
               case e of
                  E a => SOME a
                | _ => NONE
         in
            (E, project)
         end
   end*}

text {*
  The idea is that type t is the universal type and that each call to embed
  returns a new pair of functions (inject, project), where inject embeds a
  value into the universal type and project extracts the value from the
  universal type. A pair (inject, project) returned by embed works together in
  that project u will return SOME v if and only if u was created by inject
  v. If u was created by a different function inject', then project returns
  NONE.

  in library.ML
*}

ML_val{*structure Object = struct type T = exn end; *}

ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
   struct
      val (intIn: int -> U.t, intOut) = U.embed ()
      val r: U.t ref = ref (intIn 13)
      val s1 =
         case intOut (!r) of
            NONE => "NONE"
          | SOME i => Int.toString i
      val (realIn: real -> U.t, realOut) = U.embed ()
      val () = r := realIn 13.0
      val s2 =
         case intOut (!r) of
            NONE => "NONE"
          | SOME i => Int.toString i
      val s3 =
         case realOut (!r) of
            NONE => "NONE"
          | SOME x => Real.toString x
      val () = tracing (concat [s1, " ", s2, " ", s3, "\n"])
   end*}

ML_val{*structure t = Test(U) *} 

ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}

ML {* LocalTheory.restore *}
ML {* LocalTheory.set_group *}
*)

section {* Storing Theorems\label{sec:storing} (TBD) *}

text {* @{ML_ind  add_thms_dynamic in PureThy} *}

local_setup %gray {* 
  LocalTheory.note Thm.theoremK 
    ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}


(* FIXME: some code below *)

(*<*)
(*
setup {*
 Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
*}
*)
lemma "bar = (1::nat)"
  oops

(*
setup {*   
  Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
 #> PureThy.add_defs false [((@{binding "foo_def"}, 
       Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
 #> snd
*}
*)
(*
lemma "foo = (1::nat)"
  apply(simp add: foo_def)
  done

thm foo_def
*)
(*>*)

section {* Pretty-Printing\label{sec:pretty} *}

text {*
  So far we printed out only plain strings without any formatting except for
  occasional explicit line breaks using @{text [quotes] "\\n"}. This is
  sufficient for ``quick-and-dirty'' printouts. For something more
  sophisticated, Isabelle includes an infrastructure for properly formatting text.
  This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
  its functions do not operate on @{ML_type string}s, but on instances of the
  type:

  @{ML_type_ind [display, gray] "Pretty.T"}

  The function @{ML str in Pretty} transforms a (plain) string into such a pretty 
  type. For example

  @{ML_response_fake [display,gray]
  "Pretty.str \"test\"" "String (\"test\", 4)"}

  where the result indicates that we transformed a string with length 4. Once
  you have a pretty type, you can, for example, control where linebreaks may
  occur in case the text wraps over a line, or with how much indentation a
  text should be printed.  However, if you want to actually output the
  formatted text, you have to transform the pretty type back into a @{ML_type
  string}. This can be done with the function @{ML_ind  string_of in Pretty}. In what
  follows we will use the following wrapper function for printing a pretty
  type:
*}

ML{*fun pprint prt = tracing (Pretty.string_of prt)*}

text {*
  The point of the pretty-printing infrastructure is to give hints about how to
  layout text and let Isabelle do the actual layout. Let us first explain
  how you can insert places where a line break can occur. For this assume the
  following function that replicates a string n times:
*}

ML{*fun rep n str = implode (replicate n str) *}

text {*
  and suppose we want to print out the string:
*}

ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}

text {*
  We deliberately chose a large string so that it spans over more than one line. 
  If we print out the string using the usual ``quick-and-dirty'' method, then
  we obtain the ugly output:

@{ML_response_fake [display,gray]
"tracing test_str"
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
oooooooooooooobaaaaaaaaaaaar"}

  We obtain the same if we just use

@{ML_response_fake [display,gray]
"pprint (Pretty.str test_str)"
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
oooooooooooooobaaaaaaaaaaaar"}

  However by using pretty types you have the ability to indicate a possible
  line break for example at each space. You can achieve this with the function
  @{ML_ind  breaks in Pretty}, which expects a list of pretty types and inserts a
  possible line break in between every two elements in this list. To print
  this list of pretty types as a single string, we concatenate them 
  with the function @{ML_ind  blk in Pretty} as follows:


@{ML_response_fake [display,gray]
"let
  val ptrs = map Pretty.str (space_explode \" \" test_str)
in
  pprint (Pretty.blk (0, Pretty.breaks ptrs))
end"
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}

  Here the layout of @{ML test_str} is much more pleasing to the 
  eye. The @{ML "0"} in @{ML_ind  blk in Pretty} stands for no indentation
  of the printed string. You can increase the indentation and obtain
  
@{ML_response_fake [display,gray]
"let
  val ptrs = map Pretty.str (space_explode \" \" test_str)
in
  pprint (Pretty.blk (3, Pretty.breaks ptrs))
end"
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}

  where starting from the second line the indent is 3. If you want
  that every line starts with the same indent, you can use the
  function @{ML_ind  indent in Pretty} as follows:

@{ML_response_fake [display,gray]
"let
  val ptrs = map Pretty.str (space_explode \" \" test_str)
in
  pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))
end"
"          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}

  If you want to print out a list of items separated by commas and 
  have the linebreaks handled properly, you can use the function 
  @{ML_ind  commas in Pretty}. For example

@{ML_response_fake [display,gray]
"let
  val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
in
  pprint (Pretty.blk (0, Pretty.commas ptrs))
end"
"99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
100016, 100017, 100018, 100019, 100020"}

  where @{ML upto} generates a list of integers. You can print out this
  list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
  @{text [quotes] "}"}, and separated by commas using the function
  @{ML_ind  enum in Pretty}. For example
*}

text {*
  
@{ML_response_fake [display,gray]
"let
  val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
in
  pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)
end"
"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
  100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
  100016, 100017, 100018, 100019, 100020}"}

  As can be seen, this function prints out the ``set'' so that starting 
  from the second, each new line as an indentation of 2.
  
  If you print out something that goes beyond the capabilities of the
  standard functions, you can do relatively easily the formatting
  yourself. Assume you want to print out a list of items where like in ``English''
  the last two items are separated by @{text [quotes] "and"}. For this you can
  write the function

*}

ML %linenosgray{*fun and_list [] = []
  | and_list [x] = [x]
  | and_list xs = 
      let 
        val (front, last) = split_last xs
      in
        (Pretty.commas front) @ 
        [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]
      end *}

text {*
  where Line 7 prints the beginning of the list and Line
  8 the last item. We have to use @{ML "Pretty.brk 1"} in order
  to insert a space (of length 1) before the 
  @{text [quotes] "and"}. This space is also a place where a line break 
  can occur. We do the same after the @{text [quotes] "and"}. This gives you
  for example

@{ML_response_fake [display,gray]
"let
  val ptrs = map (Pretty.str o string_of_int) (1 upto 22)
in
  pprint (Pretty.blk (0, and_list ptrs))
end"
"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
and 22"}

  Next we like to pretty-print a term and its type. For this we use the
  function @{text "tell_type"}.
*}

ML %linenosgray{*fun tell_type ctxt t = 
let
  fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
  val ptrm = Pretty.quote (Syntax.pretty_term ctxt t)
  val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t))
in
  pprint (Pretty.blk (0, 
    (pstr "The term " @ [ptrm] @ pstr " has type " 
      @ [pty, Pretty.str "."])))
end*}

text {*
  In Line 3 we define a function that inserts possible linebreaks in places
  where a space is. In Lines 4 and 5 we pretty-print the term and its type
  using the functions @{ML_ind  pretty_term in Syntax} and @{ML_ind 
  pretty_typ in Syntax}. We also use the function @{ML_ind quote in
  Pretty} in order to enclose the term and type inside quotation marks. In
  Line 9 we add a period right after the type without the possibility of a
  line break, because we do not want that a line break occurs there.


  Now you can write

  @{ML_response_fake [display,gray]
  "tell_type @{context} @{term \"min (Suc 0)\"}"
  "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
  
  To see the proper line breaking, you can try out the function on a bigger term 
  and type. For example:

  @{ML_response_fake [display,gray]
  "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
  "The term \"op = (op = (op = (op = (op = op =))))\" has type 
\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}


  FIXME: TBD below
*}

ML {* pprint (Pretty.big_list "header"  (map (Pretty.str o string_of_int) (4 upto 10))) *}

text {*
chunks inserts forced breaks (unlike blk where you have to do this yourself)
*}

ML {* (Pretty.chunks [Pretty.str "a", Pretty.str "b"], 
       Pretty.blk (0, [Pretty.str "a", Pretty.str "b"])) *}

ML {*
fun setmp_show_all_types f =
   setmp show_all_types
         (! show_types orelse ! show_sorts orelse ! show_all_types) f;

val ctxt = @{context};
val t1 = @{term "undefined::nat"};
val t2 = @{term "Suc y"};
val pty =        Pretty.block (Pretty.breaks
             [(setmp show_question_marks false o setmp_show_all_types)
                  (Syntax.pretty_term ctxt) t1,
              Pretty.str "=", Syntax.pretty_term ctxt t2]);
pty |> Pretty.string_of |> priority
*}

text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}


ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}


ML {* Pretty.mark Markup.subgoal (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}

text {*
  Still to be done:

  What happens with big formulae?

  \begin{readmore}
  The general infrastructure for pretty-printing is implemented in the file
  @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
  contains pretty-printing functions for terms, types, theorems and so on.
  
  @{ML_file "Pure/General/markup.ML"}
  \end{readmore}
*}

text {*
  printing into the goal buffer as part of the proof state
*}


ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}

text {* writing into the goal buffer *}

ML {* fun my_hook interactive state =
         (interactive ? Proof.goal_message (fn () => Pretty.str  
"foo")) state
*}

setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}

lemma "False"
oops


section {* Misc (TBD) *}

ML {*Datatype.get_info @{theory} "List.list"*}

section {* Name Space Issues (TBD) *}


end