doc-src/IsarRef/Thy/HOL_Specific.thy
author haftmann
Fri Nov 26 12:03:18 2010 +0100 (2010-11-26)
changeset 40711 81bc73585eec
parent 40709 b29c70cd5c93
child 40800 330eb65c9469
permissions -rw-r--r--
globbing constant expressions use more idiomatic underscore rather than star
     1 theory HOL_Specific
     2 imports Main
     3 begin
     4 
     5 chapter {* Isabelle/HOL \label{ch:hol} *}
     6 
     7 section {* Typedef axiomatization \label{sec:hol-typedef} *}
     8 
     9 text {*
    10   \begin{matharray}{rcl}
    11     @{command_def (HOL) "typedef"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
    12   \end{matharray}
    13 
    14   \begin{rail}
    15     'typedef' altname? abstype '=' repset
    16     ;
    17 
    18     altname: '(' (name | 'open' | 'open' name) ')'
    19     ;
    20     abstype: typespecsorts mixfix?
    21     ;
    22     repset: term ('morphisms' name name)?
    23     ;
    24   \end{rail}
    25 
    26   \begin{description}
    27   
    28   \item @{command (HOL) "typedef"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = A"}
    29   axiomatizes a Gordon/HOL-style type definition in the background
    30   theory of the current context, depending on a non-emptiness result
    31   of the set @{text A} (which needs to be proven interactively).
    32 
    33   The raw type may not depend on parameters or assumptions of the
    34   context --- this is logically impossible in Isabelle/HOL --- but the
    35   non-emptiness property can be local, potentially resulting in
    36   multiple interpretations in target contexts.  Thus the established
    37   bijection between the representing set @{text A} and the new type
    38   @{text t} may semantically depend on local assumptions.
    39   
    40   By default, @{command (HOL) "typedef"} defines both a type @{text t}
    41   and a set (term constant) of the same name, unless an alternative
    42   base name is given in parentheses, or the ``@{text "(open)"}''
    43   declaration is used to suppress a separate constant definition
    44   altogether.  The injection from type to set is called @{text Rep_t},
    45   its inverse @{text Abs_t} --- this may be changed via an explicit
    46   @{keyword (HOL) "morphisms"} declaration.
    47   
    48   Theorems @{text Rep_t}, @{text Rep_t_inverse}, and @{text
    49   Abs_t_inverse} provide the most basic characterization as a
    50   corresponding injection/surjection pair (in both directions).  Rules
    51   @{text Rep_t_inject} and @{text Abs_t_inject} provide a slightly
    52   more convenient view on the injectivity part, suitable for automated
    53   proof tools (e.g.\ in @{attribute simp} or @{attribute iff}
    54   declarations).  Rules @{text Rep_t_cases}/@{text Rep_t_induct}, and
    55   @{text Abs_t_cases}/@{text Abs_t_induct} provide alternative views
    56   on surjectivity; these are already declared as set or type rules for
    57   the generic @{method cases} and @{method induct} methods.
    58   
    59   An alternative name for the set definition (and other derived
    60   entities) may be specified in parentheses; the default is to use
    61   @{text t} as indicated before.
    62 
    63   \end{description}
    64 *}
    65 
    66 
    67 section {* Adhoc tuples *}
    68 
    69 text {*
    70   \begin{matharray}{rcl}
    71     @{attribute (HOL) split_format}@{text "\<^sup>*"} & : & @{text attribute} \\
    72   \end{matharray}
    73 
    74   \begin{rail}
    75     'split_format' '(' 'complete' ')'
    76     ;
    77   \end{rail}
    78 
    79   \begin{description}
    80   
    81   \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
    82   arguments in function applications to be represented canonically
    83   according to their tuple type structure.
    84 
    85   Note that this operation tends to invent funny names for new local
    86   parameters introduced.
    87 
    88   \end{description}
    89 *}
    90 
    91 
    92 section {* Records \label{sec:hol-record} *}
    93 
    94 text {*
    95   In principle, records merely generalize the concept of tuples, where
    96   components may be addressed by labels instead of just position.  The
    97   logical infrastructure of records in Isabelle/HOL is slightly more
    98   advanced, though, supporting truly extensible record schemes.  This
    99   admits operations that are polymorphic with respect to record
   100   extension, yielding ``object-oriented'' effects like (single)
   101   inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more
   102   details on object-oriented verification and record subtyping in HOL.
   103 *}
   104 
   105 
   106 subsection {* Basic concepts *}
   107 
   108 text {*
   109   Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
   110   at the level of terms and types.  The notation is as follows:
   111 
   112   \begin{center}
   113   \begin{tabular}{l|l|l}
   114     & record terms & record types \\ \hline
   115     fixed & @{text "\<lparr>x = a, y = b\<rparr>"} & @{text "\<lparr>x :: A, y :: B\<rparr>"} \\
   116     schematic & @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} &
   117       @{text "\<lparr>x :: A, y :: B, \<dots> :: M\<rparr>"} \\
   118   \end{tabular}
   119   \end{center}
   120 
   121   \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
   122   "(| x = a |)"}.
   123 
   124   A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value
   125   @{text a} and field @{text y} of value @{text b}.  The corresponding
   126   type is @{text "\<lparr>x :: A, y :: B\<rparr>"}, assuming that @{text "a :: A"}
   127   and @{text "b :: B"}.
   128 
   129   A record scheme like @{text "\<lparr>x = a, y = b, \<dots> = m\<rparr>"} contains fields
   130   @{text x} and @{text y} as before, but also possibly further fields
   131   as indicated by the ``@{text "\<dots>"}'' notation (which is actually part
   132   of the syntax).  The improper field ``@{text "\<dots>"}'' of a record
   133   scheme is called the \emph{more part}.  Logically it is just a free
   134   variable, which is occasionally referred to as ``row variable'' in
   135   the literature.  The more part of a record scheme may be
   136   instantiated by zero or more further components.  For example, the
   137   previous scheme may get instantiated to @{text "\<lparr>x = a, y = b, z =
   138   c, \<dots> = m'\<rparr>"}, where @{text m'} refers to a different more part.
   139   Fixed records are special instances of record schemes, where
   140   ``@{text "\<dots>"}'' is properly terminated by the @{text "() :: unit"}
   141   element.  In fact, @{text "\<lparr>x = a, y = b\<rparr>"} is just an abbreviation
   142   for @{text "\<lparr>x = a, y = b, \<dots> = ()\<rparr>"}.
   143   
   144   \medskip Two key observations make extensible records in a simply
   145   typed language like HOL work out:
   146 
   147   \begin{enumerate}
   148 
   149   \item the more part is internalized, as a free term or type
   150   variable,
   151 
   152   \item field names are externalized, they cannot be accessed within
   153   the logic as first-class values.
   154 
   155   \end{enumerate}
   156 
   157   \medskip In Isabelle/HOL record types have to be defined explicitly,
   158   fixing their field names and types, and their (optional) parent
   159   record.  Afterwards, records may be formed using above syntax, while
   160   obeying the canonical order of fields as given by their declaration.
   161   The record package provides several standard operations like
   162   selectors and updates.  The common setup for various generic proof
   163   tools enable succinct reasoning patterns.  See also the Isabelle/HOL
   164   tutorial \cite{isabelle-hol-book} for further instructions on using
   165   records in practice.
   166 *}
   167 
   168 
   169 subsection {* Record specifications *}
   170 
   171 text {*
   172   \begin{matharray}{rcl}
   173     @{command_def (HOL) "record"} & : & @{text "theory \<rightarrow> theory"} \\
   174   \end{matharray}
   175 
   176   \begin{rail}
   177     'record' typespecsorts '=' (type '+')? (constdecl +)
   178     ;
   179   \end{rail}
   180 
   181   \begin{description}
   182 
   183   \item @{command (HOL) "record"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
   184   \<dots> c\<^sub>n :: \<sigma>\<^sub>n"} defines extensible record type @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"},
   185   derived from the optional parent record @{text "\<tau>"} by adding new
   186   field components @{text "c\<^sub>i :: \<sigma>\<^sub>i"} etc.
   187 
   188   The type variables of @{text "\<tau>"} and @{text "\<sigma>\<^sub>i"} need to be
   189   covered by the (distinct) parameters @{text "\<alpha>\<^sub>1, \<dots>,
   190   \<alpha>\<^sub>m"}.  Type constructor @{text t} has to be new, while @{text
   191   \<tau>} needs to specify an instance of an existing record type.  At
   192   least one new field @{text "c\<^sub>i"} has to be specified.
   193   Basically, field names need to belong to a unique record.  This is
   194   not a real restriction in practice, since fields are qualified by
   195   the record name internally.
   196 
   197   The parent record specification @{text \<tau>} is optional; if omitted
   198   @{text t} becomes a root record.  The hierarchy of all records
   199   declared within a theory context forms a forest structure, i.e.\ a
   200   set of trees starting with a root record each.  There is no way to
   201   merge multiple parent records!
   202 
   203   For convenience, @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} is made a
   204   type abbreviation for the fixed record type @{text "\<lparr>c\<^sub>1 ::
   205   \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>"}, likewise is @{text
   206   "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme"} made an abbreviation for
   207   @{text "\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
   208   \<zeta>\<rparr>"}.
   209 
   210   \end{description}
   211 *}
   212 
   213 
   214 subsection {* Record operations *}
   215 
   216 text {*
   217   Any record definition of the form presented above produces certain
   218   standard operations.  Selectors and updates are provided for any
   219   field, including the improper one ``@{text more}''.  There are also
   220   cumulative record constructor functions.  To simplify the
   221   presentation below, we assume for now that @{text "(\<alpha>\<^sub>1, \<dots>,
   222   \<alpha>\<^sub>m) t"} is a root record with fields @{text "c\<^sub>1 ::
   223   \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n"}.
   224 
   225   \medskip \textbf{Selectors} and \textbf{updates} are available for
   226   any field (including ``@{text more}''):
   227 
   228   \begin{matharray}{lll}
   229     @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
   230     @{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>"} \\
   231   \end{matharray}
   232 
   233   There is special syntax for application of updates: @{text "r\<lparr>x :=
   234   a\<rparr>"} abbreviates term @{text "x_update a r"}.  Further notation for
   235   repeated updates is also available: @{text "r\<lparr>x := a\<rparr>\<lparr>y := b\<rparr>\<lparr>z :=
   236   c\<rparr>"} may be written @{text "r\<lparr>x := a, y := b, z := c\<rparr>"}.  Note that
   237   because of postfix notation the order of fields shown here is
   238   reverse than in the actual term.  Since repeated updates are just
   239   function applications, fields may be freely permuted in @{text "\<lparr>x
   240   := a, y := b, z := c\<rparr>"}, as far as logical equality is concerned.
   241   Thus commutativity of independent updates can be proven within the
   242   logic for any two fields, but not as a general theorem.
   243 
   244   \medskip The \textbf{make} operation provides a cumulative record
   245   constructor function:
   246 
   247   \begin{matharray}{lll}
   248     @{text "t.make"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
   249   \end{matharray}
   250 
   251   \medskip We now reconsider the case of non-root records, which are
   252   derived of some parent.  In general, the latter may depend on
   253   another parent as well, resulting in a list of \emph{ancestor
   254   records}.  Appending the lists of fields of all ancestors results in
   255   a certain field prefix.  The record package automatically takes care
   256   of this by lifting operations over this context of ancestor fields.
   257   Assuming that @{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t"} has ancestor
   258   fields @{text "b\<^sub>1 :: \<rho>\<^sub>1, \<dots>, b\<^sub>k :: \<rho>\<^sub>k"},
   259   the above record operations will get the following types:
   260 
   261   \medskip
   262   \begin{tabular}{lll}
   263     @{text "c\<^sub>i"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow> \<sigma>\<^sub>i"} \\
   264     @{text "c\<^sub>i_update"} & @{text "::"} & @{text "\<sigma>\<^sub>i \<Rightarrow> 
   265       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr> \<Rightarrow>
   266       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
   267     @{text "t.make"} & @{text "::"} & @{text "\<rho>\<^sub>1 \<Rightarrow> \<dots> \<rho>\<^sub>k \<Rightarrow> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow>
   268       \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
   269   \end{tabular}
   270   \medskip
   271 
   272   \noindent Some further operations address the extension aspect of a
   273   derived record scheme specifically: @{text "t.fields"} produces a
   274   record fragment consisting of exactly the new fields introduced here
   275   (the result may serve as a more part elsewhere); @{text "t.extend"}
   276   takes a fixed record and adds a given more part; @{text
   277   "t.truncate"} restricts a record scheme to a fixed record.
   278 
   279   \medskip
   280   \begin{tabular}{lll}
   281     @{text "t.fields"} & @{text "::"} & @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>n \<Rightarrow> \<lparr>\<^vec>c :: \<^vec>\<sigma>\<rparr>"} \\
   282     @{text "t.extend"} & @{text "::"} & @{text "\<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>\<rparr> \<Rightarrow>
   283       \<zeta> \<Rightarrow> \<lparr>\<^vec>b :: \<^vec>\<rho>, \<^vec>c :: \<^vec>\<sigma>, \<dots> :: \<zeta>\<rparr>"} \\
   284     @{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>"} \\
   285   \end{tabular}
   286   \medskip
   287 
   288   \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide
   289   for root records.
   290 *}
   291 
   292 
   293 subsection {* Derived rules and proof tools *}
   294 
   295 text {*
   296   The record package proves several results internally, declaring
   297   these facts to appropriate proof tools.  This enables users to
   298   reason about record structures quite conveniently.  Assume that
   299   @{text t} is a record type as specified above.
   300 
   301   \begin{enumerate}
   302   
   303   \item Standard conversions for selectors or updates applied to
   304   record constructor terms are made part of the default Simplifier
   305   context; thus proofs by reduction of basic operations merely require
   306   the @{method simp} method without further arguments.  These rules
   307   are available as @{text "t.simps"}, too.
   308   
   309   \item Selectors applied to updated records are automatically reduced
   310   by an internal simplification procedure, which is also part of the
   311   standard Simplifier setup.
   312 
   313   \item Inject equations of a form analogous to @{prop "(x, y) = (x',
   314   y') \<equiv> x = x' \<and> y = y'"} are declared to the Simplifier and Classical
   315   Reasoner as @{attribute iff} rules.  These rules are available as
   316   @{text "t.iffs"}.
   317 
   318   \item The introduction rule for record equality analogous to @{text
   319   "x r = x r' \<Longrightarrow> y r = y r' \<dots> \<Longrightarrow> r = r'"} is declared to the Simplifier,
   320   and as the basic rule context as ``@{attribute intro}@{text "?"}''.
   321   The rule is called @{text "t.equality"}.
   322 
   323   \item Representations of arbitrary record expressions as canonical
   324   constructor terms are provided both in @{method cases} and @{method
   325   induct} format (cf.\ the generic proof methods of the same name,
   326   \secref{sec:cases-induct}).  Several variations are available, for
   327   fixed records, record schemes, more parts etc.
   328   
   329   The generic proof methods are sufficiently smart to pick the most
   330   sensible rule according to the type of the indicated record
   331   expression: users just need to apply something like ``@{text "(cases
   332   r)"}'' to a certain proof problem.
   333 
   334   \item The derived record operations @{text "t.make"}, @{text
   335   "t.fields"}, @{text "t.extend"}, @{text "t.truncate"} are \emph{not}
   336   treated automatically, but usually need to be expanded by hand,
   337   using the collective fact @{text "t.defs"}.
   338 
   339   \end{enumerate}
   340 *}
   341 
   342 
   343 section {* Datatypes \label{sec:hol-datatype} *}
   344 
   345 text {*
   346   \begin{matharray}{rcl}
   347     @{command_def (HOL) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
   348   @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   349   \end{matharray}
   350 
   351   \begin{rail}
   352     'datatype' (dtspec + 'and')
   353     ;
   354     'rep_datatype' ('(' (name +) ')')? (term +)
   355     ;
   356 
   357     dtspec: parname? typespec mixfix? '=' (cons + '|')
   358     ;
   359     cons: name ( type * ) mixfix?
   360   \end{rail}
   361 
   362   \begin{description}
   363 
   364   \item @{command (HOL) "datatype"} defines inductive datatypes in
   365   HOL.
   366 
   367   \item @{command (HOL) "rep_datatype"} represents existing types as
   368   inductive ones, generating the standard infrastructure of derived
   369   concepts (primitive recursion etc.).
   370 
   371   \end{description}
   372 
   373   The induction and exhaustion theorems generated provide case names
   374   according to the constructors involved, while parameters are named
   375   after the types (see also \secref{sec:cases-induct}).
   376 
   377   See \cite{isabelle-HOL} for more details on datatypes, but beware of
   378   the old-style theory syntax being used there!  Apart from proper
   379   proof methods for case-analysis and induction, there are also
   380   emulations of ML tactics @{method (HOL) case_tac} and @{method (HOL)
   381   induct_tac} available, see \secref{sec:hol-induct-tac}; these admit
   382   to refer directly to the internal structure of subgoals (including
   383   internally bound parameters).
   384 *}
   385 
   386 
   387 section {* Recursive functions \label{sec:recursion} *}
   388 
   389 text {*
   390   \begin{matharray}{rcl}
   391     @{command_def (HOL) "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   392     @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   393     @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
   394     @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
   395   \end{matharray}
   396 
   397   \begin{rail}
   398     'primrec' target? fixes 'where' equations
   399     ;
   400     ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
   401     ;
   402     equations: (thmdecl? prop + '|')
   403     ;
   404     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
   405     ;
   406     'termination' ( term )?
   407   \end{rail}
   408 
   409   \begin{description}
   410 
   411   \item @{command (HOL) "primrec"} defines primitive recursive
   412   functions over datatypes, see also \cite{isabelle-HOL}.
   413 
   414   \item @{command (HOL) "function"} defines functions by general
   415   wellfounded recursion. A detailed description with examples can be
   416   found in \cite{isabelle-function}. The function is specified by a
   417   set of (possibly conditional) recursive equations with arbitrary
   418   pattern matching. The command generates proof obligations for the
   419   completeness and the compatibility of patterns.
   420 
   421   The defined function is considered partial, and the resulting
   422   simplification rules (named @{text "f.psimps"}) and induction rule
   423   (named @{text "f.pinduct"}) are guarded by a generated domain
   424   predicate @{text "f_dom"}. The @{command (HOL) "termination"}
   425   command can then be used to establish that the function is total.
   426 
   427   \item @{command (HOL) "fun"} is a shorthand notation for ``@{command
   428   (HOL) "function"}~@{text "(sequential)"}, followed by automated
   429   proof attempts regarding pattern matching and termination.  See
   430   \cite{isabelle-function} for further details.
   431 
   432   \item @{command (HOL) "termination"}~@{text f} commences a
   433   termination proof for the previously defined function @{text f}.  If
   434   this is omitted, the command refers to the most recent function
   435   definition.  After the proof is closed, the recursive equations and
   436   the induction principle is established.
   437 
   438   \end{description}
   439 
   440   Recursive definitions introduced by the @{command (HOL) "function"}
   441   command accommodate
   442   reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
   443   "c.induct"} (where @{text c} is the name of the function definition)
   444   refers to a specific induction rule, with parameters named according
   445   to the user-specified equations. Cases are numbered (starting from 1).
   446 
   447   For @{command (HOL) "primrec"}, the induction principle coincides
   448   with structural recursion on the datatype the recursion is carried
   449   out.
   450 
   451   The equations provided by these packages may be referred later as
   452   theorem list @{text "f.simps"}, where @{text f} is the (collective)
   453   name of the functions defined.  Individual equations may be named
   454   explicitly as well.
   455 
   456   The @{command (HOL) "function"} command accepts the following
   457   options.
   458 
   459   \begin{description}
   460 
   461   \item @{text sequential} enables a preprocessor which disambiguates
   462   overlapping patterns by making them mutually disjoint.  Earlier
   463   equations take precedence over later ones.  This allows to give the
   464   specification in a format very similar to functional programming.
   465   Note that the resulting simplification and induction rules
   466   correspond to the transformed specification, not the one given
   467   originally. This usually means that each equation given by the user
   468   may result in several theorems.  Also note that this automatic
   469   transformation only works for ML-style datatype patterns.
   470 
   471   \item @{text domintros} enables the automated generation of
   472   introduction rules for the domain predicate. While mostly not
   473   needed, they can be helpful in some proofs about partial functions.
   474 
   475   \item @{text tailrec} generates the unconstrained recursive
   476   equations even without a termination proof, provided that the
   477   function is tail-recursive. This currently only works
   478 
   479   \item @{text "default d"} allows to specify a default value for a
   480   (partial) function, which will ensure that @{text "f x = d x"}
   481   whenever @{text "x \<notin> f_dom"}.
   482 
   483   \end{description}
   484 *}
   485 
   486 
   487 subsection {* Proof methods related to recursive definitions *}
   488 
   489 text {*
   490   \begin{matharray}{rcl}
   491     @{method_def (HOL) pat_completeness} & : & @{text method} \\
   492     @{method_def (HOL) relation} & : & @{text method} \\
   493     @{method_def (HOL) lexicographic_order} & : & @{text method} \\
   494     @{method_def (HOL) size_change} & : & @{text method} \\
   495   \end{matharray}
   496 
   497   \begin{rail}
   498     'relation' term
   499     ;
   500     'lexicographic_order' ( clasimpmod * )
   501     ;
   502     'size_change' ( orders ( clasimpmod * ) )
   503     ;
   504     orders: ( 'max' | 'min' | 'ms' ) *
   505   \end{rail}
   506 
   507   \begin{description}
   508 
   509   \item @{method (HOL) pat_completeness} is a specialized method to
   510   solve goals regarding the completeness of pattern matching, as
   511   required by the @{command (HOL) "function"} package (cf.\
   512   \cite{isabelle-function}).
   513 
   514   \item @{method (HOL) relation}~@{text R} introduces a termination
   515   proof using the relation @{text R}.  The resulting proof state will
   516   contain goals expressing that @{text R} is wellfounded, and that the
   517   arguments of recursive calls decrease with respect to @{text R}.
   518   Usually, this method is used as the initial proof step of manual
   519   termination proofs.
   520 
   521   \item @{method (HOL) "lexicographic_order"} attempts a fully
   522   automated termination proof by searching for a lexicographic
   523   combination of size measures on the arguments of the function. The
   524   method accepts the same arguments as the @{method auto} method,
   525   which it uses internally to prove local descents.  The same context
   526   modifiers as for @{method auto} are accepted, see
   527   \secref{sec:clasimp}.
   528 
   529   In case of failure, extensive information is printed, which can help
   530   to analyse the situation (cf.\ \cite{isabelle-function}).
   531 
   532   \item @{method (HOL) "size_change"} also works on termination goals,
   533   using a variation of the size-change principle, together with a
   534   graph decomposition technique (see \cite{krauss_phd} for details).
   535   Three kinds of orders are used internally: @{text max}, @{text min},
   536   and @{text ms} (multiset), which is only available when the theory
   537   @{text Multiset} is loaded. When no order kinds are given, they are
   538   tried in order. The search for a termination proof uses SAT solving
   539   internally.
   540 
   541  For local descent proofs, the same context modifiers as for @{method
   542   auto} are accepted, see \secref{sec:clasimp}.
   543 
   544   \end{description}
   545 *}
   546 
   547 subsection {* Functions with explicit partiality *}
   548 
   549 text {*
   550   \begin{matharray}{rcl}
   551     @{command_def (HOL) "partial_function"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   552     @{attribute_def (HOL) "partial_function_mono"} & : & @{text attribute} \\
   553   \end{matharray}
   554 
   555   \begin{rail}
   556     'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
   557   \end{rail}
   558 
   559   \begin{description}
   560 
   561   \item @{command (HOL) "partial_function"} defines recursive
   562   functions based on fixpoints in complete partial orders. No
   563   termination proof is required from the user or constructed
   564   internally. Instead, the possibility of non-termination is modelled
   565   explicitly in the result type, which contains an explicit bottom
   566   element.
   567 
   568   Pattern matching and mutual recursion are currently not supported.
   569   Thus, the specification consists of a single function described by a
   570   single recursive equation.
   571 
   572   There are no fixed syntactic restrictions on the body of the
   573   function, but the induced functional must be provably monotonic
   574   wrt.\ the underlying order.  The monotonicitity proof is performed
   575   internally, and the definition is rejected when it fails. The proof
   576   can be influenced by declaring hints using the
   577   @{attribute (HOL) partial_function_mono} attribute.
   578 
   579   The mandatory @{text mode} argument specifies the mode of operation
   580   of the command, which directly corresponds to a complete partial
   581   order on the result type. By default, the following modes are
   582   defined: 
   583 
   584   \begin{description}
   585   \item @{text option} defines functions that map into the @{type
   586   option} type. Here, the value @{term None} is used to model a
   587   non-terminating computation. Monotonicity requires that if @{term
   588   None} is returned by a recursive call, then the overall result
   589   must also be @{term None}. This is best achieved through the use of
   590   the monadic operator @{const "Option.bind"}.
   591   
   592   \item @{text tailrec} defines functions with an arbitrary result
   593   type and uses the slightly degenerated partial order where @{term
   594   "undefined"} is the bottom element.  Now, monotonicity requires that
   595   if @{term undefined} is returned by a recursive call, then the
   596   overall result must also be @{term undefined}. In practice, this is
   597   only satisfied when each recursive call is a tail call, whose result
   598   is directly returned. Thus, this mode of operation allows the
   599   definition of arbitrary tail-recursive functions.
   600   \end{description}
   601 
   602   Experienced users may define new modes by instantiating the locale
   603   @{const "partial_function_definitions"} appropriately.
   604 
   605   \item @{attribute (HOL) partial_function_mono} declares rules for
   606   use in the internal monononicity proofs of partial function
   607   definitions.
   608 
   609   \end{description}
   610 
   611 *}
   612 
   613 subsection {* Old-style recursive function definitions (TFL) *}
   614 
   615 text {*
   616   The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
   617   "recdef_tc"} for defining recursive are mostly obsolete; @{command
   618   (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
   619 
   620   \begin{matharray}{rcl}
   621     @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\
   622     @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
   623   \end{matharray}
   624 
   625   \begin{rail}
   626     'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
   627     ;
   628     recdeftc thmdecl? tc
   629     ;
   630     hints: '(' 'hints' ( recdefmod * ) ')'
   631     ;
   632     recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   633     ;
   634     tc: nameref ('(' nat ')')?
   635     ;
   636   \end{rail}
   637 
   638   \begin{description}
   639   
   640   \item @{command (HOL) "recdef"} defines general well-founded
   641   recursive functions (using the TFL package), see also
   642   \cite{isabelle-HOL}.  The ``@{text "(permissive)"}'' option tells
   643   TFL to recover from failed proof attempts, returning unfinished
   644   results.  The @{text recdef_simp}, @{text recdef_cong}, and @{text
   645   recdef_wf} hints refer to auxiliary rules to be used in the internal
   646   automated proof process of TFL.  Additional @{syntax clasimpmod}
   647   declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
   648   context of the Simplifier (cf.\ \secref{sec:simplifier}) and
   649   Classical reasoner (cf.\ \secref{sec:classical}).
   650   
   651   \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
   652   proof for leftover termination condition number @{text i} (default
   653   1) as generated by a @{command (HOL) "recdef"} definition of
   654   constant @{text c}.
   655   
   656   Note that in most cases, @{command (HOL) "recdef"} is able to finish
   657   its internal proofs without manual intervention.
   658 
   659   \end{description}
   660 
   661   \medskip Hints for @{command (HOL) "recdef"} may be also declared
   662   globally, using the following attributes.
   663 
   664   \begin{matharray}{rcl}
   665     @{attribute_def (HOL) recdef_simp} & : & @{text attribute} \\
   666     @{attribute_def (HOL) recdef_cong} & : & @{text attribute} \\
   667     @{attribute_def (HOL) recdef_wf} & : & @{text attribute} \\
   668   \end{matharray}
   669 
   670   \begin{rail}
   671     ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
   672     ;
   673   \end{rail}
   674 *}
   675 
   676 
   677 section {* Inductive and coinductive definitions \label{sec:hol-inductive} *}
   678 
   679 text {*
   680   An \textbf{inductive definition} specifies the least predicate (or
   681   set) @{text R} closed under given rules: applying a rule to elements
   682   of @{text R} yields a result within @{text R}.  For example, a
   683   structural operational semantics is an inductive definition of an
   684   evaluation relation.
   685 
   686   Dually, a \textbf{coinductive definition} specifies the greatest
   687   predicate~/ set @{text R} that is consistent with given rules: every
   688   element of @{text R} can be seen as arising by applying a rule to
   689   elements of @{text R}.  An important example is using bisimulation
   690   relations to formalise equivalence of processes and infinite data
   691   structures.
   692 
   693   \medskip The HOL package is related to the ZF one, which is
   694   described in a separate paper,\footnote{It appeared in CADE
   695   \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
   696   which you should refer to in case of difficulties.  The package is
   697   simpler than that of ZF thanks to implicit type-checking in HOL.
   698   The types of the (co)inductive predicates (or sets) determine the
   699   domain of the fixedpoint definition, and the package does not have
   700   to use inference rules for type-checking.
   701 
   702   \begin{matharray}{rcl}
   703     @{command_def (HOL) "inductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   704     @{command_def (HOL) "inductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   705     @{command_def (HOL) "coinductive"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   706     @{command_def (HOL) "coinductive_set"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   707     @{attribute_def (HOL) mono} & : & @{text attribute} \\
   708   \end{matharray}
   709 
   710   \begin{rail}
   711     ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
   712     ('where' clauses)? ('monos' thmrefs)?
   713     ;
   714     clauses: (thmdecl? prop + '|')
   715     ;
   716     'mono' (() | 'add' | 'del')
   717     ;
   718   \end{rail}
   719 
   720   \begin{description}
   721 
   722   \item @{command (HOL) "inductive"} and @{command (HOL)
   723   "coinductive"} define (co)inductive predicates from the
   724   introduction rules given in the @{keyword "where"} part.  The
   725   optional @{keyword "for"} part contains a list of parameters of the
   726   (co)inductive predicates that remain fixed throughout the
   727   definition.  The optional @{keyword "monos"} section contains
   728   \emph{monotonicity theorems}, which are required for each operator
   729   applied to a recursive set in the introduction rules.  There
   730   \emph{must} be a theorem of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"},
   731   for each premise @{text "M R\<^sub>i t"} in an introduction rule!
   732 
   733   \item @{command (HOL) "inductive_set"} and @{command (HOL)
   734   "coinductive_set"} are wrappers for to the previous commands,
   735   allowing the definition of (co)inductive sets.
   736 
   737   \item @{attribute (HOL) mono} declares monotonicity rules.  These
   738   rule are involved in the automated monotonicity proof of @{command
   739   (HOL) "inductive"}.
   740 
   741   \end{description}
   742 *}
   743 
   744 
   745 subsection {* Derived rules *}
   746 
   747 text {*
   748   Each (co)inductive definition @{text R} adds definitions to the
   749   theory and also proves some theorems:
   750 
   751   \begin{description}
   752 
   753   \item @{text R.intros} is the list of introduction rules as proven
   754   theorems, for the recursive predicates (or sets).  The rules are
   755   also available individually, using the names given them in the
   756   theory file;
   757 
   758   \item @{text R.cases} is the case analysis (or elimination) rule;
   759 
   760   \item @{text R.induct} or @{text R.coinduct} is the (co)induction
   761   rule.
   762 
   763   \end{description}
   764 
   765   When several predicates @{text "R\<^sub>1, \<dots>, R\<^sub>n"} are
   766   defined simultaneously, the list of introduction rules is called
   767   @{text "R\<^sub>1_\<dots>_R\<^sub>n.intros"}, the case analysis rules are
   768   called @{text "R\<^sub>1.cases, \<dots>, R\<^sub>n.cases"}, and the list
   769   of mutual induction rules is called @{text
   770   "R\<^sub>1_\<dots>_R\<^sub>n.inducts"}.
   771 *}
   772 
   773 
   774 subsection {* Monotonicity theorems *}
   775 
   776 text {*
   777   Each theory contains a default set of theorems that are used in
   778   monotonicity proofs.  New rules can be added to this set via the
   779   @{attribute (HOL) mono} attribute.  The HOL theory @{text Inductive}
   780   shows how this is done.  In general, the following monotonicity
   781   theorems may be added:
   782 
   783   \begin{itemize}
   784 
   785   \item Theorems of the form @{text "A \<le> B \<Longrightarrow> M A \<le> M B"}, for proving
   786   monotonicity of inductive definitions whose introduction rules have
   787   premises involving terms such as @{text "M R\<^sub>i t"}.
   788 
   789   \item Monotonicity theorems for logical operators, which are of the
   790   general form @{text "(\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> (\<dots> \<longrightarrow> \<dots>) \<Longrightarrow> \<dots> \<longrightarrow> \<dots>"}.  For example, in
   791   the case of the operator @{text "\<or>"}, the corresponding theorem is
   792   \[
   793   \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"}}
   794   \]
   795 
   796   \item De Morgan style equations for reasoning about the ``polarity''
   797   of expressions, e.g.
   798   \[
   799   @{prop "\<not> \<not> P \<longleftrightarrow> P"} \qquad\qquad
   800   @{prop "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"}
   801   \]
   802 
   803   \item Equations for reducing complex operators to more primitive
   804   ones whose monotonicity can easily be proved, e.g.
   805   \[
   806   @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> \<not> P \<or> Q"} \qquad\qquad
   807   @{prop "Ball A P \<equiv> \<forall>x. x \<in> A \<longrightarrow> P x"}
   808   \]
   809 
   810   \end{itemize}
   811 
   812   %FIXME: Example of an inductive definition
   813 *}
   814 
   815 
   816 section {* Arithmetic proof support *}
   817 
   818 text {*
   819   \begin{matharray}{rcl}
   820     @{method_def (HOL) arith} & : & @{text method} \\
   821     @{attribute_def (HOL) arith} & : & @{text attribute} \\
   822     @{attribute_def (HOL) arith_split} & : & @{text attribute} \\
   823   \end{matharray}
   824 
   825   The @{method (HOL) arith} method decides linear arithmetic problems
   826   (on types @{text nat}, @{text int}, @{text real}).  Any current
   827   facts are inserted into the goal before running the procedure.
   828 
   829   The @{attribute (HOL) arith} attribute declares facts that are
   830   always supplied to the arithmetic provers implicitly.
   831 
   832   The @{attribute (HOL) arith_split} attribute declares case split
   833   rules to be expanded before @{method (HOL) arith} is invoked.
   834 
   835   Note that a simpler (but faster) arithmetic prover is
   836   already invoked by the Simplifier.
   837 *}
   838 
   839 
   840 section {* Intuitionistic proof search *}
   841 
   842 text {*
   843   \begin{matharray}{rcl}
   844     @{method_def (HOL) iprover} & : & @{text method} \\
   845   \end{matharray}
   846 
   847   \begin{rail}
   848     'iprover' ( rulemod * )
   849     ;
   850   \end{rail}
   851 
   852   The @{method (HOL) iprover} method performs intuitionistic proof
   853   search, depending on specifically declared rules from the context,
   854   or given as explicit arguments.  Chained facts are inserted into the
   855   goal before commencing proof search.
   856 
   857   Rules need to be classified as @{attribute (Pure) intro},
   858   @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
   859   ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
   860   applied aggressively (without considering back-tracking later).
   861   Rules declared with ``@{text "?"}'' are ignored in proof search (the
   862   single-step @{method rule} method still observes these).  An
   863   explicit weight annotation may be given as well; otherwise the
   864   number of rule premises will be taken into account here.
   865 *}
   866 
   867 
   868 section {* Coherent Logic *}
   869 
   870 text {*
   871   \begin{matharray}{rcl}
   872     @{method_def (HOL) "coherent"} & : & @{text method} \\
   873   \end{matharray}
   874 
   875   \begin{rail}
   876     'coherent' thmrefs?
   877     ;
   878   \end{rail}
   879 
   880   The @{method (HOL) coherent} method solves problems of
   881   \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
   882   applications in confluence theory, lattice theory and projective
   883   geometry.  See @{"file" "~~/src/HOL/ex/Coherent.thy"} for some
   884   examples.
   885 *}
   886 
   887 
   888 section {* Checking and refuting propositions *}
   889 
   890 text {*
   891   Identifying incorrect propositions usually involves evaluation of
   892   particular assignments and systematic counter example search.  This
   893   is supported by the following commands.
   894 
   895   \begin{matharray}{rcl}
   896     @{command_def (HOL) "value"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   897     @{command_def (HOL) "quickcheck"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow>"} \\
   898     @{command_def (HOL) "quickcheck_params"} & : & @{text "theory \<rightarrow> theory"}
   899   \end{matharray}
   900 
   901   \begin{rail}
   902     'value' ( ( '[' name ']' ) ? ) modes? term
   903     ;
   904 
   905     'quickcheck' ( ( '[' args ']' ) ? ) nat?
   906     ;
   907 
   908     'quickcheck_params' ( ( '[' args ']' ) ? )
   909     ;
   910 
   911     modes: '(' (name + ) ')'
   912     ;
   913 
   914     args: ( name '=' value + ',' )
   915     ;
   916   \end{rail}
   917 
   918   \begin{description}
   919 
   920   \item @{command (HOL) "value"}~@{text t} evaluates and prints a
   921     term; optionally @{text modes} can be specified, which are
   922     appended to the current print mode (see also \cite{isabelle-ref}).
   923     Internally, the evaluation is performed by registered evaluators,
   924     which are invoked sequentially until a result is returned.
   925     Alternatively a specific evaluator can be selected using square
   926     brackets; typical evaluators use the current set of code equations
   927     to normalize and include @{text simp} for fully symbolic evaluation
   928     using the simplifier, @{text nbe} for \emph{normalization by evaluation}
   929     and \emph{code} for code generation in SML.
   930 
   931   \item @{command (HOL) "quickcheck"} tests the current goal for
   932     counter examples using a series of arbitrary assignments for its
   933     free variables; by default the first subgoal is tested, an other
   934     can be selected explicitly using an optional goal index.
   935     A number of configuration options are supported for
   936     @{command (HOL) "quickcheck"}, notably:
   937 
   938     \begin{description}
   939 
   940     \item[@{text size}] specifies the maximum size of the search space
   941     for assignment values.
   942 
   943     \item[@{text iterations}] sets how many sets of assignments are
   944     generated for each particular size.
   945 
   946     \item[@{text no_assms}] specifies whether assumptions in
   947     structured proofs should be ignored.
   948 
   949     \item[@{text timeout}] sets the time limit in seconds.
   950 
   951     \item[@{text default_type}] sets the type(s) generally used to
   952     instantiate type variables.
   953 
   954     \item[@{text report}] if set quickcheck reports how many tests
   955     fulfilled the preconditions.
   956 
   957     \item[@{text quiet}] if not set quickcheck informs about the
   958     current size for assignment values.
   959 
   960     \item[@{text expect}] can be used to check if the user's
   961     expectation was met (@{text no_expectation}, @{text
   962     no_counterexample}, or @{text counterexample}).
   963 
   964     \end{description}
   965 
   966     These option can be given within square brackets.
   967 
   968   \item @{command (HOL) "quickcheck_params"} changes quickcheck
   969     configuration options persitently.
   970 
   971   \end{description}
   972 *}
   973 
   974 
   975 section {* Unstructured case analysis and induction \label{sec:hol-induct-tac} *}
   976 
   977 text {*
   978   The following tools of Isabelle/HOL support cases analysis and
   979   induction in unstructured tactic scripts; see also
   980   \secref{sec:cases-induct} for proper Isar versions of similar ideas.
   981 
   982   \begin{matharray}{rcl}
   983     @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
   984     @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
   985     @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
   986     @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   987   \end{matharray}
   988 
   989   \begin{rail}
   990     'case_tac' goalspec? term rule?
   991     ;
   992     'induct_tac' goalspec? (insts * 'and') rule?
   993     ;
   994     'ind_cases' (prop +) ('for' (name +)) ?
   995     ;
   996     'inductive_cases' (thmdecl? (prop +) + 'and')
   997     ;
   998 
   999     rule: ('rule' ':' thmref)
  1000     ;
  1001   \end{rail}
  1002 
  1003   \begin{description}
  1004 
  1005   \item @{method (HOL) case_tac} and @{method (HOL) induct_tac} admit
  1006   to reason about inductive types.  Rules are selected according to
  1007   the declarations by the @{attribute cases} and @{attribute induct}
  1008   attributes, cf.\ \secref{sec:cases-induct}.  The @{command (HOL)
  1009   datatype} package already takes care of this.
  1010 
  1011   These unstructured tactics feature both goal addressing and dynamic
  1012   instantiation.  Note that named rule cases are \emph{not} provided
  1013   as would be by the proper @{method cases} and @{method induct} proof
  1014   methods (see \secref{sec:cases-induct}).  Unlike the @{method
  1015   induct} method, @{method induct_tac} does not handle structured rule
  1016   statements, only the compact object-logic conclusion of the subgoal
  1017   being addressed.
  1018   
  1019   \item @{method (HOL) ind_cases} and @{command (HOL)
  1020   "inductive_cases"} provide an interface to the internal @{ML_text
  1021   mk_cases} operation.  Rules are simplified in an unrestricted
  1022   forward manner.
  1023 
  1024   While @{method (HOL) ind_cases} is a proof method to apply the
  1025   result immediately as elimination rules, @{command (HOL)
  1026   "inductive_cases"} provides case split theorems at the theory level
  1027   for later use.  The @{keyword "for"} argument of the @{method (HOL)
  1028   ind_cases} method allows to specify a list of variables that should
  1029   be generalized before applying the resulting rule.
  1030 
  1031   \end{description}
  1032 *}
  1033 
  1034 
  1035 section {* Executable code *}
  1036 
  1037 text {*
  1038   Isabelle/Pure provides two generic frameworks to support code
  1039   generation from executable specifications.  Isabelle/HOL
  1040   instantiates these mechanisms in a way that is amenable to end-user
  1041   applications.
  1042 
  1043   \medskip One framework generates code from functional programs
  1044   (including overloading using type classes) to SML \cite{SML}, OCaml
  1045   \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
  1046   \cite{scala-overview-tech-report}.
  1047   Conceptually, code generation is split up in three steps:
  1048   \emph{selection} of code theorems, \emph{translation} into an
  1049   abstract executable view and \emph{serialization} to a specific
  1050   \emph{target language}.  Inductive specifications can be executed
  1051   using the predicate compiler which operates within HOL.
  1052   See \cite{isabelle-codegen} for an introduction.
  1053 
  1054   \begin{matharray}{rcl}
  1055     @{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  1056     @{attribute_def (HOL) code} & : & @{text attribute} \\
  1057     @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
  1058     @{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
  1059     @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  1060     @{attribute_def (HOL) code_inline} & : & @{text attribute} \\
  1061     @{attribute_def (HOL) code_post} & : & @{text attribute} \\
  1062     @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  1063     @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  1064     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
  1065     @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
  1066     @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
  1067     @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
  1068     @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
  1069     @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
  1070     @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
  1071     @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
  1072     @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
  1073     @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
  1074   \end{matharray}
  1075 
  1076   \begin{rail}
  1077      'export_code' ( constexpr + ) \\
  1078        ( ( 'in' target ( 'module_name' string ) ? \\
  1079         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
  1080     ;
  1081 
  1082     const: term
  1083     ;
  1084 
  1085     constexpr: ( const | 'name._' | '_' )
  1086     ;
  1087 
  1088     typeconstructor: nameref
  1089     ;
  1090 
  1091     class: nameref
  1092     ;
  1093 
  1094     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
  1095     ;
  1096 
  1097     'code' ( 'del' | 'abstype' | 'abstract' ) ?
  1098     ;
  1099 
  1100     'code_abort' ( const + )
  1101     ;
  1102 
  1103     'code_datatype' ( const + )
  1104     ;
  1105 
  1106     'code_inline' ( 'del' ) ?
  1107     ;
  1108 
  1109     'code_post' ( 'del' ) ?
  1110     ;
  1111 
  1112     'code_thms' ( constexpr + ) ?
  1113     ;
  1114 
  1115     'code_deps' ( constexpr + ) ?
  1116     ;
  1117 
  1118     'code_const' (const + 'and') \\
  1119       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1120     ;
  1121 
  1122     'code_type' (typeconstructor + 'and') \\
  1123       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1124     ;
  1125 
  1126     'code_class' (class + 'and') \\
  1127       ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
  1128     ;
  1129 
  1130     'code_instance' (( typeconstructor '::' class ) + 'and') \\
  1131       ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
  1132     ;
  1133 
  1134     'code_reserved' target ( string + )
  1135     ;
  1136 
  1137     'code_monad' const const target
  1138     ;
  1139 
  1140     'code_include' target ( string ( string | '-') )
  1141     ;
  1142 
  1143     'code_modulename' target ( ( string string ) + )
  1144     ;
  1145 
  1146     'code_reflect' string \\
  1147       ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
  1148       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
  1149     ;
  1150 
  1151     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
  1152     ;
  1153 
  1154   \end{rail}
  1155 
  1156   \begin{description}
  1157 
  1158   \item @{command (HOL) "export_code"} generates code for a given list
  1159   of constants in the specified target language(s).  If no
  1160   serialization instruction is given, only abstract code is generated
  1161   internally.
  1162 
  1163   Constants may be specified by giving them literally, referring to
  1164   all executable contants within a certain theory by giving @{text
  1165   "name.*"}, or referring to \emph{all} executable constants currently
  1166   available by giving @{text "*"}.
  1167 
  1168   By default, for each involved theory one corresponding name space
  1169   module is generated.  Alternativly, a module name may be specified
  1170   after the @{keyword "module_name"} keyword; then \emph{all} code is
  1171   placed in this module.
  1172 
  1173   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
  1174   refers to a single file; for \emph{Haskell}, it refers to a whole
  1175   directory, where code is generated in multiple files reflecting the
  1176   module hierarchy.  Omitting the file specification denotes standard
  1177   output.
  1178 
  1179   Serializers take an optional list of arguments in parentheses.  For
  1180   \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
  1181   explicit module signatures.
  1182   
  1183   For \emph{Haskell} a module name prefix may be given using the
  1184   ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
  1185   ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
  1186   datatype declaration.
  1187 
  1188   \item @{attribute (HOL) code} explicitly selects (or with option
  1189   ``@{text "del"}'' deselects) a code equation for code generation.
  1190   Usually packages introducing code equations provide a reasonable
  1191   default setup for selection.  Variants @{text "code abstype"} and
  1192   @{text "code abstract"} declare abstract datatype certificates or
  1193   code equations on abstract datatype representations respectively.
  1194 
  1195   \item @{command (HOL) "code_abort"} declares constants which are not
  1196   required to have a definition by means of code equations; if needed
  1197   these are implemented by program abort instead.
  1198 
  1199   \item @{command (HOL) "code_datatype"} specifies a constructor set
  1200   for a logical type.
  1201 
  1202   \item @{command (HOL) "print_codesetup"} gives an overview on
  1203   selected code equations and code generator datatypes.
  1204 
  1205   \item @{attribute (HOL) code_inline} declares (or with option
  1206   ``@{text "del"}'' removes) inlining theorems which are applied as
  1207   rewrite rules to any code equation during preprocessing.
  1208 
  1209   \item @{attribute (HOL) code_post} declares (or with option ``@{text
  1210   "del"}'' removes) theorems which are applied as rewrite rules to any
  1211   result of an evaluation.
  1212 
  1213   \item @{command (HOL) "print_codeproc"} prints the setup of the code
  1214   generator preprocessor.
  1215 
  1216   \item @{command (HOL) "code_thms"} prints a list of theorems
  1217   representing the corresponding program containing all given
  1218   constants after preprocessing.
  1219 
  1220   \item @{command (HOL) "code_deps"} visualizes dependencies of
  1221   theorems representing the corresponding program containing all given
  1222   constants after preprocessing.
  1223 
  1224   \item @{command (HOL) "code_const"} associates a list of constants
  1225   with target-specific serializations; omitting a serialization
  1226   deletes an existing serialization.
  1227 
  1228   \item @{command (HOL) "code_type"} associates a list of type
  1229   constructors with target-specific serializations; omitting a
  1230   serialization deletes an existing serialization.
  1231 
  1232   \item @{command (HOL) "code_class"} associates a list of classes
  1233   with target-specific class names; omitting a serialization deletes
  1234   an existing serialization.  This applies only to \emph{Haskell}.
  1235 
  1236   \item @{command (HOL) "code_instance"} declares a list of type
  1237   constructor / class instance relations as ``already present'' for a
  1238   given target.  Omitting a ``@{text "-"}'' deletes an existing
  1239   ``already present'' declaration.  This applies only to
  1240   \emph{Haskell}.
  1241 
  1242   \item @{command (HOL) "code_reserved"} declares a list of names as
  1243   reserved for a given target, preventing it to be shadowed by any
  1244   generated code.
  1245 
  1246   \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
  1247   to generate monadic code for Haskell.
  1248 
  1249   \item @{command (HOL) "code_include"} adds arbitrary named content
  1250   (``include'') to generated code.  A ``@{text "-"}'' as last argument
  1251   will remove an already added ``include''.
  1252 
  1253   \item @{command (HOL) "code_modulename"} declares aliasings from one
  1254   module name onto another.
  1255 
  1256   \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
  1257   argument compiles code into the system runtime environment and
  1258   modifies the code generator setup that future invocations of system
  1259   runtime code generation referring to one of the ``@{text
  1260   "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
  1261   entities.  With a ``@{text "file"}'' argument, the corresponding code
  1262   is generated into that specified file without modifying the code
  1263   generator setup.
  1264 
  1265   \end{description}
  1266 
  1267   The other framework generates code from both functional and
  1268   relational programs to SML.  See \cite{isabelle-HOL} for further
  1269   information (this actually covers the new-style theory format as
  1270   well).
  1271 
  1272   \begin{matharray}{rcl}
  1273     @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
  1274     @{command_def (HOL) "code_library"} & : & @{text "theory \<rightarrow> theory"} \\
  1275     @{command_def (HOL) "consts_code"} & : & @{text "theory \<rightarrow> theory"} \\
  1276     @{command_def (HOL) "types_code"} & : & @{text "theory \<rightarrow> theory"} \\  
  1277     @{attribute_def (HOL) code} & : & @{text attribute} \\
  1278   \end{matharray}
  1279 
  1280   \begin{rail}
  1281   ( 'code_module' | 'code_library' ) modespec ? name ? \\
  1282     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
  1283     'contains' ( ( name '=' term ) + | term + )
  1284   ;
  1285 
  1286   modespec: '(' ( name * ) ')'
  1287   ;
  1288 
  1289   'consts_code' (codespec +)
  1290   ;
  1291 
  1292   codespec: const template attachment ?
  1293   ;
  1294 
  1295   'types_code' (tycodespec +)
  1296   ;
  1297 
  1298   tycodespec: name template attachment ?
  1299   ;
  1300 
  1301   const: term
  1302   ;
  1303 
  1304   template: '(' string ')'
  1305   ;
  1306 
  1307   attachment: 'attach' modespec ? verblbrace text verbrbrace
  1308   ;
  1309 
  1310   'code' (name)?
  1311   ;
  1312   \end{rail}
  1313 
  1314 *}
  1315 
  1316 
  1317 section {* Definition by specification \label{sec:hol-specification} *}
  1318 
  1319 text {*
  1320   \begin{matharray}{rcl}
  1321     @{command_def (HOL) "specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
  1322     @{command_def (HOL) "ax_specification"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
  1323   \end{matharray}
  1324 
  1325   \begin{rail}
  1326   ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
  1327   ;
  1328   decl: ((name ':')? term '(' 'overloaded' ')'?)
  1329   \end{rail}
  1330 
  1331   \begin{description}
  1332 
  1333   \item @{command (HOL) "specification"}~@{text "decls \<phi>"} sets up a
  1334   goal stating the existence of terms with the properties specified to
  1335   hold for the constants given in @{text decls}.  After finishing the
  1336   proof, the theory will be augmented with definitions for the given
  1337   constants, as well as with theorems stating the properties for these
  1338   constants.
  1339 
  1340   \item @{command (HOL) "ax_specification"}~@{text "decls \<phi>"} sets up
  1341   a goal stating the existence of terms with the properties specified
  1342   to hold for the constants given in @{text decls}.  After finishing
  1343   the proof, the theory will be augmented with axioms expressing the
  1344   properties given in the first place.
  1345 
  1346   \item @{text decl} declares a constant to be defined by the
  1347   specification given.  The definition for the constant @{text c} is
  1348   bound to the name @{text c_def} unless a theorem name is given in
  1349   the declaration.  Overloaded constants should be declared as such.
  1350 
  1351   \end{description}
  1352 
  1353   Whether to use @{command (HOL) "specification"} or @{command (HOL)
  1354   "ax_specification"} is to some extent a matter of style.  @{command
  1355   (HOL) "specification"} introduces no new axioms, and so by
  1356   construction cannot introduce inconsistencies, whereas @{command
  1357   (HOL) "ax_specification"} does introduce axioms, but only after the
  1358   user has explicitly proven it to be safe.  A practical issue must be
  1359   considered, though: After introducing two constants with the same
  1360   properties using @{command (HOL) "specification"}, one can prove
  1361   that the two constants are, in fact, equal.  If this might be a
  1362   problem, one should use @{command (HOL) "ax_specification"}.
  1363 *}
  1364 
  1365 end