theory Essential
imports Base First_Steps
begin

chapter \<open>Isabelle Essentials\<close>

text \<open>
   \begin{flushright}
  {\em One man's obfuscation is another man's abstraction.} \\[1ex]
  Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ 
  24~Nov.~2009
  \end{flushright}

  \medskip
  Isabelle is built around a few central ideas. One central idea is the
  LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there
  is a small trusted core and everything else is built on top of this trusted
  core. The fundamental data structures involved in this core are certified
  terms and certified types, as well as theorems.
\<close>


section \<open>Terms and Types\<close>

text \<open>
  In Isabelle, there are certified terms and uncertified terms (respectively types). 
  Uncertified terms are often just called terms. One way to construct them is by 
  using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example

  @{ML_matchresult [display,gray] 
\<open>@{term "(a::nat) + b = c"}\<close> 
\<open>Const ("HOL.eq", _) $ 
  (Const ("Groups.plus_class.plus", _) $ _ $ _) $ _\<close>}

  constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
  the internal representation corresponding to the datatype @{ML_type_ind "term"}, 
  which is defined as follows: 
\<close>  

ML_val %linenosgray\<open>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\<close>

ML \<open>
let 
  val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
  val arg1 = @{term "1::int"} 
  val arg2 = @{term "2::int"}
in
  pretty_term @{context} (redex $ arg1 $ arg2)
end\<close>

text \<open>
  This datatype implements Church-style lambda-terms, where types are
  explicitly recorded in variables, constants and abstractions.  The
  important point of having terms is that you can pattern-match against them;
  this cannot be done with certified terms. As can be seen in Line 5,
  terms use the usual de Bruijn index mechanism for representing bound
  variables.  For example in

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

  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 $}.

  Be careful if you pretty-print terms. Consider pretty-printing the abstraction
  term shown above:

  @{ML_response [display, gray]
\<open>@{term "\<lambda>x y. x y"}
  |> pretty_term @{context}
  |> pwriteln\<close>
  \<open>\<lambda>x. x\<close>}

  This is one common source for puzzlement in Isabelle, which has 
  tacitly eta-contracted the output. You obtain a similar result 
  with beta-redexes

  @{ML_response [display, gray]
\<open>let 
  val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
  val arg1 = @{term "1::int"} 
  val arg2 = @{term "2::int"}
in
  pretty_term @{context} (redex $ arg1 $ arg2)
  |> pwriteln
end\<close>
  \<open>1\<close>}

  There is a dedicated configuration value for switching off tacit
  eta-contractions, namely @{ML_ind eta_contract in Syntax} (see Section
  \ref{sec:printing}), but none for beta-contractions. However you can avoid
  the beta-contractions by switching off abbreviations using the configuration
  value @{ML_ind show_abbrevs in Syntax}. For example


  @{ML_response [display, gray]
  \<open>let 
  val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
  val arg1 = @{term "1::int"} 
  val arg2 = @{term "2::int"}
  val ctxt = Config.put show_abbrevs false @{context}
in
  pretty_term ctxt (redex $ arg1 $ arg2)
  |> pwriteln
end\<close>
  \<open>(\<lambda>x y. x) 1 2\<close>}

  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 [display, gray]
\<open>let
  val v1 = Var (("x", 3), @{typ bool})
  val v2 = Var (("x1", 3), @{typ bool})
  val v3 = Free ("x", @{typ bool})
in
  pretty_terms @{context} [v1, v2, v3]
  |> pwriteln
end\<close>
\<open>?x3, ?x1.3, x\<close>}

  When constructing terms, you are usually concerned with free
  variables (as mentioned earlier, you cannot construct schematic
  variables using the built-in antiquotation \mbox{\<open>@{term
  \<dots>}\<close>}). If you deal with theorems, you have to, however, observe the
  distinction. The reason is that only schematic variables 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 [display,gray]
  \<open>@{term "x x"}\<close>
  \<open>Type unification failed: Occurs check!\<close>}

  raises a typing error, while it is perfectly ok to construct the term
  with the raw ML-constructors:

  @{ML_response [display,gray] 
\<open>let
  val omega = Free ("x", @{typ "nat \<Rightarrow> nat"}) $ Free ("x", @{typ nat})
in 
  pwriteln (pretty_term @{context} omega)
end\<close>
  "x x"}
  
  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
  need to set the printing depth to a higher value by 
  \end{exercise}
\<close>

declare [[ML_print_depth = 50]]

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

@{ML_matchresult [display,gray] \<open>(@{term "P x"}, @{prop "P x"})\<close> 
\<open>(Free ("P", _) $ Free ("x", _),
 Const ("HOL.Trueprop", _) $ (Free ("P", _) $ Free ("x", _)))\<close>}

  where a coercion is inserted in the second component and 

  @{ML_matchresult [display,gray] \<open>(@{term "P x \<Longrightarrow> Q x"}, @{prop "P x \<Longrightarrow> Q x"})\<close> 
  \<open>(Const ("Pure.imp", _) $ _ $ _, 
 Const ("Pure.imp", _) $ _ $ _)\<close>}

  where it is not (since it is already constructed by a meta-implication). 
  The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of
  an object logic, for example HOL, into the meta-logic of Isabelle. The coercion
  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 
  \<open>@{typ _}\<close>. For example:

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

  The corresponding datatype is
\<close>
  
ML_val %grayML\<open>datatype typ =
  Type  of string * typ list 
| TFree of string * sort 
| TVar  of indexname * sort\<close>

text \<open>
  Like with terms, there is the distinction between free type
  variables (term-constructor @{ML \<open>TFree\<close>}) and schematic
  type variables (term-constructor @{ML \<open>TVar\<close>} and printed with
  a leading question mark). A type constant,
  like @{typ "int"} or @{typ bool}, are types with an empty list
  of argument types. However, it needs a bit of effort to show an
  example, because Isabelle always pretty prints types (unlike terms).
  Using just the antiquotation \<open>@{typ "bool"}\<close> we only see

  @{ML_matchresult [display, gray]
  \<open>@{typ "bool"}\<close>
  \<open>bool\<close>}
  which is the pretty printed version of \<open>bool\<close>. However, in PolyML
  (version \<open>\<ge>\<close>5.3) it is easy to install your own pretty printer. With the
  function below we mimic the behaviour of the usual pretty printer for
  datatypes (it uses pretty-printing functions which will be explained in more
  detail in Section~\ref{sec:pretty}).
\<close>

ML %grayML\<open>local
  fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
  fun pp_list xs = Pretty.list "[" "]" xs
  fun pp_str s   = Pretty.str s
  fun pp_qstr s  = Pretty.quote (pp_str s)
  fun pp_int i   = pp_str (string_of_int i)
  fun pp_sort S  = pp_list (map pp_qstr S)
  fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
in
fun raw_pp_typ (TVar ((a, i), S)) = 
      pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
  | raw_pp_typ (TFree (a, S)) = 
      pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
  | raw_pp_typ (Type (a, tys)) = 
      pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
end\<close>

text \<open>
  We can install this pretty printer with the function 
  @{ML_ind ML_system_pp} as follows.
\<close>

ML %grayML\<open>ML_system_pp
  (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)\<close>

ML \<open>@{typ "bool"}\<close>
text \<open>
  Now the type bool is printed out in full detail.

  @{ML_matchresult [display,gray]
  \<open>@{typ "bool"}\<close>
  \<open>Type ("HOL.bool", [])\<close>}

  When printing out a list-type
  
  @{ML_matchresult [display,gray]
  \<open>@{typ "'a list"}\<close>
  \<open>Type ("List.list", [TFree ("'a", ["HOL.type"])])\<close>}

  we can see the full name of the type is actually \<open>List.list\<close>, indicating
  that it is defined in the theory \<open>List\<close>. However, one has to be 
  careful with names of types, because even if
  \<open>fun\<close> is defined in the theory \<open>HOL\<close>, it is  
  still represented by its simple name.

   @{ML_matchresult [display,gray]
  \<open>@{typ "bool \<Rightarrow> nat"}\<close>
  \<open>Type ("fun", [Type ("HOL.bool", []), Type ("Nat.nat", [])])\<close>}

  We can restore the usual behaviour of Isabelle's pretty printer
  with the code
\<close>

ML %grayML\<open>ML_system_pp
  (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)\<close>

text \<open>
  After that the types for booleans, lists and so on are printed out again 
  the standard Isabelle way.

  @{ML_response [display, gray]
  \<open>(@{typ "bool"},
@{typ "'a list"})\<close>
  \<open>("bool",
"'a list")\<close>}

  \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}
\<close>

section \<open>Constructing Terms and Types Manually\label{sec:terms_types_manually}\<close> 

text \<open>
  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 manually. For example, a
  function that returns the implication \<open>\<And>(x::nat). P x \<Longrightarrow> Q x\<close> taking
  @{term P} and @{term Q} as arguments can only be written as:

\<close>

ML %grayML\<open>fun make_imp P Q =
let
  val x = Free ("x", @{typ nat})
in 
  Logic.all x (Logic.mk_implies (P $ x, Q $ x))
end\<close>

text \<open>
  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.
\<close>

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

text \<open>
  To see this, apply \<open>@{term S}\<close> and \<open>@{term T}\<close> 
  to both functions. With @{ML make_imp} you obtain the intended term involving 
  the given arguments

  @{ML_matchresult [display,gray] \<open>make_imp @{term S} @{term T}\<close> 
\<open>Const _ $ 
  Abs ("x", Type ("Nat.nat",[]),
    Const _ $ (Free ("S",_) $ _) $ (Free ("T",_) $ _))\<close>}

  whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 
  and \<open>Q\<close> from the antiquotation.

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

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


@{ML_response [display,gray]
\<open>let
  val trm = @{term "P::bool \<Rightarrow> bool \<Rightarrow> bool"}
  val args = [@{term "True"}, @{term "False"}]
in
  list_comb (trm, args)
end\<close>
\<open>Free ("P", "bool \<Rightarrow> bool \<Rightarrow> bool") 
   $ Const ("HOL.True", "bool") $ Const ("HOL.False", "bool")\<close>}

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

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

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

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

  then the variable \<open>Free ("x", "nat")\<close> 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 in Term} 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 [display,gray]
\<open>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\<close>
  \<open>Free ("y", "nat \<Rightarrow> nat") $ Const ("HOL.True", "bool")\<close>}

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

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

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

ML %grayML\<open>fun strip_alls t =
let 
  fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
in
  case t of
    Const (@{const_name All}, _) $ Abs body => aux body
  | _ => ([], t)
end\<close>

text \<open>
  The function returns a pair consisting of the stripped off variables and
  the body of the universal quantification. For example

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

  Note that we produced in the body two dangling de Bruijn indices. 
  Later on we will also use the inverse function that
  builds the quantification from a body and a list of (free) variables.
\<close>
  
ML %grayML\<open>fun build_alls ([], t) = t
  | build_alls (Free (x, T) :: vs, t) = 
      Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) 
        $ Abs (x, T, build_alls (vs, t))\<close>

text \<open>
  As said above, after calling @{ML strip_alls}, you obtain a term with loose
  bound variables. With the function @{ML subst_bounds}, you can replace these
  loose @{ML_ind Bound in Term}s with the stripped off variables.

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

  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 \<open>Bound 0\<close>}, the next
  element for @{ML \<open>Bound 1\<close>} and so on. 

  Notice also that this function might introduce name clashes, since we
  substitute just a variable with the name recorded in an abstraction. This
  name is by no means unique. If clashes need to be avoided, then we should
  use the function @{ML_ind dest_abs in Term}, which returns the body where
  the loose de Bruijn index is replaced by a unique free variable. For example


  @{ML_response [display,gray]
  \<open>let
  val body = Bound 0 $ Free ("x", @{typ nat})
in
  Term.dest_abs ("x", @{typ "nat \<Rightarrow> bool"}, body)
end\<close>
  \<open>("xa", Free ("xa", "nat \<Rightarrow> bool") $ Free ("x", "nat"))\<close>}

  Sometimes it is necessary to manipulate de Bruijn indices in terms directly.
  There are many functions to do this. We describe only two. The first,
  @{ML_ind incr_boundvars in Term}, increases by an integer the indices 
  of the loose bound variables in a term. In the code below

@{ML_response [display,gray]
\<open>@{term "\<forall>x y z u. z = u"}
  |> strip_alls
  ||> incr_boundvars 2
  |> build_alls
  |> pretty_term @{context}
  |> pwriteln\<close>
  \<open>\<forall>x y z u. x = y\<close>}

  we first strip off the forall-quantified variables (thus creating two loose
  bound variables in the body); then we increase the indices of the loose
  bound variables by @{ML 2} and finally re-quantify the variables. As a
  result of @{ML incr_boundvars}, we obtain now a term that has the equation
  between the first two quantified variables.

  The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term
  contains a loose bound of a certain index. For example

  @{ML_matchresult [gray,display]
\<open>let
  val body = snd (strip_alls @{term "\<forall>x y. x = (y::bool)"})
in
  [loose_bvar1 (body, 0),
   loose_bvar1 (body, 1),
   loose_bvar1 (body, 2)]
end\<close>
  \<open>[true, true, false]\<close>}

  There are also many convenient functions that construct specific HOL-terms
  in the structure @{ML_structure HOLogic}. 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 [gray,display]
\<open>let
  val eq = HOLogic.mk_eq (@{term "True"}, @{term "False"})
in
  eq |> pretty_term @{context}
     |> pwriteln
end\<close>
  \<open>True = False\<close>}

  \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 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
  \<open>is_true\<close> as follows
\<close>

ML %grayML\<open>fun is_true @{term True} = true
  | is_true _ = false\<close>

text \<open>
  this does not work for picking out \<open>\<forall>\<close>-quantified terms. Because
  the function 
\<close>

ML %grayML\<open>fun is_all (@{term All} $ _) = true
  | is_all _ = false\<close>

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

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

  The problem is that the \<open>@term\<close>-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
\<close>

ML %grayML\<open>fun is_all (Const ("HOL.All", _) $ _) = true
  | is_all _ = false\<close>

text \<open>
  because now

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

  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 \<open>Nil\<close>-terms:
\<close>

ML %grayML\<open>fun is_nil (Const ("Nil", _)) = true
  | is_nil _ = false\<close>

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

  @{ML_matchresult [display,gray] \<open>is_nil @{term "Nil"}\<close> \<open>false\<close>}

  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 \<open>Const ("All", some_type)\<close> for some_type}. However, if you look at

  @{ML_matchresult [display,gray] \<open>@{term "Nil"}\<close> \<open>Const ("List.list.Nil", _)\<close>}

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

  @{ML_matchresult [display,gray] \<open>(@{term "0::nat"}, @{term "times"})\<close> 
 \<open>(Const ("Groups.zero_class.zero", _), 
 Const ("Groups.times_class.times", _))\<close>}

  While you could use the complete name, for example 
  @{ML \<open>Const ("List.list.Nil", some_type)\<close> for some_type}, for referring to or
  matching against \<open>Nil\<close>, 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 
  \<open>@{const_name \<dots>}\<close>. 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.
\<close>

ML %grayML\<open>fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
  | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
  | is_nil_or_all _ = false\<close>

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

  @{ML_matchresult [display,gray]
  \<open>@{type_name "list"}\<close> \<open>"List.list"\<close>}

  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:

\<close> 

ML %grayML\<open>fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2])\<close>

text \<open>This can be equally written with the combinator @{ML_ind "-->" in Term} as:\<close>

ML %grayML\<open>fun make_fun_type ty1 ty2 = ty1 --> ty2\<close>

text \<open>
  If you want to construct a function type with more than one argument
  type, then you can use @{ML_ind "--->" in Term}.
\<close>

ML %grayML\<open>fun make_fun_types tys ty = tys ---> ty\<close>

text \<open>
  A handy function for manipulating terms is @{ML_ind map_types in Term}: 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:
\<close>

ML %grayML\<open>fun nat_to_int ty =
  (case ty of
     @{typ nat} => @{typ int}
   | Type (s, tys) => Type (s, map nat_to_int tys)
   | _ => ty)\<close>

text \<open>
  Here is an example:

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

  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_matchresult [gray,display]
  \<open>Term.add_tfrees @{term "(a, b)"} []\<close>
  \<open>[("'b", ["HOL.type"]), ("'a", ["HOL.type"])]\<close>}

  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 \<open>add_*\<close> in @{ML_file "Pure/term.ML"}.

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

  \begin{exercise}\label{fun:makesum}
  Write a function that 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}\label{fun:killqnt}
  Write a function that removes trivial forall and exists quantifiers that do not
  quantify over any variables.  For example the term @{term "\<forall>x y z. P x = P
  z"} should be transformed to @{term "\<forall>x z. P x = P z"}, deleting the
  quantification @{term "y"}. Hint: use the functions @{ML incr_boundvars}
  and @{ML loose_bvar1}.
  \end{exercise}

  \begin{exercise}\label{fun:makelist}
  Write a function that takes an integer \<open>i\<close> and
  produces an Isabelle integer list from \<open>1\<close> upto \<open>i\<close>, 
  and then builds the reverse of this list using @{const rev}. 
  The relevant helper functions are @{ML upto}, 
  @{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}.
  \end{exercise}

  \begin{exercise}\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}

  This function returns for n=3 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.\footnote{Thanks to Roy
  Dyckhoff for suggesting this exercise and working out the details.} 
  \end{exercise}
\<close>

section \<open>Unification and Matching\label{sec:univ}\<close>

text \<open>
  As seen earlier, Isabelle's terms and types may contain schematic term variables
  (term-constructor @{ML Var}) and schematic type variables (term-constructor
  @{ML TVar}). These variables stand for unknown entities, which can be made
  more concrete by instantiations. Such instantiations might be a result of
  unification or matching. While in case of types, unification and matching is
  relatively straightforward, in case of terms the algorithms are
  substantially more complicated, because terms need higher-order versions of
  the unification and matching algorithms. Below we shall use the
  antiquotations \<open>@{typ_pat \<dots>}\<close> and \<open>@{term_pat \<dots>}\<close> from
  Section~\ref{sec:antiquote} in order to construct examples involving
  schematic variables.

  Let us begin with describing the unification and matching functions for
  types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})
  which map schematic type variables to types and sorts. Below we use the
  function @{ML_ind typ_unify in Sign} from the structure @{ML_structure Sign}
  for unifying the types \<open>?'a * ?'b\<close> and \<open>?'b list *
  nat\<close>. This will produce the mapping, or type environment, \<open>[?'a :=
  ?'b list, ?'b := nat]\<close>.
\<close>

ML %linenosgray\<open>val (tyenv_unif, _) = let
  val ty1 = @{typ_pat "?'a * ?'b"}
  val ty2 = @{typ_pat "?'b list * nat"}
in
  Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
end\<close>

text \<open>
  The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
  environment, which is needed for starting the unification without any
  (pre)instantiations. The \<open>0\<close> is an integer index that will be explained
  below. In case of failure, @{ML typ_unify in Sign} will raise the exception
  \<open>TUNIFY\<close>.  We can print out the resulting type environment bound to 
  @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
  structure @{ML_structure Vartab}.

  @{ML_response [display,gray]
  \<open>Vartab.dest tyenv_unif\<close>
  \<open>[(("'a", 0), (["HOL.type"], "?'b list")), 
 (("'b", 0), (["HOL.type"], "nat"))]\<close>} 
\<close>

text_raw \<open>
  \begin{figure}[t]
  \begin{minipage}{\textwidth}
  \begin{isabelle}\<close>
ML %grayML\<open>fun pretty_helper aux env =
  env |> Vartab.dest  
      |> map aux
      |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) 
      |> Pretty.enum "," "[" "]" 
      |> pwriteln

fun pretty_tyenv ctxt tyenv =
let
  fun get_typs (v, (s, T)) = (TVar (v, s), T)
  val print = apply2 (pretty_typ ctxt)
in 
  pretty_helper (print o get_typs) tyenv
end\<close>
text_raw \<open>
  \end{isabelle}
  \end{minipage}
  \caption{A pretty printing function for type environments, which are 
  produced by unification and matching.\label{fig:prettyenv}}
  \end{figure}
\<close>

text \<open>
  The first components in this list stand for the schematic type variables and
  the second are the associated sorts and types. In this example the sort is
  the default sort \<open>HOL.type\<close>. Instead of @{ML \<open>Vartab.dest\<close>}, we will
  use in what follows our own pretty-printing function from
  Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
  environment in the example this function prints out the more legible:


  @{ML_response [display, gray]
  \<open>pretty_tyenv @{context} tyenv_unif\<close>
  \<open>[?'a := ?'b list, ?'b := nat]\<close>}

  The way the unification function @{ML typ_unify in Sign} is implemented 
  using an initial type environment and initial index makes it easy to
  unify more than two terms. For example 
\<close>

ML %linenosgray\<open>val (tyenvs, _) = let
  val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
  val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
in
  fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0) 
end\<close>

text \<open>
  The index \<open>0\<close> in Line 5 is the maximal index of the schematic type
  variables occurring in \<open>tys1\<close> and \<open>tys2\<close>. This index will be
  increased whenever a new schematic type variable is introduced during
  unification.  This is for example the case when two schematic type variables
  have different, incomparable sorts. Then a new schematic type variable is
  introduced with the combined sorts. To show this let us assume two sorts,
  say \<open>s1\<close> and \<open>s2\<close>, which we attach to the schematic type
  variables \<open>?'a\<close> and \<open>?'b\<close>. Since we do not make any
  assumption about the sorts, they are incomparable.
\<close>

class s1
class s2 

ML %grayML\<open>val (tyenv, index) = let
  val ty1 = @{typ_pat "?'a::s1"}
  val ty2 = @{typ_pat "?'b::s2"}
in
  Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
end\<close>

declare[[show_sorts]]

text \<open>
  To print out the result type environment we switch on the printing 
  of sort information by setting @{ML_ind show_sorts in Syntax} to 
  true. This allows us to inspect the typing environment.

  @{ML_response [display,gray]
  \<open>pretty_tyenv @{context} tyenv\<close>
  \<open>[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]\<close>}
\<close>

declare[[show_sorts=false]]

text\<open>
  As can be seen, the type variables \<open>?'a\<close> and \<open>?'b\<close> are instantiated
  with a new type variable \<open>?'a1\<close> with sort \<open>{s1, s2}\<close>. Since a new
  type variable has been introduced the @{ML index}, originally being \<open>0\<close>, 
  has been increased to \<open>1\<close>.

  @{ML_matchresult [display,gray]
  \<open>index\<close>
  \<open>1\<close>}

  Let us now return to the unification problem \<open>?'a * ?'b\<close> and 
  \<open>?'b list * nat\<close> from the beginning of this section, and the 
  calculated type environment @{ML tyenv_unif}:

  @{ML_response [display, gray]
  \<open>pretty_tyenv @{context} tyenv_unif\<close>
  \<open>[?'a := ?'b list, ?'b := nat]\<close>}

  Observe that the type environment which the function @{ML typ_unify in
  Sign} returns is \emph{not} an instantiation in fully solved form: while \<open>?'b\<close> is instantiated to @{typ nat}, this is not propagated to the
  instantiation for \<open>?'a\<close>.  In unification theory, this is often
  called an instantiation in \emph{triangular form}. These triangular 
  instantiations, or triangular type environments, are used because of 
  performance reasons. To apply such a type environment to a type, say \<open>?'a *
  ?'b\<close>, you should use the function @{ML_ind norm_type in Envir}:

  @{ML_response [display, gray]
  \<open>Envir.norm_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
  \<open>nat list \<times> nat\<close>}

  Matching of types can be done with the function @{ML_ind typ_match in Sign}
  also from the structure @{ML_structure Sign}. This function returns a @{ML_type
  Type.tyenv} as well, but might raise the exception \<open>TYPE_MATCH\<close> in case
  of failure. For example
\<close>

ML %grayML\<open>val tyenv_match = let
  val pat = @{typ_pat "?'a * ?'b"}
  and ty  = @{typ_pat "bool list * nat"}
in
  Sign.typ_match @{theory} (pat, ty) Vartab.empty 
end\<close>

text \<open>
  Printing out the calculated matcher gives

  @{ML_response [display,gray]
  \<open>pretty_tyenv @{context} tyenv_match\<close>
  \<open>[?'a := bool list, ?'b := nat]\<close>}
  
  Unlike unification, which uses the function @{ML norm_type in Envir}, 
  applying the matcher to a type needs to be done with the function
  @{ML_ind subst_type in Envir}. For example

  @{ML_response [display, gray]
  \<open>Envir.subst_type tyenv_match @{typ_pat "?'a * ?'b"}\<close>
  \<open>bool list \<times> nat\<close>}

  Be careful to observe the difference: always use
  @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} 
  for unifiers. To show the difference, let us calculate the 
  following matcher:
\<close>

ML %grayML\<open>val tyenv_match' = let
  val pat = @{typ_pat "?'a * ?'b"}
  and ty  = @{typ_pat "?'b list * nat"}
in
  Sign.typ_match @{theory} (pat, ty) Vartab.empty 
end\<close>

text \<open>
  Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply 
  @{ML norm_type in Envir} to the type \<open>?'a * ?'b\<close> we obtain

  @{ML_response [display, gray]
  \<open>Envir.norm_type tyenv_match' @{typ_pat "?'a * ?'b"}\<close>
  \<open>nat list \<times> nat\<close>}

  which does not solve the matching problem, and if
  we apply @{ML subst_type in Envir} to the same type we obtain

  @{ML_response [display, gray]
  \<open>Envir.subst_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
  \<open>?'b list \<times> nat\<close>}
  
  which does not solve the unification problem.

  \begin{readmore}
  Unification and matching for types is implemented
  in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them
  are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments
  as results. These are implemented in @{ML_file "Pure/envir.ML"}.
  This file also includes the substitution and normalisation functions,
  which apply a type environment to a type. Type environments are lookup 
  tables which are implemented in @{ML_file "Pure/term_ord.ML"}.
  \end{readmore}
\<close>

text \<open>
  Unification and matching of terms is substantially more complicated than the
  type-case. The reason is that terms have abstractions and, in this context,  
  unification or matching modulo plain equality is often not meaningful. 
  Nevertheless, Isabelle implements the function @{ML_ind
  first_order_match in Pattern} for terms.  This matching function returns a
  type environment and a term environment.  To pretty print the latter we use
  the function \<open>pretty_env\<close>:
\<close>

ML %grayML\<open>fun pretty_env ctxt env =
let
  fun get_trms (v, (T, t)) = (Var (v, T), t) 
  val print = apply2 (pretty_term ctxt)
in
  pretty_helper (print o get_trms) env 
end\<close>

text \<open>
  As can be seen from the \<open>get_trms\<close>-function, a term environment associates 
  a schematic term variable with a type and a term.  An example of a first-order 
  matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern 
  \<open>?X ?Y\<close>.
\<close>

ML %grayML\<open>val (_, fo_env) = let
  val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
  val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"} 
  val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
  val init = (Vartab.empty, Vartab.empty) 
in
  Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init
end\<close>

text \<open>
  In this example we annotated types explicitly because then 
  the type environment is empty and can be ignored. The 
  resulting term environment is

  @{ML_response [display, gray]
  \<open>pretty_env @{context} fo_env\<close>
  \<open>[?X := P, ?Y := \<lambda>a b. Q b a]\<close>}

  The matcher can be applied to a term using the function @{ML_ind subst_term
  in Envir} (remember the same convention for types applies to terms: @{ML
  subst_term in Envir} is for matchers and @{ML norm_term in Envir} for
  unifiers). The function @{ML subst_term in Envir} expects a type environment,
  which is set to empty in the example below, and a term environment.

  @{ML_response [display, gray]
  \<open>let
  val trm = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
in
  Envir.subst_term (Vartab.empty, fo_env) trm
  |> pretty_term @{context}
  |> pwriteln
end\<close>
  \<open>P (\<lambda>a b. Q b a)\<close>}

  First-order matching is useful for matching against applications and
  variables. It can also deal with abstractions and a limited form of
  alpha-equivalence, but this kind of matching should be used with care, since
  it is not clear whether the result is meaningful. A meaningful example is
  matching \<open>\<lambda>x. P x\<close> against the pattern \<open>\<lambda>y. ?X y\<close>. In this
  case, first-order matching produces \<open>[?X := P]\<close>.

  @{ML_response [display, gray]
  \<open>let
  val fo_pat = @{term_pat "\<lambda>y. (?X::nat\<Rightarrow>bool) y"}
  val trm = @{term "\<lambda>x. (P::nat\<Rightarrow>bool) x"} 
  val init = (Vartab.empty, Vartab.empty) 
in
  Pattern.first_order_match @{theory} (fo_pat, trm) init
  |> snd 
  |> pretty_env @{context} 
end\<close>
  \<open>[?X := P]\<close>}
\<close>

text \<open>
  Unification of abstractions is more thoroughly studied in the context of
  higher-order pattern unification and higher-order pattern matching.  A
  \emph{\index*{pattern}} is a well-formed term in which the arguments to
  every schematic variable are distinct bounds.
  In particular this excludes terms where a
  schematic variable is an argument of another one and where a schematic
  variable is applied twice with the same bound variable. The function
  @{ML_ind pattern in Pattern} in the structure @{ML_structure Pattern} tests
  whether a term satisfies these restrictions under the assumptions
  that it is beta-normal, well-typed and has no loose bound variables.

  @{ML_matchresult [display, gray]
  \<open>let
  val trm_list = 
        [@{term_pat "?X"}, @{term_pat "a"},
         @{term_pat "f (\<lambda>a b. ?X a b) c"},
         @{term_pat "\<lambda>a b. (+) a b"},
         @{term_pat "\<lambda>a. (+) a ?Y"}, @{term_pat "?X ?Y"},
         @{term_pat "\<lambda>a b. ?X a b ?Y"}, @{term_pat "\<lambda>a. ?X a a"},
         @{term_pat "?X a"}] 
in
  map Pattern.pattern trm_list
end\<close>
  \<open>[true, true, true, true, true, false, false, false, false]\<close>}

  The point of the restriction to patterns is that unification and matching 
  are decidable and produce most general unifiers, respectively matchers. 
  Note that \emph{both} terms to be unified have to be higher-order patterns
  for this to work. The exception @{ML_ind Pattern in Pattern} indicates failure
  in this regard.
  In this way, matching and unification can be implemented as functions that 
  produce a type and term environment (unification actually returns a 
  record of type @{ML_type Envir.env} containing a max-index, a type environment 
  and a term environment). The corresponding functions are @{ML_ind match in Pattern}
  and @{ML_ind unify in Pattern}, both implemented in the structure
  @{ML_structure Pattern}. An example for higher-order pattern unification is

  @{ML_response [display, gray]
  \<open>let
  val trm1 = @{term_pat "\<lambda>x y. g (?X y x) (f (?Y x))"}
  val trm2 = @{term_pat "\<lambda>u v. g u (f u)"}
  val init = Envir.empty 0
  val env = Pattern.unify (Context.Proof @{context}) (trm1, trm2) init (* FIXME: Reference to generic context *)
in
  pretty_env @{context} (Envir.term_env env)
end\<close>
  \<open>[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]\<close>}

  The function @{ML_ind "Envir.empty"} generates a record with a specified
  max-index for the schematic variables (in the example the index is \<open>0\<close>) and empty type and term environments. The function @{ML_ind
  "Envir.term_env"} pulls out the term environment from the result record. The
  corresponding function for type environment is @{ML_ind
  "Envir.type_env"}. An assumption of this function is that the terms to be
  unified have already the same type. In case of failure, the exceptions that
  are raised are either \<open>Pattern\<close>, \<open>MATCH\<close> or \<open>Unif\<close>.

  As mentioned before, unrestricted higher-order unification, respectively
  unrestricted higher-order matching, is in general undecidable and might also
  not possess a single most general solution. Therefore Isabelle implements the
  unification function @{ML_ind unifiers in Unify} so that it returns a lazy
  list of potentially infinite unifiers.  An example is as follows
\<close>

ML %grayML\<open>val uni_seq =
let 
  val trm1 = @{term_pat "?X ?Y"}
  val trm2 = @{term "f a"}
  val init = Envir.empty 0
in
  Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
end\<close>

text \<open>
  The unifiers can be extracted from the lazy sequence using the 
  function @{ML_ind "Seq.pull"}. In the example we obtain three 
  unifiers \<open>un1\<dots>un3\<close>.
\<close>

ML %grayML\<open>val SOME ((un1, _), next1) = Seq.pull uni_seq;
val SOME ((un2, _), next2) = Seq.pull next1;
val SOME ((un3, _), next3) = Seq.pull next2;
val NONE = Seq.pull next3\<close>

text \<open>
  \footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?}

  We can print them out as follows.

  @{ML_response [display, gray]
  \<open>pretty_env @{context} (Envir.term_env un1)\<close>
  \<open>[?X := \<lambda>a. a, ?Y := f a]\<close>}
  @{ML_response [display, gray]
  \<open>pretty_env @{context} (Envir.term_env un2)\<close>
  \<open>[?X := f, ?Y := a]\<close>}
  @{ML_response [display, gray]
  \<open>pretty_env @{context} (Envir.term_env un3)\<close>
  \<open>[?X := \<lambda>b. f a]\<close>}


  In case of failure the function @{ML_ind unifiers in Unify} does not raise
  an exception, rather returns the empty sequence. For example

  @{ML_matchresult [display, gray]
\<open>let 
  val trm1 = @{term "a"}
  val trm2 = @{term "b"}
  val init = Envir.empty 0
in
  Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
  |> Seq.pull
end\<close>
\<open>NONE\<close>}

  In order to find a reasonable solution for a unification problem, Isabelle
  also tries first to solve the problem by higher-order pattern
  unification. Only in case of failure full higher-order unification is
  called. This function has a built-in bound, which can be accessed and
  manipulated as a configuration value. For example

  @{ML_matchresult [display,gray]
  \<open>Config.get_global @{theory} (Unify.search_bound)\<close>
  \<open>60\<close>}

  If this bound is reached during unification, Isabelle prints out the
  warning message @{text [quotes] "Unification bound exceeded"} and
  plenty of diagnostic information (sometimes annoyingly plenty of 
  information). 


  For higher-order matching the function is called @{ML_ind matchers in Unify}
  implemented in the structure @{ML_structure Unify}. Also this function returns
  sequences with possibly more than one matcher.  Like @{ML unifiers in
  Unify}, this function does not raise an exception in case of failure, but
  returns an empty sequence. It also first tries out whether the matching
  problem can be solved by first-order matching.

  Higher-order matching might be necessary for instantiating a theorem
  appropriately. More on this will be given in Section~\ref{sec:theorems}. 
  Here we only have a look at a simple case, namely the theorem 
  @{thm [source] spec}:

  \begin{isabelle}
  \isacommand{thm}~@{thm [source] spec}\\
  \<open>> \<close>~@{thm spec}
  \end{isabelle}

  as an introduction rule. Applying it directly can lead to unexpected
  behaviour since the unification has more than one solution. One way round
  this problem is to instantiate the schematic variables \<open>?P\<close> and
  \<open>?x\<close>.  Instantiation function for theorems is 
  @{ML_ind instantiate_normalize in Drule} from the structure 
  @{ML_structure Drule}. One problem, however, is
  that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"}
  respective @{ML_type "(indexname * typ) * cterm"}:

  \begin{isabelle}
  @{ML instantiate_normalize in Drule}\<open>:\<close>
  @{ML_type "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"}
  \end{isabelle}

  This means we have to transform the environment the higher-order matching 
  function returns into such an instantiation. For this we use the functions
  @{ML_ind term_env in Envir} and @{ML_ind type_env in Envir}, which extract
  from an environment the corresponding variable mappings for schematic type 
  and term variables. These mappings can be turned into proper 
  @{ML_type ctyp}-pairs with the function
\<close>

ML %grayML\<open>fun prep_trm ctxt (x, (T, t)) = 
  ((x, T), Thm.cterm_of ctxt t)\<close> 

text \<open>
  and into proper @{ML_type cterm}-pairs with
\<close>

ML %grayML\<open>fun prep_ty ctxt (x, (S, ty)) = 
  ((x, S), Thm.ctyp_of ctxt ty)\<close>

text \<open>
  We can now calculate the instantiations from the matching function. 
\<close>

ML %linenosgray\<open>fun matcher_inst ctxt pat trm i = 
let
  val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)] 
  val env = nth (Seq.list_of univ) i
  val tenv = Vartab.dest (Envir.term_env env)
  val tyenv = Vartab.dest (Envir.type_env env)
