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+
−