isabelle-cookbook: ProgTutorial/General.thy@e73ccbed776e

theory General
imports Base FirstSteps
begin

(*<*)
setup{*
open_file_with_prelude 
  "General_Code.thy"
  ["theory General", "imports Base FirstSteps", "begin"]
*}
(*>*)


chapter {* Isabelle in More Detail *}

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


section {* Terms and Types *}

text {*
  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{@{text "@{term \<dots>}"}}. For example

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

  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: 
*}  

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

text {*
  This datatype implements Church-style lambda-terms, where types are
  explicitly recorded in variables, constants and abstractions.  As can be
  seen in Line 5, terms use the usual de Bruijn index mechanism for
  representing bound variables.  For example in

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*}

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

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

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

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

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

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

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

  There are a number of handy functions that are frequently used for
  constructing terms. One is the function @{ML_ind list_comb 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_fake [display,gray]
"let
  val trm = @{term \"P::nat\"}
  val args = [@{term \"True\"}, @{term \"False\"}]
in
  list_comb (trm, args)
end"
"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}

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

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

  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
  and an abstraction, 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 @{text "P"}, the variable @{text "x"} in @{text "P x"}
  is of the same type as the abstracted variable. If it is of different type,
  as in

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

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

  There is also the function @{ML_ind subst_free 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_fake [display,gray]
"let
  val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
  val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
  val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
in
  subst_free [sub1, sub2] trm
end"
  "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}

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

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

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

ML{*fun strip_alls t =
let 
  fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
in
  case t of
    Const ("All", _) $ Abs body => aux body
  | _ => ([], t)
end*}

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

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

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

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

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

  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 lose de Bruijn index is replaced by a unique free variable. For example


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

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

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

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

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

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

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

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

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

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

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

text {* 
  because now

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  \footnote{\bf FIXME: Explain the following better; maybe put in a separate
  section and link with the comment in the antiquotation section.}

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

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

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

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

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

*} 

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

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

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

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

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

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

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

text {*
  Here is an example:

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

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

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

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

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

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

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

  \begin{exercise}\label{fun:makesum}
  Write a function 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{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}
*}


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

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

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

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

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

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

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

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

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

  where no error is detected.

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

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

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

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

  \footnote{\bf FIXME: say something about sorts.}
  \footnote{\bf FIXME: give a ``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}
*}

section {* Certified Terms and Certified Types *}

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

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

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

  This can also be written with an antiquotation:

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

  Attempting to obtain the certified term for

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

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

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

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

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

  or with the antiquotation:

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

  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 capply in Thm} produces a certified application.

  @{ML_response_fake [display,gray]
  "Thm.capply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
  "P 3"}

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

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

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

section {* Theorems *}

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


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

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

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

ML{*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 = 
        assume assm1
        |> forall_elim @{cterm "t::nat"}
  
  val Qt = implies_elim Pt_implies_Qt (assume assm2)
in
  Qt 
  |> implies_intr assm2
  |> implies_intr assm1
end*}

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

  @{ML_response_fake [display, gray]
  "tracing (string_of_thm @{context} my_thm)"
  "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}

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

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

  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 LocalTheory}.\footnote{\bf FIXME: make sure a pointer
  to the section about local-setup is given earlier.}
*}

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

text {*
  The fourth argument of @{ML note in LocalTheory} is the list of theorems we
  want to store under a name.  The first argument @{ML_ind theoremK in Thm} is
  a kind indicator, which classifies the theorem. There are several such kind
  indicators: for a theorem arising from a definition you should use @{ML_ind
  definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, and for
  ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
  in Thm}.  The second argument of @{ML note in LocalTheory} is the name under
  which we store the theorem or theorems. The third 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 in order
  add the theorem to the simpset:
*}

local_setup %gray {*
  LocalTheory.note Thm.theoremK
    ((@{binding "my_thm_simp"}, 
       [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}

text {*
  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 LocalTheory} twice
  with the same name. The attribute needs to be wrapped inside the function @{ML_ind
  internal in Attrib} from the structure @{ML_struct 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_response [display,gray]
  "let
  fun pred s = match_string \"my_thm_simp\" s
in
  exists pred (get_thm_names_from_ss @{simpset})
end"
  "true"}

  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}~@{text "my_thm"}\isanewline
   @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
  \end{isabelle}

  or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen,
  the theorem does not have any meta-variables that would be present if we proved
  this theorem on the user-level. We will see later on that we have to 
  construct meta-variables in theorems explicitly.

  \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}}
*}

text {*
  There is a multitude of functions that manage or manipulate theorems in the 
  structures @{ML_struct Thm} and @{ML_struct Drule}. For example 
  we can test theorems for alpha equality. Suppose you proved the following three 
  theorems.
*}

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

text {*
  Testing them for alpha equality using the function @{ML_ind eq_thm in Thm} produces:

  @{ML_response [display,gray]
"(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
 Thm.eq_thm (@{thm thm2}, @{thm thm3}))"
"(true, false)"}

  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_fake [display,gray]
  "let
  val eq = @{thm True_def}
in
  (Thm.lhs_of eq, Thm.rhs_of eq) 
  |> pairself (string_of_cterm @{context})
end"
  "(True, (\<lambda>x. x) = (\<lambda>x. x))"}

  Other function produce terms that can be pattern-matched. 
  Suppose the following two theorems.