in
  (map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv)
end\<close>

ML \<open>Context.get_generic_context\<close>
text \<open>
  In Line 3 we obtain the higher-order matcher. We assume there is a finite
  number of them and select the one we are interested in via the parameter 
  \<open>i\<close> in the next line. In Lines 5 and 6 we destruct the resulting 
  environments using the function @{ML_ind dest in Vartab}. Finally, we need 
  to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective 
  environments (Line 8). As a simple example we instantiate the
  @{thm [source] spec} rule so that its conclusion is of the form 
  @{term "Q True"}. 
 

  @{ML_response [gray,display,linenos] 
  \<open>let  
  val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
  val trm = @{term "Trueprop (Q True)"}
  val inst = matcher_inst @{context} pat trm 1
in
  Drule.instantiate_normalize inst @{thm spec}
end\<close>
  \<open>\<forall>x. Q x \<Longrightarrow> Q True\<close>}

  Note that we had to insert a \<open>Trueprop\<close>-coercion in Line 3 since the 
  conclusion of @{thm [source] spec} contains one.
 
  \begin{readmore}
  Unification and matching of higher-order patterns is implemented in 
  @{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher
  for terms. Full higher-order unification is implemented
  in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented
  in @{ML_file "Pure/General/seq.ML"}.
  \end{readmore}
\<close>

section \<open>Sorts (TBD)\label{sec:sorts}\<close>

text \<open>
  Type classes are formal names in the type system which are linked to
  predicates of one type variable (via the axclass mechanism) and thereby
  express extra properties on types, to be propagated by the type system.
  The type-in-class judgement is defined
  via a simple logic over types, with inferences solely based on
  modus ponens, instantiation and axiom use.
  The declared axioms of this logic are called an order-sorted algebra (see Schmidt-Schauss).
  It consists of an acyclic subclass relation and a set of image containment
  declarations for type constructors, called arities.

  A well-behaved high-level view on type classes has long been established
  (cite Haftmann-Wenzel): the predicate behind a type class is the foundation
  of a locale (for context-management reasons)
  and may use so-called type class parameters. These are type-indexed constants
  dependent on the sole type variable and are implemented via overloading.
  Overloading a constant means specifying its value on a type based on
  a well-founded reduction towards other values of constants on types.
  When instantiating type classes
  (i.e.\ proving arities) you are specifying overloading via primitive recursion.

  Sorts are finite intersections of type classes and are implemented as lists
  of type class names. The empty intersection, i.e.\ the empty list, is therefore
  inhabited by all types and is called the topsort.

  Free and schematic type variables are always annotated with sorts, thereby restricting
  the domain of types they quantify over and corresponding to an implicit hypothesis
  about the type variable.
\<close>


ML \<open>Sign.classes_of @{theory}\<close>

ML \<open>Sign.of_sort @{theory}\<close>

text \<open>
  \begin{readmore}
  Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
  
  @{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts,
    manages the order sorted algebra and offers an interface for reinterpreting
    derivations of type in class judgements
  @{ML_file "Pure/defs.ML"} manages the constant dependency graph and keeps it well-founded
    (its define function doesn't terminate for complex non-well-founded dependencies)
  @{ML_file "Pure/axclass.ML"} manages the theorems that back up subclass and arity relations
    and provides basic infrastructure for establishing the high-level view on type classes
  @{ML_file "Pure/sign.ML"} is a common interface to all the type-theory-like declarations
    (especially names, constants, paths, type classes) a
    theory acquires by theory extension mechanisms and manages associated certification
    functionality.
    It also provides the most needed functionality from individual underlying modules.
  \end{readmore}
\<close>


section \<open>Type-Checking\label{sec:typechecking}\<close>

text \<open>
  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 in Term} returns the 
  type of a term. Consider for example:

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

  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 [display,gray] 
  \<open>type_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::int"})\<close> 
  \<open>exception TYPE raised \<dots>\<close>}

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

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

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

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

  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 in Term} and then let type-inference figure out the 
  complete type. The type inference can be invoked with the function
  @{ML_ind check_term in Syntax}. An example is as follows:

  @{ML_response [display,gray] 
\<open>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\<close>
\<open>Const ("Groups.plus_class.plus", "nat \<Rightarrow> nat \<Rightarrow> nat") $
  Const ("Groups.one_class.one", "nat") $ Free ("x", "nat")\<close>}

  Instead of giving explicitly the type for the constant \<open>plus\<close> and the free 
  variable \<open>x\<close>, 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}


  \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 Appendix \ref{ch:solutions} when they receive an 
  ill-typed term as input.
  \end{exercise}
\<close>

section \<open>Certified Terms and Certified Types\<close>

text \<open>
  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 in Thm}, 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''.

  Certification is always relative to a context. For example you can 
  write:

  @{ML_response [display,gray] 
  \<open>Thm.cterm_of @{context} @{term "(a::nat) + b = c"}\<close> 
  \<open>a + b = c\<close>}

  This can also be written with an antiquotation:

  @{ML_response [display,gray] 
  \<open>@{cterm "(a::nat) + b = c"}\<close> 
  \<open>a + b = c\<close>}

  Attempting to obtain the certified term for

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

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

@{ML_response [display,gray] 
\<open>let
  val natT = @{typ "nat"}
  val zero = @{term "0::nat"}
  val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
in
  Thm.cterm_of @{context} (plus $ zero $ zero)
end\<close> 
  \<open>0 + 0\<close>}

  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 [display,gray]
  \<open>Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})\<close>
  \<open>nat \<Rightarrow> bool\<close>}

  or with the antiquotation:

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

  Since certified terms are, unlike terms, abstract objects, we cannot
  pattern-match against them. However, we can construct them. For example
  the function @{ML_ind apply in Thm} produces a certified application.

  @{ML_response [display,gray]
  \<open>Thm.apply @{cterm "P::nat \<Rightarrow> bool"} @{cterm "3::nat"}\<close>
  \<open>P 3\<close>}

  Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_structure Drule}
  applies a list of @{ML_type cterm}s.

  @{ML_response [display,gray]
  \<open>let
  val chead = @{cterm "P::unit \<Rightarrow> nat \<Rightarrow> bool"}
  val cargs = [@{cterm "()"}, @{cterm "3::nat"}]
in
  Drule.list_comb (chead, cargs)
end\<close>
  \<open>P () 3\<close>}

  \begin{readmore}
  For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
  the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and
  @{ML_file "Pure/drule.ML"}.
  \end{readmore}
\<close>

section \<open>Theorems\label{sec:theorems}\<close>

text \<open>
  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.


  To see theorems in ``action'', let us give a proof on the ML-level for the following 
  statement:
\<close>

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

text \<open>
  The corresponding ML-code is as follows:
\<close>

ML %linenosgray\<open>val my_thm = 
let
  val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
  val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}

  val Pt_implies_Qt = 
    Thm.assume assm1
    |> Thm.forall_elim @{cterm "t::nat"}
  
  val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
in
  Qt 
  |> Thm.implies_intr assm2
  |> Thm.implies_intr assm1
end\<close>

