doc-src/IsarRef/Thy/document/HOL_Specific.tex
author bulwahn
Fri Nov 05 08:16:31 2010 +0100 (2010-11-05)
changeset 40364 55a1693affb6
parent 40255 9ffbc25e1606
child 40380 ae4b67af2f37
permissions -rw-r--r--
adding documentation of some quickcheck options
     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       \item[timeout] sets the time limit in seconds.
   986 
   987       \item[default\_type] sets the type(s) generally used to instantiate
   988         type variables.
   989 
   990       \item[report] if set quickcheck reports how many tests fulfilled
   991         the preconditions.
   992 
   993       \item[quiet] if not set quickcheck informs about the current size
   994         for assignment values.
   995 
   996       \item[expect] can be used to check if the user's expectation was met
   997         (no\_expectation, no\_counterexample, or counterexample)
   998 
   999     \end{description}
  1000 
  1001     These option can be given within square brackets.
  1002 
  1003   \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isacharunderscore}params}}}} changes quickcheck
  1004     configuration options persitently.
  1005 
  1006   \end{description}%
  1007 \end{isamarkuptext}%
  1008 \isamarkuptrue%
  1009 %
  1010 \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%
  1011 }
  1012 \isamarkuptrue%
  1013 %
  1014 \begin{isamarkuptext}%
  1015 The following tools of Isabelle/HOL support cases analysis and
  1016   induction in unstructured tactic scripts; see also
  1017   \secref{sec:cases-induct} for proper Isar versions of similar ideas.
  1018 
  1019   \begin{matharray}{rcl}
  1020     \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} \\
  1021     \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} \\
  1022     \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} \\
  1023     \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}} \\
  1024   \end{matharray}
  1025 
  1026   \begin{rail}
  1027     'case_tac' goalspec? term rule?
  1028     ;
  1029     'induct_tac' goalspec? (insts * 'and') rule?
  1030     ;
  1031     'ind_cases' (prop +) ('for' (name +)) ?
  1032     ;
  1033     'inductive_cases' (thmdecl? (prop +) + 'and')
  1034     ;
  1035 
  1036     rule: ('rule' ':' thmref)
  1037     ;
  1038   \end{rail}
  1039 
  1040   \begin{description}
  1041 
  1042   \item \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} admit
  1043   to reason about inductive types.  Rules are selected according to
  1044   the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}}
  1045   attributes, cf.\ \secref{sec:cases-induct}.  The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.
  1046 
  1047   These unstructured tactics feature both goal addressing and dynamic
  1048   instantiation.  Note that named rule cases are \emph{not} provided
  1049   as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof
  1050   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
  1051   statements, only the compact object-logic conclusion of the subgoal
  1052   being addressed.
  1053   
  1054   \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
  1055   forward manner.
  1056 
  1057   While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
  1058   result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level
  1059   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
  1060   be generalized before applying the resulting rule.
  1061 
  1062   \end{description}%
  1063 \end{isamarkuptext}%
  1064 \isamarkuptrue%
  1065 %
  1066 \isamarkupsection{Executable code%
  1067 }
  1068 \isamarkuptrue%
  1069 %
  1070 \begin{isamarkuptext}%
  1071 Isabelle/Pure provides two generic frameworks to support code
  1072   generation from executable specifications.  Isabelle/HOL
  1073   instantiates these mechanisms in a way that is amenable to end-user
  1074   applications.
  1075 
  1076   \medskip One framework generates code from functional programs
  1077   (including overloading using type classes) to SML \cite{SML}, OCaml
  1078   \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
  1079   \cite{scala-overview-tech-report}.
  1080   Conceptually, code generation is split up in three steps:
  1081   \emph{selection} of code theorems, \emph{translation} into an
  1082   abstract executable view and \emph{serialization} to a specific
  1083   \emph{target language}.  Inductive specifications can be executed
  1084   using the predicate compiler which operates within HOL.
  1085   See \cite{isabelle-codegen} for an introduction.
  1086 
  1087   \begin{matharray}{rcl}
  1088     \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}} \\
  1089     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
  1090     \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}} \\
  1091     \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}} \\
  1092     \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}} \\
  1093     \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}}} & : & \isa{attribute} \\
  1094     \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}}} & : & \isa{attribute} \\
  1095     \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}} \\
  1096     \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}} \\
  1097     \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}} \\
  1098     \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}} \\
  1099     \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}} \\
  1100     \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}} \\
  1101     \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}} \\
  1102     \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}} \\
  1103     \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}} \\
  1104     \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}} \\
  1105     \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}} \\
  1106     \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}}
  1107   \end{matharray}
  1108 
  1109   \begin{rail}
  1110      'export_code' ( constexpr + ) \\
  1111        ( ( 'in' target ( 'module_name' string ) ? \\
  1112         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
  1113     ;
  1114 
  1115     const: term
  1116     ;
  1117 
  1118     constexpr: ( const | 'name.*' | '*' )
  1119     ;
  1120 
  1121     typeconstructor: nameref
  1122     ;
  1123 
  1124     class: nameref
  1125     ;
  1126 
  1127     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
  1128     ;
  1129 
  1130     'code' ( 'del' | 'abstype' | 'abstract' ) ?
  1131     ;
  1132 
  1133     'code_abort' ( const + )
  1134     ;
  1135 
  1136     'code_datatype' ( const + )
  1137     ;
  1138 
  1139     'code_inline' ( 'del' ) ?
  1140     ;
  1141 
  1142     'code_post' ( 'del' ) ?
  1143     ;
  1144 
  1145     'code_thms' ( constexpr + ) ?
  1146     ;
  1147 
  1148     'code_deps' ( constexpr + ) ?
  1149     ;
  1150 
  1151     'code_const' (const + 'and') \\
  1152       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1153     ;
  1154 
  1155     'code_type' (typeconstructor + 'and') \\
  1156       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
  1157     ;
  1158 
  1159     'code_class' (class + 'and') \\
  1160       ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
  1161     ;
  1162 
  1163     'code_instance' (( typeconstructor '::' class ) + 'and') \\
  1164       ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
  1165     ;
  1166 
  1167     'code_reserved' target ( string + )
  1168     ;
  1169 
  1170     'code_monad' const const target
  1171     ;
  1172 
  1173     'code_include' target ( string ( string | '-') )
  1174     ;
  1175 
  1176     'code_modulename' target ( ( string string ) + )
  1177     ;
  1178 
  1179     'code_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
  1180       ( 'functions' ( string + ) ) ? ( 'file' string ) ?
  1181     ;
  1182 
  1183     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
  1184     ;
  1185 
  1186   \end{rail}
  1187 
  1188   \begin{description}
  1189 
  1190   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
  1191   of constants in the specified target language(s).  If no
  1192   serialization instruction is given, only abstract code is generated
  1193   internally.
  1194 
  1195   Constants may be specified by giving them literally, referring to
  1196   all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
  1197   available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
  1198 
  1199   By default, for each involved theory one corresponding name space
  1200   module is generated.  Alternativly, a module name may be specified
  1201   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
  1202   placed in this module.
  1203 
  1204   For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
  1205   refers to a single file; for \emph{Haskell}, it refers to a whole
  1206   directory, where code is generated in multiple files reflecting the
  1207   module hierarchy.  Omitting the file specification denotes standard
  1208   output.
  1209 
  1210   Serializers take an optional list of arguments in parentheses.  For
  1211   \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
  1212   explicit module signatures.
  1213   
  1214   For \emph{Haskell} a module name prefix may be given using the
  1215   ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a
  1216   ``\verb|deriving (Read, Show)|'' clause to each appropriate
  1217   datatype declaration.
  1218 
  1219   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
  1220   ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
  1221   Usually packages introducing code equations provide a reasonable
  1222   default setup for selection.  Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
  1223   \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
  1224   code equations on abstract datatype representations respectively.
  1225 
  1226   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
  1227   required to have a definition by means of code equations; if needed
  1228   these are implemented by program abort instead.
  1229 
  1230   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
  1231   for a logical type.
  1232 
  1233   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
  1234   selected code equations and code generator datatypes.
  1235 
  1236   \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with option
  1237   ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are applied as
  1238   rewrite rules to any code equation during preprocessing.
  1239 
  1240   \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
  1241   result of an evaluation.
  1242 
  1243   \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup of the code
  1244   generator preprocessor.
  1245 
  1246   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
  1247   representing the corresponding program containing all given
  1248   constants after preprocessing.
  1249 
  1250   \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
  1251   theorems representing the corresponding program containing all given
  1252   constants after preprocessing.
  1253 
  1254   \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
  1255   with target-specific serializations; omitting a serialization
  1256   deletes an existing serialization.
  1257 
  1258   \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
  1259   constructors with target-specific serializations; omitting a
  1260   serialization deletes an existing serialization.
  1261 
  1262   \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
  1263   with target-specific class names; omitting a serialization deletes
  1264   an existing serialization.  This applies only to \emph{Haskell}.
  1265 
  1266   \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
  1267   constructor / class instance relations as ``already present'' for a
  1268   given target.  Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
  1269   ``already present'' declaration.  This applies only to
  1270   \emph{Haskell}.
  1271 
  1272   \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
  1273   reserved for a given target, preventing it to be shadowed by any
  1274   generated code.
  1275 
  1276   \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
  1277   to generate monadic code for Haskell.
  1278 
  1279   \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
  1280   (``include'') to generated code.  A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
  1281   will remove an already added ``include''.
  1282 
  1283   \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
  1284   module name onto another.
  1285 
  1286   \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} without a ``\isa{{\isachardoublequote}file{\isachardoublequote}}''
  1287   argument compiles code into the system runtime environment and
  1288   modifies the code generator setup that future invocations of system
  1289   runtime code generation referring to one of the ``\isa{{\isachardoublequote}datatypes{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}functions{\isachardoublequote}}'' entities use these precompiled
  1290   entities.  With a ``\isa{{\isachardoublequote}file{\isachardoublequote}}'' argument, the corresponding code
  1291   is generated into that specified file without modifying the code
  1292   generator setup.
  1293 
  1294   \end{description}
  1295 
  1296   The other framework generates code from both functional and
  1297   relational programs to SML.  See \cite{isabelle-HOL} for further
  1298   information (this actually covers the new-style theory format as
  1299   well).
  1300 
  1301   \begin{matharray}{rcl}
  1302     \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}} \\
  1303     \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}} \\
  1304     \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}} \\
  1305     \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}} \\  
  1306     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
  1307   \end{matharray}
  1308 
  1309   \begin{rail}
  1310   ( 'code_module' | 'code_library' ) modespec ? name ? \\
  1311     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
  1312     'contains' ( ( name '=' term ) + | term + )
  1313   ;
  1314 
  1315   modespec: '(' ( name * ) ')'
  1316   ;
  1317 
  1318   'consts_code' (codespec +)
  1319   ;
  1320 
  1321   codespec: const template attachment ?
  1322   ;
  1323 
  1324   'types_code' (tycodespec +)
  1325   ;
  1326 
  1327   tycodespec: name template attachment ?
  1328   ;
  1329 
  1330   const: term
  1331   ;
  1332 
  1333   template: '(' string ')'
  1334   ;
  1335 
  1336   attachment: 'attach' modespec ? verblbrace text verbrbrace
  1337   ;
  1338 
  1339   'code' (name)?
  1340   ;
  1341   \end{rail}%
  1342 \end{isamarkuptext}%
  1343 \isamarkuptrue%
  1344 %
  1345 \isamarkupsection{Definition by specification \label{sec:hol-specification}%
  1346 }
  1347 \isamarkuptrue%
  1348 %
  1349 \begin{isamarkuptext}%
  1350 \begin{matharray}{rcl}
  1351     \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}} \\
  1352     \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}} \\
  1353   \end{matharray}
  1354 
  1355   \begin{rail}
  1356   ('specification' | 'ax_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
  1357   ;
  1358   decl: ((name ':')? term '(' 'overloaded' ')'?)
  1359   \end{rail}
  1360 
  1361   \begin{description}
  1362 
  1363   \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up a
  1364   goal stating the existence of terms with the properties specified to
  1365   hold for the constants given in \isa{decls}.  After finishing the
  1366   proof, the theory will be augmented with definitions for the given
  1367   constants, as well as with theorems stating the properties for these
  1368   constants.
  1369 
  1370   \item \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up
  1371   a goal stating the existence of terms with the properties specified
  1372   to hold for the constants given in \isa{decls}.  After finishing
  1373   the proof, the theory will be augmented with axioms expressing the
  1374   properties given in the first place.
  1375 
  1376   \item \isa{decl} declares a constant to be defined by the
  1377   specification given.  The definition for the constant \isa{c} is
  1378   bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
  1379   the declaration.  Overloaded constants should be declared as such.
  1380 
  1381   \end{description}
  1382 
  1383   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
  1384   construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
  1385   user has explicitly proven it to be safe.  A practical issue must be
  1386   considered, though: After introducing two constants with the same
  1387   properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
  1388   that the two constants are, in fact, equal.  If this might be a
  1389   problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
  1390 \end{isamarkuptext}%
  1391 \isamarkuptrue%
  1392 %
  1393 \isadelimtheory
  1394 %
  1395 \endisadelimtheory
  1396 %
  1397 \isatagtheory
  1398 \isacommand{end}\isamarkupfalse%
  1399 %
  1400 \endisatagtheory
  1401 {\isafoldtheory}%
  1402 %
  1403 \isadelimtheory
  1404 %
  1405 \endisadelimtheory
  1406 \isanewline
  1407 \end{isabellebody}%
  1408 %%% Local Variables:
  1409 %%% mode: latex
  1410 %%% TeX-master: "root"
  1411 %%% End: