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