text \<open>
  Note that in Line 3 and 4 we use the antiquotation \<open>@{cprop \<dots>}\<close>, which
  inserts necessary \<open>Trueprop\<close>s.

  If we print out the value of @{ML my_thm} then we see only the 
  final statement of the theorem.

  @{ML_response [display, gray]
  \<open>pwriteln (pretty_thm @{context} my_thm)\<close>
  \<open>\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t\<close>}

  However, internally the code-snippet constructs the following 
  proof.

  \[
  \infer[(\<open>\<Longrightarrow>\<close>$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
    {\infer[(\<open>\<Longrightarrow>\<close>$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
       {\infer[(\<open>\<Longrightarrow>\<close>$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
          {\infer[(\<open>\<And>\<close>$-$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"}}{}
          }
       }
    }
  \]

  While we obtained a theorem as result, this theorem is not
  yet stored in Isabelle's theorem database. Consequently, it cannot be 
  referenced on the user level. One way to store it in the theorem database is
  by using the function @{ML_ind note in Local_Theory} from the structure 
  @{ML_structure Local_Theory} (the Isabelle command
  \isacommand{local\_setup} will be explained in more detail in 
  Section~\ref{sec:local}).
\<close>

(*FIXME: add forward reference to Proof_Context.export *)
ML %linenosgray\<open>val my_thm_vars =
let
  val ctxt0 = @{context}
  val (_, ctxt1) = Variable.add_fixes ["P", "Q", "t"] ctxt0
in
  singleton (Proof_Context.export ctxt1 ctxt0) my_thm
end\<close>

local_setup %gray \<open>
  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd\<close>


text \<open>
  The third argument of @{ML note in Local_Theory} is the list of theorems we
  want to store under a name. We can store more than one under a single name. 
  The first argument of @{ML note in Local_Theory} is the name under
  which we store the theorem or theorems. The second argument can contain a
  list of theorem attributes, which we will explain in detail in
  Section~\ref{sec:attributes}. Below we just use one such attribute,
  @{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset:
\<close>

local_setup %gray \<open>
  Local_Theory.note ((@{binding "my_thm_simp"}, 
       [Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd\<close>

text \<open>
  Note that we have to use another name under which the theorem is stored,
  since Isabelle does not allow us to call  @{ML_ind note in Local_Theory} twice
  with the same name. The attribute needs to be wrapped inside the function @{ML_ind
  internal in Attrib} from the structure @{ML_structure Attrib}. If we use the function 
  @{ML get_thm_names_from_ss} from
  the previous chapter, we can check whether the theorem has actually been
  added.


  @{ML_matchresult [display,gray]
  \<open>let
  fun pred s = match_string "my_thm_simp" s
in
  exists pred (get_thm_names_from_ss @{context})
end\<close>
  \<open>true\<close>}

  The main point of storing the theorems @{thm [source] my_thm} and @{thm
  [source] my_thm_simp} is that they can now also be referenced with the
  \isacommand{thm}-command on the user-level of Isabelle

    
  \begin{isabelle}
  \isacommand{thm}~\<open>my_thm my_thm_simp\<close>\isanewline
  \<open>>\<close>~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
  \<open>>\<close>~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
  \end{isabelle}

  or with the \<open>@{thm \<dots>}\<close>-antiquotation on the ML-level. Otherwise the 
  user has no access to these theorems. 

  Recall that Isabelle does not let you call @{ML note in Local_Theory} twice
  with the same theorem name. In effect, once a theorem is stored under a name, 
  this association is fixed. While this is a ``safety-net'' to make sure a
  theorem name refers to a particular theorem or collection of theorems, it is 
  also a bit too restrictive in cases where a theorem name should refer to a 
  dynamically expanding list of theorems (like a simpset). Therefore Isabelle 
  also implements a mechanism where a theorem name can refer to a custom theorem 
  list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}. 
  To see how it works let us assume we defined our own theorem list \<open>MyThmList\<close>.
\<close>

ML %grayML\<open>structure MyThmList = Generic_Data
  (type T = thm list
   val empty = []
   val extend = I
   val merge = merge Thm.eq_thm_prop)

fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))\<close>

text \<open>
  The function @{ML update} allows us to update the theorem list, for example
  by adding the theorem @{thm [source] TrueI}.
\<close>

setup %gray \<open>update @{thm TrueI}\<close>
 
text \<open>
  We can now install the theorem list so that it is visible to the user and 
  can be refered to by a theorem name. For this need to call 
  @{ML_ind add_thms_dynamic in Global_Theory}
\<close>

setup %gray \<open>
  Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) 
\<close>

text \<open>
  with a name and a function that accesses the theorem list. Now if the
  user issues the command

  \begin{isabelle}
  \isacommand{thm}~\<open>mythmlist\<close>\\
  \<open>> True\<close>
  \end{isabelle}

  the current content of the theorem list is displayed. If more theorems are stored in 
  the list, say
\<close>

setup %gray \<open>update @{thm FalseE}\<close>

text \<open>
  then the same command produces
  
  \begin{isabelle}
  \isacommand{thm}~\<open>mythmlist\<close>\\
  \<open>> False \<Longrightarrow> ?P\<close>\\
  \<open>> True\<close>
  \end{isabelle}

  Note that if we add the theorem @{thm [source] FalseE} again to the list
\<close>

setup %gray \<open>update @{thm FalseE}\<close>

text \<open>
  we still obtain the same list. The reason is that we used the function @{ML_ind
  add_thm in Thm} in our update function. This is a dedicated function which
  tests whether the theorem is already in the list.  This test is done
  according to alpha-equivalence of the proposition of the theorem. The
  corresponding testing function is @{ML_ind eq_thm_prop in Thm}.
  Suppose you proved the following three theorems.
\<close>

lemma
  shows thm1: "\<forall>x. P x" 
  and   thm2: "\<forall>y. P y" 
  and   thm3: "\<forall>y. Q y" sorry

text \<open>
  Testing them for alpha equality produces:

  @{ML_matchresult [display,gray]
\<open>(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
 Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))\<close>
\<open>(true, false)\<close>}

  Many functions destruct theorems into @{ML_type cterm}s. For example
  the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return 
  the left and right-hand side, respectively, of a meta-equality.

  @{ML_response [display,gray]
  \<open>let
  val eq = @{thm True_def}
in
  (Thm.lhs_of eq, Thm.rhs_of eq) 
  |> apply2 (YXML.content_of o Pretty.string_of o (pretty_cterm @{context}))
end\<close>
  \<open>("True", "(\<lambda>x. x) = (\<lambda>x. x)")\<close>}

  Other function produce terms that can be pattern-matched. 
  Suppose the following two theorems.
\<close>

lemma  
  shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C" 
  and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry

text \<open>
  We can destruct them into premises and conclusions as follows. 

 @{ML_matchresult_fake [display,gray]
\<open>let
  val ctxt = @{context}
  fun prems_and_concl thm =
     [[Pretty.str "Premises:", pretty_terms ctxt (Thm.prems_of thm)], 
      [Pretty.str "Conclusion:", pretty_term ctxt (Thm.concl_of thm)]]
     |> map Pretty.block
     |> Pretty.chunks
     |> pwriteln
in
  prems_and_concl @{thm foo_test1};
  prems_and_concl @{thm foo_test2}
end\<close>
\<open>Premises: ?A, ?B
Conclusion: ?C
Premises: 
Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C\<close>}

  Note that in the second case, there is no premise. The reason is that \<open>\<Longrightarrow>\<close>
  separates premises and conclusion, while \<open>\<longrightarrow>\<close> is the object implication
  from HOL, which just constructs a formula.

  \begin{readmore}
  The basic functions for theorems are defined in
  @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
  \end{readmore}

  Although we will explain the simplifier in more detail as tactic in 
  Section~\ref{sec:simplifier}, the simplifier 
  can be used to work directly over theorems, for example to unfold definitions. To show
  this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then 
  unfold the constant @{term "True"} according to its definition (Line 2).

  @{ML_response [display,gray,linenos]
  \<open>Thm.reflexive @{cterm "True"}
  |> Simplifier.rewrite_rule @{context} [@{thm True_def}]
  |> pretty_thm @{context}
  |> pwriteln\<close>
  \<open>(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)\<close>}

  Often it is necessary to transform theorems to and from the object 
  logic, that is replacing all \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close> by \<open>\<Longrightarrow>\<close> 
  and \<open>\<And>\<close>, or the other way around.  A reason for such a transformation 
  might be stating a definition. The reason is that definitions can only be 
  stated using object logic connectives, while theorems using the connectives 
  from the meta logic are more convenient for reasoning. Therefore there are
  some build in functions which help with these transformations. The function 
  @{ML_ind rulify in Object_Logic} 
  replaces all object connectives by equivalents in the meta logic. For example

  @{ML_response [display, gray]
  \<open>Object_Logic.rulify @{context} @{thm foo_test2}\<close>
  \<open>\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C\<close>}

  The transformation in the other direction can be achieved with function
  @{ML_ind atomize in Object_Logic} and the following code.

  @{ML_response [display,gray]
  \<open>let
  val thm = @{thm foo_test1}
  val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
in
  Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
end\<close>
  \<open>?A \<longrightarrow> ?B \<longrightarrow> ?C\<close>}

  In this code the function @{ML atomize in Object_Logic} produces 
  a meta-equation between the given theorem and the theorem transformed
  into the object logic. The result is the theorem with object logic 
  connectives. However, in order to completely transform a theorem
  involving meta variables, such as @{thm [source] list.induct}, which 
  is of the form 

  @{thm [display] list.induct}

  we have to first abstract over the meta variables \<open>?P\<close> and 
  \<open>?list\<close>. For this we can use the function 
  @{ML_ind forall_intr_vars in Drule}. This allows us to implement the
  following function for atomizing a theorem.
\<close>

ML %grayML\<open>fun atomize_thm ctxt thm =
let
  val thm' = forall_intr_vars thm
  val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
in
  Raw_Simplifier.rewrite_rule ctxt [thm''] thm'
end\<close>

text \<open>
  This function produces for the theorem @{thm [source] list.induct}

  @{ML_response [display, gray]
  \<open>atomize_thm @{context} @{thm list.induct}\<close>
  \<open>"\<forall>P list. P [] \<longrightarrow> (\<forall>x1 x2. P x2 \<longrightarrow> P (x1 # x2)) \<longrightarrow> P list"\<close>}

  Theorems can also be produced from terms by giving an explicit proof. 
  One way to achieve this is by using the function @{ML_ind prove in Goal}
  in the structure @{ML_structure Goal}. For example below we use this function
  to prove the term @{term "P \<Longrightarrow> P"}.
  
  @{ML_response [display,gray]
  \<open>let
  val trm = @{term "P \<Longrightarrow> P::bool"}
  val tac = K (assume_tac @{context} 1)
in
  Goal.prove @{context} ["P"] [] trm tac
end\<close>
  \<open>?P \<Longrightarrow> ?P\<close>}

  This function takes first a context and second a list of strings. This list
  specifies which variables should be turned into schematic variables once the term
  is proved (in this case only \<open>"P"\<close>).  The fourth argument is the term to be 
  proved. The fifth is a corresponding proof given in form of a tactic (we explain 
  tactics in Chapter~\ref{chp:tactical}). In the code above, the tactic proves the 
  theorem by assumption. 

  There is also the possibility of proving multiple goals at the same time
  using the function @{ML_ind prove_common in Goal}. For this let us define the
  following three helper functions.
\<close>

ML %grayML\<open>fun rep_goals i = replicate i @{prop "f x = f x"}
fun rep_tacs ctxt i = replicate i (resolve_tac ctxt [@{thm refl}])

fun multi_test ctxt i =
  Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i) 
    (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs ctxt i)) 1))\<close>

text \<open>
  With them we can now produce three theorem instances of the 
  proposition.

  @{ML_response [display, gray]
  \<open>multi_test @{context} 3\<close>
  \<open>["?f ?x = ?f ?x", "?f ?x = ?f ?x", "?f ?x = ?f ?x"]\<close>}

  However you should be careful with @{ML prove_common in Goal} and very
  large goals. If you increase the counter in the code above to \<open>3000\<close>, 
  you will notice that takes approximately ten(!) times longer than
  using @{ML map} and @{ML prove in Goal}.
\<close>
  
ML %grayML\<open>let 
  fun test_prove ctxt thm =
    Goal.prove ctxt ["P", "x"] [] thm (K (resolve_tac  @{context} [@{thm refl}] 1))
in
  map (test_prove @{context}) (rep_goals 3000)
end\<close>

text \<open>
  While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
  is the function @{ML_ind make_thm in Skip_Proof} in the structure 
  @{ML_structure Skip_Proof} that allows us to turn any proposition into a theorem.
  Potentially making the system unsound.  This is sometimes useful for developing 
  purposes, or when explicit proof construction should be omitted due to performace 
  reasons. An example of this function is as follows:

  @{ML_response [display, gray]
  \<open>Skip_Proof.make_thm @{theory} @{prop "True = False"}\<close>
  \<open>True = False\<close>}

  \begin{readmore}
  Functions that setup goal states and prove theorems are implemented in 
  @{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to
  skip proofs of theorems are implemented in @{ML_file "Pure/skip_proof.ML"}.
  \end{readmore}

  Theorems also contain auxiliary data, such as the name of the theorem, its
  kind, the names for cases and so on. This data is stored in a string-string
  list and can be retrieved with the function @{ML_ind get_tags in
  Thm}. Assume you prove the following lemma.
\<close>

theorem foo_data: 
  shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption

text \<open>
  The auxiliary data of this lemma can be retrieved using the function 
  @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is 

  @{ML_matchresult [display,gray]
  \<open>Thm.get_tags @{thm foo_data}\<close>
  \<open>[("name", "Essential.foo_data"), ("kind", "theorem")]\<close>}

  consisting of a name and a kind.  When we store lemmas in the theorem database, 
  we might want to explicitly extend this data by attaching case names to the 
  two premises of the lemma.  This can be done with the function @{ML_ind name in Rule_Cases}
  from the structure @{ML_structure Rule_Cases}.
\<close>

local_setup %gray \<open>
  Local_Theory.note ((@{binding "foo_data'"}, []), 
    [(Rule_Cases.name ["foo_case_one", "foo_case_two"] 
       @{thm foo_data})]) #> snd\<close>

text \<open>
  The data of the theorem @{thm [source] foo_data'} is then as follows:

  @{ML_matchresult [display,gray]
  \<open>Thm.get_tags @{thm foo_data'}\<close>
  \<open>[("name", "Essential.foo_data'"), 
 ("case_names", "foo_case_one;foo_case_two"), ("kind", "theorem")]\<close>}

  You can observe the case names of this lemma on the user level when using 
  the proof methods \<open>cases\<close> and \<open>induct\<close>. In the proof below
\<close>

lemma
shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
proof (cases rule: foo_data')

(*<*)oops(*>*)
text_raw\<open>
\begin{tabular}{@ {}l}
\isacommand{print\_cases}\\
\<open>> cases:\<close>\\
\<open>>   foo_case_one:\<close>\\
\<open>>     let "?case" = "?P"\<close>\\
\<open>>   foo_case_two:\<close>\\
\<open>>     let "?case" = "?P"\<close>
\end{tabular}\<close>

text \<open>
  we can proceed by analysing the cases \<open>foo_case_one\<close> and 
  \<open>foo_case_two\<close>. While if the theorem has no names, then
  the cases have standard names \<open>1\<close>, \<open>2\<close> and so 
  on. This can be seen in the proof below.
\<close>

lemma
shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
proof (cases rule: foo_data)

(*<*)oops(*>*)
text_raw\<open>
\begin{tabular}{@ {}l}
\isacommand{print\_cases}\\
\<open>> cases:\<close>\\
\<open>>   1:\<close>\\
\<open>>     let "?case" = "?P"\<close>\\
\<open>>   2:\<close>\\
\<open>>     let "?case" = "?P"\<close>
\end{tabular}\<close>

 
text \<open>
  Sometimes one wants to know the theorems that are involved in
  proving a theorem, especially when the proof is by \<open>auto\<close>. These theorems can be obtained by introspecting the proved theorem.
  To introspect a theorem, let us define the following three functions
  that analyse the @{ML_type_ind proof_body} data-structure from the
  structure @{ML_structure Proofterm}.
\<close>

ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms 
val get_names = (map Proofterm.thm_node_name) o pthms_of 
val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of
fun get_all_names thm =
let
  (*proof body with digest*)
  val body = Proofterm.strip_thm (Thm.proof_body_of thm);
  (*all theorems used in the graph of nested proofs*)
in Proofterm.fold_body_thms
     (fn {name, ...} => insert (op =) name) [body] []
end\<close>

text \<open>
  To see what their purpose is, consider the following three short proofs.
\<close>
ML \<open>

\<close>
lemma my_conjIa:
shows "A \<and> B \<Longrightarrow> A \<and> B"
apply(rule conjI)
apply(drule conjunct1)
apply(assumption)
apply(drule conjunct2)
apply(assumption)
done

lemma my_conjIb:
shows "A \<and> B \<Longrightarrow> A \<and> B"
apply(assumption)
done

lemma my_conjIc:
shows "A \<and> B \<Longrightarrow> A \<and> B"
apply(auto)
done

ML "Proofterm.proofs"
ML \<open>@{thm my_conjIa}
  |> get_all_names\<close>
text \<open>
  While the information about which theorems are used is obvious in
  the first two proofs, it is not obvious in the third, because of the
  \<open>auto\<close>-step.  Fortunately, ``behind'' every proved theorem is
  a proof-tree that records all theorems that are employed for
  establishing this theorem.  We can traverse this proof-tree
  extracting this information.  Let us first extract the name of the
  established theorem. This can be done with

  @{ML_matchresult [display,gray]
  \<open>@{thm my_conjIa}
  |> Thm.proof_body_of
  |> get_names\<close>
  \<open>["Essential.my_conjIa"]\<close>}

  whereby \<open>Essential\<close> refers to the theory name in which
  we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
  proof_body_of in Thm} returns a part of the data that is stored in a
  theorem.  Notice that the first proof above references
  three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 
  and @{thm [source] conjunct2}. We can obtain them by descending into the
  proof-tree. The function @{ML get_all_names} recursively selects all names.

  @{ML_response [display,gray]
  \<open>@{thm my_conjIa}
  |> get_all_names |> sort string_ord\<close>
  \<open>["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", "HOL.True_def", 
   "HOL.True_or_False", "HOL.allI", "HOL.and_def", "HOL.conjI",
   "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", "HOL.eqTrueE", "HOL.eqTrueI", 
   "HOL.ext", "HOL.fun_cong", "HOL.iffD1", "HOL.iffD2", "HOL.iffI",
   "HOL.impI", "HOL.mp", "HOL.or_def", "HOL.refl", "HOL.rev_iffD1", 
   "HOL.rev_iffD2", "HOL.spec", "HOL.ssubst", "HOL.subst", "HOL.sym",
   "Pure.protectD", "Pure.protectI"]\<close>}

  The theorems @{thm [source] Pure.protectD} and @{thm [source]
  Pure.protectI} that are internal theorems are always part of a
  proof in Isabelle. The other theorems are the theorems used in the proofs of the theorems
  @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. 

  Note also that applications of \<open>assumption\<close> do not
  count as a separate theorem, as you can see in the following code.

  @{ML_response [display,gray]
  \<open>@{thm my_conjIb}
  |> get_all_names |> sort string_ord\<close>
  \<open>[ "Pure.protectD", "Pure.protectI"]\<close>}


  Interestingly, but not surprisingly, the proof of @{thm [source]
  my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
  and @{thm [source] my_conjIb}, as can be seen by the theorems that
  are returned for @{thm [source] my_conjIc}.
 
  @{ML_response [display,gray]
  \<open>@{thm my_conjIc}
  |> get_all_names\<close>
  \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", "Pure.conjunctionI", 
    "HOL.rev_mp", "HOL.exI", "HOL.allE", "HOL.exE",\<dots>]\<close>}


  \begin{exercise}
  Have a look at the theorems that are used when a lemma is ``proved''
  by \isacommand{sorry}? 
  \end{exercise}

  \begin{readmore} 
  The data-structure @{ML_type proof_body} is implemented
  in the file @{ML_file "Pure/proofterm.ML"}. The implementation 
  of theorems and related functions are in @{ML_file "Pure/thm.ML"}.  
  \end{readmore}

  One great feature of Isabelle is its document preparation system, where
  proved theorems can be quoted in documents referencing directly their
  formalisation. This helps tremendously to minimise cut-and-paste errors. However,
  sometimes the verbatim quoting is not what is wanted or what can be shown to
  readers. For such situations Isabelle allows the installation of \emph{\index*{theorem 
  styles}}. These are, roughly speaking, functions from terms to terms. The input 
  term stands for the theorem to be presented; the output can be constructed to
  ones wishes.  Let us, for example, assume we want to quote theorems without
  leading \<open>\<forall>\<close>-quantifiers. For this we can implement the following function 
  that strips off \<open>\<forall>\<close>s.
\<close>

ML %linenosgray\<open>fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
      Term.dest_abs body |> snd |> strip_allq
  | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = 
      strip_allq t
  | strip_allq t = t\<close>

text \<open>
  We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions,
  since this function deals correctly with potential name clashes. This function produces
  a pair consisting of the variable and the body of the abstraction. We are only interested
  in the body, which we feed into the recursive call. In Line 3 and 4, we also
  have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 
  install this function as the theorem style named \<open>my_strip_allq\<close>. 
\<close>

setup %gray\<open>
  Term_Style.setup @{binding "my_strip_allq"} (Scan.succeed (K strip_allq)) 
\<close>

text \<open>
  We can test this theorem style with the following theorem
\<close>

theorem style_test:
shows "\<forall>x y z. (x, x) = (y, z)" sorry

text \<open>
  Now printing out in a document the theorem @{thm [source] style_test} normally
  using \<open>@{thm \<dots>}\<close> produces

  \begin{isabelle}
  \begin{graybox}
  \<open>@{thm style_test}\<close>\\
  \<open>>\<close>~@{thm style_test}
  \end{graybox}
  \end{isabelle}

  as expected. But with the theorem style \<open>@{thm (my_strip_allq) \<dots>}\<close> 
  we obtain

  \begin{isabelle}
  \begin{graybox}
  \<open>@{thm (my_strip_allq) style_test}\<close>\\
  \<open>>\<close>~@{thm (my_strip_allq) style_test}
  \end{graybox}
  \end{isabelle}
  
  without the leading quantifiers. We can improve this theorem style by explicitly 
  giving a list of strings that should be used for the replacement of the
  variables. For this we implement the function which takes a list of strings
  and uses them as name in the outermost abstractions.
\<close>

ML %grayML\<open>fun rename_allq [] t = t
  | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
      Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
  | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
      rename_allq xs t
  | rename_allq _ t = t\<close>

text \<open>
  We can now install a the modified theorem style as follows
\<close>

setup %gray \<open>let
  val parser = Scan.repeat Args.name
  fun action xs = K (rename_allq xs #> strip_allq)
in
  Term_Style.setup @{binding "my_strip_allq2"} (parser >> action)
end\<close>

text \<open>
  The parser reads a list of names. In the function \<open>action\<close> we first
  call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}
  on the resulting term. We can now suggest, for example, two variables for
  stripping off the first two \<open>\<forall>\<close>-quantifiers.

  \begin{isabelle}
  \begin{graybox}
  \<open>@{thm (my_strip_allq2 x' x'') style_test}\<close>\\
  \<open>>\<close>~@{thm (my_strip_allq2 x' x'') style_test}
  \end{graybox}
  \end{isabelle}

  Such styles allow one to print out theorems in documents formatted to 
  ones heart content. The styles can also be used in the document 
  antiquotations \<open>@{prop ...}\<close>, \<open>@{term_type ...}\<close>
  and \<open>@{typeof ...}\<close>.

  Next we explain theorem attributes, which is another
  mechanism for dealing with theorems.

  \begin{readmore}
  Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}.
  \end{readmore}
\<close>

section \<open>Theorem Attributes\label{sec:attributes}\<close>

text \<open>
  Theorem attributes are \<open>[symmetric]\<close>, \<open>[THEN \<dots>]\<close>, \<open>[simp]\<close> and so on. Such attributes are \emph{neither} tags \emph{nor} flags
  annotated to theorems, but functions that do further processing of 
  theorems. 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}\\
  \<open>> COMP:  direct composition with rules (no lifting)\<close>\\
  \<open>> HOL.dest:  declaration of Classical destruction rule\<close>\\
  \<open>> HOL.elim:  declaration of Classical elimination rule\<close>\\
  \<open>> \<dots>\<close>
  \end{isabelle}
  
  The theorem attributes fall roughly into two categories: the first category manipulates
  theorems (for example \<open>[symmetric]\<close> and \<open>[THEN \<dots>]\<close>), and the second
  stores theorems somewhere as data (for example \<open>[simp]\<close>, which adds
  theorems to the current simpset).

  To explain how to write your own attribute, let us start with an extremely simple 
  version of the attribute \<open>[symmetric]\<close>. The purpose of this attribute is
  to produce the ``symmetric'' version of an equation. The main function behind 
  this attribute is
\<close>

ML %grayML\<open>val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})\<close>

text \<open>
  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 (\<open>thm\<close>), and 
  returns another theorem (namely \<open>thm\<close> resolved with the theorem 
  @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind RS in Drule} 
  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:
\<close>

attribute_setup %gray my_sym = 
  \<open>Scan.succeed my_symmetric\<close> "applying the sym rule"

text \<open>
  Inside the \<open>\<verbopen> \<dots> \<verbclose>\<close>, we have to specify a parser
  for the theorem attribute. Since the attribute does not expect any further 
  arguments (unlike \<open>[THEN \<dots>]\<close>, for instance), we use the parser @{ML
  Scan.succeed}. An example for the attribute \<open>[my_sym]\<close> is the proof
\<close> 

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

text \<open>
  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}~\<open>test\<close>\\
  \<open>> \<close>~@{thm test}
  \end{isabelle}

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

  \begin{isabelle}
  \isacommand{thm}~\<open>test[my_sym]\<close>\\
  \<open>> \<close>~@{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:
\<close>

ML %grayML\<open>Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
  "applying the sym rule"\<close>

text \<open>
  This gives a function from @{ML_type "theory -> theory"}, which
  can be used for example with \isacommand{setup} or with
  @{ML \<open>Context.>> o Context.map_theory\<close>}.\footnote{\bf FIXME: explain what happens here.}

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

ML %grayML\<open>fun MY_THEN thms = 
let
  fun RS_rev thm1 thm2 = thm2 RS thm1
in
  Thm.rule_attribute [] (fn _ => fn thm => fold RS_rev thms thm)
end\<close>

text \<open>
  where for convenience we define the reverse and curried version of @{ML RS}. 
  The setup of this theorem attribute uses the parser @{ML thms in Attrib}, 
  which parses a list of theorems. 
\<close>

attribute_setup %gray MY_THEN = \<open>Attrib.thms >> MY_THEN\<close> 
  "resolving the list of theorems with the theorem"

text \<open>
  You can, for example, use this theorem attribute to turn an equation into a 
  meta-equation:

  \begin{isabelle}
  \isacommand{thm}~\<open>test[MY_THEN eq_reflection]\<close>\\
  \<open>> \<close>~@{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}~\<open>test[MY_THEN sym eq_reflection]\<close>\\
  \<open>> \<close>~@{thm test[MY_THEN sym eq_reflection]}
  \end{isabelle}

  It is also possible to combine different theorem attributes, as in:
  
  \begin{isabelle}
  \isacommand{thm}~\<open>test[my_sym, MY_THEN eq_reflection]\<close>\\
  \<open>> \<close>~@{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 commute in general. If you try

  \begin{isabelle}
  \isacommand{thm}~\<open>test[MY_THEN eq_reflection, my_sym]\<close>\\
  \<open>> \<close>~\<open>exception THM 1 raised: RSN: no unifiers\<close>
  \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 \<open>[simp]\<close> 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 theorem list.
\<close>

ML %grayML\<open>structure MyThms = Named_Thms
  (val name = @{binding "attr_thms"} 
   val description = "Theorems for an Attribute")\<close>

text \<open>
  We are going to modify this list by adding and deleting theorems.
  For this we use the two functions @{ML MyThms.add_thm} and
  @{ML MyThms.del_thm}. You can turn them into attributes 
  with the code
\<close>

ML %grayML\<open>val my_add = Thm.declaration_attribute MyThms.add_thm
val my_del = Thm.declaration_attribute MyThms.del_thm\<close>

text \<open>
  and set up the attributes as follows
\<close>

attribute_setup %gray my_thms = \<open>Attrib.add_del my_add my_del\<close> 
  "maintaining a list of my_thms" 

text \<open>
  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 \<open>[my_thms]\<close>
\<close>

lemma trueI_2[my_thms]: "True" by simp

text \<open>
  then you can see it is added to the initially empty list.

  @{ML_response [display,gray]
  \<open>MyThms.get @{context}\<close> 
  \<open>["True"]\<close>}

  You can also add theorems using the command \isacommand{declare}.
\<close>

declare test[my_thms] trueI_2[my_thms add]

text \<open>
  With this attribute, the \<open>add\<close> 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 [display,gray]
  \<open>MyThms.get @{context}\<close>
  \<open>["True", "Suc (Suc 0) = 2"]\<close>}

  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:
\<close>

declare test[my_thms del]

text \<open>After this, the theorem list is again: 

  @{ML_response [display,gray]
  \<open>MyThms.get @{context}\<close>
  \<open>["True"]\<close>}

  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.

  \footnote{\bf FIXME What are: \<open>theory_attributes\<close>, \<open>proof_attributes\<close>?}
  \footnote{\bf FIXME readmore}

  \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}
\<close>

section \<open>Pretty-Printing\label{sec:pretty}\<close>

text \<open>
  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. Most of its functions do not operate on @{ML_type string}s, but on
  instances of the pretty 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_matchresult_fake [display,gray]
  \<open>Pretty.str "test"\<close> \<open>String ("test", 4)\<close>}

  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:
\<close>

ML %grayML\<open>fun pprint prt = tracing (Pretty.string_of prt)\<close>
ML %invisible\<open>val pprint = YXML.content_of o Pretty.string_of\<close>
text \<open>
  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:
\<close>

ML %grayML\<open>fun rep n str = implode (replicate n str)\<close>

text \<open>
  and suppose we want to print out the string:
\<close>

ML %grayML\<open>val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "\<close>

text \<open>
  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_matchresult_fake [display,gray]
\<open>tracing test_str\<close>
\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
oooooooooooooobaaaaaaaaaaaar\<close>}

  We obtain the same if we just use the function @{ML pprint}.

@{ML_response [display,gray]
\<open>pprint (Pretty.str test_str)\<close>
\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
oooooooooooooobaaaaaaaaaaaar\<close>}

  However by using pretty types you have the ability to indicate possible
  linebreaks for example at each whitespace. 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 [display,gray]
\<open>let
  val ptrs = map Pretty.str (space_explode " " test_str)
in
  pprint (Pretty.blk (0, Pretty.breaks ptrs))
end\<close>
\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}

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

  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 [display,gray]
\<open>let
  val ptrs = map Pretty.str (space_explode " " test_str)
in
  pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))
