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