src/Doc/Isar_Ref/HOL_Specific.thy
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (23 months ago)
changeset 66822 4642cf4a7ebb
parent 66453 cc19f7ca2ed6
child 67207 ad538f6c5d2f
permissions -rw-r--r--
tuned signature;
     1 (*:maxLineLen=78:*)
     2 
     3 theory HOL_Specific
     4   imports
     5     Main
     6     "HOL-Library.Old_Datatype"
     7     "HOL-Library.Old_Recdef"
     8     "HOL-Library.Adhoc_Overloading"
     9     "HOL-Library.Dlist"
    10     "HOL-Library.FSet"
    11     Base
    12 begin
    13 
    14 
    15 chapter \<open>Higher-Order Logic\<close>
    16 
    17 text \<open>
    18   Isabelle/HOL is based on Higher-Order Logic, a polymorphic version of
    19   Church's Simple Theory of Types. HOL can be best understood as a
    20   simply-typed version of classical set theory. The logic was first
    21   implemented in Gordon's HOL system @{cite "mgordon-hol"}. It extends
    22   Church's original logic @{cite "church40"} by explicit type variables (naive
    23   polymorphism) and a sound axiomatization scheme for new types based on
    24   subsets of existing types.
    25 
    26   Andrews's book @{cite andrews86} is a full description of the original
    27   Church-style higher-order logic, with proofs of correctness and completeness
    28   wrt.\ certain set-theoretic interpretations. The particular extensions of
    29   Gordon-style HOL are explained semantically in two chapters of the 1993 HOL
    30   book @{cite pitts93}.
    31 
    32   Experience with HOL over decades has demonstrated that higher-order logic is
    33   widely applicable in many areas of mathematics and computer science. In a
    34   sense, Higher-Order Logic is simpler than First-Order Logic, because there
    35   are fewer restrictions and special cases. Note that HOL is \<^emph>\<open>weaker\<close> than
    36   FOL with axioms for ZF set theory, which is traditionally considered the
    37   standard foundation of regular mathematics, but for most applications this
    38   does not matter. If you prefer ML to Lisp, you will probably prefer HOL to
    39   ZF.
    40 
    41   \<^medskip> The syntax of HOL follows \<open>\<lambda>\<close>-calculus and functional programming.
    42   Function application is curried. To apply the function \<open>f\<close> of type \<open>\<tau>\<^sub>1 \<Rightarrow>
    43   \<tau>\<^sub>2 \<Rightarrow> \<tau>\<^sub>3\<close> to the arguments \<open>a\<close> and \<open>b\<close> in HOL, you simply write \<open>f a b\<close> (as
    44   in ML or Haskell). There is no ``apply'' operator; the existing application
    45   of the Pure \<open>\<lambda>\<close>-calculus is re-used. Note that in HOL \<open>f (a, b)\<close> means ``\<open>f\<close>
    46   applied to the pair \<open>(a, b)\<close> (which is notation for \<open>Pair a b\<close>). The latter
    47   typically introduces extra formal efforts that can be avoided by currying
    48   functions by default. Explicit tuples are as infrequent in HOL
    49   formalizations as in good ML or Haskell programs.
    50 
    51   \<^medskip> Isabelle/HOL has a distinct feel, compared to other object-logics like
    52   Isabelle/ZF. It identifies object-level types with meta-level types, taking
    53   advantage of the default type-inference mechanism of Isabelle/Pure. HOL
    54   fully identifies object-level functions with meta-level functions, with
    55   native abstraction and application.
    56 
    57   These identifications allow Isabelle to support HOL particularly nicely, but
    58   they also mean that HOL requires some sophistication from the user. In
    59   particular, an understanding of Hindley-Milner type-inference with
    60   type-classes, which are both used extensively in the standard libraries and
    61   applications.
    62 \<close>
    63 
    64 
    65 chapter \<open>Derived specification elements\<close>
    66 
    67 section \<open>Inductive and coinductive definitions \label{sec:hol-inductive}\<close>
    68 
    69 text \<open>
    70   \begin{matharray}{rcl}
    71     @{command_def (HOL) "inductive"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    72     @{command_def (HOL) "inductive_set"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    73     @{command_def (HOL) "coinductive"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    74     @{command_def (HOL) "coinductive_set"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
    75     @{command_def "print_inductives"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    76     @{attribute_def (HOL) mono} & : & \<open>attribute\<close> \\
    77   \end{matharray}
    78 
    79   An \<^emph>\<open>inductive definition\<close> specifies the least predicate or set \<open>R\<close> closed
    80   under given rules: applying a rule to elements of \<open>R\<close> yields a result within
    81   \<open>R\<close>. For example, a structural operational semantics is an inductive
    82   definition of an evaluation relation.
    83 
    84   Dually, a \<^emph>\<open>coinductive definition\<close> specifies the greatest predicate or set
    85   \<open>R\<close> that is consistent with given rules: every element of \<open>R\<close> can be seen as
    86   arising by applying a rule to elements of \<open>R\<close>. An important example is using
    87   bisimulation relations to formalise equivalence of processes and infinite
    88   data structures.
    89 
    90   Both inductive and coinductive definitions are based on the Knaster-Tarski
    91   fixed-point theorem for complete lattices. The collection of introduction
    92   rules given by the user determines a functor on subsets of set-theoretic
    93   relations. The required monotonicity of the recursion scheme is proven as a
    94   prerequisite to the fixed-point definition and the resulting consequences.
    95   This works by pushing inclusion through logical connectives and any other
    96   operator that might be wrapped around recursive occurrences of the defined
    97   relation: there must be a monotonicity theorem of the form \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M>
    98   B\<close>, for each premise \<open>\<M> R t\<close> in an introduction rule. The default rule
    99   declarations of Isabelle/HOL already take care of most common situations.
   100 
   101   @{rail \<open>
   102     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
   103       @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
   104       @{syntax vars} @{syntax for_fixes} \<newline>
   105       (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
   106     ;
   107     @@{command print_inductives} ('!'?)
   108     ;
   109     @@{attribute (HOL) mono} (() | 'add' | 'del')
   110   \<close>}
   111 
   112   \<^descr> @{command (HOL) "inductive"} and @{command (HOL) "coinductive"} define
   113   (co)inductive predicates from the introduction rules.
   114 
   115   The propositions given as \<open>clauses\<close> in the @{keyword "where"} part are
   116   either rules of the usual \<open>\<And>/\<Longrightarrow>\<close> format (with arbitrary nesting), or
   117   equalities using \<open>\<equiv>\<close>. The latter specifies extra-logical abbreviations in
   118   the sense of @{command_ref abbreviation}. Introducing abstract syntax
   119   simultaneously with the actual introduction rules is occasionally useful for
   120   complex specifications.
   121 
   122   The optional @{keyword "for"} part contains a list of parameters of the
   123   (co)inductive predicates that remain fixed throughout the definition, in
   124   contrast to arguments of the relation that may vary in each occurrence
   125   within the given \<open>clauses\<close>.
   126 
   127   The optional @{keyword "monos"} declaration contains additional
   128   \<^emph>\<open>monotonicity theorems\<close>, which are required for each operator applied to a
   129   recursive set in the introduction rules.
   130 
   131   \<^descr> @{command (HOL) "inductive_set"} and @{command (HOL) "coinductive_set"}
   132   are wrappers for to the previous commands for native HOL predicates. This
   133   allows to define (co)inductive sets, where multiple arguments are simulated
   134   via tuples.
   135 
   136   \<^descr> @{command "print_inductives"} prints (co)inductive definitions and
   137   monotonicity rules; the ``\<open>!\<close>'' option indicates extra verbosity.
   138 
   139   \<^descr> @{attribute (HOL) mono} declares monotonicity rules in the context. These
   140   rule are involved in the automated monotonicity proof of the above inductive
   141   and coinductive definitions.
   142 \<close>
   143 
   144 
   145 subsection \<open>Derived rules\<close>
   146 
   147 text \<open>
   148   A (co)inductive definition of \<open>R\<close> provides the following main theorems:
   149 
   150   \<^descr> \<open>R.intros\<close> is the list of introduction rules as proven theorems, for the
   151   recursive predicates (or sets). The rules are also available individually,
   152   using the names given them in the theory file;
   153 
   154   \<^descr> \<open>R.cases\<close> is the case analysis (or elimination) rule;
   155 
   156   \<^descr> \<open>R.induct\<close> or \<open>R.coinduct\<close> is the (co)induction rule;
   157 
   158   \<^descr> \<open>R.simps\<close> is the equation unrolling the fixpoint of the predicate one
   159   step.
   160 
   161 
   162   When several predicates \<open>R\<^sub>1, \<dots>, R\<^sub>n\<close> are defined simultaneously, the list
   163   of introduction rules is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.intros\<close>, the case analysis rules
   164   are called \<open>R\<^sub>1.cases, \<dots>, R\<^sub>n.cases\<close>, and the list of mutual induction rules
   165   is called \<open>R\<^sub>1_\<dots>_R\<^sub>n.inducts\<close>.
   166 \<close>
   167 
   168 
   169 subsection \<open>Monotonicity theorems\<close>
   170 
   171 text \<open>
   172   The context maintains a default set of theorems that are used in
   173   monotonicity proofs. New rules can be declared via the @{attribute (HOL)
   174   mono} attribute. See the main Isabelle/HOL sources for some examples. The
   175   general format of such monotonicity theorems is as follows:
   176 
   177   \<^item> Theorems of the form \<open>A \<le> B \<Longrightarrow> \<M> A \<le> \<M> B\<close>, for proving monotonicity of
   178   inductive definitions whose introduction rules have premises involving terms
   179   such as \<open>\<M> R t\<close>.
   180 
   181   \<^item> Monotonicity theorems for logical operators, which are of the general form
   182   \<open>(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>\<close>. For example, in the case of the operator \<open>\<or>\<close>,
   183   the corresponding theorem is
   184   \[
   185   \infer{\<open>P\<^sub>1 \<or> P\<^sub>2 \<longrightarrow> Q\<^sub>1 \<or> Q\<^sub>2\<close>}{\<open>P\<^sub>1 \<longrightarrow> Q\<^sub>1\<close> & \<open>P\<^sub>2 \<longrightarrow> Q\<^sub>2\<close>}
   186   \]
   187 
   188   \<^item> De Morgan style equations for reasoning about the ``polarity'' of
   189   expressions, e.g.
   190   \[
   191   @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
   192   @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
   193   \]
   194 
   195   \<^item> Equations for reducing complex operators to more primitive ones whose
   196   monotonicity can easily be proved, e.g.
   197   \[
   198   @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
   199   @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
   200   \]
   201 \<close>
   202 
   203 
   204 subsubsection \<open>Examples\<close>
   205 
   206 text \<open>The finite powerset operator can be defined inductively like this:\<close>
   207 
   208 (*<*)experiment begin(*>*)
   209 inductive_set Fin :: "'a set \<Rightarrow> 'a set set" for A :: "'a set"
   210 where
   211   empty: "{} \<in> Fin A"
   212 | insert: "a \<in> A \<Longrightarrow> B \<in> Fin A \<Longrightarrow> insert a B \<in> Fin A"
   213 
   214 text \<open>The accessible part of a relation is defined as follows:\<close>
   215 
   216 inductive acc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   217   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<prec>" 50)
   218 where acc: "(\<And>y. y \<prec> x \<Longrightarrow> acc r y) \<Longrightarrow> acc r x"
   219 (*<*)end(*>*)
   220 
   221 text \<open>
   222   Common logical connectives can be easily characterized as non-recursive
   223   inductive definitions with parameters, but without arguments.
   224 \<close>
   225 
   226 (*<*)experiment begin(*>*)
   227 inductive AND for A B :: bool
   228 where "A \<Longrightarrow> B \<Longrightarrow> AND A B"
   229 
   230 inductive OR for A B :: bool
   231 where "A \<Longrightarrow> OR A B"
   232   | "B \<Longrightarrow> OR A B"
   233 
   234 inductive EXISTS for B :: "'a \<Rightarrow> bool"
   235 where "B a \<Longrightarrow> EXISTS B"
   236 (*<*)end(*>*)
   237 
   238 text \<open>
   239   Here the \<open>cases\<close> or \<open>induct\<close> rules produced by the @{command inductive}
   240   package coincide with the expected elimination rules for Natural Deduction.
   241   Already in the original article by Gerhard Gentzen @{cite "Gentzen:1935"}
   242   there is a hint that each connective can be characterized by its
   243   introductions, and the elimination can be constructed systematically.
   244 \<close>
   245 
   246 
   247 section \<open>Recursive functions \label{sec:recursion}\<close>
   248 
   249 text \<open>
   250   \begin{matharray}{rcl}
   251     @{command_def (HOL) "primrec"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   252     @{command_def (HOL) "fun"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   253     @{command_def (HOL) "function"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
   254     @{command_def (HOL) "termination"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
   255     @{command_def (HOL) "fun_cases"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   256   \end{matharray}
   257 
   258   @{rail \<open>
   259     @@{command (HOL) primrec} @{syntax specification}
   260     ;
   261     (@@{command (HOL) fun} | @@{command (HOL) function}) opts? @{syntax specification}
   262     ;
   263     opts: '(' (('sequential' | 'domintros') + ',') ')'
   264     ;
   265     @@{command (HOL) termination} @{syntax term}?
   266     ;
   267     @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
   268   \<close>}
   269 
   270   \<^descr> @{command (HOL) "primrec"} defines primitive recursive functions over
   271   datatypes (see also @{command_ref (HOL) datatype}). The given \<open>equations\<close>
   272   specify reduction rules that are produced by instantiating the generic
   273   combinator for primitive recursion that is available for each datatype.
   274 
   275   Each equation needs to be of the form:
   276 
   277   @{text [display] "f x\<^sub>1 \<dots> x\<^sub>m (C y\<^sub>1 \<dots> y\<^sub>k) z\<^sub>1 \<dots> z\<^sub>n = rhs"}
   278 
   279   such that \<open>C\<close> is a datatype constructor, \<open>rhs\<close> contains only the free
   280   variables on the left-hand side (or from the context), and all recursive
   281   occurrences of \<open>f\<close> in \<open>rhs\<close> are of the form \<open>f \<dots> y\<^sub>i \<dots>\<close> for some \<open>i\<close>. At
   282   most one reduction rule for each constructor can be given. The order does
   283   not matter. For missing constructors, the function is defined to return a
   284   default value, but this equation is made difficult to access for users.
   285 
   286   The reduction rules are declared as @{attribute simp} by default, which
   287   enables standard proof methods like @{method simp} and @{method auto} to
   288   normalize expressions of \<open>f\<close> applied to datatype constructions, by
   289   simulating symbolic computation via rewriting.
   290 
   291   \<^descr> @{command (HOL) "function"} defines functions by general wellfounded
   292   recursion. A detailed description with examples can be found in @{cite
   293   "isabelle-function"}. The function is specified by a set of (possibly
   294   conditional) recursive equations with arbitrary pattern matching. The
   295   command generates proof obligations for the completeness and the
   296   compatibility of patterns.
   297 
   298   The defined function is considered partial, and the resulting simplification
   299   rules (named \<open>f.psimps\<close>) and induction rule (named \<open>f.pinduct\<close>) are guarded
   300   by a generated domain predicate \<open>f_dom\<close>. The @{command (HOL) "termination"}
   301   command can then be used to establish that the function is total.
   302 
   303   \<^descr> @{command (HOL) "fun"} is a shorthand notation for ``@{command (HOL)
   304   "function"}~\<open>(sequential)\<close>'', followed by automated proof attempts regarding
   305   pattern matching and termination. See @{cite "isabelle-function"} for
   306   further details.
   307 
   308   \<^descr> @{command (HOL) "termination"}~\<open>f\<close> commences a termination proof for the
   309   previously defined function \<open>f\<close>. If this is omitted, the command refers to
   310   the most recent function definition. After the proof is closed, the
   311   recursive equations and the induction principle is established.
   312 
   313   \<^descr> @{command (HOL) "fun_cases"} generates specialized elimination rules for
   314   function equations. It expects one or more function equations and produces
   315   rules that eliminate the given equalities, following the cases given in the
   316   function definition.
   317 
   318 
   319   Recursive definitions introduced by the @{command (HOL) "function"} command
   320   accommodate reasoning by induction (cf.\ @{method induct}): rule \<open>f.induct\<close>
   321   refers to a specific induction rule, with parameters named according to the
   322   user-specified equations. Cases are numbered starting from 1. For @{command
   323   (HOL) "primrec"}, the induction principle coincides with structural
   324   recursion on the datatype where the recursion is carried out.
   325 
   326   The equations provided by these packages may be referred later as theorem
   327   list \<open>f.simps\<close>, where \<open>f\<close> is the (collective) name of the functions defined.
   328   Individual equations may be named explicitly as well.
   329 
   330   The @{command (HOL) "function"} command accepts the following options.
   331 
   332   \<^descr> \<open>sequential\<close> enables a preprocessor which disambiguates overlapping
   333   patterns by making them mutually disjoint. Earlier equations take precedence
   334   over later ones. This allows to give the specification in a format very
   335   similar to functional programming. Note that the resulting simplification
   336   and induction rules correspond to the transformed specification, not the one
   337   given originally. This usually means that each equation given by the user
   338   may result in several theorems. Also note that this automatic transformation
   339   only works for ML-style datatype patterns.
   340 
   341   \<^descr> \<open>domintros\<close> enables the automated generation of introduction rules for the
   342   domain predicate. While mostly not needed, they can be helpful in some
   343   proofs about partial functions.
   344 \<close>
   345 
   346 
   347 subsubsection \<open>Example: evaluation of expressions\<close>
   348 
   349 text \<open>
   350   Subsequently, we define mutual datatypes for arithmetic and boolean
   351   expressions, and use @{command primrec} for evaluation functions that follow
   352   the same recursive structure.
   353 \<close>
   354 
   355 (*<*)experiment begin(*>*)
   356 datatype 'a aexp =
   357     IF "'a bexp"  "'a aexp"  "'a aexp"
   358   | Sum "'a aexp"  "'a aexp"
   359   | Diff "'a aexp"  "'a aexp"
   360   | Var 'a
   361   | Num nat
   362 and 'a bexp =
   363     Less "'a aexp"  "'a aexp"
   364   | And "'a bexp"  "'a bexp"
   365   | Neg "'a bexp"
   366 
   367 text \<open>\<^medskip> Evaluation of arithmetic and boolean expressions\<close>
   368 
   369 primrec evala :: "('a \<Rightarrow> nat) \<Rightarrow> 'a aexp \<Rightarrow> nat"
   370   and evalb :: "('a \<Rightarrow> nat) \<Rightarrow> 'a bexp \<Rightarrow> bool"
   371 where
   372   "evala env (IF b a1 a2) = (if evalb env b then evala env a1 else evala env a2)"
   373 | "evala env (Sum a1 a2) = evala env a1 + evala env a2"
   374 | "evala env (Diff a1 a2) = evala env a1 - evala env a2"
   375 | "evala env (Var v) = env v"
   376 | "evala env (Num n) = n"
   377 | "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
   378 | "evalb env (And b1 b2) = (evalb env b1 \<and> evalb env b2)"
   379 | "evalb env (Neg b) = (\<not> evalb env b)"
   380 
   381 text \<open>
   382   Since the value of an expression depends on the value of its variables, the
   383   functions @{const evala} and @{const evalb} take an additional parameter, an
   384   \<^emph>\<open>environment\<close> that maps variables to their values.
   385 
   386   \<^medskip>
   387   Substitution on expressions can be defined similarly. The mapping \<open>f\<close> of
   388   type @{typ "'a \<Rightarrow> 'a aexp"} given as a parameter is lifted canonically on the
   389   types @{typ "'a aexp"} and @{typ "'a bexp"}, respectively.
   390 \<close>
   391 
   392 primrec substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
   393   and substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"
   394 where
   395   "substa f (IF b a1 a2) = IF (substb f b) (substa f a1) (substa f a2)"
   396 | "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"
   397 | "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"
   398 | "substa f (Var v) = f v"
   399 | "substa f (Num n) = Num n"
   400 | "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"
   401 | "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
   402 | "substb f (Neg b) = Neg (substb f b)"
   403 
   404 text \<open>
   405   In textbooks about semantics one often finds substitution theorems, which
   406   express the relationship between substitution and evaluation. For @{typ "'a
   407   aexp"} and @{typ "'a bexp"}, we can prove such a theorem by mutual
   408   induction, followed by simplification.
   409 \<close>
   410 
   411 lemma subst_one:
   412   "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
   413   "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
   414   by (induct a and b) simp_all
   415 
   416 lemma subst_all:
   417   "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
   418   "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
   419   by (induct a and b) simp_all
   420 (*<*)end(*>*)
   421 
   422 
   423 subsubsection \<open>Example: a substitution function for terms\<close>
   424 
   425 text \<open>Functions on datatypes with nested recursion are also defined
   426   by mutual primitive recursion.\<close>
   427 
   428 (*<*)experiment begin(*>*)
   429 datatype ('a, 'b) "term" = Var 'a | App 'b "('a, 'b) term list"
   430 
   431 text \<open>
   432   A substitution function on type @{typ "('a, 'b) term"} can be defined as
   433   follows, by working simultaneously on @{typ "('a, 'b) term list"}:
   434 \<close>
   435 
   436 primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term" and
   437   subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
   438 where
   439   "subst_term f (Var a) = f a"
   440 | "subst_term f (App b ts) = App b (subst_term_list f ts)"
   441 | "subst_term_list f [] = []"
   442 | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
   443 
   444 text \<open>
   445   The recursion scheme follows the structure of the unfolded definition of
   446   type @{typ "('a, 'b) term"}. To prove properties of this substitution
   447   function, mutual induction is needed:
   448 \<close>
   449 
   450 lemma "subst_term (subst_term f1 \<circ> f2) t =
   451     subst_term f1 (subst_term f2 t)" and
   452   "subst_term_list (subst_term f1 \<circ> f2) ts =
   453     subst_term_list f1 (subst_term_list f2 ts)"
   454   by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
   455 (*<*)end(*>*)
   456 
   457 
   458 subsubsection \<open>Example: a map function for infinitely branching trees\<close>
   459 
   460 text \<open>Defining functions on infinitely branching datatypes by primitive
   461   recursion is just as easy.\<close>
   462 
   463 (*<*)experiment begin(*>*)
   464 datatype 'a tree = Atom 'a | Branch "nat \<Rightarrow> 'a tree"
   465 
   466 primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
   467 where
   468   "map_tree f (Atom a) = Atom (f a)"
   469 | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
   470 
   471 text \<open>
   472   Note that all occurrences of functions such as \<open>ts\<close> above must be applied to
   473   an argument. In particular, @{term "map_tree f \<circ> ts"} is not allowed here.
   474 
   475   \<^medskip>
   476   Here is a simple composition lemma for @{term map_tree}:
   477 \<close>
   478 
   479 lemma "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
   480   by (induct t) simp_all
   481 (*<*)end(*>*)
   482 
   483 
   484 subsection \<open>Proof methods related to recursive definitions\<close>
   485 
   486 text \<open>
   487   \begin{matharray}{rcl}
   488     @{method_def (HOL) pat_completeness} & : & \<open>method\<close> \\
   489     @{method_def (HOL) relation} & : & \<open>method\<close> \\
   490     @{method_def (HOL) lexicographic_order} & : & \<open>method\<close> \\
   491     @{method_def (HOL) size_change} & : & \<open>method\<close> \\
   492     @{method_def (HOL) induction_schema} & : & \<open>method\<close> \\
   493   \end{matharray}
   494 
   495   @{rail \<open>
   496     @@{method (HOL) relation} @{syntax term}
   497     ;
   498     @@{method (HOL) lexicographic_order} (@{syntax clasimpmod} * )
   499     ;
   500     @@{method (HOL) size_change} ( orders (@{syntax clasimpmod} * ) )
   501     ;
   502     @@{method (HOL) induction_schema}
   503     ;
   504     orders: ( 'max' | 'min' | 'ms' ) *
   505   \<close>}
   506 
   507   \<^descr> @{method (HOL) pat_completeness} is a specialized method to solve goals
   508   regarding the completeness of pattern matching, as required by the @{command
   509   (HOL) "function"} package (cf.\ @{cite "isabelle-function"}).
   510 
   511   \<^descr> @{method (HOL) relation}~\<open>R\<close> introduces a termination proof using the
   512   relation \<open>R\<close>. The resulting proof state will contain goals expressing that
   513   \<open>R\<close> is wellfounded, and that the arguments of recursive calls decrease with
   514   respect to \<open>R\<close>. Usually, this method is used as the initial proof step of
   515   manual termination proofs.
   516 
   517   \<^descr> @{method (HOL) "lexicographic_order"} attempts a fully automated
   518   termination proof by searching for a lexicographic combination of size
   519   measures on the arguments of the function. The method accepts the same
   520   arguments as the @{method auto} method, which it uses internally to prove
   521   local descents. The @{syntax clasimpmod} modifiers are accepted (as for
   522   @{method auto}).
   523 
   524   In case of failure, extensive information is printed, which can help to
   525   analyse the situation (cf.\ @{cite "isabelle-function"}).
   526 
   527   \<^descr> @{method (HOL) "size_change"} also works on termination goals, using a
   528   variation of the size-change principle, together with a graph decomposition
   529   technique (see @{cite krauss_phd} for details). Three kinds of orders are
   530   used internally: \<open>max\<close>, \<open>min\<close>, and \<open>ms\<close> (multiset), which is only available
   531   when the theory \<open>Multiset\<close> is loaded. When no order kinds are given, they
   532   are tried in order. The search for a termination proof uses SAT solving
   533   internally.
   534 
   535   For local descent proofs, the @{syntax clasimpmod} modifiers are accepted
   536   (as for @{method auto}).
   537 
   538   \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
   539   from well-founded induction and completeness of patterns. This factors out
   540   some operations that are done internally by the function package and makes
   541   them available separately. See \<^file>\<open>~~/src/HOL/ex/Induction_Schema.thy\<close> for
   542   examples.
   543 \<close>
   544 
   545 
   546 subsection \<open>Functions with explicit partiality\<close>
   547 
   548 text \<open>
   549   \begin{matharray}{rcl}
   550     @{command_def (HOL) "partial_function"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   551     @{attribute_def (HOL) "partial_function_mono"} & : & \<open>attribute\<close> \\
   552   \end{matharray}
   553 
   554   @{rail \<open>
   555     @@{command (HOL) partial_function} '(' @{syntax name} ')'
   556       @{syntax specification}
   557   \<close>}
   558 
   559   \<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines recursive functions
   560   based on fixpoints in complete partial orders. No termination proof is
   561   required from the user or constructed internally. Instead, the possibility
   562   of non-termination is modelled explicitly in the result type, which contains
   563   an explicit bottom element.
   564 
   565   Pattern matching and mutual recursion are currently not supported. Thus, the
   566   specification consists of a single function described by a single recursive
   567   equation.
   568 
   569   There are no fixed syntactic restrictions on the body of the function, but
   570   the induced functional must be provably monotonic wrt.\ the underlying
   571   order. The monotonicity proof is performed internally, and the definition is
   572   rejected when it fails. The proof can be influenced by declaring hints using
   573   the @{attribute (HOL) partial_function_mono} attribute.
   574 
   575   The mandatory \<open>mode\<close> argument specifies the mode of operation of the
   576   command, which directly corresponds to a complete partial order on the
   577   result type. By default, the following modes are defined:
   578 
   579     \<^descr> \<open>option\<close> defines functions that map into the @{type option} type. Here,
   580     the value @{term None} is used to model a non-terminating computation.
   581     Monotonicity requires that if @{term None} is returned by a recursive
   582     call, then the overall result must also be @{term None}. This is best
   583     achieved through the use of the monadic operator @{const "Option.bind"}.
   584 
   585     \<^descr> \<open>tailrec\<close> defines functions with an arbitrary result type and uses the
   586     slightly degenerated partial order where @{term "undefined"} is the bottom
   587     element. Now, monotonicity requires that if @{term undefined} is returned
   588     by a recursive call, then the overall result must also be @{term
   589     undefined}. In practice, this is only satisfied when each recursive call
   590     is a tail call, whose result is directly returned. Thus, this mode of
   591     operation allows the definition of arbitrary tail-recursive functions.
   592 
   593   Experienced users may define new modes by instantiating the locale @{const
   594   "partial_function_definitions"} appropriately.
   595 
   596   \<^descr> @{attribute (HOL) partial_function_mono} declares rules for use in the
   597   internal monotonicity proofs of partial function definitions.
   598 \<close>
   599 
   600 
   601 subsection \<open>Old-style recursive function definitions (TFL)\<close>
   602 
   603 text \<open>
   604   \begin{matharray}{rcl}
   605     @{command_def (HOL) "recdef"} & : & \<open>theory \<rightarrow> theory)\<close> \\
   606   \end{matharray}
   607 
   608   The old TFL command @{command (HOL) "recdef"} for defining recursive is
   609   mostly obsolete; @{command (HOL) "function"} or @{command (HOL) "fun"}
   610   should be used instead.
   611 
   612   @{rail \<open>
   613     @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>
   614       @{syntax name} @{syntax term} (@{syntax prop} +) hints?
   615     ;
   616     hints: '(' @'hints' ( recdefmod * ) ')'
   617     ;
   618     recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
   619       (() | 'add' | 'del') ':' @{syntax thms}) | @{syntax clasimpmod}
   620   \<close>}
   621 
   622   \<^descr> @{command (HOL) "recdef"} defines general well-founded recursive functions
   623   (using the TFL package). The ``\<open>(permissive)\<close>'' option tells TFL to recover
   624   from failed proof attempts, returning unfinished results. The \<open>recdef_simp\<close>,
   625   \<open>recdef_cong\<close>, and \<open>recdef_wf\<close> hints refer to auxiliary rules to be used in
   626   the internal automated proof process of TFL. Additional @{syntax clasimpmod}
   627   declarations may be given to tune the context of the Simplifier (cf.\
   628   \secref{sec:simplifier}) and Classical reasoner (cf.\
   629   \secref{sec:classical}).
   630 
   631 
   632   \<^medskip>
   633   Hints for @{command (HOL) "recdef"} may be also declared globally, using the
   634   following attributes.
   635 
   636   \begin{matharray}{rcl}
   637     @{attribute_def (HOL) recdef_simp} & : & \<open>attribute\<close> \\
   638     @{attribute_def (HOL) recdef_cong} & : & \<open>attribute\<close> \\
   639     @{attribute_def (HOL) recdef_wf} & : & \<open>attribute\<close> \\
   640   \end{matharray}
   641 
   642   @{rail \<open>
   643     (@@{attribute (HOL) recdef_simp} | @@{attribute (HOL) recdef_cong} |
   644       @@{attribute (HOL) recdef_wf}) (() | 'add' | 'del')
   645   \<close>}
   646 \<close>
   647 
   648 
   649 section \<open>Adhoc overloading of constants\<close>
   650 
   651 text \<open>
   652   \begin{tabular}{rcll}
   653   @{command_def "adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   654   @{command_def "no_adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
   655   @{attribute_def "show_variants"} & : & \<open>attribute\<close> & default \<open>false\<close> \\
   656   \end{tabular}
   657 
   658   \<^medskip>
   659   Adhoc overloading allows to overload a constant depending on its type.
   660   Typically this involves the introduction of an uninterpreted constant (used
   661   for input and output) and the addition of some variants (used internally).
   662   For examples see \<^file>\<open>~~/src/HOL/ex/Adhoc_Overloading_Examples.thy\<close> and
   663   \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
   664 
   665   @{rail \<open>
   666     (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
   667       (@{syntax name} (@{syntax term} + ) + @'and')
   668   \<close>}
   669 
   670   \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
   671   existing constant.
   672 
   673   \<^descr> @{command "no_adhoc_overloading"} is similar to @{command
   674   "adhoc_overloading"}, but removes the specified variants from the present
   675   context.
   676 
   677   \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded
   678   constants. If enabled, the internally used variants are printed instead of
   679   their respective overloaded constants. This is occasionally useful to check
   680   whether the system agrees with a user's expectations about derived variants.
   681 \<close>
   682 
   683 
   684 section \<open>Definition by specification \label{sec:hol-specification}\<close>
   685 
   686 text \<open>
   687   \begin{matharray}{rcl}
   688     @{command_def (HOL) "specification"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
   689   \end{matharray}
   690 
   691   @{rail \<open>
   692     @@{command (HOL) specification} '(' (decl +) ')' \<newline>
   693       (@{syntax thmdecl}? @{syntax prop} +)
   694     ;
   695     decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')?
   696   \<close>}
   697 
   698   \<^descr> @{command (HOL) "specification"}~\<open>decls \<phi>\<close> sets up a goal stating the
   699   existence of terms with the properties specified to hold for the constants
   700   given in \<open>decls\<close>. After finishing the proof, the theory will be augmented
   701   with definitions for the given constants, as well as with theorems stating
   702   the properties for these constants.
   703 
   704   \<open>decl\<close> declares a constant to be defined by the specification given. The
   705   definition for the constant \<open>c\<close> is bound to the name \<open>c_def\<close> unless a
   706   theorem name is given in the declaration. Overloaded constants should be
   707   declared as such.
   708 \<close>
   709 
   710 
   711 section \<open>Old-style datatypes \label{sec:hol-datatype}\<close>
   712 
   713 text \<open>
   714   \begin{matharray}{rcl}
   715     @{command_def (HOL) "old_datatype"} & : & \<open>theory \<rightarrow> theory\<close> \\
   716     @{command_def (HOL) "old_rep_datatype"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
   717   \end{matharray}
   718 
   719   @{rail \<open>
   720     @@{command (HOL) old_datatype} (spec + @'and')
   721     ;
   722     @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
   723     ;
   724 
   725     spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
   726     ;
   727     cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}?
   728   \<close>}
   729 
   730   \<^descr> @{command (HOL) "old_datatype"} defines old-style inductive
   731   datatypes in HOL.
   732 
   733   \<^descr> @{command (HOL) "old_rep_datatype"} represents existing types as
   734   old-style datatypes.
   735 
   736 
   737   These commands are mostly obsolete; @{command (HOL) "datatype"} should be
   738   used instead.
   739 
   740   See @{cite "isabelle-datatypes"} for more details on datatypes. Apart from
   741   proper proof methods for case analysis and induction, there are also
   742   emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
   743   induct_tac} available, see \secref{sec:hol-induct-tac}; these admit to refer
   744   directly to the internal structure of subgoals (including internally bound
   745   parameters).
   746 \<close>
   747 
   748 
   749 subsubsection \<open>Examples\<close>
   750 
   751 text \<open>
   752   We define a type of finite sequences, with slightly different names than the
   753   existing @{typ "'a list"} that is already in @{theory Main}:
   754 \<close>
   755 
   756 (*<*)experiment begin(*>*)
   757 datatype 'a seq = Empty | Seq 'a "'a seq"
   758 
   759 text \<open>We can now prove some simple lemma by structural induction:\<close>
   760 
   761 lemma "Seq x xs \<noteq> xs"
   762 proof (induct xs arbitrary: x)
   763   case Empty
   764   txt \<open>This case can be proved using the simplifier: the freeness
   765     properties of the datatype are already declared as @{attribute
   766     simp} rules.\<close>
   767   show "Seq x Empty \<noteq> Empty"
   768     by simp
   769 next
   770   case (Seq y ys)
   771   txt \<open>The step case is proved similarly.\<close>
   772   show "Seq x (Seq y ys) \<noteq> Seq y ys"
   773     using \<open>Seq y ys \<noteq> ys\<close> by simp
   774 qed
   775 
   776 text \<open>Here is a more succinct version of the same proof:\<close>
   777 
   778 lemma "Seq x xs \<noteq> xs"
   779   by (induct xs arbitrary: x) simp_all
   780 (*<*)end(*>*)
   781 
   782 
   783 section \<open>Records \label{sec:hol-record}\<close>
   784 
   785 text \<open>
   786   In principle, records merely generalize the concept of tuples, where
   787   components may be addressed by labels instead of just position. The logical
   788   infrastructure of records in Isabelle/HOL is slightly more advanced, though,
   789   supporting truly extensible record schemes. This admits operations that are
   790   polymorphic with respect to record extension, yielding ``object-oriented''
   791   effects like (single) inheritance. See also @{cite "NaraschewskiW-TPHOLs98"}
   792   for more details on object-oriented verification and record subtyping in
   793   HOL.
   794 \<close>
   795 
   796 
   797 subsection \<open>Basic concepts\<close>
   798 
   799 text \<open>
   800   Isabelle/HOL supports both \<^emph>\<open>fixed\<close> and \<^emph>\<open>schematic\<close> records at the level of
   801   terms and types. The notation is as follows:
   802 
   803   \begin{center}
   804   \begin{tabular}{l|l|l}
   805     & record terms & record types \\ \hline
   806     fixed & \<open>\<lparr>x = a, y = b\<rparr>\<close> & \<open>\<lparr>x :: A, y :: B\<rparr>\<close> \\
   807     schematic & \<open>\<lparr>x = a, y = b, \<dots> = m\<rparr>\<close> &
   808       \<open>\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>\<close> \\
   809   \end{tabular}
   810   \end{center}
   811 
   812   The ASCII representation of \<open>\<lparr>x = a\<rparr>\<close> is \<open>(| x = a |)\<close>.
   813 
   814   A fixed record \<open>\<lparr>x = a, y = b\<rparr>\<close> has field \<open>x\<close> of value \<open>a\<close> and field \<open>y\<close> of
   815   value \<open>b\<close>. The corresponding type is \<open>\<lparr>x :: A, y :: B\<rparr>\<close>, assuming that \<open>a ::
   816   A\<close> and \<open>b :: B\<close>.
   817 
   818   A record scheme like \<open>\<lparr>x = a, y = b, \<dots> = m\<rparr>\<close> contains fields \<open>x\<close> and \<open>y\<close> as
   819   before, but also possibly further fields as indicated by the ``\<open>\<dots>\<close>''
   820   notation (which is actually part of the syntax). The improper field ``\<open>\<dots>\<close>''
   821   of a record scheme is called the \<^emph>\<open>more part\<close>. Logically it is just a free
   822   variable, which is occasionally referred to as ``row variable'' in the
   823   literature. The more part of a record scheme may be instantiated by zero or
   824   more further components. For example, the previous scheme may get
   825   instantiated to \<open>\<lparr>x = a, y = b, z = c, \<dots> = m'\<rparr>\<close>, where \<open>m'\<close> refers to a
   826   different more part. Fixed records are special instances of record schemes,
   827   where ``\<open>\<dots>\<close>'' is properly terminated by the \<open>() :: unit\<close> element. In fact,
   828   \<open>\<lparr>x = a, y = b\<rparr>\<close> is just an abbreviation for \<open>\<lparr>x = a, y = b, \<dots> = ()\<rparr>\<close>.
   829 
   830   \<^medskip>
   831   Two key observations make extensible records in a simply typed language like
   832   HOL work out:
   833 
   834   \<^enum> the more part is internalized, as a free term or type variable,
   835 
   836   \<^enum> field names are externalized, they cannot be accessed within the logic as
   837   first-class values.
   838 
   839 
   840   \<^medskip>
   841   In Isabelle/HOL record types have to be defined explicitly, fixing their
   842   field names and types, and their (optional) parent record. Afterwards,
   843   records may be formed using above syntax, while obeying the canonical order
   844   of fields as given by their declaration. The record package provides several
   845   standard operations like selectors and updates. The common setup for various
   846   generic proof tools enable succinct reasoning patterns. See also the
   847   Isabelle/HOL tutorial @{cite "isabelle-hol-book"} for further instructions
   848   on using records in practice.
   849 \<close>
   850 
   851 
   852 subsection \<open>Record specifications\<close>
   853 
   854 text \<open>
   855   \begin{matharray}{rcl}
   856     @{command_def (HOL) "record"} & : & \<open>theory \<rightarrow> theory\<close> \\
   857     @{command_def (HOL) "print_record"} & : & \<open>context \<rightarrow>\<close> \\
   858   \end{matharray}
   859 
   860   @{rail \<open>
   861     @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \<newline>
   862       (@{syntax type} '+')? (constdecl +)
   863     ;
   864     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
   865     ;
   866     @@{command (HOL) print_record} modes? @{syntax typespec_sorts}
   867     ;
   868     modes: '(' (@{syntax name} +) ')'
   869   \<close>}
   870 
   871   \<^descr> @{command (HOL) "record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1 \<dots> c\<^sub>n :: \<sigma>\<^sub>n\<close>
   872   defines extensible record type \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>, derived from the optional
   873   parent record \<open>\<tau>\<close> by adding new field components \<open>c\<^sub>i :: \<sigma>\<^sub>i\<close> etc.
   874 
   875   The type variables of \<open>\<tau>\<close> and \<open>\<sigma>\<^sub>i\<close> need to be covered by the (distinct)
   876   parameters \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m\<close>. Type constructor \<open>t\<close> has to be new, while \<open>\<tau>\<close>
   877   needs to specify an instance of an existing record type. At least one new
   878   field \<open>c\<^sub>i\<close> has to be specified. Basically, field names need to belong to a
   879   unique record. This is not a real restriction in practice, since fields are
   880   qualified by the record name internally.
   881 
   882   The parent record specification \<open>\<tau>\<close> is optional; if omitted \<open>t\<close> becomes a
   883   root record. The hierarchy of all records declared within a theory context
   884   forms a forest structure, i.e.\ a set of trees starting with a root record
   885   each. There is no way to merge multiple parent records!
   886 
   887   For convenience, \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> is made a type abbreviation for the fixed
   888   record type \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>\<close>, likewise is \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>)
   889   t_scheme\<close> made an abbreviation for \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> :: \<zeta>\<rparr>\<close>.
   890 
   891   \<^descr> @{command (HOL) "print_record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> prints the definition of
   892   record \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>. Optionally \<open>modes\<close> can be specified, which are
   893   appended to the current print mode; see \secref{sec:print-modes}.
   894 \<close>
   895 
   896 
   897 subsection \<open>Record operations\<close>
   898 
   899 text \<open>
   900   Any record definition of the form presented above produces certain standard
   901   operations. Selectors and updates are provided for any field, including the
   902   improper one ``\<open>more\<close>''. There are also cumulative record constructor
   903   functions. To simplify the presentation below, we assume for now that \<open>(\<alpha>\<^sub>1,
   904   \<dots>, \<alpha>\<^sub>m) t\<close> is a root record with fields \<open>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<close>.
   905 
   906   \<^medskip>
   907   \<^bold>\<open>Selectors\<close> and \<^bold>\<open>updates\<close> are available for any
   908   field (including ``\<open>more\<close>''):
   909 
   910   \begin{matharray}{lll}
   911     \<open>c\<^sub>i\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i\<close> \\
   912     \<open>c\<^sub>i_update\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>i \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>\<close> \\
   913   \end{matharray}
   914 
   915   There is special syntax for application of updates: \<open>r\<lparr>x := a\<rparr>\<close> abbreviates
   916   term \<open>x_update a r\<close>. Further notation for repeated updates is also
   917   available: \<open>r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z := c\<rparr>\<close> may be written \<open>r\<lparr>x := a, y := b, z
   918   := c\<rparr>\<close>. Note that because of postfix notation the order of fields shown here
   919   is reverse than in the actual term. Since repeated updates are just function
   920   applications, fields may be freely permuted in \<open>\<lparr>x := a, y := b, z := c\<rparr>\<close>,
   921   as far as logical equality is concerned. Thus commutativity of independent
   922   updates can be proven within the logic for any two fields, but not as a
   923   general theorem.
   924 
   925   \<^medskip>
   926   The \<^bold>\<open>make\<close> operation provides a cumulative record constructor function:
   927 
   928   \begin{matharray}{lll}
   929     \<open>t.make\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
   930   \end{matharray}
   931 
   932   \<^medskip>
   933   We now reconsider the case of non-root records, which are derived of some
   934   parent. In general, the latter may depend on another parent as well,
   935   resulting in a list of \<^emph>\<open>ancestor records\<close>. Appending the lists of fields of
   936   all ancestors results in a certain field prefix. The record package
   937   automatically takes care of this by lifting operations over this context of
   938   ancestor fields. Assuming that \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> has ancestor fields \<open>b\<^sub>1 ::
   939   \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k\<close>, the above record operations will get the following
   940   types:
   941 
   942   \<^medskip>
   943   \begin{tabular}{lll}
   944     \<open>c\<^sub>i\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i\<close> \\
   945     \<open>c\<^sub>i_update\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>i \<Rightarrow>
   946       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
   947       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>\<close> \\
   948     \<open>t.make\<close> & \<open>::\<close> & \<open>\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
   949       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
   950   \end{tabular}
   951   \<^medskip>
   952 
   953   Some further operations address the extension aspect of a derived record
   954   scheme specifically: \<open>t.fields\<close> produces a record fragment consisting of
   955   exactly the new fields introduced here (the result may serve as a more part
   956   elsewhere); \<open>t.extend\<close> takes a fixed record and adds a given more part;
   957   \<open>t.truncate\<close> restricts a record scheme to a fixed record.
   958 
   959   \<^medskip>
   960   \begin{tabular}{lll}
   961     \<open>t.fields\<close> & \<open>::\<close> & \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
   962     \<open>t.extend\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
   963       \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>\<close> \\
   964     \<open>t.truncate\<close> & \<open>::\<close> & \<open>\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>\<close> \\
   965   \end{tabular}
   966   \<^medskip>
   967 
   968   Note that \<open>t.make\<close> and \<open>t.fields\<close> coincide for root records.
   969 \<close>
   970 
   971 
   972 subsection \<open>Derived rules and proof tools\<close>
   973 
   974 text \<open>
   975   The record package proves several results internally, declaring these facts
   976   to appropriate proof tools. This enables users to reason about record
   977   structures quite conveniently. Assume that \<open>t\<close> is a record type as specified
   978   above.
   979 
   980   \<^enum> Standard conversions for selectors or updates applied to record
   981   constructor terms are made part of the default Simplifier context; thus
   982   proofs by reduction of basic operations merely require the @{method simp}
   983   method without further arguments. These rules are available as \<open>t.simps\<close>,
   984   too.
   985 
   986   \<^enum> Selectors applied to updated records are automatically reduced by an
   987   internal simplification procedure, which is also part of the standard
   988   Simplifier setup.
   989 
   990   \<^enum> Inject equations of a form analogous to @{prop "(x, y) = (x', y') \<equiv> x = x'
   991   \<and> y = y'"} are declared to the Simplifier and Classical Reasoner as
   992   @{attribute iff} rules. These rules are available as \<open>t.iffs\<close>.
   993 
   994   \<^enum> The introduction rule for record equality analogous to \<open>x r = x r' \<Longrightarrow> y r =
   995   y r' \<dots> \<Longrightarrow> r = r'\<close> is declared to the Simplifier, and as the basic rule
   996   context as ``@{attribute intro}\<open>?\<close>''. The rule is called \<open>t.equality\<close>.
   997 
   998   \<^enum> Representations of arbitrary record expressions as canonical constructor
   999   terms are provided both in @{method cases} and @{method induct} format (cf.\
  1000   the generic proof methods of the same name, \secref{sec:cases-induct}).
  1001   Several variations are available, for fixed records, record schemes, more
  1002   parts etc.
  1003 
  1004   The generic proof methods are sufficiently smart to pick the most sensible
  1005   rule according to the type of the indicated record expression: users just
  1006   need to apply something like ``\<open>(cases r)\<close>'' to a certain proof problem.
  1007 
  1008   \<^enum> The derived record operations \<open>t.make\<close>, \<open>t.fields\<close>, \<open>t.extend\<close>,
  1009   \<open>t.truncate\<close> are \<^emph>\<open>not\<close> treated automatically, but usually need to be
  1010   expanded by hand, using the collective fact \<open>t.defs\<close>.
  1011 \<close>
  1012 
  1013 
  1014 subsubsection \<open>Examples\<close>
  1015 
  1016 text \<open>See \<^file>\<open>~~/src/HOL/ex/Records.thy\<close>, for example.\<close>
  1017 
  1018 
  1019 section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
  1020 
  1021 text \<open>
  1022   \begin{matharray}{rcl}
  1023     @{command_def (HOL) "typedef"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
  1024   \end{matharray}
  1025 
  1026   A type definition identifies a new type with a non-empty subset of an
  1027   existing type. More precisely, the new type is defined by exhibiting an
  1028   existing type \<open>\<tau>\<close>, a set \<open>A :: \<tau> set\<close>, and proving @{prop "\<exists>x. x \<in> A"}. Thus
  1029   \<open>A\<close> is a non-empty subset of \<open>\<tau>\<close>, and the new type denotes this subset. New
  1030   functions are postulated that establish an isomorphism between the new type
  1031   and the subset. In general, the type \<open>\<tau>\<close> may involve type variables \<open>\<alpha>\<^sub>1, \<dots>,
  1032   \<alpha>\<^sub>n\<close> which means that the type definition produces a type constructor \<open>(\<alpha>\<^sub>1,
  1033   \<dots>, \<alpha>\<^sub>n) t\<close> depending on those type arguments.
  1034 
  1035   @{rail \<open>
  1036     @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
  1037     ;
  1038     @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
  1039     ;
  1040     abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
  1041     ;
  1042     rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})?
  1043   \<close>}
  1044 
  1045   To understand the concept of type definition better, we need to recount its
  1046   somewhat complex history. The HOL logic goes back to the ``Simple Theory of
  1047   Types'' (STT) of A. Church @{cite "church40"}, which is further explained in
  1048   the book by P. Andrews @{cite "andrews86"}. The overview article by W.
  1049   Farmer @{cite "Farmer:2008"} points out the ``seven virtues'' of this
  1050   relatively simple family of logics. STT has only ground types, without
  1051   polymorphism and without type definitions.
  1052 
  1053   \<^medskip>
  1054   M. Gordon @{cite "Gordon:1985:HOL"} augmented Church's STT by adding
  1055   schematic polymorphism (type variables and type constructors) and a facility
  1056   to introduce new types as semantic subtypes from existing types. This
  1057   genuine extension of the logic was explained semantically by A. Pitts in the
  1058   book of the original Cambridge HOL88 system @{cite "pitts93"}. Type
  1059   definitions work in this setting, because the general model-theory of STT is
  1060   restricted to models that ensure that the universe of type interpretations
  1061   is closed by forming subsets (via predicates taken from the logic).
  1062 
  1063   \<^medskip>
  1064   Isabelle/HOL goes beyond Gordon-style HOL by admitting overloaded constant
  1065   definitions @{cite "Wenzel:1997:TPHOL" and "Haftmann-Wenzel:2006:classes"},
  1066   which are actually a concept of Isabelle/Pure and do not depend on
  1067   particular set-theoretic semantics of HOL. Over many years, there was no
  1068   formal checking of semantic type definitions in Isabelle/HOL versus
  1069   syntactic constant definitions in Isabelle/Pure. So the @{command typedef}
  1070   command was described as ``axiomatic'' in the sense of
  1071   \secref{sec:axiomatizations}, only with some local checks of the given type
  1072   and its representing set.
  1073 
  1074   Recent clarification of overloading in the HOL logic proper @{cite
  1075   "Kuncar-Popescu:2015"} demonstrates how the dissimilar concepts of constant
  1076   definitions versus type definitions may be understood uniformly. This
  1077   requires an interpretation of Isabelle/HOL that substantially reforms the
  1078   set-theoretic model of A. Pitts @{cite "pitts93"}, by taking a schematic
  1079   view on polymorphism and interpreting only ground types in the set-theoretic
  1080   sense of HOL88. Moreover, type-constructors may be explicitly overloaded,
  1081   e.g.\ by making the subset depend on type-class parameters (cf.\
  1082   \secref{sec:class}). This is semantically like a dependent type: the meaning
  1083   relies on the operations provided by different type-class instances.
  1084 
  1085   \<^descr> @{command (HOL) "typedef"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A\<close> defines a new type \<open>(\<alpha>\<^sub>1,
  1086   \<dots>, \<alpha>\<^sub>n) t\<close> from the set \<open>A\<close> over an existing type. The set \<open>A\<close> may contain
  1087   type variables \<open>\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n\<close> as specified on the LHS, but no term variables.
  1088   Non-emptiness of \<open>A\<close> needs to be proven on the spot, in order to turn the
  1089   internal conditional characterization into usable theorems.
  1090 
  1091   The ``\<open>(overloaded)\<close>'' option allows the @{command "typedef"} specification
  1092   to depend on constants that are not (yet) specified and thus left open as
  1093   parameters, e.g.\ type-class parameters.
  1094 
  1095   Within a local theory specification, the newly introduced type constructor
  1096   cannot depend on parameters or assumptions of the context: this is
  1097   syntactically impossible in HOL. The non-emptiness proof may formally depend
  1098   on local assumptions, but this has little practical relevance.
  1099 
  1100   For @{command (HOL) "typedef"}~\<open>t = A\<close> the newly introduced type \<open>t\<close> is
  1101   accompanied by a pair of morphisms to relate it to the representing set over
  1102   the old type. By default, the injection from type to set is called \<open>Rep_t\<close>
  1103   and its inverse \<open>Abs_t\<close>: An explicit @{keyword (HOL) "morphisms"}
  1104   specification allows to provide alternative names.
  1105 
  1106   The logical characterization of @{command typedef} uses the predicate of
  1107   locale @{const type_definition} that is defined in Isabelle/HOL. Various
  1108   basic consequences of that are instantiated accordingly, re-using the locale
  1109   facts with names derived from the new type constructor. Thus the generic
  1110   theorem @{thm type_definition.Rep} is turned into the specific \<open>Rep_t\<close>, for
  1111   example.
  1112 
  1113   Theorems @{thm type_definition.Rep}, @{thm type_definition.Rep_inverse}, and
  1114   @{thm type_definition.Abs_inverse} provide the most basic characterization
  1115   as a corresponding injection/surjection pair (in both directions). The
  1116   derived rules @{thm type_definition.Rep_inject} and @{thm
  1117   type_definition.Abs_inject} provide a more convenient version of
  1118   injectivity, suitable for automated proof tools (e.g.\ in declarations
  1119   involving @{attribute simp} or @{attribute iff}). Furthermore, the rules
  1120   @{thm type_definition.Rep_cases}~/ @{thm type_definition.Rep_induct}, and
  1121   @{thm type_definition.Abs_cases}~/ @{thm type_definition.Abs_induct} provide
  1122   alternative views on surjectivity. These rules are already declared as set
  1123   or type rules for the generic @{method cases} and @{method induct} methods,
  1124   respectively.
  1125 \<close>
  1126 
  1127 
  1128 subsubsection \<open>Examples\<close>
  1129 
  1130 text \<open>
  1131   The following trivial example pulls a three-element type into existence
  1132   within the formal logical environment of Isabelle/HOL.\<close>
  1133 
  1134 (*<*)experiment begin(*>*)
  1135 typedef three = "{(True, True), (True, False), (False, True)}"
  1136   by blast
  1137 
  1138 definition "One = Abs_three (True, True)"
  1139 definition "Two = Abs_three (True, False)"
  1140 definition "Three = Abs_three (False, True)"
  1141 
  1142 lemma three_distinct: "One \<noteq> Two"  "One \<noteq> Three"  "Two \<noteq> Three"
  1143   by (simp_all add: One_def Two_def Three_def Abs_three_inject)
  1144 
  1145 lemma three_cases:
  1146   fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
  1147   by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
  1148 (*<*)end(*>*)
  1149 
  1150 text \<open>Note that such trivial constructions are better done with
  1151   derived specification mechanisms such as @{command datatype}:\<close>
  1152 
  1153 (*<*)experiment begin(*>*)
  1154 datatype three = One | Two | Three
  1155 (*<*)end(*>*)
  1156 
  1157 text \<open>This avoids re-doing basic definitions and proofs from the
  1158   primitive @{command typedef} above.\<close>
  1159 
  1160 
  1161 
  1162 section \<open>Functorial structure of types\<close>
  1163 
  1164 text \<open>
  1165   \begin{matharray}{rcl}
  1166     @{command_def (HOL) "functor"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>
  1167   \end{matharray}
  1168 
  1169   @{rail \<open>
  1170     @@{command (HOL) functor} (@{syntax name} ':')? @{syntax term}
  1171   \<close>}
  1172 
  1173   \<^descr> @{command (HOL) "functor"}~\<open>prefix: m\<close> allows to prove and register
  1174   properties about the functorial structure of type constructors. These
  1175   properties then can be used by other packages to deal with those type
  1176   constructors in certain type constructions. Characteristic theorems are
  1177   noted in the current local theory. By default, they are prefixed with the
  1178   base name of the type constructor, an explicit prefix can be given
  1179   alternatively.
  1180 
  1181   The given term \<open>m\<close> is considered as \<^emph>\<open>mapper\<close> for the corresponding type
  1182   constructor and must conform to the following type pattern:
  1183 
  1184   \begin{matharray}{lll}
  1185     \<open>m\<close> & \<open>::\<close> &
  1186       \<open>\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>k \<Rightarrow> (\<^vec>\<alpha>\<^sub>n) t \<Rightarrow> (\<^vec>\<beta>\<^sub>n) t\<close> \\
  1187   \end{matharray}
  1188 
  1189   where \<open>t\<close> is the type constructor, \<open>\<^vec>\<alpha>\<^sub>n\<close> and \<open>\<^vec>\<beta>\<^sub>n\<close> are
  1190   distinct type variables free in the local theory and \<open>\<sigma>\<^sub>1\<close>, \ldots, \<open>\<sigma>\<^sub>k\<close> is
  1191   a subsequence of \<open>\<alpha>\<^sub>1 \<Rightarrow> \<beta>\<^sub>1\<close>, \<open>\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1\<close>, \ldots, \<open>\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n\<close>, \<open>\<beta>\<^sub>n \<Rightarrow> \<alpha>\<^sub>n\<close>.
  1192 \<close>
  1193 
  1194 
  1195 section \<open>Quotient types with lifting and transfer\<close>
  1196 
  1197 text \<open>
  1198   The quotient package defines a new quotient type given a raw type and a
  1199   partial equivalence relation (\secref{sec:quotient-type}). The package also
  1200   historically includes automation for transporting definitions and theorems
  1201   (\secref{sec:old-quotient}), but most of this automation was superseded by
  1202   the Lifting (\secref{sec:lifting}) and Transfer (\secref{sec:transfer})
  1203   packages.
  1204 \<close>
  1205 
  1206 
  1207 subsection \<open>Quotient type definition \label{sec:quotient-type}\<close>
  1208 
  1209 text \<open>
  1210   \begin{matharray}{rcl}
  1211     @{command_def (HOL) "quotient_type"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>\\
  1212   \end{matharray}
  1213 
  1214   @{rail \<open>
  1215     @@{command (HOL) quotient_type} @{syntax "overloaded"}? \<newline>
  1216       @{syntax typespec} @{syntax mixfix}? '=' quot_type \<newline>
  1217       quot_morphisms? quot_parametric?
  1218     ;
  1219     quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
  1220     ;
  1221     quot_morphisms: @'morphisms' @{syntax name} @{syntax name}
  1222     ;
  1223     quot_parametric: @'parametric' @{syntax thm}
  1224   \<close>}
  1225 
  1226   \<^descr> @{command (HOL) "quotient_type"} defines a new quotient type \<open>\<tau>\<close>. The
  1227   injection from a quotient type to a raw type is called \<open>rep_\<tau>\<close>, its inverse
  1228   \<open>abs_\<tau>\<close> unless explicit @{keyword (HOL) "morphisms"} specification provides
  1229   alternative names. @{command (HOL) "quotient_type"} requires the user to
  1230   prove that the relation is an equivalence relation (predicate \<open>equivp\<close>),
  1231   unless the user specifies explicitly \<open>partial\<close> in which case the obligation
  1232   is \<open>part_equivp\<close>. A quotient defined with \<open>partial\<close> is weaker in the sense
  1233   that less things can be proved automatically.
  1234 
  1235   The command internally proves a Quotient theorem and sets up the Lifting
  1236   package by the command @{command (HOL) setup_lifting}. Thus the Lifting and
  1237   Transfer packages can be used also with quotient types defined by @{command
  1238   (HOL) "quotient_type"} without any extra set-up. The parametricity theorem
  1239   for the equivalence relation R can be provided as an extra argument of the
  1240   command and is passed to the corresponding internal call of @{command (HOL)
  1241   setup_lifting}. This theorem allows the Lifting package to generate a
  1242   stronger transfer rule for equality.
  1243 \<close>
  1244 
  1245 
  1246 subsection \<open>Lifting package \label{sec:lifting}\<close>
  1247 
  1248 text \<open>
  1249   The Lifting package allows users to lift terms of the raw type to the
  1250   abstract type, which is a necessary step in building a library for an
  1251   abstract type. Lifting defines a new constant by combining coercion
  1252   functions (@{term Abs} and @{term Rep}) with the raw term. It also proves an
  1253   appropriate transfer rule for the Transfer (\secref{sec:transfer}) package
  1254   and, if possible, an equation for the code generator.
  1255 
  1256   The Lifting package provides two main commands: @{command (HOL)
  1257   "setup_lifting"} for initializing the package to work with a new type, and
  1258   @{command (HOL) "lift_definition"} for lifting constants. The Lifting
  1259   package works with all four kinds of type abstraction: type copies,
  1260   subtypes, total quotients and partial quotients.
  1261 
  1262   Theoretical background can be found in @{cite
  1263   "Huffman-Kuncar:2013:lifting_transfer"}.
  1264 
  1265   \begin{matharray}{rcl}
  1266     @{command_def (HOL) "setup_lifting"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
  1267     @{command_def (HOL) "lift_definition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>\\
  1268     @{command_def (HOL) "lifting_forget"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
  1269     @{command_def (HOL) "lifting_update"} & : & \<open>local_theory \<rightarrow> local_theory\<close>\\
  1270     @{command_def (HOL) "print_quot_maps"} & : & \<open>context \<rightarrow>\<close>\\
  1271     @{command_def (HOL) "print_quotients"} & : & \<open>context \<rightarrow>\<close>\\
  1272     @{attribute_def (HOL) "quot_map"} & : & \<open>attribute\<close> \\
  1273     @{attribute_def (HOL) "relator_eq_onp"} & : & \<open>attribute\<close> \\
  1274     @{attribute_def (HOL) "relator_mono"} & : & \<open>attribute\<close> \\
  1275     @{attribute_def (HOL) "relator_distr"} & : & \<open>attribute\<close> \\
  1276     @{attribute_def (HOL) "quot_del"} & : & \<open>attribute\<close> \\
  1277     @{attribute_def (HOL) "lifting_restore"} & : & \<open>attribute\<close> \\
  1278   \end{matharray}
  1279 
  1280   @{rail \<open>
  1281     @@{command (HOL) setup_lifting} @{syntax thm} @{syntax thm}? \<newline>
  1282       (@'parametric' @{syntax thm})?
  1283     ;
  1284     @@{command (HOL) lift_definition} ('(' 'code_dt' ')')? \<newline>
  1285       @{syntax name} '::' @{syntax type} @{syntax mixfix}? 'is' @{syntax term} \<newline>
  1286       (@'parametric' (@{syntax thm}+))?
  1287     ;
  1288     @@{command (HOL) lifting_forget} @{syntax name}
  1289     ;
  1290     @@{command (HOL) lifting_update} @{syntax name}
  1291     ;
  1292     @@{attribute (HOL) lifting_restore}
  1293       @{syntax thm} (@{syntax thm} @{syntax thm})?
  1294   \<close>}
  1295 
  1296   \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work with
  1297   a user-defined type. The command supports two modes.
  1298 
  1299     \<^enum> The first one is a low-level mode when the user must provide as a first
  1300     argument of @{command (HOL) "setup_lifting"} a quotient theorem @{term
  1301     "Quotient R Abs Rep T"}. The package configures a transfer rule for
  1302     equality, a domain transfer rules and sets up the @{command_def (HOL)
  1303     "lift_definition"} command to work with the abstract type. An optional
  1304     theorem @{term "reflp R"}, which certifies that the equivalence relation R
  1305     is total, can be provided as a second argument. This allows the package to
  1306     generate stronger transfer rules. And finally, the parametricity theorem
  1307     for @{term R} can be provided as a third argument. This allows the package
  1308     to generate a stronger transfer rule for equality.
  1309 
  1310     Users generally will not prove the \<open>Quotient\<close> theorem manually for new
  1311     types, as special commands exist to automate the process.
  1312 
  1313     \<^enum> When a new subtype is defined by @{command (HOL) typedef}, @{command
  1314     (HOL) "lift_definition"} can be used in its second mode, where only the
  1315     @{term type_definition} theorem @{term "type_definition Rep Abs A"} is
  1316     used as an argument of the command. The command internally proves the
  1317     corresponding @{term Quotient} theorem and registers it with @{command
  1318     (HOL) setup_lifting} using its first mode.
  1319 
  1320   For quotients, the command @{command (HOL) quotient_type} can be used. The
  1321   command defines a new quotient type and similarly to the previous case, the
  1322   corresponding Quotient theorem is proved and registered by @{command (HOL)
  1323   setup_lifting}.
  1324 
  1325   \<^medskip>
  1326   The command @{command (HOL) "setup_lifting"} also sets up the code generator
  1327   for the new type. Later on, when a new constant is defined by @{command
  1328   (HOL) "lift_definition"}, the Lifting package proves and registers a code
  1329   equation (if there is one) for the new constant.
  1330 
  1331   \<^descr> @{command (HOL) "lift_definition"} \<open>f :: \<tau>\<close> @{keyword (HOL) "is"} \<open>t\<close>
  1332   Defines a new function \<open>f\<close> with an abstract type \<open>\<tau>\<close> in terms of a
  1333   corresponding operation \<open>t\<close> on a representation type. More formally, if \<open>t
  1334   :: \<sigma>\<close>, then the command builds a term \<open>F\<close> as a corresponding combination of
  1335   abstraction and representation functions such that \<open>F :: \<sigma> \<Rightarrow> \<tau>\<close> and defines
  1336   \<open>f \<equiv> F t\<close>. The term \<open>t\<close> does not have to be necessarily a constant but it
  1337   can be any term.
  1338 
  1339   The command opens a proof and the user must discharge a respectfulness proof
  1340   obligation. For a type copy, i.e.\ a typedef with \<open>UNIV\<close>, the obligation is
  1341   discharged automatically. The proof goal is presented in a user-friendly,
  1342   readable form. A respectfulness theorem in the standard format \<open>f.rsp\<close> and a
  1343   transfer rule \<open>f.transfer\<close> for the Transfer package are generated by the
  1344   package.
  1345 
  1346   The user can specify a parametricity theorems for \<open>t\<close> after the keyword
  1347   @{keyword "parametric"}, which allows the command to generate parametric
  1348   transfer rules for \<open>f\<close>.
  1349 
  1350   For each constant defined through trivial quotients (type copies or
  1351   subtypes) \<open>f.rep_eq\<close> is generated. The equation is a code certificate that
  1352   defines \<open>f\<close> using the representation function.
  1353 
  1354   For each constant \<open>f.abs_eq\<close> is generated. The equation is unconditional for
  1355   total quotients. The equation defines \<open>f\<close> using the abstraction function.
  1356 
  1357   \<^medskip>
  1358   Integration with [@{attribute code} abstract]: For subtypes (e.g.\
  1359   corresponding to a datatype invariant, such as @{typ "'a dlist"}), @{command
  1360   (HOL) "lift_definition"} uses a code certificate theorem \<open>f.rep_eq\<close> as a
  1361   code equation. Because of the limitation of the code generator, \<open>f.rep_eq\<close>
  1362   cannot be used as a code equation if the subtype occurs inside the result
  1363   type rather than at the top level (e.g.\ function returning @{typ "'a dlist
  1364   option"} vs. @{typ "'a dlist"}).
  1365 
  1366   In this case, an extension of @{command (HOL) "lift_definition"} can be
  1367   invoked by specifying the flag \<open>code_dt\<close>. This extension enables code
  1368   execution through series of internal type and lifting definitions if the
  1369   return type \<open>\<tau>\<close> meets the following inductive conditions:
  1370 
  1371     \<^descr> \<open>\<tau>\<close> is a type variable
  1372 
  1373     \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>, where \<open>\<kappa>\<close> is an abstract type constructor and \<open>\<tau>\<^sub>1 \<dots>
  1374     \<tau>\<^sub>n\<close> do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed
  1375     whereas @{typ "int dlist dlist"} not)
  1376 
  1377     \<^descr> \<open>\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>\<close>, \<open>\<kappa>\<close> is a type constructor that was defined as a
  1378     (co)datatype whose constructor argument types do not contain either
  1379     non-free datatypes or the function type.
  1380 
  1381   Integration with [@{attribute code} equation]: For total quotients,
  1382   @{command (HOL) "lift_definition"} uses \<open>f.abs_eq\<close> as a code equation.
  1383 
  1384   \<^descr> @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} These
  1385   two commands serve for storing and deleting the set-up of the Lifting
  1386   package and corresponding transfer rules defined by this package. This is
  1387   useful for hiding of type construction details of an abstract type when the
  1388   construction is finished but it still allows additions to this construction
  1389   when this is later necessary.
  1390 
  1391   Whenever the Lifting package is set up with a new abstract type \<open>\<tau>\<close> by
  1392   @{command_def (HOL) "lift_definition"}, the package defines a new bundle
  1393   that is called \<open>\<tau>.lifting\<close>. This bundle already includes set-up for the
  1394   Lifting package. The new transfer rules introduced by @{command (HOL)
  1395   "lift_definition"} can be stored in the bundle by the command @{command
  1396   (HOL) "lifting_update"} \<open>\<tau>.lifting\<close>.
  1397 
  1398   The command @{command (HOL) "lifting_forget"} \<open>\<tau>.lifting\<close> deletes set-up of
  1399   the Lifting package for \<open>\<tau>\<close> and deletes all the transfer rules that were
  1400   introduced by @{command (HOL) "lift_definition"} using \<open>\<tau>\<close> as an abstract
  1401   type.
  1402 
  1403   The stored set-up in a bundle can be reintroduced by the Isar commands for
  1404   including a bundle (@{command "include"}, @{keyword "includes"} and
  1405   @{command "including"}).
  1406 
  1407   \<^descr> @{command (HOL) "print_quot_maps"} prints stored quotient map theorems.
  1408 
  1409   \<^descr> @{command (HOL) "print_quotients"} prints stored quotient theorems.
  1410 
  1411   \<^descr> @{attribute (HOL) quot_map} registers a quotient map theorem, a theorem
  1412   showing how to ``lift'' quotients over type constructors. E.g.\ @{term
  1413   "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image Rep)
  1414   (rel_set T)"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
  1415   \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
  1416   involved type is BNF without dead variables.
  1417 
  1418   \<^descr> @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a
  1419   relator applied to an equality restricted by a predicate @{term P} (i.e.\
  1420   @{term "eq_onp P"}) is equal to a predicator applied to the @{term P}. The
  1421   combinator @{const eq_onp} is used for internal encoding of proper subtypes.
  1422   Such theorems allows the package to hide \<open>eq_onp\<close> from a user in a
  1423   user-readable form of a respectfulness theorem. For examples see
  1424   \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
  1425   is proved automatically if the involved type is BNF without dead variables.
  1426 
  1427   \<^descr> @{attribute (HOL) "relator_mono"} registers a property describing a
  1428   monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
  1429   This property is needed for proving a stronger transfer rule in
  1430   @{command_def (HOL) "lift_definition"} when a parametricity theorem for the
  1431   raw term is specified and also for the reflexivity prover. For examples see
  1432   \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
  1433   is proved automatically if the involved type is BNF without dead variables.
  1434 
  1435   \<^descr> @{attribute (HOL) "relator_distr"} registers a property describing a
  1436   distributivity of the relation composition and a relator. E.g.\ \<open>rel_set R
  1437   \<circ>\<circ> rel_set S = rel_set (R \<circ>\<circ> S)\<close>. This property is needed for proving a
  1438   stronger transfer rule in @{command_def (HOL) "lift_definition"} when a
  1439   parametricity theorem for the raw term is specified. When this equality does
  1440   not hold unconditionally (e.g.\ for the function type), the user can
  1441   specified each direction separately and also register multiple theorems with
  1442   different set of assumptions. This attribute can be used only after the
  1443   monotonicity property was already registered by @{attribute (HOL)
  1444   "relator_mono"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
  1445   \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
  1446   involved type is BNF without dead variables.
  1447 
  1448   \<^descr> @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from
  1449   the Lifting infrastructure and thus de-register the corresponding quotient.
  1450   This effectively causes that @{command (HOL) lift_definition} will not do
  1451   any lifting for the corresponding type. This attribute is rather used for
  1452   low-level manipulation with set-up of the Lifting package because @{command
  1453   (HOL) lifting_forget} is preferred for normal usage.
  1454 
  1455   \<^descr> @{attribute (HOL) lifting_restore} \<open>Quotient_thm pcr_def pcr_cr_eq_thm\<close>
  1456   registers the Quotient theorem \<open>Quotient_thm\<close> in the Lifting infrastructure
  1457   and thus sets up lifting for an abstract type \<open>\<tau>\<close> (that is defined by
  1458   \<open>Quotient_thm\<close>). Optional theorems \<open>pcr_def\<close> and \<open>pcr_cr_eq_thm\<close> can be
  1459   specified to register the parametrized correspondence relation for \<open>\<tau>\<close>.
  1460   E.g.\ for @{typ "'a dlist"}, \<open>pcr_def\<close> is \<open>pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
  1461   cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (op =) = (op =)\<close>. This attribute
  1462   is rather used for low-level manipulation with set-up of the Lifting package
  1463   because using of the bundle \<open>\<tau>.lifting\<close> together with the commands @{command
  1464   (HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
  1465   normal usage.
  1466 
  1467   \<^descr> Integration with the BNF package @{cite "isabelle-datatypes"}: As already
  1468   mentioned, the theorems that are registered by the following attributes are
  1469   proved and registered automatically if the involved type is BNF without dead
  1470   variables: @{attribute (HOL) quot_map}, @{attribute (HOL) relator_eq_onp},
  1471   @{attribute (HOL) "relator_mono"}, @{attribute (HOL) "relator_distr"}. Also
  1472   the definition of a relator and predicator is provided automatically.
  1473   Moreover, if the BNF represents a datatype, simplification rules for a
  1474   predicator are again proved automatically.
  1475 \<close>
  1476 
  1477 
  1478 subsection \<open>Transfer package \label{sec:transfer}\<close>
  1479 
  1480 text \<open>
  1481   \begin{matharray}{rcl}
  1482     @{method_def (HOL) "transfer"} & : & \<open>method\<close> \\
  1483     @{method_def (HOL) "transfer'"} & : & \<open>method\<close> \\
  1484     @{method_def (HOL) "transfer_prover"} & : & \<open>method\<close> \\
  1485     @{attribute_def (HOL) "Transfer.transferred"} & : & \<open>attribute\<close> \\
  1486     @{attribute_def (HOL) "untransferred"} & : & \<open>attribute\<close> \\
  1487     @{method_def (HOL) "transfer_start"} & : & \<open>method\<close> \\
  1488     @{method_def (HOL) "transfer_prover_start"} & : & \<open>method\<close> \\
  1489     @{method_def (HOL) "transfer_step"} & : & \<open>method\<close> \\
  1490     @{method_def (HOL) "transfer_end"} & : & \<open>method\<close> \\
  1491     @{method_def (HOL) "transfer_prover_end"} & : & \<open>method\<close> \\
  1492     @{attribute_def (HOL) "transfer_rule"} & : & \<open>attribute\<close> \\
  1493     @{attribute_def (HOL) "transfer_domain_rule"} & : & \<open>attribute\<close> \\
  1494     @{attribute_def (HOL) "relator_eq"} & : & \<open>attribute\<close> \\
  1495     @{attribute_def (HOL) "relator_domain"} & : & \<open>attribute\<close> \\
  1496   \end{matharray}
  1497 
  1498   \<^descr> @{method (HOL) "transfer"} method replaces the current subgoal with a
  1499   logically equivalent one that uses different types and constants. The
  1500   replacement of types and constants is guided by the database of transfer
  1501   rules. Goals are generalized over all free variables by default; this is
  1502   necessary for variables whose types change, but can be overridden for
  1503   specific variables with e.g. \<open>transfer fixing: x y z\<close>.
  1504 
  1505   \<^descr> @{method (HOL) "transfer'"} is a variant of @{method (HOL) transfer} that
  1506   allows replacing a subgoal with one that is logically stronger (rather than
  1507   equivalent). For example, a subgoal involving equality on a quotient type
  1508   could be replaced with a subgoal involving equality (instead of the
  1509   corresponding equivalence relation) on the underlying raw type.
  1510 
  1511   \<^descr> @{method (HOL) "transfer_prover"} method assists with proving a transfer
  1512   rule for a new constant, provided the constant is defined in terms of other
  1513   constants that already have transfer rules. It should be applied after
  1514   unfolding the constant definitions.
  1515 
  1516   \<^descr> @{method (HOL) "transfer_start"}, @{method (HOL) "transfer_step"},
  1517   @{method (HOL) "transfer_end"}, @{method (HOL) "transfer_prover_start"} and
  1518   @{method (HOL) "transfer_prover_end"} methods are meant to be used for
  1519   debugging of @{method (HOL) "transfer"} and @{method (HOL)
  1520   "transfer_prover"}, which we can decompose as follows: @{method (HOL)
  1521   "transfer"} = (@{method (HOL) "transfer_start"}, @{method (HOL)
  1522   "transfer_step"}+, @{method (HOL) "transfer_end"}) and @{method (HOL)
  1523   "transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, @{method
  1524   (HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}). For usage
  1525   examples see \<^file>\<open>~~/src/HOL/ex/Transfer_Debug.thy\<close>.
  1526 
  1527   \<^descr> @{attribute (HOL) "untransferred"} proves the same equivalent theorem as
  1528   @{method (HOL) "transfer"} internally does.
  1529 
  1530   \<^descr> @{attribute (HOL) Transfer.transferred} works in the opposite direction
  1531   than @{method (HOL) "transfer'"}. E.g.\ given the transfer relation \<open>ZN x n
  1532   \<equiv> (x = int n)\<close>, corresponding transfer rules and the theorem \<open>\<forall>x::int \<in>
  1533   {0..}. x < x + 1\<close>, the attribute would prove \<open>\<forall>n::nat. n < n + 1\<close>. The
  1534   attribute is still in experimental phase of development.
  1535 
  1536   \<^descr> @{attribute (HOL) "transfer_rule"} attribute maintains a collection of
  1537   transfer rules, which relate constants at two different types. Typical
  1538   transfer rules may relate different type instances of the same polymorphic
  1539   constant, or they may relate an operation on a raw type to a corresponding
  1540   operation on an abstract type (quotient or subtype). For example:
  1541 
  1542     \<open>((A ===> B) ===> list_all2 A ===> list_all2 B) map map\<close> \\
  1543     \<open>(cr_int ===> cr_int ===> cr_int) (\<lambda>(x,y) (u,v). (x+u, y+v)) plus\<close>
  1544 
  1545   Lemmas involving predicates on relations can also be registered using the
  1546   same attribute. For example:
  1547 
  1548     \<open>bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct\<close> \\
  1549     \<open>\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)\<close>
  1550 
  1551   Preservation of predicates on relations (\<open>bi_unique, bi_total, right_unique,
  1552   right_total, left_unique, left_total\<close>) with the respect to a relator is
  1553   proved automatically if the involved type is BNF @{cite
  1554   "isabelle-datatypes"} without dead variables.
  1555 
  1556   \<^descr> @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
  1557   of rules, which specify a domain of a transfer relation by a predicate.
  1558   E.g.\ given the transfer relation \<open>ZN x n \<equiv> (x = int n)\<close>, one can register
  1559   the following transfer domain rule: \<open>Domainp ZN = (\<lambda>x. x \<ge> 0)\<close>. The rules
  1560   allow the package to produce more readable transferred goals, e.g.\ when
  1561   quantifiers are transferred.
  1562 
  1563   \<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for
  1564   relators of various type constructors, e.g. @{term "rel_set (op =) = (op
  1565   =)"}. The @{method (HOL) transfer} method uses these lemmas to infer
  1566   transfer rules for non-polymorphic constants on the fly. For examples see
  1567   \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
  1568   is proved automatically if the involved type is BNF without dead variables.
  1569 
  1570   \<^descr> @{attribute_def (HOL) "relator_domain"} attribute collects rules
  1571   describing domains of relators by predicators. E.g.\ @{term "Domainp
  1572   (rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package to lift
  1573   transfer domain rules through type constructors. For examples see
  1574   \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
  1575   is proved automatically if the involved type is BNF without dead variables.
  1576 
  1577 
  1578   Theoretical background can be found in @{cite
  1579   "Huffman-Kuncar:2013:lifting_transfer"}.
  1580 \<close>
  1581 
  1582 
  1583 subsection \<open>Old-style definitions for quotient types \label{sec:old-quotient}\<close>
  1584 
  1585 text \<open>
  1586   \begin{matharray}{rcl}
  1587     @{command_def (HOL) "quotient_definition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close>\\
  1588     @{command_def (HOL) "print_quotmapsQ3"} & : & \<open>context \<rightarrow>\<close>\\
  1589     @{command_def (HOL) "print_quotientsQ3"} & : & \<open>context \<rightarrow>\<close>\\
  1590     @{command_def (HOL) "print_quotconsts"} & : & \<open>context \<rightarrow>\<close>\\
  1591     @{method_def (HOL) "lifting"} & : & \<open>method\<close> \\
  1592     @{method_def (HOL) "lifting_setup"} & : & \<open>method\<close> \\
  1593     @{method_def (HOL) "descending"} & : & \<open>method\<close> \\
  1594     @{method_def (HOL) "descending_setup"} & : & \<open>method\<close> \\
  1595     @{method_def (HOL) "partiality_descending"} & : & \<open>method\<close> \\
  1596     @{method_def (HOL) "partiality_descending_setup"} & : & \<open>method\<close> \\
  1597     @{method_def (HOL) "regularize"} & : & \<open>method\<close> \\
  1598     @{method_def (HOL) "injection"} & : & \<open>method\<close> \\
  1599     @{method_def (HOL) "cleaning"} & : & \<open>method\<close> \\
  1600     @{attribute_def (HOL) "quot_thm"} & : & \<open>attribute\<close> \\
  1601     @{attribute_def (HOL) "quot_lifted"} & : & \<open>attribute\<close> \\
  1602     @{attribute_def (HOL) "quot_respect"} & : & \<open>attribute\<close> \\
  1603     @{attribute_def (HOL) "quot_preserve"} & : & \<open>attribute\<close> \\
  1604   \end{matharray}
  1605 
  1606   @{rail \<open>
  1607     @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \<newline>
  1608     @{syntax term} 'is' @{syntax term}
  1609     ;
  1610     constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
  1611     ;
  1612     @@{method (HOL) lifting} @{syntax thms}?
  1613     ;
  1614     @@{method (HOL) lifting_setup} @{syntax thms}?
  1615   \<close>}
  1616 
  1617   \<^descr> @{command (HOL) "quotient_definition"} defines a constant on the quotient
  1618   type.
  1619 
  1620   \<^descr> @{command (HOL) "print_quotmapsQ3"} prints quotient map functions.
  1621 
  1622   \<^descr> @{command (HOL) "print_quotientsQ3"} prints quotients.
  1623 
  1624   \<^descr> @{command (HOL) "print_quotconsts"} prints quotient constants.
  1625 
  1626   \<^descr> @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"} methods
  1627   match the current goal with the given raw theorem to be lifted producing
  1628   three new subgoals: regularization, injection and cleaning subgoals.
  1629   @{method (HOL) "lifting"} tries to apply the heuristics for automatically
  1630   solving these three subgoals and leaves only the subgoals unsolved by the
  1631   heuristics to the user as opposed to @{method (HOL) "lifting_setup"} which
  1632   leaves the three subgoals unsolved.
  1633 
  1634   \<^descr> @{method (HOL) "descending"} and @{method (HOL) "descending_setup"} try to
  1635   guess a raw statement that would lift to the current subgoal. Such statement
  1636   is assumed as a new subgoal and @{method (HOL) "descending"} continues in
  1637   the same way as @{method (HOL) "lifting"} does. @{method (HOL) "descending"}
  1638   tries to solve the arising regularization, injection and cleaning subgoals
  1639   with the analogous method @{method (HOL) "descending_setup"} which leaves
  1640   the four unsolved subgoals.
  1641 
  1642   \<^descr> @{method (HOL) "partiality_descending"} finds the regularized theorem that
  1643   would lift to the current subgoal, lifts it and leaves as a subgoal. This
  1644   method can be used with partial equivalence quotients where the non
  1645   regularized statements would not be true. @{method (HOL)
  1646   "partiality_descending_setup"} leaves the injection and cleaning subgoals
  1647   unchanged.
  1648 
  1649   \<^descr> @{method (HOL) "regularize"} applies the regularization heuristics to the
  1650   current subgoal.
  1651 
  1652   \<^descr> @{method (HOL) "injection"} applies the injection heuristics to the
  1653   current goal using the stored quotient respectfulness theorems.
  1654 
  1655   \<^descr> @{method (HOL) "cleaning"} applies the injection cleaning heuristics to
  1656   the current subgoal using the stored quotient preservation theorems.
  1657 
  1658   \<^descr> @{attribute (HOL) quot_lifted} attribute tries to automatically transport
  1659   the theorem to the quotient type. The attribute uses all the defined
  1660   quotients types and quotient constants often producing undesired results or
  1661   theorems that cannot be lifted.
  1662 
  1663   \<^descr> @{attribute (HOL) quot_respect} and @{attribute (HOL) quot_preserve}
  1664   attributes declare a theorem as a respectfulness and preservation theorem
  1665   respectively. These are stored in the local theory store and used by the
  1666   @{method (HOL) "injection"} and @{method (HOL) "cleaning"} methods
  1667   respectively.
  1668 
  1669   \<^descr> @{attribute (HOL) quot_thm} declares that a certain theorem is a quotient
  1670   extension theorem. Quotient extension theorems allow for quotienting inside
  1671   container types. Given a polymorphic type that serves as a container, a map
  1672   function defined for this container using @{command (HOL) "functor"} and a
  1673   relation map defined for for the container type, the quotient extension
  1674   theorem should be @{term "Quotient3 R Abs Rep \<Longrightarrow> Quotient3 (rel_map R) (map
  1675   Abs) (map Rep)"}. Quotient extension theorems are stored in a database and
  1676   are used all the steps of lifting theorems.
  1677 \<close>
  1678 
  1679 
  1680 chapter \<open>Proof tools\<close>
  1681 
  1682 section \<open>Proving propositions\<close>
  1683 
  1684 text \<open>
  1685   In addition to the standard proof methods, a number of diagnosis tools
  1686   search for proofs and provide an Isar proof snippet on success. These tools
  1687   are available via the following commands.
  1688 
  1689   \begin{matharray}{rcl}
  1690     @{command_def (HOL) "solve_direct"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
  1691     @{command_def (HOL) "try"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
  1692     @{command_def (HOL) "try0"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
  1693     @{command_def (HOL) "sledgehammer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
  1694     @{command_def (HOL) "sledgehammer_params"} & : & \<open>theory \<rightarrow> theory\<close>
  1695   \end{matharray}
  1696 
  1697   @{rail \<open>
  1698     @@{command (HOL) try}
  1699     ;
  1700 
  1701     @@{command (HOL) try0} ( ( ( 'simp' | 'intro' | 'elim' | 'dest' ) ':' @{syntax thms} ) + ) ?
  1702       @{syntax nat}?
  1703     ;
  1704 
  1705     @@{command (HOL) sledgehammer} ( '[' args ']' )? facts? @{syntax nat}?
  1706     ;
  1707 
  1708     @@{command (HOL) sledgehammer_params} ( ( '[' args ']' ) ? )
  1709     ;
  1710     args: ( @{syntax name} '=' value + ',' )
  1711     ;
  1712     facts: '(' ( ( ( ( 'add' | 'del' ) ':' ) ? @{syntax thms} ) + ) ? ')'
  1713   \<close>} % FIXME check args "value"
  1714 
  1715   \<^descr> @{command (HOL) "solve_direct"} checks whether the current subgoals can be
  1716   solved directly by an existing theorem. Duplicate lemmas can be detected in
  1717   this way.
  1718 
  1719   \<^descr> @{command (HOL) "try0"} attempts to prove a subgoal using a combination of
  1720   standard proof methods (@{method auto}, @{method simp}, @{method blast},
  1721   etc.). Additional facts supplied via \<open>simp:\<close>, \<open>intro:\<close>, \<open>elim:\<close>, and \<open>dest:\<close>
  1722   are passed to the appropriate proof methods.
  1723 
  1724   \<^descr> @{command (HOL) "try"} attempts to prove or disprove a subgoal using a
  1725   combination of provers and disprovers (@{command (HOL) "solve_direct"},
  1726   @{command (HOL) "quickcheck"}, @{command (HOL) "try0"}, @{command (HOL)
  1727   "sledgehammer"}, @{command (HOL) "nitpick"}).
  1728 
  1729   \<^descr> @{command (HOL) "sledgehammer"} attempts to prove a subgoal using external
  1730   automatic provers (resolution provers and SMT solvers). See the Sledgehammer
  1731   manual @{cite "isabelle-sledgehammer"} for details.
  1732 
  1733   \<^descr> @{command (HOL) "sledgehammer_params"} changes @{command (HOL)
  1734   "sledgehammer"} configuration options persistently.
  1735 \<close>
  1736 
  1737 
  1738 section \<open>Checking and refuting propositions\<close>
  1739 
  1740 text \<open>
  1741   Identifying incorrect propositions usually involves evaluation of particular
  1742   assignments and systematic counterexample search. This is supported by the
  1743   following commands.
  1744 
  1745   \begin{matharray}{rcl}
  1746     @{command_def (HOL) "value"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  1747     @{command_def (HOL) "values"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  1748     @{command_def (HOL) "quickcheck"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
  1749     @{command_def (HOL) "nitpick"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow>\<close> \\
  1750     @{command_def (HOL) "quickcheck_params"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1751     @{command_def (HOL) "nitpick_params"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1752     @{command_def (HOL) "quickcheck_generator"} & : & \<open>theory \<rightarrow> theory\<close> \\
  1753     @{command_def (HOL) "find_unused_assms"} & : & \<open>context \<rightarrow>\<close>
  1754   \end{matharray}
  1755 
  1756   @{rail \<open>
  1757     @@{command (HOL) value} ( '[' @{syntax name} ']' )? modes? @{syntax term}
  1758     ;
  1759 
  1760     @@{command (HOL) values} modes? @{syntax nat}? @{syntax term}
  1761     ;
  1762 
  1763     (@@{command (HOL) quickcheck} | @@{command (HOL) nitpick})
  1764       ( '[' args ']' )? @{syntax nat}?
  1765     ;
  1766 
  1767     (@@{command (HOL) quickcheck_params} |
  1768       @@{command (HOL) nitpick_params}) ( '[' args ']' )?
  1769     ;
  1770 
  1771     @@{command (HOL) quickcheck_generator} @{syntax name} \<newline>
  1772       'operations:' ( @{syntax term} +)
  1773     ;
  1774 
  1775     @@{command (HOL) find_unused_assms} @{syntax name}?
  1776     ;
  1777     modes: '(' (@{syntax name} +) ')'
  1778     ;
  1779     args: ( @{syntax name} '=' value + ',' )
  1780   \<close>} % FIXME check "value"
  1781 
  1782   \<^descr> @{command (HOL) "value"}~\<open>t\<close> evaluates and prints a term; optionally
  1783   \<open>modes\<close> can be specified, which are appended to the current print mode; see
  1784   \secref{sec:print-modes}. Evaluation is tried first using ML, falling back
  1785   to normalization by evaluation if this fails. Alternatively a specific
  1786   evaluator can be selected using square brackets; typical evaluators use the
  1787   current set of code equations to normalize and include \<open>simp\<close> for fully
  1788   symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
  1789   evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
  1790 
  1791   \<^descr> @{command (HOL) "values"}~\<open>t\<close> enumerates a set comprehension by evaluation
  1792   and prints its values up to the given number of solutions; optionally
  1793   \<open>modes\<close> can be specified, which are appended to the current print mode; see
  1794   \secref{sec:print-modes}.
  1795 
  1796   \<^descr> @{command (HOL) "quickcheck"} tests the current goal for counterexamples
  1797   using a series of assignments for its free variables; by default the first
  1798   subgoal is tested, an other can be selected explicitly using an optional
  1799   goal index. Assignments can be chosen exhausting the search space up to a
  1800   given size, or using a fixed number of random assignments in the search
  1801   space, or exploring the search space symbolically using narrowing. By
  1802   default, quickcheck uses exhaustive testing. A number of configuration
  1803   options are supported for @{command (HOL) "quickcheck"}, notably:
  1804 
  1805     \<^descr>[\<open>tester\<close>] specifies which testing approach to apply. There are three
  1806     testers, \<open>exhaustive\<close>, \<open>random\<close>, and \<open>narrowing\<close>. An unknown configuration
  1807     option is treated as an argument to tester, making \<open>tester =\<close> optional.
  1808     When multiple testers are given, these are applied in parallel. If no
  1809     tester is specified, quickcheck uses the testers that are set active,
  1810     i.e.\ configurations @{attribute quickcheck_exhaustive_active},
  1811     @{attribute quickcheck_random_active}, @{attribute
  1812     quickcheck_narrowing_active} are set to true.
  1813 
  1814     \<^descr>[\<open>size\<close>] specifies the maximum size of the search space for assignment
  1815     values.
  1816 
  1817     \<^descr>[\<open>genuine_only\<close>] sets quickcheck only to return genuine counterexample,
  1818     but not potentially spurious counterexamples due to underspecified
  1819     functions.
  1820 
  1821     \<^descr>[\<open>abort_potential\<close>] sets quickcheck to abort once it found a potentially
  1822     spurious counterexample and to not continue to search for a further
  1823     genuine counterexample. For this option to be effective, the
  1824     \<open>genuine_only\<close> option must be set to false.
  1825 
  1826     \<^descr>[\<open>eval\<close>] takes a term or a list of terms and evaluates these terms under
  1827     the variable assignment found by quickcheck. This option is currently only
  1828     supported by the default (exhaustive) tester.
  1829 
  1830     \<^descr>[\<open>iterations\<close>] sets how many sets of assignments are generated for each
  1831     particular size.
  1832 
  1833     \<^descr>[\<open>no_assms\<close>] specifies whether assumptions in structured proofs should be
  1834     ignored.
  1835 
  1836     \<^descr>[\<open>locale\<close>] specifies how to process conjectures in a locale context,
  1837     i.e.\ they can be interpreted or expanded. The option is a
  1838     whitespace-separated list of the two words \<open>interpret\<close> and \<open>expand\<close>. The
  1839     list determines the order they are employed. The default setting is to
  1840     first use interpretations and then test the expanded conjecture. The
  1841     option is only provided as attribute declaration, but not as parameter to
  1842     the command.
  1843 
  1844     \<^descr>[\<open>timeout\<close>] sets the time limit in seconds.
  1845 
  1846     \<^descr>[\<open>default_type\<close>] sets the type(s) generally used to instantiate type
  1847     variables.
  1848 
  1849     \<^descr>[\<open>report\<close>] if set quickcheck reports how many tests fulfilled the
  1850     preconditions.
  1851 
  1852     \<^descr>[\<open>use_subtype\<close>] if set quickcheck automatically lifts conjectures to
  1853     registered subtypes if possible, and tests the lifted conjecture.
  1854 
  1855     \<^descr>[\<open>quiet\<close>] if set quickcheck does not output anything while testing.
  1856 
  1857     \<^descr>[\<open>verbose\<close>] if set quickcheck informs about the current size and
  1858     cardinality while testing.
  1859 
  1860     \<^descr>[\<open>expect\<close>] can be used to check if the user's expectation was met
  1861     (\<open>no_expectation\<close>, \<open>no_counterexample\<close>, or \<open>counterexample\<close>).
  1862 
  1863   These option can be given within square brackets.
  1864 
  1865   Using the following type classes, the testers generate values and convert
  1866   them back into Isabelle terms for displaying counterexamples.
  1867 
  1868     \<^descr>[\<open>exhaustive\<close>] The parameters of the type classes @{class exhaustive} and
  1869     @{class full_exhaustive} implement the testing. They take a testing
  1870     function as a parameter, which takes a value of type @{typ "'a"} and
  1871     optionally produces a counterexample, and a size parameter for the test
  1872     values. In @{class full_exhaustive}, the testing function parameter
  1873     additionally expects a lazy term reconstruction in the type @{typ
  1874     Code_Evaluation.term} of the tested value.
  1875 
  1876     The canonical implementation for \<open>exhaustive\<close> testers calls the given
  1877     testing function on all values up to the given size and stops as soon as a
  1878     counterexample is found.
  1879 
  1880     \<^descr>[\<open>random\<close>] The operation @{const Quickcheck_Random.random} of the type
  1881     class @{class random} generates a pseudo-random value of the given size
  1882     and a lazy term reconstruction of the value in the type @{typ
  1883     Code_Evaluation.term}. A pseudo-randomness generator is defined in theory
  1884     @{theory Random}.
  1885 
  1886     \<^descr>[\<open>narrowing\<close>] implements Haskell's Lazy Smallcheck @{cite
  1887     "runciman-naylor-lindblad"} using the type classes @{class narrowing} and
  1888     @{class partial_term_of}. Variables in the current goal are initially
  1889     represented as symbolic variables. If the execution of the goal tries to
  1890     evaluate one of them, the test engine replaces it with refinements
  1891     provided by @{const narrowing}. Narrowing views every value as a
  1892     sum-of-products which is expressed using the operations @{const
  1893     Quickcheck_Narrowing.cons} (embedding a value), @{const
  1894     Quickcheck_Narrowing.apply} (product) and @{const
  1895     Quickcheck_Narrowing.sum} (sum). The refinement should enable further
  1896     evaluation of the goal.
  1897 
  1898     For example, @{const narrowing} for the list type @{typ "'a :: narrowing list"}
  1899     can be recursively defined as
  1900     @{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
  1901               (Quickcheck_Narrowing.apply
  1902                 (Quickcheck_Narrowing.apply
  1903                   (Quickcheck_Narrowing.cons (op #))
  1904                   narrowing)
  1905                 narrowing)"}.
  1906     If a symbolic variable of type @{typ "_ list"} is evaluated, it is
  1907     replaced by (i)~the empty list @{term "[]"} and (ii)~by a non-empty list
  1908     whose head and tail can then be recursively refined if needed.
  1909 
  1910     To reconstruct counterexamples, the operation @{const partial_term_of}
  1911     transforms \<open>narrowing\<close>'s deep representation of terms to the type @{typ
  1912     Code_Evaluation.term}. The deep representation models symbolic variables
  1913     as @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally
  1914     converted to @{const Code_Evaluation.Free}, and refined values as @{term
  1915     "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i ::
  1916     integer"} denotes the index in the sum of refinements. In the above
  1917     example for lists, @{term "0"} corresponds to @{term "[]"} and @{term "1"}
  1918     to @{term "op #"}.
  1919 
  1920     The command @{command (HOL) "code_datatype"} sets up @{const
  1921     partial_term_of} such that the @{term "i"}-th refinement is interpreted as
  1922     the @{term "i"}-th constructor, but it does not ensures consistency with
  1923     @{const narrowing}.
  1924 
  1925   \<^descr> @{command (HOL) "quickcheck_params"} changes @{command (HOL) "quickcheck"}
  1926   configuration options persistently.
  1927 
  1928   \<^descr> @{command (HOL) "quickcheck_generator"} creates random and exhaustive
  1929   value generators for a given type and operations. It generates values by
  1930   using the operations as if they were constructors of that type.
  1931 
  1932   \<^descr> @{command (HOL) "nitpick"} tests the current goal for counterexamples
  1933   using a reduction to first-order relational logic. See the Nitpick manual
  1934   @{cite "isabelle-nitpick"} for details.
  1935 
  1936   \<^descr> @{command (HOL) "nitpick_params"} changes @{command (HOL) "nitpick"}
  1937   configuration options persistently.
  1938 
  1939   \<^descr> @{command (HOL) "find_unused_assms"} finds potentially superfluous
  1940   assumptions in theorems using quickcheck. It takes the theory name to be
  1941   checked for superfluous assumptions as optional argument. If not provided,
  1942   it checks the current theory. Options to the internal quickcheck invocations
  1943   can be changed with common configuration declarations.
  1944 \<close>
  1945 
  1946 
  1947 section \<open>Coercive subtyping\<close>
  1948 
  1949 text \<open>
  1950   \begin{matharray}{rcl}
  1951     @{attribute_def (HOL) coercion} & : & \<open>attribute\<close> \\
  1952     @{attribute_def (HOL) coercion_delete} & : & \<open>attribute\<close> \\
  1953     @{attribute_def (HOL) coercion_enabled} & : & \<open>attribute\<close> \\
  1954     @{attribute_def (HOL) coercion_map} & : & \<open>attribute\<close> \\
  1955     @{attribute_def (HOL) coercion_args} & : & \<open>attribute\<close> \\
  1956   \end{matharray}
  1957 
  1958   Coercive subtyping allows the user to omit explicit type conversions, also
  1959   called \<^emph>\<open>coercions\<close>. Type inference will add them as necessary when parsing
  1960   a term. See @{cite "traytel-berghofer-nipkow-2011"} for details.
  1961 
  1962   @{rail \<open>
  1963     @@{attribute (HOL) coercion} (@{syntax term})
  1964     ;
  1965     @@{attribute (HOL) coercion_delete} (@{syntax term})
  1966     ;
  1967     @@{attribute (HOL) coercion_map} (@{syntax term})
  1968     ;
  1969     @@{attribute (HOL) coercion_args} (@{syntax const}) (('+' | '0' | '-')+)
  1970   \<close>}
  1971 
  1972   \<^descr> @{attribute (HOL) "coercion"}~\<open>f\<close> registers a new coercion function \<open>f ::
  1973   \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> where \<open>\<sigma>\<^sub>1\<close> and \<open>\<sigma>\<^sub>2\<close> are type constructors without arguments.
  1974   Coercions are composed by the inference algorithm if needed. Note that the
  1975   type inference algorithm is complete only if the registered coercions form a
  1976   lattice.
  1977 
  1978   \<^descr> @{attribute (HOL) "coercion_delete"}~\<open>f\<close> deletes a preceding declaration
  1979   (using @{attribute (HOL) "coercion"}) of the function \<open>f :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2\<close> as a
  1980   coercion.
  1981 
  1982   \<^descr> @{attribute (HOL) "coercion_map"}~\<open>map\<close> registers a new map function to
  1983   lift coercions through type constructors. The function \<open>map\<close> must conform to
  1984   the following type pattern
  1985 
  1986   \begin{matharray}{lll}
  1987     \<open>map\<close> & \<open>::\<close> &
  1988       \<open>f\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> f\<^sub>n \<Rightarrow> (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t \<Rightarrow> (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n) t\<close> \\
  1989   \end{matharray}
  1990 
  1991   where \<open>t\<close> is a type constructor and \<open>f\<^sub>i\<close> is of type \<open>\<alpha>\<^sub>i \<Rightarrow> \<beta>\<^sub>i\<close> or \<open>\<beta>\<^sub>i \<Rightarrow>
  1992   \<alpha>\<^sub>i\<close>. Registering a map function overwrites any existing map function for
  1993   this particular type constructor.
  1994 
  1995   \<^descr> @{attribute (HOL) "coercion_args"} can be used to disallow coercions to be
  1996   inserted in certain positions in a term. For example, given the constant \<open>c
  1997   :: \<sigma>\<^sub>1 \<Rightarrow> \<sigma>\<^sub>2 \<Rightarrow> \<sigma>\<^sub>3 \<Rightarrow> \<sigma>\<^sub>4\<close> and the list of policies \<open>- + 0\<close> as arguments,
  1998   coercions will not be inserted in the first argument of \<open>c\<close> (policy \<open>-\<close>);
  1999   they may be inserted in the second argument (policy \<open>+\<close>) even if the
  2000   constant \<open>c\<close> itself is in a position where coercions are disallowed; the
  2001   third argument inherits the allowance of coercsion insertion from the
  2002   position of the constant \<open>c\<close> (policy \<open>0\<close>). The standard usage of policies is
  2003   the definition of syntatic constructs (usually extralogical, i.e., processed
  2004   and stripped during type inference), that should not be destroyed by the
  2005   insertion of coercions (see, for example, the setup for the case syntax in
  2006   @{theory Ctr_Sugar}).
  2007 
  2008   \<^descr> @{attribute (HOL) "coercion_enabled"} enables the coercion inference
  2009   algorithm.
  2010 \<close>
  2011 
  2012 
  2013 section \<open>Arithmetic proof support\<close>
  2014 
  2015 text \<open>
  2016   \begin{matharray}{rcl}
  2017     @{method_def (HOL) arith} & : & \<open>method\<close> \\
  2018     @{attribute_def (HOL) arith} & : & \<open>attribute\<close> \\
  2019     @{attribute_def (HOL) arith_split} & : & \<open>attribute\<close> \\
  2020   \end{matharray}
  2021 
  2022   \<^descr> @{method (HOL) arith} decides linear arithmetic problems (on types \<open>nat\<close>,
  2023   \<open>int\<close>, \<open>real\<close>). Any current facts are inserted into the goal before running
  2024   the procedure.
  2025 
  2026   \<^descr> @{attribute (HOL) arith} declares facts that are supplied to the
  2027   arithmetic provers implicitly.
  2028 
  2029   \<^descr> @{attribute (HOL) arith_split} attribute declares case split rules to be
  2030   expanded before @{method (HOL) arith} is invoked.
  2031 
  2032 
  2033   Note that a simpler (but faster) arithmetic prover is already invoked by the
  2034   Simplifier.
  2035 \<close>
  2036 
  2037 
  2038 section \<open>Intuitionistic proof search\<close>
  2039 
  2040 text \<open>
  2041   \begin{matharray}{rcl}
  2042     @{method_def (HOL) iprover} & : & \<open>method\<close> \\
  2043   \end{matharray}
  2044 
  2045   @{rail \<open>
  2046     @@{method (HOL) iprover} (@{syntax rulemod} *)
  2047   \<close>}
  2048 
  2049   \<^descr> @{method (HOL) iprover} performs intuitionistic proof search, depending on
  2050   specifically declared rules from the context, or given as explicit
  2051   arguments. Chained facts are inserted into the goal before commencing proof
  2052   search.
  2053 
  2054   Rules need to be classified as @{attribute (Pure) intro}, @{attribute (Pure)
  2055   elim}, or @{attribute (Pure) dest}; here the ``\<open>!\<close>'' indicator refers to
  2056   ``safe'' rules, which may be applied aggressively (without considering
  2057   back-tracking later). Rules declared with ``\<open>?\<close>'' are ignored in proof
  2058   search (the single-step @{method (Pure) rule} method still observes these).
  2059   An explicit weight annotation may be given as well; otherwise the number of
  2060   rule premises will be taken into account here.
  2061 \<close>
  2062 
  2063 
  2064 section \<open>Model Elimination and Resolution\<close>
  2065 
  2066 text \<open>
  2067   \begin{matharray}{rcl}
  2068     @{method_def (HOL) "meson"} & : & \<open>method\<close> \\
  2069     @{method_def (HOL) "metis"} & : & \<open>method\<close> \\
  2070   \end{matharray}
  2071 
  2072   @{rail \<open>
  2073     @@{method (HOL) meson} @{syntax thms}?
  2074     ;
  2075     @@{method (HOL) metis}
  2076       ('(' ('partial_types' | 'full_types' | 'no_types' | @{syntax name}) ')')?
  2077       @{syntax thms}?
  2078   \<close>}
  2079 
  2080   \<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
  2081   @{cite "loveland-78"}. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
  2082 
  2083   \<^descr> @{method (HOL) metis} combines ordered resolution and ordered
  2084   paramodulation to find first-order (or mildly higher-order) proofs. The
  2085   first optional argument specifies a type encoding; see the Sledgehammer
  2086   manual @{cite "isabelle-sledgehammer"} for details. The directory
  2087   \<^dir>\<open>~~/src/HOL/Metis_Examples\<close> contains several small theories developed to a
  2088   large extent using @{method (HOL) metis}.
  2089 \<close>
  2090 
  2091 
  2092 section \<open>Algebraic reasoning via Gr\"obner bases\<close>
  2093 
  2094 text \<open>
  2095   \begin{matharray}{rcl}
  2096     @{method_def (HOL) "algebra"} & : & \<open>method\<close> \\
  2097     @{attribute_def (HOL) algebra} & : & \<open>attribute\<close> \\
  2098   \end{matharray}
  2099 
  2100   @{rail \<open>
  2101     @@{method (HOL) algebra}
  2102       ('add' ':' @{syntax thms})?
  2103       ('del' ':' @{syntax thms})?
  2104     ;
  2105     @@{attribute (HOL) algebra} (() | 'add' | 'del')
  2106   \<close>}
  2107 
  2108   \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gr\"obner bases,
  2109   see also @{cite "Chaieb-Wenzel:2007"} and @{cite \<open>\S3.2\<close> "Chaieb-thesis"}.
  2110   The method handles deals with two main classes of problems:
  2111 
  2112     \<^enum> Universal problems over multivariate polynomials in a
  2113     (semi)-ring/field/idom; the capabilities of the method are augmented
  2114     according to properties of these structures. For this problem class the
  2115     method is only complete for algebraically closed fields, since the
  2116     underlying method is based on Hilbert's Nullstellensatz, where the
  2117     equivalence only holds for algebraically closed fields.
  2118 
  2119     The problems can contain equations \<open>p = 0\<close> or inequations \<open>q \<noteq> 0\<close> anywhere
  2120     within a universal problem statement.
  2121 
  2122     \<^enum> All-exists problems of the following restricted (but useful) form:
  2123 
  2124     @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
  2125       e\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<and> \<dots> \<and> e\<^sub>m(x\<^sub>1, \<dots>, x\<^sub>n) = 0 \<longrightarrow>
  2126       (\<exists>y\<^sub>1 \<dots> y\<^sub>k.
  2127         p\<^sub>1\<^sub>1(x\<^sub>1, \<dots> ,x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>1\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0 \<and>
  2128         \<dots> \<and>
  2129         p\<^sub>t\<^sub>1(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>1 + \<dots> + p\<^sub>t\<^sub>k(x\<^sub>1, \<dots>, x\<^sub>n) * y\<^sub>k = 0)"}
  2130 
  2131     Here \<open>e\<^sub>1, \<dots>, e\<^sub>n\<close> and the \<open>p\<^sub>i\<^sub>j\<close> are multivariate polynomials only in
  2132     the variables mentioned as arguments.
  2133 
  2134   The proof method is preceded by a simplification step, which may be modified
  2135   by using the form \<open>(algebra add: ths\<^sub>1 del: ths\<^sub>2)\<close>. This acts like
  2136   declarations for the Simplifier (\secref{sec:simplifier}) on a private
  2137   simpset for this tool.
  2138 
  2139   \<^descr> @{attribute algebra} (as attribute) manages the default collection of
  2140   pre-simplification rules of the above proof method.
  2141 \<close>
  2142 
  2143 
  2144 subsubsection \<open>Example\<close>
  2145 
  2146 text \<open>
  2147   The subsequent example is from geometry: collinearity is invariant by
  2148   rotation.
  2149 \<close>
  2150 
  2151 (*<*)experiment begin(*>*)
  2152 type_synonym point = "int \<times> int"
  2153 
  2154 fun collinear :: "point \<Rightarrow> point \<Rightarrow> point \<Rightarrow> bool" where
  2155   "collinear (Ax, Ay) (Bx, By) (Cx, Cy) \<longleftrightarrow>
  2156     (Ax - Bx) * (By - Cy) = (Ay - By) * (Bx - Cx)"
  2157 
  2158 lemma collinear_inv_rotation:
  2159   assumes "collinear (Ax, Ay) (Bx, By) (Cx, Cy)" and "c\<^sup>2 + s\<^sup>2 = 1"
  2160   shows "collinear (Ax * c - Ay * s, Ay * c + Ax * s)
  2161     (Bx * c - By * s, By * c + Bx * s) (Cx * c - Cy * s, Cy * c + Cx * s)"
  2162   using assms by (algebra add: collinear.simps)
  2163 (*<*)end(*>*)
  2164 
  2165 text \<open>
  2166   See also \<^file>\<open>~~/src/HOL/ex/Groebner_Examples.thy\<close>.
  2167 \<close>
  2168 
  2169 
  2170 section \<open>Coherent Logic\<close>
  2171 
  2172 text \<open>
  2173   \begin{matharray}{rcl}
  2174     @{method_def (HOL) "coherent"} & : & \<open>method\<close> \\
  2175   \end{matharray}
  2176 
  2177   @{rail \<open>
  2178     @@{method (HOL) coherent} @{syntax thms}?
  2179   \<close>}
  2180 
  2181   \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
  2182   "Bezem-Coquand:2005"}, which covers applications in confluence theory,
  2183   lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/ex/Coherent.thy\<close>
  2184   for some examples.
  2185 \<close>
  2186 
  2187 
  2188 section \<open>Unstructured case analysis and induction \label{sec:hol-induct-tac}\<close>
  2189 
  2190 text \<open>
  2191   The following tools of Isabelle/HOL support cases analysis and induction in
  2192   unstructured tactic scripts; see also \secref{sec:cases-induct} for proper
  2193   Isar versions of similar ideas.
  2194 
  2195   \begin{matharray}{rcl}
  2196     @{method_def (HOL) case_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
  2197     @{method_def (HOL) induct_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
  2198     @{method_def (HOL) ind_cases}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
  2199     @{command_def (HOL) "inductive_cases"}\<open>\<^sup>*\<close> & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
  2200   \end{matharray}
  2201 
  2202   @{rail \<open>
  2203     @@{method (HOL) case_tac} @{syntax goal_spec}? @{syntax term} rule?
  2204     ;
  2205     @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
  2206     ;
  2207     @@{method (HOL) ind_cases} (@{syntax prop}+) @{syntax for_fixes}
  2208     ;
  2209     @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
  2210     ;
  2211     rule: 'rule' ':' @{syntax thm}
  2212   \<close>}
  2213 
  2214   \<^descr> @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit to reason
  2215   about inductive types. Rules are selected according to the declarations by
  2216   the @{attribute cases} and @{attribute induct} attributes, cf.\
  2217   \secref{sec:cases-induct}. The @{command (HOL) datatype} package already
  2218   takes care of this.
  2219 
  2220   These unstructured tactics feature both goal addressing and dynamic
  2221   instantiation. Note that named rule cases are \<^emph>\<open>not\<close> provided as would be by
  2222   the proper @{method cases} and @{method induct} proof methods (see
  2223   \secref{sec:cases-induct}). Unlike the @{method induct} method, @{method
  2224   induct_tac} does not handle structured rule statements, only the compact
  2225   object-logic conclusion of the subgoal being addressed.
  2226 
  2227   \<^descr> @{method (HOL) ind_cases} and @{command (HOL) "inductive_cases"} provide
  2228   an interface to the internal @{ML_text mk_cases} operation. Rules are
  2229   simplified in an unrestricted forward manner.
  2230 
  2231   While @{method (HOL) ind_cases} is a proof method to apply the result
  2232   immediately as elimination rules, @{command (HOL) "inductive_cases"}
  2233   provides case split theorems at the theory level for later use. The
  2234   @{keyword "for"} argument of the @{method (HOL) ind_cases} method allows to
  2235   specify a list of variables that should be generalized before applying the
  2236   resulting rule.
  2237 \<close>
  2238 
  2239 
  2240 section \<open>Adhoc tuples\<close>
  2241 
  2242 text \<open>
  2243   \begin{matharray}{rcl}
  2244     @{attribute_def (HOL) split_format}\<open>\<^sup>*\<close> & : & \<open>attribute\<close> \\
  2245   \end{matharray}
  2246 
  2247   @{rail \<open>
  2248     @@{attribute (HOL) split_format} ('(' 'complete' ')')?
  2249   \<close>}
  2250 
  2251   \<^descr> @{attribute (HOL) split_format}\ \<open>(complete)\<close> causes arguments in function
  2252   applications to be represented canonically according to their tuple type
  2253   structure.
  2254 
  2255   Note that this operation tends to invent funny names for new local
  2256   parameters introduced.
  2257 \<close>
  2258 
  2259 
  2260 chapter \<open>Executable code\<close>
  2261 
  2262 text \<open>
  2263   For validation purposes, it is often useful to \<^emph>\<open>execute\<close> specifications. In
  2264   principle, execution could be simulated by Isabelle's inference kernel, i.e.
  2265   by a combination of resolution and simplification. Unfortunately, this
  2266   approach is rather inefficient. A more efficient way of executing
  2267   specifications is to translate them into a functional programming language
  2268   such as ML.
  2269 
  2270   Isabelle provides a generic framework to support code generation from
  2271   executable specifications. Isabelle/HOL instantiates these mechanisms in a
  2272   way that is amenable to end-user applications. Code can be generated for
  2273   functional programs (including overloading using type classes) targeting SML
  2274   @{cite SML}, OCaml @{cite OCaml}, Haskell @{cite "haskell-revised-report"}
  2275   and Scala @{cite "scala-overview-tech-report"}. Conceptually, code
  2276   generation is split up in three steps: \<^emph>\<open>selection\<close> of code theorems,
  2277   \<^emph>\<open>translation\<close> into an abstract executable view and \<^emph>\<open>serialization\<close> to a
  2278   specific \<^emph>\<open>target language\<close>. Inductive specifications can be executed using
  2279   the predicate compiler which operates within HOL. See @{cite
  2280   "isabelle-codegen"} for an introduction.
  2281 
  2282   \begin{matharray}{rcl}
  2283     @{command_def (HOL) "export_code"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  2284     @{attribute_def (HOL) code} & : & \<open>attribute\<close> \\
  2285     @{command_def (HOL) "code_datatype"} & : & \<open>theory \<rightarrow> theory\<close> \\
  2286     @{command_def (HOL) "print_codesetup"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  2287     @{attribute_def (HOL) code_unfold} & : & \<open>attribute\<close> \\
  2288     @{attribute_def (HOL) code_post} & : & \<open>attribute\<close> \\
  2289     @{attribute_def (HOL) code_abbrev} & : & \<open>attribute\<close> \\
  2290     @{command_def (HOL) "print_codeproc"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  2291     @{command_def (HOL) "code_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  2292     @{command_def (HOL) "code_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
  2293     @{command_def (HOL) "code_reserved"} & : & \<open>theory \<rightarrow> theory\<close> \\
  2294     @{command_def (HOL) "code_printing"} & : & \<open>theory \<rightarrow> theory\<close> \\
  2295     @{command_def (HOL) "code_identifier"} & : & \<open>theory \<rightarrow> theory\<close> \\
  2296     @{command_def (HOL) "code_monad"} & : & \<open>theory \<rightarrow> theory\<close> \\
  2297     @{command_def (HOL) "code_reflect"} & : & \<open>theory \<rightarrow> theory\<close> \\
  2298     @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close>
  2299   \end{matharray}
  2300 
  2301   @{rail \<open>
  2302     @@{command (HOL) export_code} ( @'open' ) ? ( constexpr + ) \<newline>
  2303        ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
  2304         ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
  2305     ;
  2306     const: @{syntax term}
  2307     ;
  2308     constexpr: ( const | 'name._' | '_' )
  2309     ;
  2310     typeconstructor: @{syntax name}
  2311     ;
  2312     class: @{syntax name}
  2313     ;
  2314     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
  2315     ;
  2316     @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
  2317       | 'drop:' ( const + ) | 'abort:' ( const + ) )?
  2318     ;
  2319     @@{command (HOL) code_datatype} ( const + )
  2320     ;
  2321     @@{attribute (HOL) code_unfold} ( 'del' ) ?
  2322     ;
  2323     @@{attribute (HOL) code_post} ( 'del' ) ?
  2324     ;
  2325     @@{attribute (HOL) code_abbrev}
  2326     ;
  2327     @@{command (HOL) code_thms} ( constexpr + ) ?
  2328     ;
  2329     @@{command (HOL) code_deps} ( constexpr + ) ?
  2330     ;
  2331     @@{command (HOL) code_reserved} target ( @{syntax string} + )
  2332     ;
  2333     symbol_const: ( @'constant' const )
  2334     ;
  2335     symbol_typeconstructor: ( @'type_constructor' typeconstructor )
  2336     ;
  2337     symbol_class: ( @'type_class' class )
  2338     ;
  2339     symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )
  2340     ;
  2341     symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )
  2342     ;
  2343     symbol_module: ( @'code_module' name )
  2344     ;
  2345     syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
  2346     ;
  2347     printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \<newline>
  2348       ( '(' target ')' syntax ? + @'and' )
  2349     ;
  2350     printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \<newline>
  2351       ( '(' target ')' syntax ? + @'and' )
  2352     ;
  2353     printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \<newline>
  2354       ( '(' target ')' @{syntax string} ? + @'and' )
  2355     ;
  2356     printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \<newline>
  2357       ( '(' target ')' @{syntax string} ? + @'and' )
  2358     ;
  2359     printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \<newline>
  2360       ( '(' target ')' '-' ? + @'and' )
  2361     ;
  2362     printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \<newline>
  2363       ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
  2364     ;
  2365     @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
  2366       | printing_class | printing_class_relation | printing_class_instance
  2367       | printing_module ) + '|' )
  2368     ;
  2369     @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
  2370       | symbol_class | symbol_class_relation | symbol_class_instance
  2371       | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
  2372       ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
  2373     ;
  2374     @@{command (HOL) code_monad} const const target
  2375     ;
  2376     @@{command (HOL) code_reflect} @{syntax string} \<newline>
  2377       ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \<newline>
  2378       ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
  2379     ;
  2380     @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
  2381     ;
  2382     modedecl: (modes | ((const ':' modes) \<newline>
  2383         (@'and' ((const ':' modes @'and') +))?))
  2384     ;
  2385     modes: mode @'as' const
  2386   \<close>}
  2387 
  2388   \<^descr> @{command (HOL) "export_code"} generates code for a given list of
  2389   constants in the specified target language(s). If no serialization
  2390   instruction is given, only abstract code is generated internally.
  2391 
  2392   Constants may be specified by giving them literally, referring to all
  2393   executable constants within a certain theory by giving \<open>name._\<close>, or
  2394   referring to \<^emph>\<open>all\<close> executable constants currently available by giving \<open>_\<close>.
  2395 
  2396   By default, exported identifiers are minimized per module. This can be
  2397   suppressed by prepending @{keyword "open"} before the list of constants.
  2398 
  2399   By default, for each involved theory one corresponding name space module is
  2400   generated. Alternatively, a module name may be specified after the @{keyword
  2401   "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module.
  2402 
  2403   For \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single
  2404   file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is
  2405   generated in multiple files reflecting the module hierarchy. Omitting the
  2406   file specification denotes standard output.
  2407 
  2408   Serializers take an optional list of arguments in parentheses. For
  2409   \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' argument;
  2410   ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause to each
  2411   appropriate datatype declaration.
  2412 
  2413   \<^descr> @{attribute (HOL) code} declare code equations for code generation.
  2414   Variant \<open>code equation\<close> declares a conventional equation as code equation.
  2415   Variants \<open>code abstype\<close> and \<open>code abstract\<close> declare abstract datatype
  2416   certificates or code equations on abstract datatype representations
  2417   respectively. Vanilla \<open>code\<close> falls back to \<open>code equation\<close> or \<open>code abstype\<close>
  2418   depending on the syntactic shape of the underlying equation. Variant \<open>code
  2419   del\<close> deselects a code equation for code generation.
  2420 
  2421   Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
  2422   and drop all code equations declared for them. In the case of {text abort},
  2423   these constants then are are not required to have a definition by means of
  2424   code equations; if needed these are implemented by program abort (exception)
  2425   instead.
  2426 
  2427   Usually packages introducing code equations provide a reasonable default
  2428   setup for selection.
  2429 
  2430   \<^descr> @{command (HOL) "code_datatype"} specifies a constructor set for a logical
  2431   type.
  2432 
  2433   \<^descr> @{command (HOL) "print_codesetup"} gives an overview on selected code
  2434   equations and code generator datatypes.
  2435 
  2436   \<^descr> @{attribute (HOL) code_unfold} declares (or with option ``\<open>del\<close>'' removes)
  2437   theorems which during preprocessing are applied as rewrite rules to any code
  2438   equation or evaluation input.
  2439 
  2440   \<^descr> @{attribute (HOL) code_post} declares (or with option ``\<open>del\<close>'' removes)
  2441   theorems which are applied as rewrite rules to any result of an evaluation.
  2442 
  2443   \<^descr> @{attribute (HOL) code_abbrev} declares (or with option ``\<open>del\<close>'' removes)
  2444   equations which are applied as rewrite rules to any result of an evaluation
  2445   and symmetrically during preprocessing to any code equation or evaluation
  2446   input.
  2447 
  2448   \<^descr> @{command (HOL) "print_codeproc"} prints the setup of the code generator
  2449   preprocessor.
  2450 
  2451   \<^descr> @{command (HOL) "code_thms"} prints a list of theorems representing the
  2452   corresponding program containing all given constants after preprocessing.
  2453 
  2454   \<^descr> @{command (HOL) "code_deps"} visualizes dependencies of theorems
  2455   representing the corresponding program containing all given constants after
  2456   preprocessing.
  2457 
  2458   \<^descr> @{command (HOL) "code_reserved"} declares a list of names as reserved for
  2459   a given target, preventing it to be shadowed by any generated code.
  2460 
  2461   \<^descr> @{command (HOL) "code_printing"} associates a series of symbols
  2462   (constants, type constructors, classes, class relations, instances, module
  2463   names) with target-specific serializations; omitting a serialization deletes
  2464   an existing serialization.
  2465 
  2466   \<^descr> @{command (HOL) "code_monad"} provides an auxiliary mechanism to generate
  2467   monadic code for Haskell.
  2468 
  2469   \<^descr> @{command (HOL) "code_identifier"} associates a a series of symbols
  2470   (constants, type constructors, classes, class relations, instances, module
  2471   names) with target-specific hints how these symbols shall be named. These
  2472   hints gain precedence over names for symbols with no hints at all.
  2473   Conflicting hints are subject to name disambiguation. \<^emph>\<open>Warning:\<close> It is at
  2474   the discretion of the user to ensure that name prefixes of identifiers in
  2475   compound statements like type classes or datatypes are still the same.
  2476 
  2477   \<^descr> @{command (HOL) "code_reflect"} without a ``\<open>file\<close>'' argument compiles
  2478   code into the system runtime environment and modifies the code generator
  2479   setup that future invocations of system runtime code generation referring to
  2480   one of the ``\<open>datatypes\<close>'' or ``\<open>functions\<close>'' entities use these precompiled
  2481   entities. With a ``\<open>file\<close>'' argument, the corresponding code is generated
  2482   into that specified file without modifying the code generator setup.
  2483 
  2484   \<^descr> @{command (HOL) "code_pred"} creates code equations for a predicate given
  2485   a set of introduction rules. Optional mode annotations determine which
  2486   arguments are supposed to be input or output. If alternative introduction
  2487   rules are declared, one must prove a corresponding elimination rule.
  2488 \<close>
  2489 
  2490 end