Quelle  HOL_Specific.thy

(*:maxLineLen=78:*)

theory HOL_Specific
  imports
    Main
    "HOL-Library.Old_Datatype"
    "HOL-Library.Old_Recdef"
    "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 ‹τ₁ ==>
 τ₂ ==> τ₃› 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 ==> M A ≤ M
 B›, for each premise ‹M R t› in an introduction rule. The default rule
 declarations of Isabelle/HOL already take care of most common situations.

 🪙‹
 (@@{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 ‹R₁, …, R_n› are defined simultaneously, the list
 of introduction rules is called ‹R₁_…_R_n.intros›, the case analysis rules
 are called ‹R₁.cases, …, R_n.cases›, and the list of mutual induction rules
 is called ‹R₁_…_R_n.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 ==> M A ≤ M B›, for proving monotonicity of
 inductive definitions whose introduction rules have premises involving terms
 such as ‹M 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{‹P₁ ∨ P₂ ⟶ Q₁ ∨ Q₂›}{‹P₁ ⟶ Q₁› & ‹P₂ ⟶ Q₂›}
 \]

 ▪ 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}

 🪙‹
 @@{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 x₁ … x_m (C y₁ … y_k) z₁ … z_n = 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 … y_i …› 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 🍋‹'a ==> 'a aexp› given as a parameter is lifted canonically on the
 types 🍋‹'a aexp› and 🍋‹'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 🍋‹'a
 aexp› and 🍋‹'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 🍋‹('a, 'b) term› can be defined as
 follows, by working simultaneously on 🍋‹('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 🍋‹('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}

 🪙‹
 @@{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}

 🪙‹
 @@{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 🪙‹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.

 🪙‹
 @@{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}
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 \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}

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


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

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

 🪙‹
 @@{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}

 🪙‹
 @@{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 🍋‹'a list› that is already in 🍋‹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}

 🪙‹
 @@{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"}~‹(α₁, …, α_m) t = τ + c₁ :: σ₁ … c_n :: σ_n›
 defines extensible record type ‹(α₁, …, α_m) t›, derived from the optional
 parent record ‹τ› by adding new field components ‹c_i :: σ_i› etc.

 The type variables of ‹τ› and ‹σ_i› need to be covered by the (distinct)
 parameters ‹α₁, …, α_m›. Type constructor ‹t› has to be new, while ‹τ›
 needs to specify an instance of an existing record type. At least one new
 field ‹c_i› 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, ‹(α₁, …, α_m) t› is made a type abbreviation for the fixed
 record type ‹(c₁ :: σ₁, …, c_n :: σ_n)›, likewise is ‹(α₁, …, α_m, ζ)
 t_scheme› made an abbreviation for ‹(c₁ :: σ₁, …, c_n :: σ_n, … :: ζ)›.

 🪙 @{command (HOL) "print_record"}~‹(α₁, …, α_m) t› prints the definition of
 record ‹(α₁, …, α_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 ‹(α₁,
 …, α_m) t› is a root record with fields ‹c₁ :: σ₁, …, c_n :: σ_n›.

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

 \begin{matharray}{lll}
 ‹c_i› & ‹::› & ‹(🪙c :: 🪙σ, … :: ζ) ==> σ_i› \\
 ‹c_{i_update}› & ‹::› & ‹(σ_i ==> σ_i) ==> (🪙c :: 🪙σ, … :: ζ) ==> (🪙c :: 🪙σ, … :: ζ)› \\
 \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› & ‹::› & ‹σ₁ ==> … σ_n ==> (??c :: 🪙σ)› \\
 \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 ‹(α₁, …, α_m) t› has ancestor fields ‹b₁ ::
 ρ₁, …, b_k :: ρ_k›, the above record operations will get the following
 types:

 🪙
 \begin{tabular}{lll}
 ‹c_i› & ‹::› & ‹(🪙b :: 🪙ρ, 🪙c :: ??σ, … :: ζ) ==> σ_i› \\
 ‹c_{i_update}› & ‹::› & ‹(σ_i ==> σ_i) ==>
 (🪙b :: 🪙ρ, 🪙c :: 🪙σ, … :: ζ) ==>
 (🪙b :: 🪙ρ, 🪙c :: 🪙σ, … :: ζ)› \\
 ‹t.make› & ‹::› & ‹ρ₁ ==> … ρ_k ==> σ₁ ==> … σ_n ==>
 (🪙b :: 🪙ρ, 🪙c :: 🪙σ)› \\
 \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› & ‹::› & ‹σ₁ ==> … σ_n ==> (🪙c :: 🪙σ)› \\
 ‹t.extend› & ‹::› & ‹(🪙b :: 🪙ρ, 🪙c :: 🪙σ) ==>
 ζ ==> (🪙b :: 🪙ρ, 🪙c :: 🪙σ, … :: ζ)› \\
 ‹t.truncate› & ‹::› & ‹(🪙b :: 🪙ρ, 🪙c :: 🪙σ, … :: ζ) ==> (🪙b :: 🪙ρ, 🪙c :: 🪙σ)› \\
 \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
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 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 ‹α₁, …,
 α_n› which means that the type definition produces a type constructor ‹(α₁,
 …, α_n) t› depending on those type arguments.

 🪙‹
 @@{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,
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 \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"}~‹(α₁, …, α_n) t = A› defines a new type ‹(α₁,
 …, α_n) t› from the set ‹A› over an existing type. The set ‹A› may contain
 type variables ‹α₁, …, α_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}

 🪙‹
 @@{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› & ‹::› &
 ‹σ₁ ==> … σ_k ==> (🪙α_n) t ==> (🪙β_n) t› \\
 \end{matharray}

 where ‹t› is the type constructor, ‹🪙α_n› and ‹🪙β_n› are
 distinct type variables free in the local theory and ‹σ₁›, \ldots, ‹σ_k› is
 a subsequence of ‹α₁ ==> β₁›, ‹β₁ ==> α₁›, \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}

 🪙‹
 @@{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}

 🪙‹
 @@{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.

 🪙
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 corresponding to a datatype invariant, such as 🍋‹'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 🍋‹'a dlist
 option› vs. 🍋‹'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

 🪙 ‹τ = τ₁ … τ_n κ›, where ‹κ› is an abstract type constructor and ‹τ₁ …
 τ_n› do not contain abstract types (i.e.\ 🍋‹int dlist› is allowed
 whereas 🍋‹int dlist dlist› not)

 🪙 ‹τ = τ₁ … τ_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
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
 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 🍋‹'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}

 🪙‹
 @@{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}

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

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

 @@{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}

 🪙‹
 @@{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 🍋‹exhaustive› and
 🍋‹full_exhaustive› implement the testing. They take a testing
 function as a parameter, which takes a value of type 🍋‹'a› and
 optionally produces a counterexample, and a size parameter for the test
 values. In 🍋‹full_exhaustive›, the testing function parameter
 additionally expects a lazy term reconstruction in the type 🍋‹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 🍋‹random› generates a pseudo-random value of the given size
 and a lazy term reconstruction of the value in the type 🍋‹Code_Evaluation.term›. A pseudo-randomness generator is defined in theory
 🍋‹HOL.Random›.

 🪙[‹narrowing›] implements Haskell's Lazy Smallcheck cite‹"runciman-naylor-lindblad"› using the type classes 🍋‹narrowing› and
 🍋‹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 🍋‹'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 🍋‹_ 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 🍋‹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.

 🪙‹
 @@{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 ::
 σ₁ ==> σ₂› where ‹σ₁› and ‹σ₂› 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 :: σ₁ ==> σ₂› 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› & ‹::› &
 ‹f₁ ==> … ==> f_n ==> (α₁, …, α_n) t ==> (β₁, …, β_n) t› \\
 \end{matharray}

 where ‹t› is a type constructor and ‹f_i› 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
 :: σ₁ ==> σ₂ ==> σ₃ ==> σ₄› 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
 🍋‹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}

 🪙‹
 @@{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}

 🪙‹
 @@{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}

 🪙‹
 @@{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] "∀x₁ … x_n.
 e₁(x₁, …, x_n) = 0 ∧ … ∧ e_m(x₁, …, x_n) = 0 ⟶
 (∃y₁ … y_k.
 p₁₁(x₁, … ,x_n) * y₁ + … + p_1k(x₁, …, x_n) * y_k = 0 ∧
 … ∧
 p_t1(x₁, …, x_n) * y₁ + … + p_tk(x₁, …, x_n) * y_k = 0)"}

 Here ‹e₁, …, e_n› and the ‹p_ij› 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: ths₁ del: ths₂)›. 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 "c² + s² = 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}

 🪙‹
 @@{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<open>Unstructured case analysis and induction \label{sec:hol-induct-tac}›

text java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
  The following tools of Isabelle/HOL support casesnalysisalysis 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}\<open>\<^sup>*\<close> & : & \<open>method\> \\
    @{method_def (HOL) induct_tac}\<open>\<^sup>*\<close>:&<>method\<close> \\
    @{method_def (HOL) ind_cases}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
    @{command_def (HOL) "inductive_cases"}\<open>\<^sup>*\<close> & : & \<open>local_theory \<rightarrow> local_theory\<close> \java.lang.StringIndexOutOfBoundsException: Index 129 out of bounds for length 129
  \end{matharray}

  \<^rail\open
    @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
    ;
    tool_def_ lac olairectpererr he Scalala piler
    ;
    @@{method (HOL) ind_cases} (@{syntax prop}+) @{syntax for_fixes}
    ;
    @@{command (HOL) inductive_cases} (@{syntax thmdecl(xop})'and)
    ;
    rule: 'rule' ':' @{syntax thm}
  \<close>

  \<^descr> @{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 (. \<erbatim<>ISABELLE_HOMELLE_HOMEE_HOMEclose>).

  These unstructured tactics feature both goal addressing and dynamic
  instantiationtantiationntiationNoteatd e ases \\emph\open>not\<close> provided as would be by
  the proper @{method cases} and @{method induct} proof methods (see
  \secref{secasess-uctct)nlikekehe @{thodnductt hod {thodd
  induct_tac} does not handle structured rule statements, only the compact
  object-logic conclusion of the subgoal being addressed.

  \<^descr@od(nd_cases}d@commandnd(OL"nductive_casesrovide
  an interface to the internal \<^ML_text>\<open>mk_cases\<>operation. Rules are
  implifiedinan unrestricted forward manner.

  While @{method (HOL) ind_cases} is a proof method to apply the result
  immediately as elimination rules, @{command (HOL) "inductive_casesjava.lang.StringIndexOutOfBoundsException: Index 70 out of bounds for length 70
  provides case split theorems at the theory level for later use. The
  @{keyword "for"} argument of the @notxpandedecursively
  specify a list of variables that should be generalized before applying the
  resulting rule.
\<close>


section \<open>Adhoc tuples\<close>

text \<open>
  \begin{matharray}{rcl}
    @{attribute_def <>tsabelleeld:scalauild<
  \end{matharray}

  \<^rail>\<open>
    @@{attribute (HOL) split_format} ('(' 'complete' ')')?
  \<close>

  \<^descr> @{attribute (HOL) split_format}\ \<open>(complete)\<close> causes arguments in function
  applications to be represented canonically according to their tuple type
  structure.

  unnyesrewal
  parameters introduced.
\<close>


chapter \<open>Executable code \label{ch:export-code}\<close>

text \<open>
  For validation purposes, it is often useful to \<^emph>\<open>execute\<
  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
  
  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>\<open>SML\<close>, OCaml \<^cite>\OCaml\<close>, Haskell \<^cite>\<open>"haskell-revised-report"\<close>
  and Scala \<^cite>\<open>"scala-overview-tech-report"\<close>. Conceptually, code
  generation is split up in three steps: \<\selection\<close> of code theorems,
  \<^emph>\<open>translation\<close> into an abstract executableew ^><open>serialization\<close> to a
  specific \<^emph>\<open>target language\<close>. Inductive specifications can be executed using
  the predicate compiler which operates within HOL. See \<^cite>\<open>"isabelle-codegen"\<close> for \\<open>$ISABELLE_HOME/etc/build.props\<close>. The overall list of registered functions

  \begin{matharray}{rcl}
    @{command_def (HOL) "export_code"}\<open>\<^sup>*\<close> & : & \<open>local_theory \<rightarrow> local_theory\close\\
    @{attribute_def (HOL) code  \<^><open>isabelle.Scala.Fun_String\<close> for type
    @{command_def (HOL)java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
    @{command_def (HOL) "print_codesetup"}\<open>\<^sup>*\<close> & : & \context \<rightarrow>\<close> \\
    ttribute_defL)unfold& \>ttributebute\>\\
    @{attribute_def (HOL) code_post} & : & \<open>attribute\<close> \\
    @{attribute_def (HOL) code_abbrev} & : & \<open>attribute\<close> \\
    @{command_def (HOL) "print_codeproc"}\<open>\<up>*close& : & \<open>context \<rightarrow>\<close> \\
    @{command_def (HOL) "code_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<theDEcolIn sabellelle/hisppearsarsas unction f typepe
    @{command_def (HOL) "code_deps"}\<open>\<^sup>*\<closeScala.Null\<close> in ML. The execution
    @
    @{command_def (HOL) "code_printing"} & : & \<open>theory \<rightarrow> theory\<close> \\
    @{command_def (HOL) "code_identifier"} & : & \<open>theory \<rightarrowheoryry<close \\
    @{command_def (HOL) "code_monad
    @{command_def (HOL) "code_reflect"} & : & \<open>theory \<rightarrow> theory\<close> \\
    @{command_def (HOL) "code_pred"} &ML\<open>
    @{attribute_def (HOLde_timingimingng}&  & \<open>attribute\<close> \\
    @{attribute_def (HOL) code_simp_trace} & : & \<open>attribute\<close> \\
    @{attribute_def
  \end{matharray}

  \<^railsubsequentuentdocumentttiquotationsshelp  ocument sabelleala
    @@{command (HOL) export_code} @'open'? \<newline> (const_expr+) (export_target*)
    ;
    export_target‹
 
 (@'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:@{syax embedded}
 ;
 @ object: 🍋c
 'drop:' (onst+) 'op'| 'abort:' (const+ | 'a'aortt')?
 ;

 ;
 @@{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}+) + @'and')
 ;
 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
 ;
 target_syntax: @{syntax embedded}
 ;
 rich_syntax: target_syntax | (@'infix' | @'infixl' | @'infixr')
 @{syntax nat} target_syntax
 ;
 printing_const: symbol_const ('⇀' | '=>') 🍋
 ('(' target ')' rich_syntax ? + @'and')
 ;
 printing_type_constructor: symbol_type_constructor ('⇀' | '=>') 🍋
 ('(' target ')' rich_syntax ? + @'and')
 ;
 printing_class: symbol_class ('⇀' | '=>') 🍋
 ('(' target ')' target_syntax ? + @'and')
 ;
 printing_class_relation: symbol_class_relation ('⇀' | '=>') 🍋
 ('(' target ')' target_syntax ? + @'and')
 ;
 printing_class_instance: symbol_class_instance ('⇀'| '=>') 🍋
 ('(' target ')' '-' ? + @'and')
 ;
 printing_module: symbol_module ('⇀' | '=>') 🍋
 ('(' target ')' 🍋
 ((target_syntax | @'file' path) 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.

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

  Multiple ‹code equation› / ‹code nbe› declarations referring to the same
  constant within the same theory are handled as 🪙‹one› function declaration
  for that particular constant: the first code declaration within a theory
  disregards any previous function declaration and superseedes any equations
  from preceeding theories.

  Each code equation is prepended to existing code equations declared in
  the same theory, with syntactically subsumed equations removed.

  Packages usually provide reasonable default code equations; an explicit
  declaration of a code equation superseedes any preceeding default code
  equations.

  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.

  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). Variants ‹code drop› and ‹code abort› derive the affected
  constants from the underlying theorems interpreted as code equations.

  🪙 @{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