doc-src/IsarRef/Thy/document/HOL_Specific.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 40254 6d1ebaa7a4ba
child 40364 55a1693affb6
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     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     ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
   415     ;
   416     equations: (thmdecl? prop + '|')
   417     ;
   418     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
   419     ;
   420     'termination' ( term )?
   421   \end{rail}
   422 
   423   \begin{description}
   424 
   425   \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
   426   functions over datatypes, see also \cite{isabelle-HOL}.
   427 
   428   \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
   429   wellfounded recursion. A detailed description with examples can be
   430   found in \cite{isabelle-function}. The function is specified by a
   431   set of (possibly conditional) recursive equations with arbitrary
   432   pattern matching. The command generates proof obligations for the
   433   completeness and the compatibility of patterns.
   434 
   435   The defined function is considered partial, and the resulting
   436   simplification rules (named \isa{{\isachardoublequote}f{\isachardot}psimps{\isachardoublequote}}) and induction rule
   437   (named \isa{{\isachardoublequote}f{\isachardot}pinduct{\isachardoublequote}}) are guarded by a generated domain
   438   predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
   439   command can then be used to establish that the function is total.
   440 
   441   \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
   442   proof attempts regarding pattern matching and termination.  See
   443   \cite{isabelle-function} for further details.
   444 
   445   \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
   446   termination proof for the previously defined function \isa{f}.  If
   447   this is omitted, the command refers to the most recent function
   448   definition.  After the proof is closed, the recursive equations and
   449   the induction principle is established.
   450 
   451   \end{description}
   452 
   453   Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
   454   command accommodate
   455   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)
   456   refers to a specific induction rule, with parameters named according
   457   to the user-specified equations. Cases are numbered (starting from 1).
   458 
   459   For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
   460   with structural recursion on the datatype the recursion is carried
   461   out.
   462 
   463   The equations provided by these packages may be referred later as
   464   theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)
   465   name of the functions defined.  Individual equations may be named
   466   explicitly as well.
   467 
   468   The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
   469   options.
   470 
   471   \begin{description}
   472 
   473   \item \isa{sequential} enables a preprocessor which disambiguates
   474   overlapping patterns by making them mutually disjoint.  Earlier
   475   equations take precedence over later ones.  This allows to give the
   476   specification in a format very similar to functional programming.
   477   Note that the resulting simplification and induction rules
   478   correspond to the transformed specification, not the one given
   479   originally. This usually means that each equation given by the user
   480   may result in several theorems.  Also note that this automatic
   481   transformation only works for ML-style datatype patterns.
   482 
   483   \item \isa{domintros} enables the automated generation of
   484   introduction rules for the domain predicate. While mostly not
   485   needed, they can be helpful in some proofs about partial functions.
   486 
   487   \item \isa{tailrec} generates the unconstrained recursive
   488   equations even without a termination proof, provided that the
   489   function is tail-recursive. This currently only works
   490 
   491   \item \isa{{\isachardoublequote}default\ d{\isachardoublequote}} allows to specify a default value for a
   492   (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}}
   493   whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}.
   494 
   495   \end{description}%
   496 \end{isamarkuptext}%
   497 \isamarkuptrue%
   498 %
   499 \isamarkupsubsection{Proof methods related to recursive definitions%
   500 }
   501 \isamarkuptrue%
   502 %
   503 \begin{isamarkuptext}%
   504 \begin{matharray}{rcl}
   505     \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
   506     \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
   507     \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
   508     \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}}} & : & \isa{method} \\
   509   \end{matharray}
   510 
   511   \begin{rail}
   512     'relation' term
   513     ;
   514     'lexicographic_order' ( clasimpmod * )
   515     ;
   516     'size_change' ( orders ( clasimpmod * ) )
   517     ;
   518     orders: ( 'max' | 'min' | 'ms' ) *
   519   \end{rail}
   520 
   521   \begin{description}
   522 
   523   \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}} is a specialized method to
   524   solve goals regarding the completeness of pattern matching, as
   525   required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
   526   \cite{isabelle-function}).
   527 
   528   \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
   529   proof using the relation \isa{R}.  The resulting proof state will
   530   contain goals expressing that \isa{R} is wellfounded, and that the
   531   arguments of recursive calls decrease with respect to \isa{R}.
   532   Usually, this method is used as the initial proof step of manual
   533   termination proofs.
   534 
   535   \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}} attempts a fully
   536   automated termination proof by searching for a lexicographic
   537   combination of size measures on the arguments of the function. The
   538   method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
   539   which it uses internally to prove local descents.  The same context
   540   modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see
   541   \secref{sec:clasimp}.
   542 
   543   In case of failure, extensive information is printed, which can help
   544   to analyse the situation (cf.\ \cite{isabelle-function}).
   545 
   546   \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}} also works on termination goals,
   547   using a variation of the size-change principle, together with a
   548   graph decomposition technique (see \cite{krauss_phd} for details).
   549   Three kinds of orders are used internally: \isa{max}, \isa{min},
   550   and \isa{ms} (multiset), which is only available when the theory
   551   \isa{Multiset} is loaded. When no order kinds are given, they are
   552   tried in order. The search for a termination proof uses SAT solving
   553   internally.
   554 
   555  For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
   556 
   557   \end{description}%
   558 \end{isamarkuptext}%
   559 \isamarkuptrue%
   560 %
   561 \isamarkupsubsection{Functions with explicit partiality%
   562 }
   563 \isamarkuptrue%
   564 %
   565 \begin{isamarkuptext}%
   566 \begin{matharray}{rcl}
   567     \indexdef{HOL}{command}{partial\_function}\hypertarget{command.HOL.partial-function}{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isacharunderscore}function}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
   568     \indexdef{HOL}{attribute}{partial\_function\_mono}\hypertarget{attribute.HOL.partial-function-mono}{\hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}}} & : & \isa{attribute} \\
   569   \end{matharray}
   570 
   571   \begin{rail}
   572     'partial_function' target? '(' mode ')' fixes \\ 'where' thmdecl? prop
   573   \end{rail}
   574 
   575   \begin{description}
   576 
   577   \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isacharunderscore}function}}}} defines recursive
   578   functions based on fixpoints in complete partial orders. No
   579   termination proof is required from the user or constructed
   580   internally. Instead, the possibility of non-termination is modelled
   581   explicitly in the result type, which contains an explicit bottom
   582   element.
   583 
   584   Pattern matching and mutual recursion are currently not supported.
   585   Thus, the specification consists of a single function described by a
   586   single recursive equation.
   587 
   588   There are no fixed syntactic restrictions on the body of the
   589   function, but the induced functional must be provably monotonic
   590   wrt.\ the underlying order.  The monotonicitity proof is performed
   591   internally, and the definition is rejected when it fails. The proof
   592   can be influenced by declaring hints using the
   593   \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}} attribute.
   594 
   595   The mandatory \isa{mode} argument specifies the mode of operation
   596   of the command, which directly corresponds to a complete partial
   597   order on the result type. By default, the following modes are
   598   defined: 
   599 
   600   \begin{description}
   601   \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
   602   non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
   603   must also be \isa{None}. This is best achieved through the use of
   604   the monadic operator \isa{{\isachardoublequote}Option{\isachardot}bind{\isachardoublequote}}.
   605   
   606   \item \isa{tailrec} defines functions with an arbitrary result
   607   type and uses the slightly degenerated partial order where \isa{{\isachardoublequote}undefined{\isachardoublequote}} is the bottom element.  Now, monotonicity requires that
   608   if \isa{undefined} is returned by a recursive call, then the
   609   overall result must also be \isa{undefined}. In practice, this is
   610   only satisfied when each recursive call is a tail call, whose result
   611   is directly returned. Thus, this mode of operation allows the
   612   definition of arbitrary tail-recursive functions.
   613   \end{description}
   614 
   615   Experienced users may define new modes by instantiating the locale
   616   \isa{{\isachardoublequote}partial{\isacharunderscore}function{\isacharunderscore}definitions{\isachardoublequote}} appropriately.
   617 
   618   \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isacharunderscore}function{\isacharunderscore}mono}}} declares rules for
   619   use in the internal monononicity proofs of partial function
   620   definitions.
   621 
   622   \end{description}%
   623 \end{isamarkuptext}%
   624 \isamarkuptrue%
   625 %
   626 \isamarkupsubsection{Old-style recursive function definitions (TFL)%
   627 }
   628 \isamarkuptrue%
   629 %
   630 \begin{isamarkuptext}%
   631 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.
   632 
   633   \begin{matharray}{rcl}
   634     \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isacharparenright}{\isachardoublequote}} \\
   635     \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}} \\
   636   \end{matharray}
   637 
   638   \begin{rail}
   639     'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
   640     ;
   641     recdeftc thmdecl? tc
   642     ;
   643     hints: '(' 'hints' ( recdefmod * ) ')'
   644     ;
   645     recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   646     ;
   647     tc: nameref ('(' nat ')')?
   648     ;
   649   \end{rail}
   650 
   651   \begin{description}
   652   
   653   \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
   654   recursive functions (using the TFL package), see also
   655   \cite{isabelle-HOL}.  The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells
   656   TFL to recover from failed proof attempts, returning unfinished
   657   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
   658   automated proof process of TFL.  Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
   659   declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
   660   context of the Simplifier (cf.\ \secref{sec:simplifier}) and
   661   Classical reasoner (cf.\ \secref{sec:classical}).
   662   
   663   \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} recommences the
   664   proof for leftover termination condition number \isa{i} (default
   665   1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
   666   constant \isa{c}.
   667   
   668   Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
   669   its internal proofs without manual intervention.
   670 
   671   \end{description}
   672 
   673   \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
   674   globally, using the following attributes.
   675 
   676   \begin{matharray}{rcl}
   677     \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isa{attribute} \\
   678     \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isa{attribute} \\
   679     \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isa{attribute} \\
   680   \end{matharray}
   681 
   682   \begin{rail}
   683     ('recdef_simp' | 'recdef_cong' | 'recdef_wf') (() | 'add' | 'del')
   684     ;
   685   \end{rail}%
   686 \end{isamarkuptext}%
   687 \isamarkuptrue%
   688 %
   689 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
   690 }
   691 \isamarkuptrue%
   692 %
   693 \begin{isamarkuptext}%
   694 An \textbf{inductive definition} specifies the least predicate (or
   695   set) \isa{R} closed under given rules: applying a rule to elements
   696   of \isa{R} yields a result within \isa{R}.  For example, a
   697   structural operational semantics is an inductive definition of an
   698   evaluation relation.
   699 
   700   Dually, a \textbf{coinductive definition} specifies the greatest
   701   predicate~/ set \isa{R} that is consistent with given rules: every
   702   element of \isa{R} can be seen as arising by applying a rule to
   703   elements of \isa{R}.  An important example is using bisimulation
   704   relations to formalise equivalence of processes and infinite data
   705   structures.
   706 
   707   \medskip The HOL package is related to the ZF one, which is
   708   described in a separate paper,\footnote{It appeared in CADE
   709   \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
   710   which you should refer to in case of difficulties.  The package is
   711   simpler than that of ZF thanks to implicit type-checking in HOL.
   712   The types of the (co)inductive predicates (or sets) determine the
   713   domain of the fixedpoint definition, and the package does not have
   714   to use inference rules for type-checking.
   715 
   716   \begin{matharray}{rcl}
   717     \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}} \\
   718     \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}} \\
   719     \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}} \\
   720     \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}} \\
   721     \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
   722   \end{matharray}
   723 
   724   \begin{rail}
   725     ('inductive' | 'inductive_set' | 'coinductive' | 'coinductive_set') target? fixes ('for' fixes)? \\
   726     ('where' clauses)? ('monos' thmrefs)?
   727     ;
   728     clauses: (thmdecl? prop + '|')
   729     ;
   730     'mono' (() | 'add' | 'del')
   731     ;
   732   \end{rail}
   733 
   734   \begin{description}
   735 
   736   \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the
   737   introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part.  The
   738   optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
   739   (co)inductive predicates that remain fixed throughout the
   740   definition.  The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains
   741   \emph{monotonicity theorems}, which are required for each operator
   742   applied to a recursive set in the introduction rules.  There
   743   \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
   744   for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
   745 
   746   \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,
   747   allowing the definition of (co)inductive sets.
   748 
   749   \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules.  These
   750   rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
   751 
   752   \end{description}%
   753 \end{isamarkuptext}%
   754 \isamarkuptrue%
   755 %
   756 \isamarkupsubsection{Derived rules%
   757 }
   758 \isamarkuptrue%
   759 %
   760 \begin{isamarkuptext}%
   761 Each (co)inductive definition \isa{R} adds definitions to the
   762   theory and also proves some theorems:
   763 
   764   \begin{description}
   765 
   766   \item \isa{R{\isachardot}intros} is the list of introduction rules as proven
   767   theorems, for the recursive predicates (or sets).  The rules are
   768   also available individually, using the names given them in the
   769   theory file;
   770 
   771   \item \isa{R{\isachardot}cases} is the case analysis (or elimination) rule;
   772 
   773   \item \isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct} is the (co)induction
   774   rule.
   775 
   776   \end{description}
   777 
   778   When several predicates \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardoublequote}} are
   779   defined simultaneously, the list of introduction rules is called
   780   \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}intros{\isachardoublequote}}, the case analysis rules are
   781   called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isachardot}cases{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardot}cases{\isachardoublequote}}, and the list
   782   of mutual induction rules is called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}inducts{\isachardoublequote}}.%
   783 \end{isamarkuptext}%
   784 \isamarkuptrue%
   785 %
   786 \isamarkupsubsection{Monotonicity theorems%
   787 }
   788 \isamarkuptrue%
   789 %
   790 \begin{isamarkuptext}%
   791 Each theory contains a default set of theorems that are used in
   792   monotonicity proofs.  New rules can be added to this set via the
   793   \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute.  The HOL theory \isa{Inductive}
   794   shows how this is done.  In general, the following monotonicity
   795   theorems may be added:
   796 
   797   \begin{itemize}
   798 
   799   \item Theorems of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, for proving
   800   monotonicity of inductive definitions whose introduction rules have
   801   premises involving terms such as \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}}.
   802 
   803   \item Monotonicity theorems for logical operators, which are of the
   804   general form \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isachardoublequote}}.  For example, in
   805   the case of the operator \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, the corresponding theorem is
   806   \[
   807   \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}}}
   808   \]
   809 
   810   \item De Morgan style equations for reasoning about the ``polarity''
   811   of expressions, e.g.
   812   \[
   813   \isa{{\isachardoublequote}{\isasymnot}\ {\isasymnot}\ P\ {\isasymlongleftrightarrow}\ P{\isachardoublequote}} \qquad\qquad
   814   \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ {\isasymnot}\ Q{\isachardoublequote}}
   815   \]
   816 
   817   \item Equations for reducing complex operators to more primitive
   818   ones whose monotonicity can easily be proved, e.g.
   819   \[
   820   \isa{{\isachardoublequote}{\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ Q{\isachardoublequote}} \qquad\qquad
   821   \isa{{\isachardoublequote}Ball\ A\ P\ {\isasymequiv}\ {\isasymforall}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}}
   822   \]
   823 
   824   \end{itemize}
   825 
   826   %FIXME: Example of an inductive definition%
   827 \end{isamarkuptext}%
   828 \isamarkuptrue%
   829 %
   830 \isamarkupsection{Arithmetic proof support%
   831 }
   832 \isamarkuptrue%
   833 %
   834 \begin{isamarkuptext}%
   835 \begin{matharray}{rcl}
   836     \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\
   837     \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\
   838     \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isa{attribute} \\
   839   \end{matharray}
   840 
   841   The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
   842   (on types \isa{nat}, \isa{int}, \isa{real}).  Any current
   843   facts are inserted into the goal before running the procedure.
   844 
   845   The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are
   846   always supplied to the arithmetic provers implicitly.
   847 
   848   The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
   849   rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked.
   850 
   851   Note that a simpler (but faster) arithmetic prover is
   852   already invoked by the Simplifier.%
   853 \end{isamarkuptext}%
   854 \isamarkuptrue%
   855 %
   856 \isamarkupsection{Intuitionistic proof search%
   857 }
   858 \isamarkuptrue%
   859 %
   860 \begin{isamarkuptext}%
   861 \begin{matharray}{rcl}
   862     \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
   863   \end{matharray}
   864 
   865   \begin{rail}
   866     'iprover' ( rulemod * )
   867     ;
   868   \end{rail}
   869 
   870   The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
   871   search, depending on specifically declared rules from the context,
   872   or given as explicit arguments.  Chained facts are inserted into the
   873   goal before commencing proof search.
   874 
   875   Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
   876   \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
   877   ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
   878   applied aggressively (without considering back-tracking later).
   879   Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the
   880   single-step \hyperlink{method.rule}{\mbox{\isa{rule}}} method still observes these).  An
   881   explicit weight annotation may be given as well; otherwise the
   882   number of rule premises will be taken into account here.%
   883 \end{isamarkuptext}%
   884 \isamarkuptrue%
   885 %
   886 \isamarkupsection{Coherent Logic%
   887 }
   888 \isamarkuptrue%
   889 %
   890 \begin{isamarkuptext}%
   891 \begin{matharray}{rcl}
   892     \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
   893   \end{matharray}
   894 
   895   \begin{rail}
   896     'coherent' thmrefs?
   897     ;
   898   \end{rail}
   899 
   900   The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
   901   \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
   902   applications in confluence theory, lattice theory and projective
   903   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
   904   examples.%
   905 \end{isamarkuptext}%
   906 \isamarkuptrue%
   907 %
   908 \isamarkupsection{Checking and refuting propositions%
   909 }
   910 \isamarkuptrue%
   911 %
   912 \begin{isamarkuptext}%
   913 Identifying incorrect propositions usually involves evaluation of
   914   particular assignments and systematic counter example search.  This
   915   is supported by the following commands.
   916 
   917   \begin{matharray}{rcl}
   918     \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}} \\
   919     \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}} \\
   920     \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}}
   921   \end{matharray}
   922 
   923   \begin{rail}
   924     'value' ( ( '[' name ']' ) ? ) modes? term
   925     ;
   926 
   927     'quickcheck' ( ( '[' args ']' ) ? ) nat?
   928     ;
   929 
   930     'quickcheck_params' ( ( '[' args ']' ) ? )
   931     ;
   932 
   933     modes: '(' (name + ) ')'
   934     ;
   935 
   936     args: ( name '=' value + ',' )
   937     ;
   938   \end{rail}
   939 
   940   \begin{description}
   941 
   942   \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a
   943     term; optionally \isa{modes} can be specified, which are
   944     appended to the current print mode (see also \cite{isabelle-ref}).
   945     Internally, the evaluation is performed by registered evaluators,
   946     which are invoked sequentially until a result is returned.
   947     Alternatively a specific evaluator can be selected using square
   948     brackets; typical evaluators use the current set of code equations
   949     to normalize and include \isa{simp} for fully symbolic evaluation
   950     using the simplifier, \isa{nbe} for \emph{normalization by evaluation}
   951     and \emph{code} for code generation in SML.
   952 
   953   \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
   954     counter examples using a series of arbitrary assignments for its
   955     free variables; by default the first subgoal is tested, an other
   956     can be selected explicitly using an optional goal index.
   957     A number of configuration options are supported for
   958     \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
   959 
   960     \begin{description}
   961 
   962     \item[\isa{size}] specifies the maximum size of the search space
   963     for assignment values.
   964 
   965     \item[\isa{iterations}] sets how many sets of assignments are
   966     generated for each particular size.
   967 
   968     \item[\isa{no{\isacharunderscore}assms}] specifies whether assumptions in
   969     structured proofs should be ignored.
   970 
   971     \item[\isa{timeout}] sets the time limit in seconds.
   972 
   973     \item[\isa{default{\isacharunderscore}type}] sets the type(s) generally used to
   974     instantiate type variables.
   975 
   976     \item[\isa{report}] if set quickcheck reports how many tests
   977     fulfilled the preconditions.
   978 
   979     \item[\isa{quiet}] if not set quickcheck informs about the
   980     current size for assignment values.
   981 
   982     \item[\isa{expect}] can be used to check if the user's
   983     expectation was met (\isa{no{\isacharunderscore}expectation}, \isa{no{\isacharunderscore}counterexample}, or \isa{counterexample}).
   984 
   985     \end{description}
   986 
   987     These option can be given within square brackets.
   988 
   989   \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}} changes quickcheck
   990     configuration options persitently.
   991 
   992   \end{description}%
   993 \end{isamarkuptext}%
   994 \isamarkuptrue%
   995 %
   996 \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%
   997 }
   998 \isamarkuptrue%
   999 %
  1000 \begin{isamarkuptext}%
  1001 The following tools of Isabelle/HOL support cases analysis and
  1002   induction in unstructured tactic scripts; see also
  1003   \secref{sec:cases-induct} for proper Isar versions of similar ideas.
  1004 
  1005   \begin{matharray}{rcl}
  1006     \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} \\
  1007     \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} \\
  1008     \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} \\
  1009     \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}} \\
  1010   \end{matharray}
  1011 
  1012   \begin{rail}
  1013     'case_tac' goalspec? term rule?
  1014     ;
  1015     'induct_tac' goalspec? (insts * 'and') rule?
  1016     ;
  1017     'ind_cases' (prop +) ('for' (name +)) ?
  1018     ;
  1019     'inductive_cases' (thmdecl? (prop +) + 'and')
  1020     ;
  1021 
  1022     rule: ('rule' ':' thmref)
  1023     ;
  1024   \end{rail}
  1025 
  1026   \begin{description}
  1027 
  1028   \item \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} admit
  1029   to reason about inductive types.  Rules are selected according to
  1030   the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}}
  1031   attributes, cf.\ \secref{sec:cases-induct}.  The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.
  1032 
  1033   These unstructured tactics feature both goal addressing and dynamic
  1034   instantiation.  Note that named rule cases are \emph{not} provided
  1035   as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof
  1036   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
  1037   statements, only the compact object-logic conclusion of the subgoal
  1038   being addressed.
  1039   
  1040   \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
  1041   forward manner.
  1042 
  1043   While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
  1044   result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level
  1045   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
  1046   be generalized before applying the resulting rule.
  1047 
  1048   \end{description}%
  1049 \end{isamarkuptext}%
  1050 \isamarkuptrue%
  1051 %
  1052 \isamarkupsection{Executable code%
  1053 }
  1054 \isamarkuptrue%
  1055 %
  1056 \begin{isamarkuptext}%
  1057 Isabelle/Pure provides two generic frameworks to support code
  1058   generation from executable specifications.  Isabelle/HOL
  1059   instantiates these mechanisms in a way that is amenable to end-user
  1060   applications.
  1061 
  1062   \medskip One framework generates code from functional programs
  1063   (including overloading using type classes) to SML \cite{SML}, OCaml
  1064   \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
  1065   \cite{scala-overview-tech-report}.
  1066   Conceptually, code generation is split up in three steps:
  1067   \emph{selection} of code theorems, \emph{translation} into an
  1068   abstract executable view and \emph{serialization} to a specific
  1069   \emph{target language}.  Inductive specifications can be executed
  1070   using the predicate compiler which operates within HOL.
  1071   See \cite{isabelle-codegen} for an introduction.
  1072 
  1073   \begin{matharray}{rcl}
  1074     \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}} \\
  1075     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
  1076     \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}} \\
  1077     \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}} \\
  1078     \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}} \\
  1079     \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}}} & : & \isa{attribute} \\
  1080     \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}}} & : & \isa{attribute} \\
  1081     \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}} \\
  1082     \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}} \\
  1083     \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}} \\
  1084     \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}} \\
  1085     \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}} \\
  1086     \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}} \\
  1087     \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}} \\
  1088     \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}} \\
  1089     \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}} \\
  1090     \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}} \\
  1091     \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}} \\
  1092     \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
  1093   \end{matharray}
  1094 
  1095   \begin{rail}
  1096      'export_code' ( constexpr + ) \\
  1097        ( ( 'in' target ( 'module_name' string ) ? \\
  1098         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
  1099     ;
  1100 
  1101     const: term
  1102     ;
  1103 
  1104     constexpr: ( const | 'name.*' | '*' )
  1105     ;
  1106 
  1107     typeconstructor: nameref
  1108     ;
  1109 
  1110     class: nameref
  1111     ;
  1112 
  1113     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
  1114     ;
  1115 
  1116     'code' ( 'del' | 'abstype' | 'abstract' ) ?
  1117     ;
  1118 
  1119     'code_abort' ( const + )
  1120     ;
  1121 
  1122     'code_datatype' ( const + )
  1123     ;
  1124 
  1125     'code_inline' ( 'del' ) ?
  1126     ;
  1127 
  1128     'code_post' ( 'del' ) ?
  1129     ;
  1130 
  1131     'code_thms' ( constexpr + ) ?
  1132     ;
  1133 
  1134     'code_deps' ( constexpr + ) ?
  1135     ;
  1136 
  1137     'code_const' (const + 'and') \\
  1138       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1139     ;
  1140 
  1141     'code_type' (typeconstructor + 'and') \\
  1142       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1143     ;
  1144 
  1145     'code_class' (class + 'and') \\
  1146       ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
  1147     ;
  1148 
  1149     'code_instance' (( typeconstructor '::' class ) + 'and') \\
  1150       ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
  1151     ;
  1152 
  1153     'code_reserved' target ( string + )
  1154     ;
  1155 
  1156     'code_monad' const const target
  1157     ;
  1158 
  1159     'code_include' target ( string ( string | '-') )
  1160     ;
  1161 
  1162     'code_modulename' target ( ( string string ) + )
  1163     ;
  1164 
  1165     'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
  1166       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
  1167     ;
  1168 
  1169     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
  1170     ;
  1171 
  1172   \end{rail}
  1173 
  1174   \begin{description}
  1175 
  1176   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
  1177   of constants in the specified target language(s).  If no
  1178   serialization instruction is given, only abstract code is generated
  1179   internally.
  1180 
  1181   Constants may be specified by giving them literally, referring to
  1182   all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
  1183   available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
  1184 
  1185   By default, for each involved theory one corresponding name space
  1186   module is generated.  Alternativly, a module name may be specified
  1187   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
  1188   placed in this module.
  1189 
  1190   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
  1191   refers to a single file; for \emph{Haskell}, it refers to a whole
  1192   directory, where code is generated in multiple files reflecting the
  1193   module hierarchy.  Omitting the file specification denotes standard
  1194   output.
  1195 
  1196   Serializers take an optional list of arguments in parentheses.  For
  1197   \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
  1198   explicit module signatures.
  1199   
  1200   For \emph{Haskell} a module name prefix may be given using the
  1201   ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a
  1202   ``\verb|deriving (Read, Show)|'' clause to each appropriate
  1203   datatype declaration.
  1204 
  1205   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
  1206   ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
  1207   Usually packages introducing code equations provide a reasonable
  1208   default setup for selection.  Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
  1209   \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
  1210   code equations on abstract datatype representations respectively.
  1211 
  1212   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
  1213   required to have a definition by means of code equations; if needed
  1214   these are implemented by program abort instead.
  1215 
  1216   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
  1217   for a logical type.
  1218 
  1219   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
  1220   selected code equations and code generator datatypes.
  1221 
  1222   \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with option
  1223   ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are applied as
  1224   rewrite rules to any code equation during preprocessing.
  1225 
  1226   \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are applied as rewrite rules to any
  1227   result of an evaluation.
  1228 
  1229   \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup of the code
  1230   generator preprocessor.
  1231 
  1232   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
  1233   representing the corresponding program containing all given
  1234   constants after preprocessing.
  1235 
  1236   \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
  1237   theorems representing the corresponding program containing all given
  1238   constants after preprocessing.
  1239 
  1240   \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
  1241   with target-specific serializations; omitting a serialization
  1242   deletes an existing serialization.
  1243 
  1244   \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
  1245   constructors with target-specific serializations; omitting a
  1246   serialization deletes an existing serialization.
  1247 
  1248   \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
  1249   with target-specific class names; omitting a serialization deletes
  1250   an existing serialization.  This applies only to \emph{Haskell}.
  1251 
  1252   \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
  1253   constructor / class instance relations as ``already present'' for a
  1254   given target.  Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
  1255   ``already present'' declaration.  This applies only to
  1256   \emph{Haskell}.
  1257 
  1258   \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
  1259   reserved for a given target, preventing it to be shadowed by any
  1260   generated code.
  1261 
  1262   \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
  1263   to generate monadic code for Haskell.
  1264 
  1265   \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
  1266   (``include'') to generated code.  A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
  1267   will remove an already added ``include''.
  1268 
  1269   \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
  1270   module name onto another.
  1271 
  1272   \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} without a ``\isa{{\isachardoublequote}file{\isachardoublequote}}''
  1273   argument compiles code into the system runtime environment and
  1274   modifies the code generator setup that future invocations of system
  1275   runtime code generation referring to one of the ``\isa{{\isachardoublequote}datatypes{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}functions{\isachardoublequote}}'' entities use these precompiled
  1276   entities.  With a ``\isa{{\isachardoublequote}file{\isachardoublequote}}'' argument, the corresponding code
  1277   is generated into that specified file without modifying the code
  1278   generator setup.
  1279 
  1280   \end{description}
  1281 
  1282   The other framework generates code from both functional and
  1283   relational programs to SML.  See \cite{isabelle-HOL} for further
  1284   information (this actually covers the new-style theory format as
  1285   well).
  1286 
  1287   \begin{matharray}{rcl}
  1288     \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}} \\
  1289     \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}} \\
  1290     \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}} \\
  1291     \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}} \\  
  1292     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
  1293   \end{matharray}
  1294 
  1295   \begin{rail}
  1296   ( 'code_module' | 'code_library' ) modespec ? name ? \\
  1297     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
  1298     'contains' ( ( name '=' term ) + | term + )
  1299   ;
  1300 
  1301   modespec: '(' ( name * ) ')'
  1302   ;
  1303 
  1304   'consts_code' (codespec +)
  1305   ;
  1306 
  1307   codespec: const template attachment ?
  1308   ;
  1309 
  1310   'types_code' (tycodespec +)
  1311   ;
  1312 
  1313   tycodespec: name template attachment ?
  1314   ;
  1315 
  1316   const: term
  1317   ;
  1318 
  1319   template: '(' string ')'
  1320   ;
  1321 
  1322   attachment: 'attach' modespec ? verblbrace text verbrbrace
  1323   ;
  1324 
  1325   'code' (name)?
  1326   ;
  1327   \end{rail}%
  1328 \end{isamarkuptext}%
  1329 \isamarkuptrue%
  1330 %
  1331 \isamarkupsection{Definition by specification \label{sec:hol-specification}%
  1332 }
  1333 \isamarkuptrue%
  1334 %
  1335 \begin{isamarkuptext}%
  1336 \begin{matharray}{rcl}
  1337     \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}} \\
  1338     \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}} \\
  1339   \end{matharray}
  1340 
  1341   \begin{rail}
  1342   ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
  1343   ;
  1344   decl: ((name ':')? term '(' 'overloaded' ')'?)
  1345   \end{rail}
  1346 
  1347   \begin{description}
  1348 
  1349   \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up a
  1350   goal stating the existence of terms with the properties specified to
  1351   hold for the constants given in \isa{decls}.  After finishing the
  1352   proof, the theory will be augmented with definitions for the given
  1353   constants, as well as with theorems stating the properties for these
  1354   constants.
  1355 
  1356   \item \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up
  1357   a goal stating the existence of terms with the properties specified
  1358   to hold for the constants given in \isa{decls}.  After finishing
  1359   the proof, the theory will be augmented with axioms expressing the
  1360   properties given in the first place.
  1361 
  1362   \item \isa{decl} declares a constant to be defined by the
  1363   specification given.  The definition for the constant \isa{c} is
  1364   bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
  1365   the declaration.  Overloaded constants should be declared as such.
  1366 
  1367   \end{description}
  1368 
  1369   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
  1370   construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
  1371   user has explicitly proven it to be safe.  A practical issue must be
  1372   considered, though: After introducing two constants with the same
  1373   properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
  1374   that the two constants are, in fact, equal.  If this might be a
  1375   problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
  1376 \end{isamarkuptext}%
  1377 \isamarkuptrue%
  1378 %
  1379 \isadelimtheory
  1380 %
  1381 \endisadelimtheory
  1382 %
  1383 \isatagtheory
  1384 \isacommand{end}\isamarkupfalse%
  1385 %
  1386 \endisatagtheory
  1387 {\isafoldtheory}%
  1388 %
  1389 \isadelimtheory
  1390 %
  1391 \endisadelimtheory
  1392 \isanewline
  1393 \end{isabellebody}%
  1394 %%% Local Variables:
  1395 %%% mode: latex
  1396 %%% TeX-master: "root"
  1397 %%% End: