Theory HOL_Specific

(*:maxLineLen=78:*)

theory HOL_Specific
  imports
    Main
    "HOL-Library.Old_Datatype"
    "HOL-Library.Old_Recdef"
    "HOL-Library.Adhoc_Overloading"
    "HOL-Library.Dlist"
    "HOL-Library.FSet"
    Base
begin


chapter ‹Higher-Order Logic›

text ‹
  Isabelle/HOL is based on Higher-Order Logic, a polymorphic version of
  Church's Simple Theory of Types. HOL can be best understood as a
  simply-typed version of classical set theory. The logic was first
  implemented in Gordon's HOL system cite‹"mgordon-hol"›. It extends
  Church's original logic cite‹"church40"› by explicit type variables (naive
  polymorphism) and a sound axiomatization scheme for new types based on
  subsets of existing types.

  Andrews's book cite‹andrews86› is a full description of the original
  Church-style higher-order logic, with proofs of correctness and completeness
  wrt.\ certain set-theoretic interpretations. The particular extensions of
  Gordon-style HOL are explained semantically in two chapters of the 1993 HOL
  book cite‹pitts93›.

  Experience with HOL over decades has demonstrated that higher-order logic is
  widely applicable in many areas of mathematics and computer science. In a
  sense, Higher-Order Logic is simpler than First-Order Logic, because there
  are fewer restrictions and special cases. Note that HOL is ∗‹weaker› than
  FOL with axioms for ZF set theory, which is traditionally considered the
  standard foundation of regular mathematics, but for most applications this
  does not matter. If you prefer ML to Lisp, you will probably prefer HOL to
  ZF.

  ┉ The syntax of HOL follows ‹λ›-calculus and functional programming.
  Function application is curried. To apply the function ‹f› of type ‹τ1 ⇒
  τ2 ⇒ τ3› to the arguments ‹a› and ‹b› in HOL, you simply write ‹f a b› (as
  in ML or Haskell). There is no ``apply'' operator; the existing application
  of the Pure ‹λ›-calculus is re-used. Note that in HOL ‹f (a, b)› means ``‹f›
  applied to the pair ‹(a, b)› (which is notation for ‹Pair a b›). The latter
  typically introduces extra formal efforts that can be avoided by currying
  functions by default. Explicit tuples are as infrequent in HOL
  formalizations as in good ML or Haskell programs.

  ┉ Isabelle/HOL has a distinct feel, compared to other object-logics like
  Isabelle/ZF. It identifies object-level types with meta-level types, taking
  advantage of the default type-inference mechanism of Isabelle/Pure. HOL
  fully identifies object-level functions with meta-level functions, with
  native abstraction and application.

  These identifications allow Isabelle to support HOL particularly nicely, but
  they also mean that HOL requires some sophistication from the user. In
  particular, an understanding of Hindley-Milner type-inference with
  type-classes, which are both used extensively in the standard libraries and
  applications.
›


chapter ‹Derived specification elements›

section ‹Inductive and coinductive definitions \label{sec:hol-inductive}›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "inductive"} & : & ‹local_theory → local_theory› \\
    @{command_def (HOL) "inductive_set"} & : & ‹local_theory → local_theory› \\
    @{command_def (HOL) "coinductive"} & : & ‹local_theory → local_theory› \\
    @{command_def (HOL) "coinductive_set"} & : & ‹local_theory → local_theory› \\
    @{command_def "print_inductives"}‹*› & : & ‹context →› \\
    @{attribute_def (HOL) mono} & : & ‹attribute› \\
  \end{matharray}

  An ∗‹inductive definition› specifies the least predicate or set ‹R› closed
  under given rules: applying a rule to elements of ‹R› yields a result within
  ‹R›. For example, a structural operational semantics is an inductive
  definition of an evaluation relation.

  Dually, a ∗‹coinductive definition› specifies the greatest predicate or set
  ‹R› that is consistent with given rules: every element of ‹R› can be seen as
  arising by applying a rule to elements of ‹R›. An important example is using
  bisimulation relations to formalise equivalence of processes and infinite
  data structures.

  Both inductive and coinductive definitions are based on the Knaster-Tarski
  fixed-point theorem for complete lattices. The collection of introduction
  rules given by the user determines a functor on subsets of set-theoretic
  relations. The required monotonicity of the recursion scheme is proven as a
  prerequisite to the fixed-point definition and the resulting consequences.
  This works by pushing inclusion through logical connectives and any other
  operator that might be wrapped around recursive occurrences of the defined
  relation: there must be a monotonicity theorem of the form ‹A ≤ B ⟹ ℳ A ≤ ℳ
  B›, for each premise ‹ℳ R t› in an introduction rule. The default rule
  declarations of Isabelle/HOL already take care of most common situations.

  rail‹
    (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
      @{syntax vars} @{syntax for_fixes} ⏎
      (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
    ;
    @@{command print_inductives} ('!'?)
    ;
    @@{attribute (HOL) mono} (() | 'add' | 'del')
  ›

  ➧ @{command (HOL) "inductive"} and @{command (HOL) "coinductive"} define
  (co)inductive predicates from the introduction rules.

  The propositions given as ‹clauses› in the @{keyword "where"} part are
  either rules of the usual ‹⋀/⟹› format (with arbitrary nesting), or
  equalities using ‹≡›. The latter specifies extra-logical abbreviations in
  the sense of @{command_ref abbreviation}. Introducing abstract syntax
  simultaneously with the actual introduction rules is occasionally useful for
  complex specifications.

  The optional @{keyword "for"} part contains a list of parameters of the
  (co)inductive predicates that remain fixed throughout the definition, in
  contrast to arguments of the relation that may vary in each occurrence
  within the given ‹clauses›.

  The optional @{keyword "monos"} declaration contains additional
  ∗‹monotonicity theorems›, which are required for each operator applied to a
  recursive set in the introduction rules.

  ➧ @{command (HOL) "inductive_set"} and @{command (HOL) "coinductive_set"}
  are wrappers for to the previous commands for native HOL predicates. This
  allows to define (co)inductive sets, where multiple arguments are simulated
  via tuples.

  ➧ @{command "print_inductives"} prints (co)inductive definitions and
  monotonicity rules; the ``‹!›'' option indicates extra verbosity.

  ➧ @{attribute (HOL) mono} declares monotonicity rules in the context. These
  rule are involved in the automated monotonicity proof of the above inductive
  and coinductive definitions.
›


subsection ‹Derived rules›

text ‹
  A (co)inductive definition of ‹R› provides the following main theorems:

  ➧ ‹R.intros› is the list of introduction rules as proven theorems, for the
  recursive predicates (or sets). The rules are also available individually,
  using the names given them in the theory file;

  ➧ ‹R.cases› is the case analysis (or elimination) rule;

  ➧ ‹R.induct› or ‹R.coinduct› is the (co)induction rule;

  ➧ ‹R.simps› is the equation unrolling the fixpoint of the predicate one
  step.


  When several predicates ‹R1, …, Rn› are defined simultaneously, the list
  of introduction rules is called ‹R1_…_Rn.intros›, the case analysis rules
  are called ‹R1.cases, …, Rn.cases›, and the list of mutual induction rules
  is called ‹R1_…_Rn.inducts›.
›


subsection ‹Monotonicity theorems›

text ‹
  The context maintains a default set of theorems that are used in
  monotonicity proofs. New rules can be declared via the @{attribute (HOL)
  mono} attribute. See the main Isabelle/HOL sources for some examples. The
  general format of such monotonicity theorems is as follows:

  ▪ Theorems of the form ‹A ≤ B ⟹ ℳ A ≤ ℳ B›, for proving monotonicity of
  inductive definitions whose introduction rules have premises involving terms
  such as ‹ℳ R t›.

  ▪ Monotonicity theorems for logical operators, which are of the general form
  ‹(… ⟶ …) ⟹ … (… ⟶ …) ⟹ … ⟶ …›. For example, in the case of the operator ‹∨›,
  the corresponding theorem is
  \[
  \infer{‹P1 ∨ P2 ⟶ Q1 ∨ Q2›}{‹P1 ⟶ Q1› & ‹P2 ⟶ Q2›}
  \]

  ▪ De Morgan style equations for reasoning about the ``polarity'' of
  expressions, e.g.
  \[
  prop‹¬ ¬ P ⟷ P› \qquad\qquad
  prop‹¬ (P ∧ Q) ⟷ ¬ P ∨ ¬ Q›
  \]

  ▪ Equations for reducing complex operators to more primitive ones whose
  monotonicity can easily be proved, e.g.
  \[
  prop‹(P ⟶ Q) ⟷ ¬ P ∨ Q› \qquad\qquad
  prop‹Ball A P ≡ ∀x. x ∈ A ⟶ P x›
  \]
›


subsubsection ‹Examples›

text ‹The finite powerset operator can be defined inductively like this:›

(*<*)experiment begin(*>*)
inductive_set Fin :: "'a set ⇒ 'a set set" for A :: "'a set"
where
  empty: "{} ∈ Fin A"
| insert: "a ∈ A ⟹ B ∈ Fin A ⟹ insert a B ∈ Fin A"

text ‹The accessible part of a relation is defined as follows:›

inductive acc :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool"
  for r :: "'a ⇒ 'a ⇒ bool"  (infix "≺" 50)
where acc: "(⋀y. y ≺ x ⟹ acc r y) ⟹ acc r x"
(*<*)end(*>*)

text ‹
  Common logical connectives can be easily characterized as non-recursive
  inductive definitions with parameters, but without arguments.
›

(*<*)experiment begin(*>*)
inductive AND for A B :: bool
where "A ⟹ B ⟹ AND A B"

inductive OR for A B :: bool
where "A ⟹ OR A B"
  | "B ⟹ OR A B"

inductive EXISTS for B :: "'a ⇒ bool"
where "B a ⟹ EXISTS B"
(*<*)end(*>*)

text ‹
  Here the ‹cases› or ‹induct› rules produced by the @{command inductive}
  package coincide with the expected elimination rules for Natural Deduction.
  Already in the original article by Gerhard Gentzen cite‹"Gentzen:1935"›
  there is a hint that each connective can be characterized by its
  introductions, and the elimination can be constructed systematically.
›


section ‹Recursive functions \label{sec:recursion}›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "primrec"} & : & ‹local_theory → local_theory› \\
    @{command_def (HOL) "fun"} & : & ‹local_theory → local_theory› \\
    @{command_def (HOL) "function"} & : & ‹local_theory → proof(prove)› \\
    @{command_def (HOL) "termination"} & : & ‹local_theory → proof(prove)› \\
    @{command_def (HOL) "fun_cases"} & : & ‹local_theory → local_theory› \\
  \end{matharray}

  rail‹
    @@{command (HOL) primrec} @{syntax specification}
    ;
    (@@{command (HOL) fun} | @@{command (HOL) function}) opts? @{syntax specification}
    ;
    opts: '(' (('sequential' | 'domintros') + ',') ')'
    ;
    @@{command (HOL) termination} @{syntax term}?
    ;
    @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
  ›

  ➧ @{command (HOL) "primrec"} defines primitive recursive functions over
  datatypes (see also @{command_ref (HOL) datatype}). The given ‹equations›
  specify reduction rules that are produced by instantiating the generic
  combinator for primitive recursion that is available for each datatype.

  Each equation needs to be of the form:

  @{text [display] "f x1 … xm (C y1 … yk) z1 … zn = rhs"}

  such that ‹C› is a datatype constructor, ‹rhs› contains only the free
  variables on the left-hand side (or from the context), and all recursive
  occurrences of ‹f› in ‹rhs› are of the form ‹f … yi …› for some ‹i›. At
  most one reduction rule for each constructor can be given. The order does
  not matter. For missing constructors, the function is defined to return a
  default value, but this equation is made difficult to access for users.

  The reduction rules are declared as @{attribute simp} by default, which
  enables standard proof methods like @{method simp} and @{method auto} to
  normalize expressions of ‹f› applied to datatype constructions, by
  simulating symbolic computation via rewriting.

  ➧ @{command (HOL) "function"} defines functions by general wellfounded
  recursion. A detailed description with examples can be found in cite‹"isabelle-function"›. The function is specified by a set of (possibly
  conditional) recursive equations with arbitrary pattern matching. The
  command generates proof obligations for the completeness and the
  compatibility of patterns.

  The defined function is considered partial, and the resulting simplification
  rules (named ‹f.psimps›) and induction rule (named ‹f.pinduct›) are guarded
  by a generated domain predicate ‹f_dom›. The @{command (HOL) "termination"}
  command can then be used to establish that the function is total.

  ➧ @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL)
  "function"}~‹(sequential)›'', followed by automated proof attempts regarding
  pattern matching and termination. See cite‹"isabelle-function"› for
  further details.

  ➧ @{command (HOL) "termination"}~‹f› commences a termination proof for the
  previously defined function ‹f›. If this is omitted, the command refers to
  the most recent function definition. After the proof is closed, the
  recursive equations and the induction principle is established.

  ➧ @{command (HOL) "fun_cases"} generates specialized elimination rules for
  function equations. It expects one or more function equations and produces
  rules that eliminate the given equalities, following the cases given in the
  function definition.


  Recursive definitions introduced by the @{command (HOL) "function"} command
  accommodate reasoning by induction (cf.\ @{method induct}): rule ‹f.induct›
  refers to a specific induction rule, with parameters named according to the
  user-specified equations. Cases are numbered starting from 1. For @{command
  (HOL) "primrec"}, the induction principle coincides with structural
  recursion on the datatype where the recursion is carried out.

  The equations provided by these packages may be referred later as theorem
  list ‹f.simps›, where ‹f› is the (collective) name of the functions defined.
  Individual equations may be named explicitly as well.

  The @{command (HOL) "function"} command accepts the following options.

  ➧ ‹sequential› enables a preprocessor which disambiguates overlapping
  patterns by making them mutually disjoint. Earlier equations take precedence
  over later ones. This allows to give the specification in a format very
  similar to functional programming. Note that the resulting simplification
  and induction rules correspond to the transformed specification, not the one
  given originally. This usually means that each equation given by the user
  may result in several theorems. Also note that this automatic transformation
  only works for ML-style datatype patterns.

  ➧ ‹domintros› enables the automated generation of introduction rules for the
  domain predicate. While mostly not needed, they can be helpful in some
  proofs about partial functions.
›


subsubsection ‹Example: evaluation of expressions›

text ‹
  Subsequently, we define mutual datatypes for arithmetic and boolean
  expressions, and use @{command primrec} for evaluation functions that follow
  the same recursive structure.
›

(*<*)experiment begin(*>*)
datatype 'a aexp =
    IF "'a bexp"  "'a aexp"  "'a aexp"
  | Sum "'a aexp"  "'a aexp"
  | Diff "'a aexp"  "'a aexp"
  | Var 'a
  | Num nat
and 'a bexp =
    Less "'a aexp"  "'a aexp"
  | And "'a bexp"  "'a bexp"
  | Neg "'a bexp"

text ‹┉ Evaluation of arithmetic and boolean expressions›

primrec evala :: "('a ⇒ nat) ⇒ 'a aexp ⇒ nat"
  and evalb :: "('a ⇒ nat) ⇒ 'a bexp ⇒ bool"
where
  "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
| "evala env (Sum a1 a2) = evala env a1 + evala env a2"
| "evala env (Diff a1 a2) = evala env a1 - evala env a2"
| "evala env (Var v) = env v"
| "evala env (Num n) = n"
| "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
| "evalb env (And b1 b2) = (evalb env b1 ∧ evalb env b2)"
| "evalb env (Neg b) = (¬ evalb env b)"

text ‹
  Since the value of an expression depends on the value of its variables, the
  functions const‹evala› and const‹evalb› take an additional parameter, an
  ∗‹environment› that maps variables to their values.

  ┉
  Substitution on expressions can be defined similarly. The mapping ‹f› of
  type typ‹'a ⇒ 'a aexp› given as a parameter is lifted canonically on the
  types typ‹'a aexp› and typ‹'a bexp›, respectively.
›

primrec substa :: "('a ⇒ 'b aexp) ⇒ 'a aexp ⇒ 'b aexp"
  and substb :: "('a ⇒ 'b aexp) ⇒ 'a bexp ⇒ 'b bexp"
where
  "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
| "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
| "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
| "substa f (Var v) = f v"
| "substa f (Num n) = Num n"
| "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
| "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
| "substb f (Neg b) = Neg (substb f b)"

text ‹
  In textbooks about semantics one often finds substitution theorems, which
  express the relationship between substitution and evaluation. For typ‹'a
  aexp› and typ‹'a bexp›, we can prove such a theorem by mutual
  induction, followed by simplification.
›

lemma subst_one:
  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
  "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
  by (induct a and b) simp_all

lemma subst_all:
  "evala env (substa s a) = evala (λx. evala env (s x)) a"
  "evalb env (substb s b) = evalb (λx. evala env (s x)) b"
  by (induct a and b) simp_all
(*<*)end(*>*)


subsubsection ‹Example: a substitution function for terms›

text ‹Functions on datatypes with nested recursion are also defined
  by mutual primitive recursion.›

(*<*)experiment begin(*>*)
datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"

text ‹
  A substitution function on type typ‹('a, 'b) term› can be defined as
  follows, by working simultaneously on typ‹('a, 'b) term list›:
›

primrec subst_term :: "('a ⇒ ('a, 'b) term) ⇒ ('a, 'b) term ⇒ ('a, 'b) term" and
  subst_term_list :: "('a ⇒ ('a, 'b) term) ⇒ ('a, 'b) term list ⇒ ('a, 'b) term list"
where
  "subst_term f (Var a) = f a"
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
| "subst_term_list f [] = []"
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"

text ‹
  The recursion scheme follows the structure of the unfolded definition of
  type typ‹('a, 'b) term›. To prove properties of this substitution
  function, mutual induction is needed:
›

lemma "subst_term (subst_term f1 ∘ f2) t =
    subst_term f1 (subst_term f2 t)" and
  "subst_term_list (subst_term f1 ∘ f2) ts =
    subst_term_list f1 (subst_term_list f2 ts)"
  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
(*<*)end(*>*)


subsubsection ‹Example: a map function for infinitely branching trees›

text ‹Defining functions on infinitely branching datatypes by primitive
  recursion is just as easy.›

(*<*)experiment begin(*>*)
datatype 'a tree = Atom 'a | Branch "nat ⇒ 'a tree"

primrec map_tree :: "('a ⇒ 'b) ⇒ 'a tree ⇒ 'b tree"
where
  "map_tree f (Atom a) = Atom (f a)"
| "map_tree f (Branch ts) = Branch (λx. map_tree f (ts x))"

text ‹
  Note that all occurrences of functions such as ‹ts› above must be applied to
  an argument. In particular, term‹map_tree f ∘ ts› is not allowed here.

  ┉
  Here is a simple composition lemma for term‹map_tree›:
›

lemma "map_tree g (map_tree f t) = map_tree (g ∘ f) t"
  by (induct t) simp_all
(*<*)end(*>*)


subsection ‹Proof methods related to recursive definitions›

text ‹
  \begin{matharray}{rcl}
    @{method_def (HOL) pat_completeness} & : & ‹method› \\
    @{method_def (HOL) relation} & : & ‹method› \\
    @{method_def (HOL) lexicographic_order} & : & ‹method› \\
    @{method_def (HOL) size_change} & : & ‹method› \\
    @{attribute_def (HOL) termination_simp} & : & ‹attribute› \\
    @{method_def (HOL) induction_schema} & : & ‹method› \\
  \end{matharray}

  rail‹
    @@{method (HOL) relation} @{syntax term}
    ;
    @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )
    ;
    @@{method (HOL) size_change} ( orders (@{syntax clasimpmod} * ) )
    ;
    @@{method (HOL) induction_schema}
    ;
    orders: ( 'max' | 'min' | 'ms' ) *
  ›

  ➧ @{method (HOL) pat_completeness} is a specialized method to solve goals
  regarding the completeness of pattern matching, as required by the @{command
  (HOL) "function"} package (cf.\ cite‹"isabelle-function"›).

  ➧ @{method (HOL) relation}~‹R› introduces a termination proof using the
  relation ‹R›. The resulting proof state will contain goals expressing that
  ‹R› is wellfounded, and that the arguments of recursive calls decrease with
  respect to ‹R›. Usually, this method is used as the initial proof step of
  manual termination proofs.

  ➧ @{method (HOL) "lexicographic_order"} attempts a fully automated
  termination proof by searching for a lexicographic combination of size
  measures on the arguments of the function. The method accepts the same
  arguments as the @{method auto} method, which it uses internally to prove
  local descents. The @{syntax clasimpmod} modifiers are accepted (as for
  @{method auto}).

  In case of failure, extensive information is printed, which can help to
  analyse the situation (cf.\ cite‹"isabelle-function"›).

  ➧ @{method (HOL) "size_change"} also works on termination goals, using a
  variation of the size-change principle, together with a graph decomposition
  technique (see cite‹krauss_phd› for details). Three kinds of orders are
  used internally: ‹max›, ‹min›, and ‹ms› (multiset), which is only available
  when the theory ‹Multiset› is loaded. When no order kinds are given, they
  are tried in order. The search for a termination proof uses SAT solving
  internally.

  For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
  (as for @{method auto}).

  ➧ @{attribute (HOL) termination_simp} declares extra rules for the
  simplifier, when invoked in termination proofs. This can be useful, e.g.,
  for special rules involving size estimations.

  ➧ @{method (HOL) induction_schema} derives user-specified induction rules
  from well-founded induction and completeness of patterns. This factors out
  some operations that are done internally by the function package and makes
  them available separately. See 🗏‹~~/src/HOL/Examples/Induction_Schema.thy› for
  examples.
›


subsection ‹Functions with explicit partiality›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "partial_function"} & : & ‹local_theory → local_theory› \\
    @{attribute_def (HOL) "partial_function_mono"} & : & ‹attribute› \\
  \end{matharray}

  rail‹
    @@{command (HOL) partial_function} '(' @{syntax name} ')'
      @{syntax specification}
  ›

  ➧ @{command (HOL) "partial_function"}~‹(mode)› defines recursive functions
  based on fixpoints in complete partial orders. No termination proof is
  required from the user or constructed internally. Instead, the possibility
  of non-termination is modelled explicitly in the result type, which contains
  an explicit bottom element.

  Pattern matching and mutual recursion are currently not supported. Thus, the
  specification consists of a single function described by a single recursive
  equation.

  There are no fixed syntactic restrictions on the body of the function, but
  the induced functional must be provably monotonic wrt.\ the underlying
  order. The monotonicity proof is performed internally, and the definition is
  rejected when it fails. The proof can be influenced by declaring hints using
  the @{attribute (HOL) partial_function_mono} attribute.

  The mandatory ‹mode› argument specifies the mode of operation of the
  command, which directly corresponds to a complete partial order on the
  result type. By default, the following modes are defined:

    ➧ ‹option› defines functions that map into the type‹option› type. Here,
    the value term‹None› is used to model a non-terminating computation.
    Monotonicity requires that if term‹None› is returned by a recursive
    call, then the overall result must also be term‹None›. This is best
    achieved through the use of the monadic operator const‹Option.bind›.

    ➧ ‹tailrec› defines functions with an arbitrary result type and uses the
    slightly degenerated partial order where term‹undefined› is the bottom
    element. Now, monotonicity requires that if term‹undefined› is returned
    by a recursive call, then the overall result must also be term‹undefined›. In practice, this is only satisfied when each recursive call
    is a tail call, whose result is directly returned. Thus, this mode of
    operation allows the definition of arbitrary tail-recursive functions.

  Experienced users may define new modes by instantiating the locale const‹partial_function_definitions› appropriately.

  ➧ @{attribute (HOL) partial_function_mono} declares rules for use in the
  internal monotonicity proofs of partial function definitions.
›


subsection ‹Old-style recursive function definitions (TFL)›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "recdef"} & : & ‹theory → theory)› \\
  \end{matharray}

  The old TFL command @{command (HOL) "recdef"} for defining recursive is
  mostly obsolete; @{command (HOL) "function"} or @{command (HOL) "fun"}
  should be used instead.

  rail‹
    @@{command (HOL) recdef} ('(' @'permissive' ')')? ⏎
      @{syntax name} @{syntax term} (@{syntax prop} +) hints?
    ;
    hints: '(' @'hints' ( recdefmod * ) ')'
    ;
    recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
      (() | 'add' | 'del') ':' @{syntax thms}) | @{syntax clasimpmod}
  ›

  ➧ @{command (HOL) "recdef"} defines general well-founded recursive functions
  (using the TFL package). The ``‹(permissive)›'' option tells TFL to recover
  from failed proof attempts, returning unfinished results. The ‹recdef_simp›,
  ‹recdef_cong›, and ‹recdef_wf› hints refer to auxiliary rules to be used in
  the internal automated proof process of TFL. Additional @{syntax clasimpmod}
  declarations may be given to tune the context of the Simplifier (cf.\
  \secref{sec:simplifier}) and Classical reasoner (cf.\
  \secref{sec:classical}).


  ┉
  Hints for @{command (HOL) "recdef"} may be also declared globally, using the
  following attributes.

  \begin{matharray}{rcl}
    @{attribute_def (HOL) recdef_simp} & : & ‹attribute› \\
    @{attribute_def (HOL) recdef_cong} & : & ‹attribute› \\
    @{attribute_def (HOL) recdef_wf} & : & ‹attribute› \\
  \end{matharray}

  rail‹
    (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |
      @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')
  ›
›


section ‹Adhoc overloading of constants›

text ‹
  \begin{tabular}{rcll}
  @{command_def "adhoc_overloading"} & : & ‹local_theory → local_theory› \\
  @{command_def "no_adhoc_overloading"} & : & ‹local_theory → local_theory› \\
  @{attribute_def "show_variants"} & : & ‹attribute› & default ‹false› \\
  \end{tabular}

  ┉
  Adhoc overloading allows to overload a constant depending on its type.
  Typically this involves the introduction of an uninterpreted constant (used
  for input and output) and the addition of some variants (used internally).
  For examples see 🗏‹~~/src/HOL/Examples/Adhoc_Overloading_Examples.thy› and
  🗏‹~~/src/HOL/Library/Monad_Syntax.thy›.

  rail‹
    (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
      (@{syntax name} (@{syntax term} + ) + @'and')
  ›

  ➧ @{command "adhoc_overloading"}~‹c v1 ... vn› associates variants with an
  existing constant.

  ➧ @{command "no_adhoc_overloading"} is similar to @{command
  "adhoc_overloading"}, but removes the specified variants from the present
  context.

  ➧ @{attribute "show_variants"} controls printing of variants of overloaded
  constants. If enabled, the internally used variants are printed instead of
  their respective overloaded constants. This is occasionally useful to check
  whether the system agrees with a user's expectations about derived variants.
›


section ‹Definition by specification \label{sec:hol-specification}›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "specification"} & : & ‹theory → proof(prove)› \\
  \end{matharray}

  rail‹
    @@{command (HOL) specification} '(' (decl +) ')' ⏎
      (@{syntax thmdecl}? @{syntax prop} +)
    ;
    decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')?
  ›

  ➧ @{command (HOL) "specification"}~‹decls φ› sets up a goal stating the
  existence of terms with the properties specified to hold for the constants
  given in ‹decls›. After finishing the proof, the theory will be augmented
  with definitions for the given constants, as well as with theorems stating
  the properties for these constants.

  ‹decl› declares a constant to be defined by the specification given. The
  definition for the constant ‹c› is bound to the name ‹c_def› unless a
  theorem name is given in the declaration. Overloaded constants should be
  declared as such.
›


section ‹Old-style datatypes \label{sec:hol-datatype}›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "old_rep_datatype"} & : & ‹theory → proof(prove)› \\
  \end{matharray}

  rail‹
    @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
    ;

    spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
    ;
    cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
  ›

  ➧ @{command (HOL) "old_rep_datatype"} represents existing types as
  old-style datatypes.


  These commands are mostly obsolete; @{command (HOL) "datatype"} should be
  used instead.

  See cite‹"isabelle-datatypes"› for more details on datatypes. Apart from
  proper proof methods for case analysis and induction, there are also
  emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
  induct_tac} available, see \secref{sec:hol-induct-tac}; these admit to refer
  directly to the internal structure of subgoals (including internally bound
  parameters).