*}

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

text {*
  We can destruct them into premises and conclusions as follows. 

 @{ML_response_fake [display,gray]
"let
  val ctxt = @{context}
  fun prems_and_concl thm =
     [\"Premises: \"   ^ (string_of_terms ctxt (Thm.prems_of thm))] @ 
     [\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))]
     |> cat_lines
     |> tracing
in
  prems_and_concl @{thm foo_test1};
  prems_and_concl @{thm foo_test2}
end"
"Premises: ?A, ?B
Conclusion: ?C
Premises: 
Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}

  Note that in the second case, there is no premise.

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

  The simplifier can be used to unfold definition in theorems. 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_fake [display,gray,linenos]
  "Thm.reflexive @{cterm \"True\"}
  |> Simplifier.rewrite_rule [@{thm True_def}]
  |> string_of_thm @{context}
  |> tracing"
  "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}

  Often it is necessary to transform theorems to and from the object 
  logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"} 
  and @{text "\<And>"}, 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 ObjectLogic} 
  replaces all object connectives by equivalents in the meta logic. For example

  @{ML_response_fake [display, gray]
  "ObjectLogic.rulify @{thm foo_test2}"
  "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}

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

  @{ML_response_fake [display,gray]
  "let
  val thm = @{thm foo_test1}
  val meta_eq = ObjectLogic.atomize (cprop_of thm)
in
  MetaSimplifier.rewrite_rule [meta_eq] thm
end"
  "?A \<longrightarrow> ?B \<longrightarrow> ?C"}

  In this code the function @{ML atomize in ObjectLogic} 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 @{text "?P"} and 
  @{text "?list"}. 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.
*}

ML{*fun atomize_thm thm =
let
  val thm' = forall_intr_vars thm
  val thm'' = ObjectLogic.atomize (cprop_of thm')
in
  MetaSimplifier.rewrite_rule [thm''] thm'
end*}

text {*
  This function produces for the theorem @{thm [source] list.induct}

  @{ML_response_fake [display, gray]
  "atomize_thm @{thm list.induct}"
  "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}

  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_struct Goal}. For example below we use this function
  to prove the term @{term "P \<Longrightarrow> P"}.
  
  @{ML_response_fake [display,gray]
  "let
  val trm = @{term \"P \<Longrightarrow> P::bool\"}
  val tac = K (atac 1)
in
  Goal.prove @{context} [\"P\"] [] trm tac
end"
  "?P \<Longrightarrow> ?P"}

  This function takes first a context and second a list of strings. This list
  specifies which variables should be turned into meta-variables once the term
  is proved.  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. As before this code will produce a theorem, but the theorem
  is not yet stored in the theorem database. 

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

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

text {*
  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_response_fake [display,gray]
  "Thm.get_tags @{thm foo_data}"
  "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}

  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 RuleCases}
  from the structure @{ML_struct RuleCases}.
*}

local_setup %gray {*
  LocalTheory.note Thm.lemmaK
    ((@{binding "foo_data'"}, []), 
      [(RuleCases.name ["foo_case_one", "foo_case_two"] 
        @{thm foo_data})]) #> snd *}

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

  @{ML_response_fake [display,gray]
  "Thm.get_tags @{thm foo_data'}"
  "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), 
 (\"case_names\", \"foo_case_one;foo_case_two\")]"}

  You can observe the case names of this lemma on the user level when using 
  the proof methods @{ML_text cases} and @{ML_text induct}. In the proof below
*}

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

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

text {*
  we can proceed by analysing the cases @{text "foo_case_one"} and 
  @{text "foo_case_two"}. While if the theorem has no names, then
  the cases have standard names @{text 1}, @{text 2} and so 
  on. This can be seen in the proof below.
*}

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

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


text {*
  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{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 @{text \<forall>}-quantifiers. For this we can implement the following function 
  that strips off meta-quantifiers.
*}

ML %linenosgray {*fun strip_all_qnt (Const (@{const_name "All"}, _) $ Abs body) = 
      Term.dest_abs body |> snd |> strip_all_qnt
  | strip_all_qnt (Const (@{const_name "Trueprop"}, _) $ t) = 
      strip_all_qnt t
  | strip_all_qnt t = t*}

text {*
  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 @{text "my_strip_all_qnt"}. 
*}

setup %gray {*
  Term_Style.setup "my_strip_all_qnt" (Scan.succeed (K strip_all_qnt)) 
*}

text {*
  We can test this theorem style with the following theorem
*}

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

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

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

  as expected. But with the theorem style @{text "@{thm (my_strip_all_qnt) \<dots>}"} 
  we obtain

  \begin{isabelle}
  @{text "@{thm (my_strip_all_qnt) style_test}"}\\
  @{text ">"}~@{thm (my_strip_all_qnt) style_test}\\
  \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.
*}

ML {*fun rename_all [] t = t
  | rename_all (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
      Const (@{const_name "All"}, U) $ Abs (x, T, rename_all xs t)
  | rename_all xs (Const (@{const_name "Trueprop"}, U) $ t) =
      rename_all xs t
  | rename_all _ t = t*}

text {*
  We can now install a the modified theorem style as follows
*}

setup %gray {*
let
  val parser = Scan.repeat Args.name
  fun action xs = K (rename_all xs #> strip_all_qnt)
in
  Term_Style.setup "my_strip_all_qnt2" (parser >> action)
end *}

text {*
  We can now suggest, for example, two variables for stripping 
  off the @{text \<forall>}-quantifiers, namely:

  \begin{isabelle}
  @{text "@{thm (my_strip_all_qnt2 x' x'') style_test}"}\\
  @{text ">"}~@{thm (my_strip_all_qnt2 x' x'') style_test}
  \end{isabelle}

  Such theorem styles allow one to print out theorems in documents formatted to
  ones heart content. 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}
*}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ML{*structure MyThms = Named_Thms
  (val name = "attr_thms" 
   val description = "Theorems for an Attribute") *}

text {* 
  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
*}

ML{*val my_add = Thm.declaration_attribute MyThms.add_thm
val my_del = Thm.declaration_attribute MyThms.del_thm *}

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

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

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

lemma trueI_2[my_thms]: "True" by simp

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

  @{ML_response_fake [display,gray]
  "MyThms.get @{context}" 
  "[\"True\"]"}

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

declare test[my_thms] trueI_2[my_thms add]

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

  @{ML_response_fake [display,gray]
  "MyThms.get @{context}"
  "[\"True\", \"Suc (Suc 0) = 2\"]"}

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

declare test[my_thms del]

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

  @{ML_response_fake [display,gray]
  "MyThms.get @{context}"
  "[\"True\"]"}

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

  \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}

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

section {* Setups (TBD) *}

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

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

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

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

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

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

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

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

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

section {* Theories\label{sec:theories} (TBD) *}

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

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

section {* Contexts (TBD) *}

section {* Local Theories (TBD) *}


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

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

thm foo_def
*)


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

text {*
  So far we printed out only plain strings without any formatting except for
  occasional explicit line breaks using @{text [quotes] "\\n"}. This is
  sufficient for ``quick-and-dirty'' printouts. For something more
  sophisticated, Isabelle includes an infrastructure for properly formatting
  text. 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_response_fake [display,gray]
  "Pretty.str \"test\"" "String (\"test\", 4)"}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

*}

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

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

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

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

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

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

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

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

  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_fake [display,gray]
  "let
  val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
in
  pprint (Pretty.big_list \"header\" pstrs)
end"
  "header
  4
  5
  6
  7
  8
  9
  10"}

  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_fake [display,gray]
  "let
  val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
in
  pprint (Pretty.blk (0, a_and_b));
  pprint (Pretty.chunks a_and_b)
end"
"ab
a
b"}
  
  \footnote{\bf What happens with printing big formulae?}

  

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

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

text {* writing into the goal buffer *}

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

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

lemma "False"
oops
*)

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

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

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


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


section {* Misc (TBD) *}

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

text {* 
FIXME: association lists:
@{ML_file "Pure/General/alist.ML"}

FIXME: calling the ML-compiler

*}



section {* Managing Name Spaces (TBD) *}

section {* Summary *}

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

end
author	Christian Urban <urbanc@in.tum.de>
	Mon, 19 Oct 2009 14:10:42 +0200 (2009-10-19)
changeset 353	e73ccbed776e
parent 352	9f12e53eb121
child 354	544c149005cf
permissions	-rw-r--r--