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