›


subsubsection ‹Examples›

text ‹
  We define a type of finite sequences, with slightly different names than the
  existing typ‹'a list› that is already in theory‹Main›:
›

(*<*)experiment begin(*>*)
datatype 'a seq = Empty | Seq 'a "'a seq"

text ‹We can now prove some simple lemma by structural induction:›

lemma "Seq x xs ≠ xs"
proof (induct xs arbitrary: x)
  case Empty
  txt ‹This case can be proved using the simplifier: the freeness
    properties of the datatype are already declared as @{attribute
    simp} rules.›
  show "Seq x Empty ≠ Empty"
    by simp
next
  case (Seq y ys)
  txt ‹The step case is proved similarly.›
  show "Seq x (Seq y ys) ≠ Seq y ys"
    using ‹Seq y ys ≠ ys› by simp
qed

text ‹Here is a more succinct version of the same proof:›

lemma "Seq x xs ≠ xs"
  by (induct xs arbitrary: x) simp_all
(*<*)end(*>*)


section ‹Records \label{sec:hol-record}›

text ‹
  In principle, records merely generalize the concept of tuples, where
  components may be addressed by labels instead of just position. The logical
  infrastructure of records in Isabelle/HOL is slightly more advanced, though,
  supporting truly extensible record schemes. This admits operations that are
  polymorphic with respect to record extension, yielding ``object-oriented''
  effects like (single) inheritance. See also cite‹"NaraschewskiW-TPHOLs98"›
  for more details on object-oriented verification and record subtyping in
  HOL.
›


subsection ‹Basic concepts›

text ‹
  Isabelle/HOL supports both ∗‹fixed› and ∗‹schematic› records at the level of
  terms and types. The notation is as follows:

  \begin{center}
  \begin{tabular}{l|l|l}
    & record terms & record types \\ \hline
    fixed & ‹⦇x = a, y = b⦈› & ‹⦇x :: A, y :: B⦈› \\
    schematic & ‹⦇x = a, y = b, … = m⦈› &
      ‹⦇x :: A, y :: B, … :: M⦈› \\
  \end{tabular}
  \end{center}

  The ASCII representation of ‹⦇x = a⦈› is ‹(| x = a |)›.

  A fixed record ‹⦇x = a, y = b⦈› has field ‹x› of value ‹a› and field ‹y› of
  value ‹b›. The corresponding type is ‹⦇x :: A, y :: B⦈›, assuming that ‹a ::
  A› and ‹b :: B›.

  A record scheme like ‹⦇x = a, y = b, … = m⦈› contains fields ‹x› and ‹y› as
  before, but also possibly further fields as indicated by the ``‹…›''
  notation (which is actually part of the syntax). The improper field ``‹…›''
  of a record scheme is called the ∗‹more part›. Logically it is just a free
  variable, which is occasionally referred to as ``row variable'' in the
  literature. The more part of a record scheme may be instantiated by zero or
  more further components. For example, the previous scheme may get
  instantiated to ‹⦇x = a, y = b, z = c, … = m'⦈›, where ‹m'› refers to a
  different more part. Fixed records are special instances of record schemes,
  where ``‹…›'' is properly terminated by the ‹() :: unit› element. In fact,
  ‹⦇x = a, y = b⦈› is just an abbreviation for ‹⦇x = a, y = b, … = ()⦈›.

  ┉
  Two key observations make extensible records in a simply typed language like
  HOL work out:

  ▸ the more part is internalized, as a free term or type variable,

  ▸ field names are externalized, they cannot be accessed within the logic as
  first-class values.


  ┉
  In Isabelle/HOL record types have to be defined explicitly, fixing their
  field names and types, and their (optional) parent record. Afterwards,
  records may be formed using above syntax, while obeying the canonical order
  of fields as given by their declaration. The record package provides several
  standard operations like selectors and updates. The common setup for various
  generic proof tools enable succinct reasoning patterns. See also the
  Isabelle/HOL tutorial cite‹"isabelle-hol-book"› for further instructions
  on using records in practice.
›


subsection ‹Record specifications›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "record"} & : & ‹theory → theory› \\
    @{command_def (HOL) "print_record"} & : & ‹context →› \\
  \end{matharray}

  rail‹
    @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' ⏎
      (@{syntax type} '+')? (constdecl +)
    ;
    constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
    ;
    @@{command (HOL) print_record} modes? @{syntax typespec_sorts}
    ;
    modes: '(' (@{syntax name} +) ')'
  ›

  ➧ @{command (HOL) "record"}~‹(α1, …, αm) t = τ + c1 :: σ1 … cn :: σn›
  defines extensible record type ‹(α1, …, αm) t›, derived from the optional
  parent record ‹τ› by adding new field components ‹ci :: σi› etc.

  The type variables of ‹τ› and ‹σi› need to be covered by the (distinct)
  parameters ‹α1, …, αm›. Type constructor ‹t› has to be new, while ‹τ›
  needs to specify an instance of an existing record type. At least one new
  field ‹ci› has to be specified. Basically, field names need to belong to a
  unique record. This is not a real restriction in practice, since fields are
  qualified by the record name internally.

  The parent record specification ‹τ› is optional; if omitted ‹t› becomes a
  root record. The hierarchy of all records declared within a theory context
  forms a forest structure, i.e.\ a set of trees starting with a root record
  each. There is no way to merge multiple parent records!

  For convenience, ‹(α1, …, αm) t› is made a type abbreviation for the fixed
  record type ‹⦇c1 :: σ1, …, cn :: σn⦈›, likewise is ‹(α1, …, αm, ζ)
  t_scheme› made an abbreviation for ‹⦇c1 :: σ1, …, cn :: σn, … :: ζ⦈›.

  ➧ @{command (HOL) "print_record"}~‹(α1, …, αm) t› prints the definition of
  record ‹(α1, …, αm) t›. Optionally ‹modes› can be specified, which are
  appended to the current print mode; see \secref{sec:print-modes}.
›


subsection ‹Record operations›

text ‹
  Any record definition of the form presented above produces certain standard
  operations. Selectors and updates are provided for any field, including the
  improper one ``‹more›''. There are also cumulative record constructor
  functions. To simplify the presentation below, we assume for now that ‹(α1,
  …, αm) t› is a root record with fields ‹c1 :: σ1, …, cn :: σn›.

  ┉
  ❙‹Selectors› and ❙‹updates› are available for any
  field (including ``‹more›''):

  \begin{matharray}{lll}
    ‹ci› & ‹::› & ‹⦇vecc :: vecσ, … :: ζ⦈ ⇒ σi› \\
    ‹ci_update› & ‹::› & ‹(σi ⇒ σi) ⇒ ⦇vecc :: vecσ, … :: ζ⦈ ⇒ ⦇vecc :: vecσ, … :: ζ⦈› \\
  \end{matharray}

  There is special syntax for application of updates: ‹r⦇x := a⦈› abbreviates
  term ‹x_update (λ_. a) r›. Further notation for repeated updates is also
  available: ‹r⦇x := a⦈⦇y := b⦈⦇z := c⦈› may be written ‹r⦇x := a, y := b, z
  := c⦈›. Note that because of postfix notation the order of fields shown here
  is reverse than in the actual term. Since repeated updates are just function
  applications, fields may be freely permuted in ‹⦇x := a, y := b, z := c⦈›,
  as far as logical equality is concerned. Thus commutativity of independent
  updates can be proven within the logic for any two fields, but not as a
  general theorem.

  ┉
  The ❙‹make› operation provides a cumulative record constructor function:

  \begin{matharray}{lll}
    ‹t.make› & ‹::› & ‹σ1 ⇒ … σn ⇒ ⦇vecc :: vecσ⦈› \\
  \end{matharray}

  ┉
  We now reconsider the case of non-root records, which are derived of some
  parent. In general, the latter may depend on another parent as well,
  resulting in a list of ∗‹ancestor records›. Appending the lists of fields of
  all ancestors results in a certain field prefix. The record package
  automatically takes care of this by lifting operations over this context of
  ancestor fields. Assuming that ‹(α1, …, αm) t› has ancestor fields ‹b1 ::
  ρ1, …, bk :: ρk›, the above record operations will get the following
  types:

  ┉
  \begin{tabular}{lll}
    ‹ci› & ‹::› & ‹⦇vecb :: vecρ, vecc :: vecσ, … :: ζ⦈ ⇒ σi› \\
    ‹ci_update› & ‹::› & ‹(σi ⇒ σi) ⇒
      ⦇vecb :: vecρ, vecc :: vecσ, … :: ζ⦈ ⇒
      ⦇vecb :: vecρ, vecc :: vecσ, … :: ζ⦈› \\
    ‹t.make› & ‹::› & ‹ρ1 ⇒ … ρk ⇒ σ1 ⇒ … σn ⇒
      ⦇vecb :: vecρ, vecc :: vecσ⦈› \\
  \end{tabular}
  ┉

  Some further operations address the extension aspect of a derived record
  scheme specifically: ‹t.fields› produces a record fragment consisting of
  exactly the new fields introduced here (the result may serve as a more part
  elsewhere); ‹t.extend› takes a fixed record and adds a given more part;
  ‹t.truncate› restricts a record scheme to a fixed record.

  ┉
  \begin{tabular}{lll}
    ‹t.fields› & ‹::› & ‹σ1 ⇒ … σn ⇒ ⦇vecc :: vecσ⦈› \\
    ‹t.extend› & ‹::› & ‹⦇vecb :: vecρ, vecc :: vecσ⦈ ⇒
      ζ ⇒ ⦇vecb :: vecρ, vecc :: vecσ, … :: ζ⦈› \\
    ‹t.truncate› & ‹::› & ‹⦇vecb :: vecρ, vecc :: vecσ, … :: ζ⦈ ⇒ ⦇vecb :: vecρ, vecc :: vecσ⦈› \\
  \end{tabular}
  ┉

  Note that ‹t.make› and ‹t.fields› coincide for root records.
›


subsection ‹Derived rules and proof tools›

text ‹
  The record package proves several results internally, declaring these facts
  to appropriate proof tools. This enables users to reason about record
  structures quite conveniently. Assume that ‹t› is a record type as specified
  above.

  ▸ Standard conversions for selectors or updates applied to record
  constructor terms are made part of the default Simplifier context; thus
  proofs by reduction of basic operations merely require the @{method simp}
  method without further arguments. These rules are available as ‹t.simps›,
  too.

  ▸ Selectors applied to updated records are automatically reduced by an
  internal simplification procedure, which is also part of the standard
  Simplifier setup.

  ▸ Inject equations of a form analogous to prop‹(x, y) = (x', y') ≡ x = x'
  ∧ y = y'› are declared to the Simplifier and Classical Reasoner as
  @{attribute iff} rules. These rules are available as ‹t.iffs›.

  ▸ The introduction rule for record equality analogous to ‹x r = x r' ⟹ y r =
  y r' … ⟹ r = r'› is declared to the Simplifier, and as the basic rule
  context as ``@{attribute intro}‹?›''. The rule is called ‹t.equality›.

  ▸ Representations of arbitrary record expressions as canonical constructor
  terms are provided both in @{method cases} and @{method induct} format (cf.\
  the generic proof methods of the same name, \secref{sec:cases-induct}).
  Several variations are available, for fixed records, record schemes, more
  parts etc.

  The generic proof methods are sufficiently smart to pick the most sensible
  rule according to the type of the indicated record expression: users just
  need to apply something like ``‹(cases r)›'' to a certain proof problem.

  ▸ The derived record operations ‹t.make›, ‹t.fields›, ‹t.extend›,
  ‹t.truncate› are ∗‹not› treated automatically, but usually need to be
  expanded by hand, using the collective fact ‹t.defs›.
›


subsubsection ‹Examples›

text ‹See 🗏‹~~/src/HOL/Examples/Records.thy›, for example.›


section ‹Semantic subtype definitions \label{sec:hol-typedef}›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "typedef"} & : & ‹local_theory → proof(prove)› \\
  \end{matharray}

  A type definition identifies a new type with a non-empty subset of an
  existing type. More precisely, the new type is defined by exhibiting an
  existing type ‹τ›, a set ‹A :: τ set›, and proving prop‹∃x. x ∈ A›. Thus
  ‹A› is a non-empty subset of ‹τ›, and the new type denotes this subset. New
  functions are postulated that establish an isomorphism between the new type
  and the subset. In general, the type ‹τ› may involve type variables ‹α1, …,
  αn› which means that the type definition produces a type constructor ‹(α1,
  …, αn) t› depending on those type arguments.

  rail‹
    @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
    ;
    @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
    ;
    abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
    ;
    rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
  ›

  To understand the concept of type definition better, we need to recount its
  somewhat complex history. The HOL logic goes back to the ``Simple Theory of
  Types'' (STT) of A. Church cite‹"church40"›, which is further explained in
  the book by P. Andrews cite‹"andrews86"›. The overview article by W.
  Farmer cite‹"Farmer:2008"› points out the ``seven virtues'' of this
  relatively simple family of logics. STT has only ground types, without
  polymorphism and without type definitions.

  ┉
  M. Gordon cite‹"Gordon:1985:HOL"› augmented Church's STT by adding
  schematic polymorphism (type variables and type constructors) and a facility
  to introduce new types as semantic subtypes from existing types. This
  genuine extension of the logic was explained semantically by A. Pitts in the
  book of the original Cambridge HOL88 system cite‹"pitts93"›. Type
  definitions work in this setting, because the general model-theory of STT is
  restricted to models that ensure that the universe of type interpretations
  is closed by forming subsets (via predicates taken from the logic).

  ┉
  Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded constant
  definitions cite‹"Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"›,
  which are actually a concept of Isabelle/Pure and do not depend on
  particular set-theoretic semantics of HOL. Over many years, there was no
  formal checking of semantic type definitions in Isabelle/HOL versus
  syntactic constant definitions in Isabelle/Pure. So the @{command typedef}
  command was described as ``axiomatic'' in the sense of
  \secref{sec:axiomatizations}, only with some local checks of the given type
  and its representing set.

  Recent clarification of overloading in the HOL logic proper cite‹"Kuncar-Popescu:2015"› demonstrates how the dissimilar concepts of constant
  definitions versus type definitions may be understood uniformly. This
  requires an interpretation of Isabelle/HOL that substantially reforms the
  set-theoretic model of A. Pitts cite‹"pitts93"›, by taking a schematic
  view on polymorphism and interpreting only ground types in the set-theoretic
  sense of HOL88. Moreover, type-constructors may be explicitly overloaded,
  e.g.\ by making the subset depend on type-class parameters (cf.\
  \secref{sec:class}). This is semantically like a dependent type: the meaning
  relies on the operations provided by different type-class instances.

  ➧ @{command (HOL) "typedef"}~‹(α1, …, αn) t = A› defines a new type ‹(α1,
  …, αn) t› from the set ‹A› over an existing type. The set ‹A› may contain
  type variables ‹α1, …, αn› as specified on the LHS, but no term variables.
  Non-emptiness of ‹A› needs to be proven on the spot, in order to turn the
  internal conditional characterization into usable theorems.

  The ``‹(overloaded)›'' option allows the @{command "typedef"} specification
  to depend on constants that are not (yet) specified and thus left open as
  parameters, e.g.\ type-class parameters.

  Within a local theory specification, the newly introduced type constructor
  cannot depend on parameters or assumptions of the context: this is
  syntactically impossible in HOL. The non-emptiness proof may formally depend
  on local assumptions, but this has little practical relevance.

  For @{command (HOL) "typedef"}~‹t = A› the newly introduced type ‹t› is
  accompanied by a pair of morphisms to relate it to the representing set over
  the old type. By default, the injection from type to set is called ‹Rep_t›
  and its inverse ‹Abs_t›: An explicit @{keyword (HOL) "morphisms"}
  specification allows to provide alternative names.

  The logical characterization of @{command typedef} uses the predicate of
  locale const‹type_definition› that is defined in Isabelle/HOL. Various
  basic consequences of that are instantiated accordingly, re-using the locale
  facts with names derived from the new type constructor. Thus the generic
  theorem @{thm type_definition.Rep} is turned into the specific ‹Rep_t›, for
  example.

  Theorems @{thm type_definition.Rep}, @{thm type_definition.Rep_inverse}, and
  @{thm type_definition.Abs_inverse} provide the most basic characterization
  as a corresponding injection/surjection pair (in both directions). The
  derived rules @{thm type_definition.Rep_inject} and @{thm
  type_definition.Abs_inject} provide a more convenient version of
  injectivity, suitable for automated proof tools (e.g.\ in declarations
  involving @{attribute simp} or @{attribute iff}). Furthermore, the rules
  @{thm type_definition.Rep_cases}~/ @{thm type_definition.Rep_induct}, and
  @{thm type_definition.Abs_cases}~/ @{thm type_definition.Abs_induct} provide
  alternative views on surjectivity. These rules are already declared as set
  or type rules for the generic @{method cases} and @{method induct} methods,
  respectively.
›


subsubsection ‹Examples›

text ‹
  The following trivial example pulls a three-element type into existence
  within the formal logical environment of Isabelle/HOL.›

(*<*)experiment begin(*>*)
typedef three = "{(True, True), (True, False), (False, True)}"
  by blast

definition "One = Abs_three (True, True)"
definition "Two = Abs_three (True, False)"
definition "Three = Abs_three (False, True)"

lemma three_distinct: "One ≠ Two"  "One ≠ Three"  "Two ≠ Three"
  by (simp_all add: One_def Two_def Three_def Abs_three_inject)

lemma three_cases:
  fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
  by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
(*<*)end(*>*)

text ‹Note that such trivial constructions are better done with
  derived specification mechanisms such as @{command datatype}:›

(*<*)experiment begin(*>*)
datatype three = One | Two | Three
(*<*)end(*>*)

text ‹This avoids re-doing basic definitions and proofs from the
  primitive @{command typedef} above.›



section ‹Functorial structure of types›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "functor"} & : & ‹local_theory → proof(prove)›
  \end{matharray}

  rail‹
    @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
  ›

  ➧ @{command (HOL) "functor"}~‹prefix: m› allows to prove and register
  properties about the functorial structure of type constructors. These
  properties then can be used by other packages to deal with those type
  constructors in certain type constructions. Characteristic theorems are
  noted in the current local theory. By default, they are prefixed with the
  base name of the type constructor, an explicit prefix can be given
  alternatively.

  The given term ‹m› is considered as ∗‹mapper› for the corresponding type
  constructor and must conform to the following type pattern:

  \begin{matharray}{lll}
    ‹m› & ‹::› &
      ‹σ1 ⇒ … σk ⇒ (vecαn) t ⇒ (vecβn) t› \\
  \end{matharray}

  where ‹t› is the type constructor, ‹vecαn› and ‹vecβn› are
  distinct type variables free in the local theory and ‹σ1›, \ldots, ‹σk› is
  a subsequence of ‹α1 ⇒ β1›, ‹β1 ⇒ α1›, \ldots, ‹αn ⇒ βn›, ‹βn ⇒ αn›.
›


section ‹Quotient types with lifting and transfer›

text ‹
  The quotient package defines a new quotient type given a raw type and a
  partial equivalence relation (\secref{sec:quotient-type}). The package also
  historically includes automation for transporting definitions and theorems
  (\secref{sec:old-quotient}), but most of this automation was superseded by
  the Lifting (\secref{sec:lifting}) and Transfer (\secref{sec:transfer})
  packages.
›


subsection ‹Quotient type definition \label{sec:quotient-type}›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "quotient_type"} & : & ‹local_theory → proof(prove)›\\
  \end{matharray}

  rail‹
    @@{command (HOL) quotient_type} @{syntax "overloaded"}? ⏎
      @{syntax typespec} @{syntax mixfix}? '=' quot_type ⏎
      quot_morphisms? quot_parametric?
    ;
    quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
    ;
    quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
    ;
    quot_parametric: @'parametric' @{syntax thm}
  ›

  ➧ @{command (HOL) "quotient_type"} defines a new quotient type ‹τ›. The
  injection from a quotient type to a raw type is called ‹rep_τ›, its inverse
  ‹abs_τ› unless explicit @{keyword (HOL) "morphisms"} specification provides
  alternative names. @{command (HOL) "quotient_type"} requires the user to
  prove that the relation is an equivalence relation (predicate ‹equivp›),
  unless the user specifies explicitly ‹partial› in which case the obligation
  is ‹part_equivp›. A quotient defined with ‹partial› is weaker in the sense
  that less things can be proved automatically.

  The command internally proves a Quotient theorem and sets up the Lifting
  package by the command @{command (HOL) setup_lifting}. Thus the Lifting and
  Transfer packages can be used also with quotient types defined by @{command
  (HOL) "quotient_type"} without any extra set-up. The parametricity theorem
  for the equivalence relation R can be provided as an extra argument of the
  command and is passed to the corresponding internal call of @{command (HOL)
  setup_lifting}. This theorem allows the Lifting package to generate a
  stronger transfer rule for equality.
›


subsection ‹Lifting package \label{sec:lifting}›

