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