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