text ‹
  The Lifting package allows users to lift terms of the raw type to the
  abstract type, which is a necessary step in building a library for an
  abstract type. Lifting defines a new constant by combining coercion
  functions (term‹Abs› and term‹Rep›) with the raw term. It also proves an
  appropriate transfer rule for the Transfer (\secref{sec:transfer}) package
  and, if possible, an equation for the code generator.

  The Lifting package provides two main commands: @{command (HOL)
  "setup_lifting"} for initializing the package to work with a new type, and
  @{command (HOL) "lift_definition"} for lifting constants. The Lifting
  package works with all four kinds of type abstraction: type copies,
  subtypes, total quotients and partial quotients.

  Theoretical background can be found in cite‹"Huffman-Kuncar:2013:lifting_transfer"›.

  \begin{matharray}{rcl}
    @{command_def (HOL) "setup_lifting"} & : & ‹local_theory → local_theory›\\
    @{command_def (HOL) "lift_definition"} & : & ‹local_theory → proof(prove)›\\
    @{command_def (HOL) "lifting_forget"} & : & ‹local_theory → local_theory›\\
    @{command_def (HOL) "lifting_update"} & : & ‹local_theory → local_theory›\\
    @{command_def (HOL) "print_quot_maps"} & : & ‹context →›\\
    @{command_def (HOL) "print_quotients"} & : & ‹context →›\\
    @{attribute_def (HOL) "quot_map"} & : & ‹attribute› \\
    @{attribute_def (HOL) "relator_eq_onp"} & : & ‹attribute› \\
    @{attribute_def (HOL) "relator_mono"} & : & ‹attribute› \\
    @{attribute_def (HOL) "relator_distr"} & : & ‹attribute› \\
    @{attribute_def (HOL) "quot_del"} & : & ‹attribute› \\
    @{attribute_def (HOL) "lifting_restore"} & : & ‹attribute› \\
  \end{matharray}

  rail‹
    @@{command (HOL) setup_lifting} @{syntax thm} @{syntax thm}? ⏎
      (@'parametric' @{syntax thm})?
    ;
    @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? ⏎
      @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} ⏎
      (@'parametric' (@{syntax thm}+))?
    ;
    @@{command (HOL) lifting_forget} @{syntax name}
    ;
    @@{command (HOL) lifting_update} @{syntax name}
    ;
    @@{attribute (HOL) lifting_restore}
      @{syntax thm} (@{syntax thm} @{syntax thm})?
  ›

  ➧ @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with
  a user-defined type. The command supports two modes.

    ▸ The first one is a low-level mode when the user must provide as a first
    argument of @{command (HOL) "setup_lifting"} a quotient theorem term‹Quotient R Abs Rep T›. The package configures a transfer rule for
    equality, a domain transfer rules and sets up the @{command_def (HOL)
    "lift_definition"} command to work with the abstract type. An optional
    theorem term‹reflp R›, which certifies that the equivalence relation R
    is total, can be provided as a second argument. This allows the package to
    generate stronger transfer rules. And finally, the parametricity theorem
    for term‹R› can be provided as a third argument. This allows the package
    to generate a stronger transfer rule for equality.

    Users generally will not prove the ‹Quotient› theorem manually for new
    types, as special commands exist to automate the process.

    ▸ When a new subtype is defined by @{command (HOL) typedef}, @{command
    (HOL) "lift_definition"} can be used in its second mode, where only the
    term‹type_definition› theorem term‹type_definition Rep Abs A› is
    used as an argument of the command. The command internally proves the
    corresponding term‹Quotient› theorem and registers it with @{command
    (HOL) setup_lifting} using its first mode.

  For quotients, the command @{command (HOL) quotient_type} can be used. The
  command defines a new quotient type and similarly to the previous case, the
  corresponding Quotient theorem is proved and registered by @{command (HOL)
  setup_lifting}.

  ┉
  The command @{command (HOL) "setup_lifting"} also sets up the code generator
  for the new type. Later on, when a new constant is defined by @{command
  (HOL) "lift_definition"}, the Lifting package proves and registers a code
  equation (if there is one) for the new constant.

  ➧ @{command (HOL) "lift_definition"} ‹f :: τ› @{keyword (HOL) "is"} ‹t›
  Defines a new function ‹f› with an abstract type ‹τ› in terms of a
  corresponding operation ‹t› on a representation type. More formally, if ‹t
  :: σ›, then the command builds a term ‹F› as a corresponding combination of
  abstraction and representation functions such that ‹F :: σ ⇒ τ› and defines
  ‹f ≡ F t›. The term ‹t› does not have to be necessarily a constant but it
  can be any term.

  The command opens a proof and the user must discharge a respectfulness proof
  obligation. For a type copy, i.e.\ a typedef with ‹UNIV›, the obligation is
  discharged automatically. The proof goal is presented in a user-friendly,
  readable form. A respectfulness theorem in the standard format ‹f.rsp› and a
  transfer rule ‹f.transfer› for the Transfer package are generated by the
  package.

  The user can specify a parametricity theorems for ‹t› after the keyword
  @{keyword "parametric"}, which allows the command to generate parametric
  transfer rules for ‹f›.

  For each constant defined through trivial quotients (type copies or
  subtypes) ‹f.rep_eq› is generated. The equation is a code certificate that
  defines ‹f› using the representation function.

  For each constant ‹f.abs_eq› is generated. The equation is unconditional for
  total quotients. The equation defines ‹f› using the abstraction function.

  ┉
  Integration with [@{attribute code} abstract]: For subtypes (e.g.\
  corresponding to a datatype invariant, such as typ‹'a dlist›), @{command
  (HOL) "lift_definition"} uses a code certificate theorem ‹f.rep_eq› as a
  code equation. Because of the limitation of the code generator, ‹f.rep_eq›
  cannot be used as a code equation if the subtype occurs inside the result
  type rather than at the top level (e.g.\ function returning typ‹'a dlist
  option› vs. typ‹'a dlist›).

  In this case, an extension of @{command (HOL) "lift_definition"} can be
  invoked by specifying the flag ‹code_dt›. This extension enables code
  execution through series of internal type and lifting definitions if the
  return type ‹τ› meets the following inductive conditions:

    ➧ ‹τ› is a type variable

    ➧ ‹τ = τ1 … τn κ›, where ‹κ› is an abstract type constructor and ‹τ1 …
    τn› do not contain abstract types (i.e.\ typ‹int dlist› is allowed
    whereas typ‹int dlist dlist› not)

    ➧ ‹τ = τ1 … τn κ›, ‹κ› is a type constructor that was defined as a
    (co)datatype whose constructor argument types do not contain either
    non-free datatypes or the function type.

  Integration with [@{attribute code} equation]: For total quotients,
  @{command (HOL) "lift_definition"} uses ‹f.abs_eq› as a code equation.

  ➧ @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} These
  two commands serve for storing and deleting the set-up of the Lifting
  package and corresponding transfer rules defined by this package. This is
  useful for hiding of type construction details of an abstract type when the
  construction is finished but it still allows additions to this construction
  when this is later necessary.

  Whenever the Lifting package is set up with a new abstract type ‹τ› by
  @{command_def (HOL) "lift_definition"}, the package defines a new bundle
  that is called ‹τ.lifting›. This bundle already includes set-up for the
  Lifting package. The new transfer rules introduced by @{command (HOL)
  "lift_definition"} can be stored in the bundle by the command @{command
  (HOL) "lifting_update"} ‹τ.lifting›.

  The command @{command (HOL) "lifting_forget"} ‹τ.lifting› deletes set-up of
  the Lifting package for ‹τ› and deletes all the transfer rules that were
  introduced by @{command (HOL) "lift_definition"} using ‹τ› as an abstract
  type.

  The stored set-up in a bundle can be reintroduced by the Isar commands for
  including a bundle (@{command "include"}, @{keyword "includes"} and
  @{command "including"}).

  ➧ @{command (HOL) "print_quot_maps"} prints stored quotient map theorems.

  ➧ @{command (HOL) "print_quotients"} prints stored quotient theorems.

  ➧ @{attribute (HOL) quot_map} registers a quotient map theorem, a theorem
  showing how to ``lift'' quotients over type constructors. E.g.\ term‹Quotient R Abs Rep T ⟹ Quotient (rel_set R) (image Abs) (image Rep)
  (rel_set T)›. For examples see 🗏‹~~/src/HOL/Lifting_Set.thy› or
  🗏‹~~/src/HOL/Lifting.thy›. This property is proved automatically if the
  involved type is BNF without dead variables.

  ➧ @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a
  relator applied to an equality restricted by a predicate term‹P› (i.e.\
  term‹eq_onp P›) is equal to a predicator applied to the term‹P›. The
  combinator const‹eq_onp› is used for internal encoding of proper subtypes.
  Such theorems allows the package to hide ‹eq_onp› from a user in a
  user-readable form of a respectfulness theorem. For examples see
  🗏‹~~/src/HOL/Lifting_Set.thy› or 🗏‹~~/src/HOL/Lifting.thy›. This property
  is proved automatically if the involved type is BNF without dead variables.

  ➧ @{attribute (HOL) "relator_mono"} registers a property describing a
  monotonicity of a relator. E.g.\ prop‹A ≤ B ⟹ rel_set A ≤ rel_set B›.
  This property is needed for proving a stronger transfer rule in
  @{command_def (HOL) "lift_definition"} when a parametricity theorem for the
  raw term is specified and also for the reflexivity prover. For examples see
  🗏‹~~/src/HOL/Lifting_Set.thy› or 🗏‹~~/src/HOL/Lifting.thy›. This property
  is proved automatically if the involved type is BNF without dead variables.

  ➧ @{attribute (HOL) "relator_distr"} registers a property describing a
  distributivity of the relation composition and a relator. E.g.\ ‹rel_set R
  ∘∘ rel_set S = rel_set (R ∘∘ S)›. This property is needed for proving a
  stronger transfer rule in @{command_def (HOL) "lift_definition"} when a
  parametricity theorem for the raw term is specified. When this equality does
  not hold unconditionally (e.g.\ for the function type), the user can
  specified each direction separately and also register multiple theorems with
  different set of assumptions. This attribute can be used only after the
  monotonicity property was already registered by @{attribute (HOL)
  "relator_mono"}. For examples see 🗏‹~~/src/HOL/Lifting_Set.thy› or
  🗏‹~~/src/HOL/Lifting.thy›. This property is proved automatically if the
  involved type is BNF without dead variables.

  ➧ @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from
  the Lifting infrastructure and thus de-register the corresponding quotient.
  This effectively causes that @{command (HOL) lift_definition} will not do
  any lifting for the corresponding type. This attribute is rather used for
  low-level manipulation with set-up of the Lifting package because @{command
  (HOL) lifting_forget} is preferred for normal usage.

  ➧ @{attribute (HOL) lifting_restore} ‹Quotient_thm pcr_def pcr_cr_eq_thm›
  registers the Quotient theorem ‹Quotient_thm› in the Lifting infrastructure
  and thus sets up lifting for an abstract type ‹τ› (that is defined by
  ‹Quotient_thm›). Optional theorems ‹pcr_def› and ‹pcr_cr_eq_thm› can be
  specified to register the parametrized correspondence relation for ‹τ›.
  E.g.\ for typ‹'a dlist›, ‹pcr_def› is ‹pcr_dlist A ≡ list_all2 A ∘∘
  cr_dlist› and ‹pcr_cr_eq_thm› is ‹pcr_dlist (=) = (=)›. This attribute
  is rather used for low-level manipulation with set-up of the Lifting package
  because using of the bundle ‹τ.lifting› together with the commands @{command
  (HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
  normal usage.

  ➧ Integration with the BNF package cite‹"isabelle-datatypes"›: As already
  mentioned, the theorems that are registered by the following attributes are
  proved and registered automatically if the involved type is BNF without dead
  variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
  @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also
  the definition of a relator and predicator is provided automatically.
  Moreover, if the BNF represents a datatype, simplification rules for a
  predicator are again proved automatically.
›


subsection ‹Transfer package \label{sec:transfer}›

text ‹
  \begin{matharray}{rcl}
    @{method_def (HOL) "transfer"} & : & ‹method› \\
    @{method_def (HOL) "transfer'"} & : & ‹method› \\
    @{method_def (HOL) "transfer_prover"} & : & ‹method› \\
    @{attribute_def (HOL) "Transfer.transferred"} & : & ‹attribute› \\
    @{attribute_def (HOL) "untransferred"} & : & ‹attribute› \\
    @{method_def (HOL) "transfer_start"} & : & ‹method› \\
    @{method_def (HOL) "transfer_prover_start"} & : & ‹method› \\
    @{method_def (HOL) "transfer_step"} & : & ‹method› \\
    @{method_def (HOL) "transfer_end"} & : & ‹method› \\
    @{method_def (HOL) "transfer_prover_end"} & : & ‹method› \\
    @{attribute_def (HOL) "transfer_rule"} & : & ‹attribute› \\
    @{attribute_def (HOL) "transfer_domain_rule"} & : & ‹attribute› \\
    @{attribute_def (HOL) "relator_eq"} & : & ‹attribute› \\
    @{attribute_def (HOL) "relator_domain"} & : & ‹attribute› \\
  \end{matharray}

  ➧ @{method (HOL) "transfer"} method replaces the current subgoal with a
  logically equivalent one that uses different types and constants. The
  replacement of types and constants is guided by the database of transfer
  rules. Goals are generalized over all free variables by default; this is
  necessary for variables whose types change, but can be overridden for
  specific variables with e.g. ‹transfer fixing: x y z›.

  ➧ @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer} that
  allows replacing a subgoal with one that is logically stronger (rather than
  equivalent). For example, a subgoal involving equality on a quotient type
  could be replaced with a subgoal involving equality (instead of the
  corresponding equivalence relation) on the underlying raw type.

  ➧ @{method (HOL) "transfer_prover"} method assists with proving a transfer
  rule for a new constant, provided the constant is defined in terms of other
  constants that already have transfer rules. It should be applied after
  unfolding the constant definitions.

  ➧ @{method (HOL) "transfer_start"}, @{method (HOL) "transfer_step"},
  @{method (HOL) "transfer_end"}, @{method (HOL) "transfer_prover_start"} and
  @{method (HOL) "transfer_prover_end"} methods are meant to be used for
  debugging of @{method (HOL) "transfer"} and @{method (HOL)
  "transfer_prover"}, which we can decompose as follows: @{method (HOL)
  "transfer"} = (@{method (HOL) "transfer_start"}, @{method (HOL)
  "transfer_step"}+, @{method (HOL) "transfer_end"}) and @{method (HOL)
  "transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, @{method
  (HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}). For usage
  examples see 🗏‹~~/src/HOL/ex/Transfer_Debug.thy›.

  ➧ @{attribute (HOL) "untransferred"} proves the same equivalent theorem as
  @{method (HOL) "transfer"} internally does.

  ➧ @{attribute (HOL) Transfer.transferred} works in the opposite direction
  than @{method (HOL) "transfer'"}. E.g.\ given the transfer relation ‹ZN x n
  ≡ (x = int n)›, corresponding transfer rules and the theorem ‹∀x::int ∈
  {0..}. x < x + 1›, the attribute would prove ‹∀n::nat. n < n + 1›. The
  attribute is still in experimental phase of development.

  ➧ @{attribute (HOL) "transfer_rule"} attribute maintains a collection of
  transfer rules, which relate constants at two different types. Typical
  transfer rules may relate different type instances of the same polymorphic
  constant, or they may relate an operation on a raw type to a corresponding
  operation on an abstract type (quotient or subtype). For example:

    ‹((A ===> B) ===> list_all2 A ===> list_all2 B) map map› \\
    ‹(cr_int ===> cr_int ===> cr_int) (λ(x,y) (u,v). (x+u, y+v)) plus›

  Lemmas involving predicates on relations can also be registered using the
  same attribute. For example:

    ‹bi_unique A ⟹ (list_all2 A ===> (=)) distinct distinct› \\
    ‹⟦bi_unique A; bi_unique B⟧ ⟹ bi_unique (rel_prod A B)›

  Preservation of predicates on relations (‹bi_unique, bi_total, right_unique,
  right_total, left_unique, left_total›) with the respect to a relator is
  proved automatically if the involved type is BNF cite‹"isabelle-datatypes"› without dead variables.

  ➧ @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
  of rules, which specify a domain of a transfer relation by a predicate.
  E.g.\ given the transfer relation ‹ZN x n ≡ (x = int n)›, one can register
  the following transfer domain rule: ‹Domainp ZN = (λx. x ≥ 0)›. The rules
  allow the package to produce more readable transferred goals, e.g.\ when
  quantifiers are transferred.

  ➧ @{attribute (HOL) relator_eq} attribute collects identity laws for
  relators of various type constructors, e.g. term‹rel_set (=) = (=)›.
  The @{method (HOL) transfer} method uses these lemmas to infer
  transfer rules for non-polymorphic constants on the fly. For examples see
  🗏‹~~/src/HOL/Lifting_Set.thy› or 🗏‹~~/src/HOL/Lifting.thy›. This property
  is proved automatically if the involved type is BNF without dead variables.

  ➧ @{attribute_def (HOL) "relator_domain"} attribute collects rules
  describing domains of relators by predicators. E.g.\ term‹Domainp
  (rel_set T) = (λA. Ball A (Domainp T))›. This allows the package to lift
  transfer domain rules through type constructors. For examples see
  🗏‹~~/src/HOL/Lifting_Set.thy› or 🗏‹~~/src/HOL/Lifting.thy›. This property
  is proved automatically if the involved type is BNF without dead variables.


  Theoretical background can be found in cite‹"Huffman-Kuncar:2013:lifting_transfer"›.
›


subsection ‹Old-style definitions for quotient types \label{sec:old-quotient}›

text ‹
  \begin{matharray}{rcl}
    @{command_def (HOL) "quotient_definition"} & : & ‹local_theory → proof(prove)›\\
    @{command_def (HOL) "print_quotmapsQ3"} & : & ‹context →›\\
    @{command_def (HOL) "print_quotientsQ3"} & : & ‹context →›\\
    @{command_def (HOL) "print_quotconsts"} & : & ‹context →›\\
    @{method_def (HOL) "lifting"} & : & ‹method› \\
    @{method_def (HOL) "lifting_setup"} & : & ‹method› \\
    @{method_def (HOL) "descending"} & : & ‹method› \\
    @{method_def (HOL) "descending_setup"} & : & ‹method› \\
    @{method_def (HOL) "partiality_descending"} & : & ‹method› \\
    @{method_def (HOL) "partiality_descending_setup"} & : & ‹method› \\
    @{method_def (HOL) "regularize"} & : & ‹method› \\
    @{method_def (HOL) "injection"} & : & ‹method› \\
    @{method_def (HOL) "cleaning"} & : & ‹method› \\
    @{attribute_def (HOL) "quot_thm"} & : & ‹attribute› \\
    @{attribute_def (HOL) "quot_lifted"} & : & ‹attribute› \\
    @{attribute_def (HOL) "quot_respect"} & : & ‹attribute› \\
    @{attribute_def (HOL) "quot_preserve"} & : & ‹attribute› \\
  \end{matharray}

  rail‹
    @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? ⏎
    @{syntax term} 'is' @{syntax term}
    ;
    constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
    ;
    @@{method (HOL) lifting} @{syntax thms}?
    ;
    @@{method (HOL) lifting_setup} @{syntax thms}?
  ›

  ➧ @{command (HOL) "quotient_definition"} defines a constant on the quotient
  type.

  ➧ @{command (HOL) "print_quotmapsQ3"} prints quotient map functions.

  ➧ @{command (HOL) "print_quotientsQ3"} prints quotients.

  ➧ @{command (HOL) "print_quotconsts"} prints quotient constants.

  ➧ @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"} methods
  match the current goal with the given raw theorem to be lifted producing
  three new subgoals: regularization, injection and cleaning subgoals.
  @{method (HOL) "lifting"} tries to apply the heuristics for automatically
  solving these three subgoals and leaves only the subgoals unsolved by the
  heuristics to the user as opposed to @{method (HOL) "lifting_setup"} which
  leaves the three subgoals unsolved.

  ➧ @{method (HOL) "descending"} and @{method (HOL) "descending_setup"} try to
  guess a raw statement that would lift to the current subgoal. Such statement
  is assumed as a new subgoal and @{method (HOL) "descending"} continues in
  the same way as @{method (HOL) "lifting"} does. @{method (HOL) "descending"}
  tries to solve the arising regularization, injection and cleaning subgoals
  with the analogous method @{method (HOL) "descending_setup"} which leaves
  the four unsolved subgoals.

  ➧ @{method (HOL) "partiality_descending"} finds the regularized theorem that
  would lift to the current subgoal, lifts it and leaves as a subgoal. This
  method can be used with partial equivalence quotients where the non
  regularized statements would not be true. @{method (HOL)
  "partiality_descending_setup"} leaves the injection and cleaning subgoals
  unchanged.

  ➧ @{method (HOL) "regularize"} applies the regularization heuristics to the
  current subgoal.

  ➧ @{method (HOL) "injection"} applies the injection heuristics to the
  current goal using the stored quotient respectfulness theorems.

  ➧ @{method (HOL) "cleaning"} applies the injection cleaning heuristics to
  the current subgoal using the stored quotient preservation theorems.

  ➧ @{attribute (HOL) quot_lifted} attribute tries to automatically transport
  the theorem to the quotient type. The attribute uses all the defined
  quotients types and quotient constants often producing undesired results or
  theorems that cannot be lifted.

  ➧ @{attribute (HOL) quot_respect} and @{attribute (HOL) quot_preserve}
  attributes declare a theorem as a respectfulness and preservation theorem
  respectively. These are stored in the local theory store and used by the
  @{method (HOL) "injection"} and @{method (HOL) "cleaning"} methods
  respectively.

  ➧ @{attribute (HOL) quot_thm} declares that a certain theorem is a quotient
  extension theorem. Quotient extension theorems allow for quotienting inside
  container types. Given a polymorphic type that serves as a container, a map
  function defined for this container using @{command (HOL) "functor"} and a
  relation map defined for for the container type, the quotient extension
  theorem should be term‹Quotient3 R Abs Rep ⟹ Quotient3 (rel_map R) (map
  Abs) (map Rep)›. Quotient extension theorems are stored in a database and
  are used all the steps of lifting theorems.
›


chapter ‹Proof tools›

section ‹Proving propositions›

text ‹
  In addition to the standard proof methods, a number of diagnosis tools
  search for proofs and provide an Isar proof snippet on success. These tools
  are available via the following commands.

  \begin{matharray}{rcl}
    @{command_def (HOL) "solve_direct"}‹*› & : & ‹proof →› \\
    @{command_def (HOL) "try"}‹*› & : & ‹proof →› \\
    @{command_def (HOL) "try0"}‹*› & : & ‹proof →› \\
    @{command_def (HOL) "sledgehammer"}‹*› & : & ‹proof →› \\
    @{command_def (HOL) "sledgehammer_params"} & : & ‹theory → theory›
  \end{matharray}

  rail‹
    @@{command (HOL) try}
    ;

    @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
      @{syntax nat}?
    ;

    @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
    ;

    @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
    ;
    args: ( @{syntax name} '=' value + ',' )
    ;
    facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thms} ) + ) ? ')'
  › % FIXME check args "value"

  ➧ @{command (HOL) "solve_direct"} checks whether the current subgoals can be
  solved directly by an existing theorem. Duplicate lemmas can be detected in
  this way.

  ➧ @{command (HOL) "try0"} attempts to prove a subgoal using a combination of
  standard proof methods (@{method auto}, @{method simp}, @{method blast},
  etc.). Additional facts supplied via ‹simp:›, ‹intro:›, ‹elim:›, and ‹dest:›
  are passed to the appropriate proof methods.

  ➧ @{command (HOL) "try"} attempts to prove or disprove a subgoal using a
  combination of provers and disprovers (@{command (HOL) "solve_direct"},
  @{command (HOL) "quickcheck"}, @{command (HOL) "try0"}, @{command (HOL)
  "sledgehammer"}, @{command (HOL) "nitpick"}).

  ➧ @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
  automatic provers (resolution provers and SMT solvers). See the Sledgehammer
  manual cite‹"isabelle-sledgehammer"› for details.

  ➧ @{command (HOL) "sledgehammer_params"} changes @{command (HOL)
  "sledgehammer"} configuration options persistently.