end\<close>
\<open>          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}

  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 [display,gray]
\<open>let
  val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
in
  pprint (Pretty.blk (0, Pretty.commas ptrs))
end\<close>
\<open>99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
100016, 100017, 100018, 100019, 100020\<close>}

  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
\<close>

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

  As can be seen, this function prints out the ``set'' so that starting 
  from the second, each new line has 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

\<close>

ML %linenosgray\<open>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\<close>

text \<open>
  where Line 7 prints the beginning of the list and Line
  8 the last item. We have to use @{ML \<open>Pretty.brk 1\<close>} 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 [display,gray]
\<open>let
  val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
in
  pprint (Pretty.blk (0, and_list ptrs1))
end\<close>
\<open>1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
and 22\<close>}
@{ML_response [display,gray]
\<open>let
  val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
in
  pprint (Pretty.blk (0, and_list ptrs2))
end\<close>
\<open>10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
28\<close>}

  Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out 
  a list of items, but automatically inserts forced breaks between each item.
  Compare

  @{ML_response [display,gray]
  \<open>let
  val a_and_b = [Pretty.str "a", Pretty.str "b"]
in
  pprint (Pretty.blk (0, a_and_b))
end\<close>
\<open>ab\<close>}
 @{ML_response [display,gray]
  \<open>let
  val a_and_b = [Pretty.str "a", Pretty.str "b"]
in
  pprint (Pretty.chunks a_and_b)
end\<close>
\<open>a
b\<close>}

  The function @{ML_ind big_list in Pretty} helps with printing long lists.
  It is used for example in the command \isacommand{print\_theorems}. An
  example is as follows.

  @{ML_response [display,gray]
  \<open>let
  val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
in
  pprint (Pretty.big_list "header" pstrs)
end\<close>
  \<open>header
  4
  5
  6
  7
  8
  9
  10\<close>}

  The point of the pretty-printing functions is to conveninetly obtain 
  a lay-out of terms and types that is pleasing to the eye. If we print
  out the the terms produced by the the function @{ML de_bruijn} from 
  exercise~\ref{ex:debruijn} we obtain the following: 

  @{ML_response [display,gray]
  \<open>pprint (Syntax.pretty_term  @{context} (de_bruijn 4))\<close>
  \<open>(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
(P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
(P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and> 
(P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>
P 4 \<and> P 3 \<and> P 2 \<and> P 1\<close>}

  We use the function @{ML_ind pretty_term in Syntax} for pretty-printing
  terms. Next we like to pretty-print a term and its type. For this we use the
  function \<open>tell_type\<close>.
\<close>

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

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

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

  \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/PIDE/markup.ML"}
  \end{readmore}
\<close>

section \<open>Summary\<close>

text \<open>
  \begin{conventions}
  \begin{itemize}
  \item Start with a proper context and then pass it around 
  through all your functions.
  \end{itemize}
  \end{conventions}
\<close>

end