›


section ‹Checking and refuting propositions›

text ‹
  Identifying incorrect propositions usually involves evaluation of particular
  assignments and systematic counterexample search. This is supported by the
  following commands.

  \begin{matharray}{rcl}
    @{command_def (HOL) "value"}‹*› & : & ‹context →› \\
    @{command_def (HOL) "values"}‹*› & : & ‹context →› \\
    @{command_def (HOL) "quickcheck"}‹*› & : & ‹proof →› \\
    @{command_def (HOL) "nitpick"}‹*› & : & ‹proof →› \\
    @{command_def (HOL) "quickcheck_params"} & : & ‹theory → theory› \\
    @{command_def (HOL) "nitpick_params"} & : & ‹theory → theory› \\
    @{command_def (HOL) "quickcheck_generator"} & : & ‹theory → theory› \\
    @{command_def (HOL) "find_unused_assms"} & : & ‹context →›
  \end{matharray}

  rail‹
    @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
    ;

    @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
    ;

    (@@{command (HOL) quickcheck} | @@{command (HOL) nitpick})
      ( '[' args ']' )? @{syntax nat}?
    ;

    (@@{command (HOL) quickcheck_params} |
      @@{command (HOL) nitpick_params}) ( '[' args ']' )?
    ;

    @@{command (HOL) quickcheck_generator} @{syntax name} ⏎
      'operations:' ( @{syntax term} +)
    ;

    @@{command (HOL) find_unused_assms} @{syntax name}?
    ;
    modes: '(' (@{syntax name} +) ')'
    ;
    args: ( @{syntax name} '=' value + ',' )
  › % FIXME check "value"

  ➧ @{command (HOL) "value"}~‹t› evaluates and prints a term; optionally
  ‹modes› can be specified, which are appended to the current print mode; see
  \secref{sec:print-modes}. Evaluation is tried first using ML, falling back
  to normalization by evaluation if this fails. Alternatively a specific
  evaluator can be selected using square brackets; typical evaluators use the
  current set of code equations to normalize and include ‹simp› for fully
  symbolic evaluation using the simplifier, ‹nbe› for ∗‹normalization by
  evaluation› and ∗‹code› for code generation in SML.

  ➧ @{command (HOL) "values"}~‹t› enumerates a set comprehension by evaluation
  and prints its values up to the given number of solutions; optionally
  ‹modes› can be specified, which are appended to the current print mode; see
  \secref{sec:print-modes}.

  ➧ @{command (HOL) "quickcheck"} tests the current goal for counterexamples
  using a series of assignments for its free variables; by default the first
  subgoal is tested, an other can be selected explicitly using an optional
  goal index. Assignments can be chosen exhausting the search space up to a
  given size, or using a fixed number of random assignments in the search
  space, or exploring the search space symbolically using narrowing. By
  default, quickcheck uses exhaustive testing. A number of configuration
  options are supported for @{command (HOL) "quickcheck"}, notably:

    ➧[‹tester›] specifies which testing approach to apply. There are three
    testers, ‹exhaustive›, ‹random›, and ‹narrowing›. An unknown configuration
    option is treated as an argument to tester, making ‹tester =› optional.
    When multiple testers are given, these are applied in parallel. If no
    tester is specified, quickcheck uses the testers that are set active,
    i.e.\ configurations @{attribute quickcheck_exhaustive_active},
    @{attribute quickcheck_random_active}, @{attribute
    quickcheck_narrowing_active} are set to true.

    ➧[‹size›] specifies the maximum size of the search space for assignment
    values.

    ➧[‹genuine_only›] sets quickcheck only to return genuine counterexample,
    but not potentially spurious counterexamples due to underspecified
    functions.

    ➧[‹abort_potential›] sets quickcheck to abort once it found a potentially
    spurious counterexample and to not continue to search for a further
    genuine counterexample. For this option to be effective, the
    ‹genuine_only› option must be set to false.

    ➧[‹eval›] takes a term or a list of terms and evaluates these terms under
    the variable assignment found by quickcheck. This option is currently only
    supported by the default (exhaustive) tester.

    ➧[‹iterations›] sets how many sets of assignments are generated for each
    particular size.

    ➧[‹no_assms›] specifies whether assumptions in structured proofs should be
    ignored.

    ➧[‹locale›] specifies how to process conjectures in a locale context,
    i.e.\ they can be interpreted or expanded. The option is a
    whitespace-separated list of the two words ‹interpret› and ‹expand›. The
    list determines the order they are employed. The default setting is to
    first use interpretations and then test the expanded conjecture. The
    option is only provided as attribute declaration, but not as parameter to
    the command.

    ➧[‹timeout›] sets the time limit in seconds.

    ➧[‹default_type›] sets the type(s) generally used to instantiate type
    variables.

    ➧[‹report›] if set quickcheck reports how many tests fulfilled the
    preconditions.

    ➧[‹use_subtype›] if set quickcheck automatically lifts conjectures to
    registered subtypes if possible, and tests the lifted conjecture.

    ➧[‹quiet›] if set quickcheck does not output anything while testing.

    ➧[‹verbose›] if set quickcheck informs about the current size and
    cardinality while testing.

    ➧[‹expect›] can be used to check if the user's expectation was met
    (‹no_expectation›, ‹no_counterexample›, or ‹counterexample›).

  These option can be given within square brackets.

  Using the following type classes, the testers generate values and convert
  them back into Isabelle terms for displaying counterexamples.

    ➧[‹exhaustive›] The parameters of the type classes class‹exhaustive› and
    class‹full_exhaustive› implement the testing. They take a testing
    function as a parameter, which takes a value of type typ‹'a› and
    optionally produces a counterexample, and a size parameter for the test
    values. In class‹full_exhaustive›, the testing function parameter
    additionally expects a lazy term reconstruction in the type typ‹Code_Evaluation.term› of the tested value.

    The canonical implementation for ‹exhaustive› testers calls the given
    testing function on all values up to the given size and stops as soon as a
    counterexample is found.

    ➧[‹random›] The operation const‹Quickcheck_Random.random› of the type
    class class‹random› generates a pseudo-random value of the given size
    and a lazy term reconstruction of the value in the type typ‹Code_Evaluation.term›. A pseudo-randomness generator is defined in theory
    theory‹HOL.Random›.

    ➧[‹narrowing›] implements Haskell's Lazy Smallcheck cite‹"runciman-naylor-lindblad"› using the type classes class‹narrowing› and
    class‹partial_term_of›. Variables in the current goal are initially
    represented as symbolic variables. If the execution of the goal tries to
    evaluate one of them, the test engine replaces it with refinements
    provided by const‹narrowing›. Narrowing views every value as a
    sum-of-products which is expressed using the operations const‹Quickcheck_Narrowing.cons› (embedding a value), const‹Quickcheck_Narrowing.apply› (product) and const‹Quickcheck_Narrowing.sum› (sum). The refinement should enable further
    evaluation of the goal.

    For example, const‹narrowing› for the list type typ‹'a :: narrowing list›
    can be recursively defined as
    term‹Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
              (Quickcheck_Narrowing.apply
                (Quickcheck_Narrowing.apply
                  (Quickcheck_Narrowing.cons (#))
                  narrowing)
                narrowing)›.
    If a symbolic variable of type typ‹_ list› is evaluated, it is
    replaced by (i)~the empty list term‹[]› and (ii)~by a non-empty list
    whose head and tail can then be recursively refined if needed.

    To reconstruct counterexamples, the operation const‹partial_term_of›
    transforms ‹narrowing›'s deep representation of terms to the type typ‹Code_Evaluation.term›. The deep representation models symbolic variables
    as const‹Quickcheck_Narrowing.Narrowing_variable›, which are normally
    converted to const‹Code_Evaluation.Free›, and refined values as term‹Quickcheck_Narrowing.Narrowing_constructor i args›, where term‹i ::
    integer› denotes the index in the sum of refinements. In the above
    example for lists, term‹0› corresponds to term‹[]› and term‹1›
    to term‹(#)›.

    The command @{command (HOL) "code_datatype"} sets up const‹partial_term_of› such that the term‹i›-th refinement is interpreted as
    the term‹i›-th constructor, but it does not ensures consistency with
    const‹narrowing›.

  ➧ @{command (HOL) "quickcheck_params"} changes @{command (HOL) "quickcheck"}
  configuration options persistently.

  ➧ @{command (HOL) "quickcheck_generator"} creates random and exhaustive
  value generators for a given type and operations. It generates values by
  using the operations as if they were constructors of that type.

  ➧ @{command (HOL) "nitpick"} tests the current goal for counterexamples
  using a reduction to first-order relational logic. See the Nitpick manual
  cite‹"isabelle-nitpick"› for details.

  ➧ @{command (HOL) "nitpick_params"} changes @{command (HOL) "nitpick"}
  configuration options persistently.

  ➧ @{command (HOL) "find_unused_assms"} finds potentially superfluous
  assumptions in theorems using quickcheck. It takes the theory name to be
  checked for superfluous assumptions as optional argument. If not provided,
  it checks the current theory. Options to the internal quickcheck invocations
  can be changed with common configuration declarations.
›


section ‹Coercive subtyping›

text ‹
  \begin{matharray}{rcl}
    @{attribute_def (HOL) coercion} & : & ‹attribute› \\
    @{attribute_def (HOL) coercion_delete} & : & ‹attribute› \\
    @{attribute_def (HOL) coercion_enabled} & : & ‹attribute› \\
    @{attribute_def (HOL) coercion_map} & : & ‹attribute› \\
    @{attribute_def (HOL) coercion_args} & : & ‹attribute› \\
  \end{matharray}

  Coercive subtyping allows the user to omit explicit type conversions, also
  called ∗‹coercions›. Type inference will add them as necessary when parsing
  a term. See cite‹"traytel-berghofer-nipkow-2011"› for details.

  rail‹
    @@{attribute (HOL) coercion} (@{syntax term})
    ;
    @@{attribute (HOL) coercion_delete} (@{syntax term})
    ;
    @@{attribute (HOL) coercion_map} (@{syntax term})
    ;
    @@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+)
  ›

  ➧ @{attribute (HOL) "coercion"}~‹f› registers a new coercion function ‹f ::
  σ1 ⇒ σ2› where ‹σ1› and ‹σ2› are type constructors without arguments.
  Coercions are composed by the inference algorithm if needed. Note that the
  type inference algorithm is complete only if the registered coercions form a
  lattice.

  ➧ @{attribute (HOL) "coercion_delete"}~‹f› deletes a preceding declaration
  (using @{attribute (HOL) "coercion"}) of the function ‹f :: σ1 ⇒ σ2› as a
  coercion.

  ➧ @{attribute (HOL) "coercion_map"}~‹map› registers a new map function to
  lift coercions through type constructors. The function ‹map› must conform to
  the following type pattern

  \begin{matharray}{lll}
    ‹map› & ‹::› &
      ‹f1 ⇒ … ⇒ fn ⇒ (α1, …, αn) t ⇒ (β1, …, βn) t› \\
  \end{matharray}

  where ‹t› is a type constructor and ‹fi› is of type ‹αi ⇒ βi› or ‹βi ⇒
  αi›. Registering a map function overwrites any existing map function for
  this particular type constructor.

  ➧ @{attribute (HOL) "coercion_args"} can be used to disallow coercions to be
  inserted in certain positions in a term. For example, given the constant ‹c
  :: σ1 ⇒ σ2 ⇒ σ3 ⇒ σ4› and the list of policies ‹- + 0› as arguments,
  coercions will not be inserted in the first argument of ‹c› (policy ‹-›);
  they may be inserted in the second argument (policy ‹+›) even if the
  constant ‹c› itself is in a position where coercions are disallowed; the
  third argument inherits the allowance of coercsion insertion from the
  position of the constant ‹c› (policy ‹0›). The standard usage of policies is
  the definition of syntatic constructs (usually extralogical, i.e., processed
  and stripped during type inference), that should not be destroyed by the
  insertion of coercions (see, for example, the setup for the case syntax in
  theory‹HOL.Ctr_Sugar›).

  ➧ @{attribute (HOL) "coercion_enabled"} enables the coercion inference
  algorithm.
›


section ‹Arithmetic proof support›

text ‹
  \begin{matharray}{rcl}
    @{method_def (HOL) arith} & : & ‹method› \\
    @{attribute_def (HOL) arith} & : & ‹attribute› \\
    @{attribute_def (HOL) linarith_split} & : & ‹attribute› \\
  \end{matharray}

  ➧ @{method (HOL) arith} decides linear arithmetic problems (on types ‹nat›,
  ‹int›, ‹real›). Any current facts are inserted into the goal before running
  the procedure.

  ➧ @{attribute (HOL) arith} declares facts that are supplied to the
  arithmetic provers implicitly.

  ➧ @{attribute (HOL) linarith_split} attribute declares case split rules to be
  expanded before @{method (HOL) arith} is invoked.


  Note that a simpler (but faster) arithmetic prover is already invoked by the
  Simplifier.
›


section ‹Intuitionistic proof search›

text ‹
  \begin{matharray}{rcl}
    @{method_def (HOL) iprover} & : & ‹method› \\
  \end{matharray}

  rail‹
    @@{method (HOL) iprover} (@{syntax rulemod} *)
  ›

  ➧ @{method (HOL) iprover} performs intuitionistic proof search, depending on
  specifically declared rules from the context, or given as explicit
  arguments. Chained facts are inserted into the goal before commencing proof
  search.

  Rules need to be classified as @{attribute (Pure) intro}, @{attribute (Pure)
  elim}, or @{attribute (Pure) dest}; here the ``‹!›'' indicator refers to
  ``safe'' rules, which may be applied aggressively (without considering
  back-tracking later). Rules declared with ``‹?›'' are ignored in proof
  search (the single-step @{method (Pure) rule} method still observes these).
  An explicit weight annotation may be given as well; otherwise the number of
  rule premises will be taken into account here.
›


section ‹Model Elimination and Resolution›

text ‹
  \begin{matharray}{rcl}
    @{method_def (HOL) "meson"} & : & ‹method› \\
    @{method_def (HOL) "metis"} & : & ‹method› \\
  \end{matharray}

  rail‹
    @@{method (HOL) meson} @{syntax thms}?
    ;
    @@{method (HOL) metis}
      ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
      @{syntax thms}?
  ›

  ➧ @{method (HOL) meson} implements Loveland's model elimination procedure
  cite‹"loveland-78"›. See 🗏‹~~/src/HOL/ex/Meson_Test.thy› for examples.

  ➧ @{method (HOL) metis} combines ordered resolution and ordered
  paramodulation to find first-order (or mildly higher-order) proofs. The
  first optional argument specifies a type encoding; see the Sledgehammer
  manual cite‹"isabelle-sledgehammer"› for details. The directory
  🗀‹~~/src/HOL/Metis_Examples› contains several small theories developed to a
  large extent using @{method (HOL) metis}.
›


section ‹Algebraic reasoning via Gröbner bases›

text ‹
  \begin{matharray}{rcl}
    @{method_def (HOL) "algebra"} & : & ‹method› \\
    @{attribute_def (HOL) algebra} & : & ‹attribute› \\
  \end{matharray}

  rail‹
    @@{method (HOL) algebra}
      ('add' ':' @{syntax thms})?
      ('del' ':' @{syntax thms})?
    ;
    @@{attribute (HOL) algebra} (() | 'add' | 'del')
  ›

  ➧ @{method (HOL) algebra} performs algebraic reasoning via Gröbner bases,
  see also cite‹"Chaieb-Wenzel:2007"› and cite‹‹\S3.2› in "Chaieb-thesis"›.
  The method handles deals with two main classes of problems:

    ▸ Universal problems over multivariate polynomials in a
    (semi)-ring/field/idom; the capabilities of the method are augmented
    according to properties of these structures. For this problem class the
    method is only complete for algebraically closed fields, since the
    underlying method is based on Hilbert's Nullstellensatz, where the
    equivalence only holds for algebraically closed fields.

    The problems can contain equations ‹p = 0› or inequations ‹q ≠ 0› anywhere
    within a universal problem statement.

    ▸ All-exists problems of the following restricted (but useful) form:

    @{text [display] "∀x1 … xn.
      e1(x1, …, xn) = 0 ∧ … ∧ em(x1, …, xn) = 0 ⟶
      (∃y1 … yk.
        p11(x1, … ,xn) * y1 + … + p1k(x1, …, xn) * yk = 0 ∧
        … ∧
        pt1(x1, …, xn) * y1 + … + ptk(x1, …, xn) * yk = 0)"}

    Here ‹e1, …, en› and the ‹pij› are multivariate polynomials only in
    the variables mentioned as arguments.

  The proof method is preceded by a simplification step, which may be modified
  by using the form ‹(algebra add: ths1 del: ths2)›. This acts like
  declarations for the Simplifier (\secref{sec:simplifier}) on a private
  simpset for this tool.

  ➧ @{attribute algebra} (as attribute) manages the default collection of
  pre-simplification rules of the above proof method.
›


subsubsection ‹Example›

text ‹
  The subsequent example is from geometry: collinearity is invariant by
  rotation.
›

(*<*)experiment begin(*>*)
type_synonym point = "int × int"

fun collinear :: "point ⇒ point ⇒ point ⇒ bool" where
  "collinear (Ax, Ay) (Bx, By) (Cx, Cy) ⟷
    (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"

lemma collinear_inv_rotation:
  assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c2 + s2 = 1"
  shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
    (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
  using assms by (algebra add: collinear.simps)
(*<*)end(*>*)

text ‹
  See also 🗏‹~~/src/HOL/Examples/Groebner_Examples.thy›.
›


section ‹Coherent Logic›

text ‹
  \begin{matharray}{rcl}
    @{method_def (HOL) "coherent"} & : & ‹method› \\
  \end{matharray}

  rail‹
    @@{method (HOL) coherent} @{syntax thms}?
  ›

  ➧ @{method (HOL) coherent} solves problems of ∗‹Coherent Logic› cite‹"Bezem-Coquand:2005"›, which covers applications in confluence theory,
  lattice theory and projective geometry. See 🗏‹~~/src/HOL/Examples/Coherent.thy›
  for some examples.
›


section ‹Unstructured case analysis and induction \label{sec:hol-induct-tac}›

text ‹
  The following tools of Isabelle/HOL support cases analysis and induction in
  unstructured tactic scripts; see also \secref{sec:cases-induct} for proper
  Isar versions of similar ideas.

  \begin{matharray}{rcl}
    @{method_def (HOL) case_tac}‹*› & : & ‹method› \\
    @{method_def (HOL) induct_tac}‹*› & : & ‹method› \\
    @{method_def (HOL) ind_cases}‹*› & : & ‹method› \\
    @{command_def (HOL) "inductive_cases"}‹*› & : & ‹local_theory → local_theory› \\
  \end{matharray}

  rail‹
    @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
    ;
    @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
    ;
    @@{method (HOL) ind_cases} (@{syntax prop}+) @{syntax for_fixes}
    ;
    @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
    ;
    rule: 'rule' ':' @{syntax thm}
  ›

  ➧ @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit to reason
  about inductive types. Rules are selected according to the declarations by
  the @{attribute cases} and @{attribute induct} attributes, cf.\
  \secref{sec:cases-induct}. The @{command (HOL) datatype} package already
  takes care of this.

  These unstructured tactics feature both goal addressing and dynamic
  instantiation. Note that named rule cases are ∗‹not› provided as would be by
  the proper @{method cases} and @{method induct} proof methods (see
  \secref{sec:cases-induct}). Unlike the @{method induct} method, @{method
  induct_tac} does not handle structured rule statements, only the compact
  object-logic conclusion of the subgoal being addressed.

  ➧ @{method (HOL) ind_cases} and @{command (HOL) "inductive_cases"} provide
  an interface to the internal ML_text‹mk_cases› operation. Rules are
  simplified in an unrestricted forward manner.

  While @{method (HOL) ind_cases} is a proof method to apply the result
  immediately as elimination rules, @{command (HOL) "inductive_cases"}
  provides case split theorems at the theory level for later use. The
  @{keyword "for"} argument of the @{method (HOL) ind_cases} method allows to
  specify a list of variables that should be generalized before applying the
  resulting rule.
›


section ‹Adhoc tuples›

text ‹
  \begin{matharray}{rcl}
    @{attribute_def (HOL) split_format}‹*› & : & ‹attribute› \\
  \end{matharray}

  rail‹
    @@{attribute (HOL) split_format} ('(' 'complete' ')')?
  ›

  ➧ @{attribute (HOL) split_format}\ ‹(complete)› causes arguments in function
  applications to be represented canonically according to their tuple type
  structure.

  Note that this operation tends to invent funny names for new local
  parameters introduced.
›


chapter ‹Executable code \label{ch:export-code}›

text ‹
  For validation purposes, it is often useful to ∗‹execute› specifications. In
  principle, execution could be simulated by Isabelle's inference kernel, i.e.
  by a combination of resolution and simplification. Unfortunately, this
  approach is rather inefficient. A more efficient way of executing
  specifications is to translate them into a functional programming language
  such as ML.

  Isabelle provides a generic framework to support code generation from
  executable specifications. Isabelle/HOL instantiates these mechanisms in a
  way that is amenable to end-user applications. Code can be generated for
  functional programs (including overloading using type classes) targeting SML
  cite‹SML›, OCaml cite‹OCaml›, Haskell cite‹"haskell-revised-report"›
  and Scala cite‹"scala-overview-tech-report"›. Conceptually, code
  generation is split up in three steps: ∗‹selection› of code theorems,
  ∗‹translation› into an abstract executable view and ∗‹serialization› to a
  specific ∗‹target language›. Inductive specifications can be executed using
  the predicate compiler which operates within HOL. See cite‹"isabelle-codegen"› for an introduction.

  \begin{matharray}{rcl}
    @{command_def (HOL) "export_code"}‹*› & : & ‹local_theory → local_theory› \\
    @{attribute_def (HOL) code} & : & ‹attribute› \\
    @{command_def (HOL) "code_datatype"} & : & ‹theory → theory› \\
    @{command_def (HOL) "print_codesetup"}‹*› & : & ‹context →› \\
    @{attribute_def (HOL) code_unfold} & : & ‹attribute› \\
    @{attribute_def (HOL) code_post} & : & ‹attribute› \\
    @{attribute_def (HOL) code_abbrev} & : & ‹attribute› \\
    @{command_def (HOL) "print_codeproc"}‹*› & : & ‹context →› \\
    @{command_def (HOL) "code_thms"}‹*› & : & ‹context →› \\
    @{command_def (HOL) "code_deps"}‹*› & : & ‹context →› \\
    @{command_def (HOL) "code_reserved"} & : & ‹theory → theory› \\
    @{command_def (HOL) "code_printing"} & : & ‹theory → theory› \\
    @{command_def (HOL) "code_identifier"} & : & ‹theory → theory› \\
    @{command_def (HOL) "code_monad"} & : & ‹theory → theory› \\
    @{command_def (HOL) "code_reflect"} & : & ‹theory → theory› \\
    @{command_def (HOL) "code_pred"} & : & ‹theory → proof(prove)› \\
    @{attribute_def (HOL) code_timing} & : & ‹attribute› \\
    @{attribute_def (HOL) code_simp_trace} & : & ‹attribute› \\
    @{attribute_def (HOL) code_runtime_trace} & : & ‹attribute›
  \end{matharray}

  rail‹
    @@{command (HOL) export_code} @'open'? ⏎ (const_expr+) (export_target*)
    ;
    export_target:
      @'in' target (@'module_name' @{syntax name})? ⏎
      (@'file_prefix' @{syntax path})? ('(' args ')')?
    ;
    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
    ;
    const_expr: (const | 'name._' | '_')
    ;
    const: @{syntax term}
    ;
    type_constructor: @{syntax name}
    ;
    class: @{syntax name}
    ;
    path: @{syntax embedded}
    ;
    @@{attribute (HOL) code} ('equation' | 'nbe' | 'abstype' | 'abstract'
      | 'del' | 'drop:' (const+) | 'abort:' (const+))?
    ;
    @@{command (HOL) code_datatype} (const+)
    ;
    @@{attribute (HOL) code_unfold} 'del'?
    ;
    @@{attribute (HOL) code_post} 'del'?
    ;
    @@{attribute (HOL) code_abbrev} 'del'?
    ;
    @@{command (HOL) code_thms} (const_expr+)
    ;
    @@{command (HOL) code_deps} (const_expr+)
    ;
    @@{command (HOL) code_reserved} target (@{syntax string}+)
    ;
    symbol_const: @'constant' const
    ;
    symbol_type_constructor: @'type_constructor' type_constructor
    ;
    symbol_class: @'type_class' class
    ;
    symbol_class_relation: @'class_relation' class ('<' | '⊆') class
    ;
    symbol_class_instance: @'class_instance' type_constructor @'::' class
    ;
    symbol_module: @'code_module' name
    ;
    syntax: @{syntax string} | (@'infix' | @'infixl' | @'infixr')
      @{syntax nat} @{syntax string}
    ;
    printing_const: symbol_const ('⇀' | '=>') ⏎
      ('(' target ')' syntax ? + @'and')
    ;
    printing_type_constructor: symbol_type_constructor ('⇀' | '=>') ⏎
      ('(' target ')' syntax ? + @'and')
    ;
    printing_class: symbol_class ('⇀' | '=>') ⏎
      ('(' target ')' @{syntax string} ? + @'and')
    ;
    printing_class_relation: symbol_class_relation ('⇀' | '=>') ⏎
      ('(' target ')' @{syntax string} ? + @'and')
    ;
    printing_class_instance: symbol_class_instance ('⇀'| '=>') ⏎
      ('(' target ')' '-' ? + @'and')
    ;
    printing_module: symbol_module ('⇀' | '=>') ⏎
      ('(' target ')' (@{syntax string} for_symbol?)? + @'and')
    ;
    for_symbol:
      @'for'
        ((symbol_const | symbol_typeconstructor |
          symbol_class | symbol_class_relation | symbol_class_instance)+)
    ;
    @@{command (HOL) code_printing} ((printing_const | printing_type_constructor
      | printing_class | printing_class_relation | printing_class_instance
      | printing_module) + '|')
    ;
    @@{command (HOL) code_identifier} ((symbol_const | symbol_type_constructor
      | symbol_class | symbol_class_relation | symbol_class_instance
      | symbol_module ) ('⇀' | '=>') ⏎
      ('(' target ')' @{syntax string} ? + @'and') + '|')
    ;
    @@{command (HOL) code_monad} const const target
    ;
    @@{command (HOL) code_reflect} @{syntax string} ⏎
      (@'datatypes' (@{syntax string} '=' ('_' | (@{syntax string} + '|') + @'and')))? ⏎
      (@'functions' (@{syntax string} +))? (@'file_prefix' @{syntax path})?
    ;
    @@{command (HOL) code_pred} ⏎ ('(' @'modes' ':' modedecl ')')? ⏎ const
    ;
    modedecl: (modes | ((const ':' modes) ⏎
      (@'and' ((const ':' modes @'and')+))?))
    ;
    modes: mode @'as' const
  ›

  ➧ @{command (HOL) "export_code"} generates code for a given list of
  constants in the specified target language(s). If no serialization
  instruction is given, only abstract code is generated internally.

  Constants may be specified by giving them literally, referring to all
  executable constants within a certain theory by giving ‹name._›, or
  referring to ∗‹all› executable constants currently available by giving ‹_›.

  By default, exported identifiers are minimized per module. This can be
  suppressed by prepending @{keyword "open"} before the list of constants.

  By default, for each involved theory one corresponding name space module is
  generated. Alternatively, a module name may be specified after the @{keyword
  "module_name"} keyword; then ∗‹all› code is placed in this module.

  Generated code is output as logical files within the theory context, as well
  as session exports that can be retrieved using @{tool_ref export}, or @{tool
  build} with option ▩‹-e› and suitable \isakeyword{export\_files}
  specifications in the session ▩‹ROOT› entry. All files have a common
  directory prefix: the long theory name plus ``▩‹code›''. The actual file
  name is determined by the target language together with an optional
  ⬚‹file_prefix› (the default is ``▩‹export›'' with a consecutive number
  within the current theory). For ‹SML›, ‹OCaml› and ‹Scala›, the file prefix
  becomes a plain file with extension (e.g.\ ``▩‹.ML›'' for SML). For
  ‹Haskell› the file prefix becomes a directory that is populated with a
  separate file for each module (with extension ``▩‹.hs›'').

  Serializers take an optional list of arguments in parentheses.

      ▪ For ∗‹Haskell› a module name prefix may be given using the ``‹root:›''
      argument; ``‹string_classes›'' adds a ``▩‹deriving (Read, Show)›'' clause 
      to each appropriate datatype declaration.

      ▪ For ∗‹Scala›, ``‹case_insensitive›'' avoids name clashes on
      case-insensitive file systems.

  ➧ @{attribute (HOL) code} declares code equations for code generation.

  Variant ‹code equation› declares a conventional equation as code equation.

  Variants ‹code abstype› and ‹code abstract› declare abstract datatype
  certificates or code equations on abstract datatype representations
  respectively.

  Vanilla ‹code› falls back to ‹code equation› or ‹code abstract›
  depending on the syntactic shape of the underlying equation.

  Variant ‹code del› deselects a code equation for code generation.

  Variant ‹code nbe› accepts also non-left-linear equations for
  ∗‹normalization by evaluation› only.

  Variants ‹code drop:› and ‹code abort:› take a list of constants as arguments
  and drop all code equations declared for them. In the case of ‹abort›,
  these constants if needed are implemented by program abort
  (exception).

  Packages declaring code equations usually provide a reasonable default
  setup.

  ➧ @{command (HOL) "code_datatype"} specifies a constructor set for a logical
  type.

  ➧ @{command (HOL) "print_codesetup"} gives an overview on selected code
  equations and code generator datatypes.

  ➧ @{attribute (HOL) code_unfold} declares (or with option ``‹del›'' removes)
  theorems which during preprocessing are applied as rewrite rules to any code
  equation or evaluation input.

  ➧ @{attribute (HOL) code_post} declares (or with option ``‹del›'' removes)
  theorems which are applied as rewrite rules to any result of an evaluation.

  ➧ @{attribute (HOL) code_abbrev} declares (or with option ``‹del›'' removes)
  equations which are applied as rewrite rules to any result of an evaluation
  and symmetrically during preprocessing to any code equation or evaluation
  input.

  ➧ @{command (HOL) "print_codeproc"} prints the setup of the code generator
  preprocessor.

  ➧ @{command (HOL) "code_thms"} prints a list of theorems representing the
  corresponding program containing all given constants after preprocessing.

  ➧ @{command (HOL) "code_deps"} visualizes dependencies of theorems
  representing the corresponding program containing all given constants after
  preprocessing.

  ➧ @{command (HOL) "code_reserved"} declares a list of names as reserved for
  a given target, preventing it to be shadowed by any generated code.

  ➧ @{command (HOL) "code_printing"} associates a series of symbols
  (constants, type constructors, classes, class relations, instances, module
  names) with target-specific serializations; omitting a serialization deletes
  an existing serialization.

  ➧ @{command (HOL) "code_monad"} provides an auxiliary mechanism to generate
  monadic code for Haskell.

  ➧ @{command (HOL) "code_identifier"} associates a a series of symbols
  (constants, type constructors, classes, class relations, instances, module
  names) with target-specific hints how these symbols shall be named. These
  hints gain precedence over names for symbols with no hints at all.
  Conflicting hints are subject to name disambiguation. ∗‹Warning:› It is at
  the discretion of the user to ensure that name prefixes of identifiers in
  compound statements like type classes or datatypes are still the same.

  ➧ @{command (HOL) "code_reflect"} without a ``⬚‹file_prefix›'' argument
  compiles code into the system runtime environment and modifies the code
  generator setup that future invocations of system runtime code generation
  referring to one of the ``‹datatypes›'' or ``‹functions›'' entities use
  these precompiled entities. With a ``⬚‹file_prefix›'' argument, the
  corresponding code is generated/exported to the specified file (as for
  ⬚‹export_code›) without modifying the code generator setup.

  ➧ @{command (HOL) "code_pred"} creates code equations for a predicate given
  a set of introduction rules. Optional mode annotations determine which
  arguments are supposed to be input or output. If alternative introduction
  rules are declared, one must prove a corresponding elimination rule.

  ➧ @{attribute (HOL) "code_timing"} scrapes timing samples from different
  stages of the code generator.

  ➧ @{attribute (HOL) "code_simp_trace"} traces the simplifier when it is
  used with code equations.

  ➧ @{attribute (HOL) "code_runtime_trace"} traces ML code generated
  dynamically for execution.
›

end