doc-src/IsarRef/Thy/document/HOL_Specific.tex
 author wenzelm Wed Oct 15 21:06:15 2008 +0200 (2008-10-15) changeset 28603 b40800eef8a7 parent 28562 4e74209f113e child 28687 150a8a1eae1a permissions -rw-r--r--
     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{HOL{\isacharunderscore}Specific}%

     4 %

     5 \isadelimtheory

     6 \isanewline

     7 \isanewline

     8 %

     9 \endisadelimtheory

    10 %

    11 \isatagtheory

    12 \isacommand{theory}\isamarkupfalse%

    13 \ HOL{\isacharunderscore}Specific\isanewline

    14 \isakeyword{imports}\ Main\isanewline

    15 \isakeyword{begin}%

    16 \endisatagtheory

    17 {\isafoldtheory}%

    18 %

    19 \isadelimtheory

    20 %

    21 \endisadelimtheory

    22 %

    23 \isamarkupchapter{Isabelle/HOL \label{ch:hol}%

    24 }

    25 \isamarkuptrue%

    26 %

    27 \isamarkupsection{Primitive types \label{sec:hol-typedef}%

    28 }

    29 \isamarkuptrue%

    30 %

    31 \begin{isamarkuptext}%

    32 \begin{matharray}{rcl}

    33     \indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isartrans{theory}{theory} \\

    34     \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isartrans{theory}{proof(prove)} \\

    35   \end{matharray}

    36

    37   \begin{rail}

    38     'typedecl' typespec infix?

    39     ;

    40     'typedef' altname? abstype '=' repset

    41     ;

    42

    43     altname: '(' (name | 'open' | 'open' name) ')'

    44     ;

    45     abstype: typespec infix?

    46     ;

    47     repset: term ('morphisms' name name)?

    48     ;

    49   \end{rail}

    50

    51   \begin{descr}

    52

    53   \item [\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}] is similar to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of

    54   Isabelle/Pure (see \secref{sec:types-pure}), but also declares type

    55   arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an

    56   actual HOL type constructor.   %FIXME check, update

    57

    58   \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}}] sets up a goal stating non-emptiness of the set \isa{A}.

    59   After finishing the proof, the theory will be augmented by a

    60   Gordon/HOL-style type definition, which establishes a bijection

    61   between the representing set \isa{A} and the new type \isa{t}.

    62

    63   Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base

    64   name may be given in parentheses).  The injection from type to set

    65   is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be

    66   changed via an explicit \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 may be specified in parentheses; the default is

    79   to use \isa{t} as indicated before.  The \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''

    80   declaration suppresses a separate constant definition for the

    81   representing set.

    82

    83   \end{descr}

    84

    85   Note that raw type declarations are rarely used in practice; the

    86   main application is with experimental (or even axiomatic!) theory

    87   fragments.  Instead of primitive HOL type definitions, user-level

    88   theories usually refer to higher-level packages such as \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}} (see \secref{sec:hol-record}) or \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} (see \secref{sec:hol-datatype}).%

    89 \end{isamarkuptext}%

    90 \isamarkuptrue%

    91 %

    92 \isamarkupsection{Adhoc tuples%

    93 }

    94 \isamarkuptrue%

    95 %

    96 \begin{isamarkuptext}%

    97 \begin{matharray}{rcl}

    98     \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\

    99   \end{matharray}

   100

   101   \begin{rail}

   102     'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))

   103     ;

   104   \end{rail}

   105

   106   \begin{descr}

   107

   108   \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

   109   low-level tuple types into canonical form as specified by the

   110   arguments given; the \isa{i}-th collection of arguments refers to

   111   occurrences in premise \isa{i} of the rule.  The \isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all} arguments in function

   112   applications to be represented canonically according to their tuple

   113   type structure.

   114

   115   Note that these operations tend to invent funny names for new local

   116   parameters to be introduced.

   117

   118   \end{descr}%

   119 \end{isamarkuptext}%

   120 \isamarkuptrue%

   121 %

   122 \isamarkupsection{Records \label{sec:hol-record}%

   123 }

   124 \isamarkuptrue%

   125 %

   126 \begin{isamarkuptext}%

   127 In principle, records merely generalize the concept of tuples, where

   128   components may be addressed by labels instead of just position.  The

   129   logical infrastructure of records in Isabelle/HOL is slightly more

   130   advanced, though, supporting truly extensible record schemes.  This

   131   admits operations that are polymorphic with respect to record

   132   extension, yielding object-oriented'' effects like (single)

   133   inheritance.  See also \cite{NaraschewskiW-TPHOLs98} for more

   134   details on object-oriented verification and record subtyping in HOL.%

   135 \end{isamarkuptext}%

   136 \isamarkuptrue%

   137 %

   138 \isamarkupsubsection{Basic concepts%

   139 }

   140 \isamarkuptrue%

   141 %

   142 \begin{isamarkuptext}%

   143 Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records

   144   at the level of terms and types.  The notation is as follows:

   145

   146   \begin{center}

   147   \begin{tabular}{l|l|l}

   148     & record terms & record types \\ \hline

   149     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}} \\

   150     schematic & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} &

   151       \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ M{\isasymrparr}{\isachardoublequote}} \\

   152   \end{tabular}

   153   \end{center}

   154

   155   \noindent The ASCII representation of \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} is \isa{{\isachardoublequote}{\isacharparenleft}{\isacharbar}\ x\ {\isacharequal}\ a\ {\isacharbar}{\isacharparenright}{\isachardoublequote}}.

   156

   157   A fixed record \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} has field \isa{x} of value

   158   \isa{a} and field \isa{y} of value \isa{b}.  The corresponding

   159   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}}

   160   and \isa{{\isachardoublequote}b\ {\isacharcolon}{\isacharcolon}\ B{\isachardoublequote}}.

   161

   162   A record scheme like \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} contains fields

   163   \isa{x} and \isa{y} as before, but also possibly further fields

   164   as indicated by the \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' notation (which is actually part

   165   of the syntax).  The improper field \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' of a record

   166   scheme is called the \emph{more part}.  Logically it is just a free

   167   variable, which is occasionally referred to as row variable'' in

   168   the literature.  The more part of a record scheme may be

   169   instantiated by zero or more further components.  For example, the

   170   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.

   171   Fixed records are special instances of record schemes, where

   172   \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' is properly terminated by the \isa{{\isachardoublequote}{\isacharparenleft}{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ unit{\isachardoublequote}}

   173   element.  In fact, \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} is just an abbreviation

   174   for \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}{\isachardoublequote}}.

   175

   176   \medskip Two key observations make extensible records in a simply

   177   typed language like HOL work out:

   178

   179   \begin{enumerate}

   180

   181   \item the more part is internalized, as a free term or type

   182   variable,

   183

   184   \item field names are externalized, they cannot be accessed within

   185   the logic as first-class values.

   186

   187   \end{enumerate}

   188

   189   \medskip In Isabelle/HOL record types have to be defined explicitly,

   190   fixing their field names and types, and their (optional) parent

   191   record.  Afterwards, records may be formed using above syntax, while

   192   obeying the canonical order of fields as given by their declaration.

   193   The record package provides several standard operations like

   194   selectors and updates.  The common setup for various generic proof

   195   tools enable succinct reasoning patterns.  See also the Isabelle/HOL

   196   tutorial \cite{isabelle-hol-book} for further instructions on using

   197   records in practice.%

   198 \end{isamarkuptext}%

   199 \isamarkuptrue%

   200 %

   201 \isamarkupsubsection{Record specifications%

   202 }

   203 \isamarkuptrue%

   204 %

   205 \begin{isamarkuptext}%

   206 \begin{matharray}{rcl}

   207     \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isartrans{theory}{theory} \\

   208   \end{matharray}

   209

   210   \begin{rail}

   211     'record' typespec '=' (type '+')? (constdecl +)

   212     ;

   213   \end{rail}

   214

   215   \begin{descr}

   216

   217   \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

   218   extensible record type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}},

   219   derived from the optional parent record \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} by adding new

   220   field components \isa{{\isachardoublequote}c\isactrlsub i\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} etc.

   221

   222   The type variables of \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i{\isachardoublequote}} need to be

   223   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

   224   least one new field \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} has to be specified.

   225   Basically, field names need to belong to a unique record.  This is

   226   not a real restriction in practice, since fields are qualified by

   227   the record name internally.

   228

   229   The parent record specification \isa{{\isasymtau}} is optional; if omitted

   230   \isa{t} becomes a root record.  The hierarchy of all records

   231   declared within a theory context forms a forest structure, i.e.\ a

   232   set of trees starting with a root record each.  There is no way to

   233   merge multiple parent records!

   234

   235   For convenience, \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is made a

   236   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

   237   \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}}.

   238

   239   \end{descr}%

   240 \end{isamarkuptext}%

   241 \isamarkuptrue%

   242 %

   243 \isamarkupsubsection{Record operations%

   244 }

   245 \isamarkuptrue%

   246 %

   247 \begin{isamarkuptext}%

   248 Any record definition of the form presented above produces certain

   249   standard operations.  Selectors and updates are provided for any

   250   field, including the improper one \isa{more}''.  There are also

   251   cumulative record constructor functions.  To simplify the

   252   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}}.

   253

   254   \medskip \textbf{Selectors} and \textbf{updates} are available for

   255   any field (including \isa{more}''):

   256

   257   \begin{matharray}{lll}

   258     \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}} \\

   259     \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}} \\

   260   \end{matharray}

   261

   262   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

   263   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

   264   because of postfix notation the order of fields shown here is

   265   reverse than in the actual term.  Since repeated updates are just

   266   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.

   267   Thus commutativity of independent updates can be proven within the

   268   logic for any two fields, but not as a general theorem.

   269

   270   \medskip The \textbf{make} operation provides a cumulative record

   271   constructor function:

   272

   273   \begin{matharray}{lll}

   274     \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}} \\

   275   \end{matharray}

   276

   277   \medskip We now reconsider the case of non-root records, which are

   278   derived of some parent.  In general, the latter may depend on

   279   another parent as well, resulting in a list of \emph{ancestor

   280   records}.  Appending the lists of fields of all ancestors results in

   281   a certain field prefix.  The record package automatically takes care

   282   of this by lifting operations over this context of ancestor fields.

   283   Assuming that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} has ancestor

   284   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}},

   285   the above record operations will get the following types:

   286

   287   \medskip

   288   \begin{tabular}{lll}

   289     \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}} \\

   290     \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}} \\

   291     \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}} \\

   292   \end{tabular}

   293   \medskip

   294

   295   \noindent Some further operations address the extension aspect of a

   296   derived record scheme specifically: \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} produces a

   297   record fragment consisting of exactly the new fields introduced here

   298   (the result may serve as a more part elsewhere); \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}

   299   takes a fixed record and adds a given more part; \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} restricts a record scheme to a fixed record.

   300

   301   \medskip

   302   \begin{tabular}{lll}

   303     \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}} \\

   304     \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}} \\

   305     \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}} \\

   306   \end{tabular}

   307   \medskip

   308

   309   \noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide

   310   for root records.%

   311 \end{isamarkuptext}%

   312 \isamarkuptrue%

   313 %

   314 \isamarkupsubsection{Derived rules and proof tools%

   315 }

   316 \isamarkuptrue%

   317 %

   318 \begin{isamarkuptext}%

   319 The record package proves several results internally, declaring

   320   these facts to appropriate proof tools.  This enables users to

   321   reason about record structures quite conveniently.  Assume that

   322   \isa{t} is a record type as specified above.

   323

   324   \begin{enumerate}

   325

   326   \item Standard conversions for selectors or updates applied to

   327   record constructor terms are made part of the default Simplifier

   328   context; thus proofs by reduction of basic operations merely require

   329   the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments.  These rules

   330   are available as \isa{{\isachardoublequote}t{\isachardot}simps{\isachardoublequote}}, too.

   331

   332   \item Selectors applied to updated records are automatically reduced

   333   by an internal simplification procedure, which is also part of the

   334   standard Simplifier setup.

   335

   336   \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

   337   Reasoner as \hyperlink{attribute.iff}{\mbox{\isa{iff}}} rules.  These rules are available as

   338   \isa{{\isachardoublequote}t{\isachardot}iffs{\isachardoublequote}}.

   339

   340   \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,

   341   and as the basic rule context as \hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''.

   342   The rule is called \isa{{\isachardoublequote}t{\isachardot}equality{\isachardoublequote}}.

   343

   344   \item Representations of arbitrary record expressions as canonical

   345   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,

   346   \secref{sec:cases-induct}).  Several variations are available, for

   347   fixed records, record schemes, more parts etc.

   348

   349   The generic proof methods are sufficiently smart to pick the most

   350   sensible rule according to the type of the indicated record

   351   expression: users just need to apply something like \isa{{\isachardoublequote}{\isacharparenleft}cases\ r{\isacharparenright}{\isachardoublequote}}'' to a certain proof problem.

   352

   353   \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}

   354   treated automatically, but usually need to be expanded by hand,

   355   using the collective fact \isa{{\isachardoublequote}t{\isachardot}defs{\isachardoublequote}}.

   356

   357   \end{enumerate}%

   358 \end{isamarkuptext}%

   359 \isamarkuptrue%

   360 %

   361 \isamarkupsection{Datatypes \label{sec:hol-datatype}%

   362 }

   363 \isamarkuptrue%

   364 %

   365 \begin{isamarkuptext}%

   366 \begin{matharray}{rcl}

   367     \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isartrans{theory}{theory} \\

   368   \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{proof} \\

   369   \end{matharray}

   370

   371   \begin{rail}

   372     'datatype' (dtspec + 'and')

   373     ;

   374     'rep\_datatype' ('(' (name +) ')')? (term +)

   375     ;

   376

   377     dtspec: parname? typespec infix? '=' (cons + '|')

   378     ;

   379     cons: name (type *) mixfix?

   380   \end{rail}

   381

   382   \begin{descr}

   383

   384   \item [\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}] defines inductive datatypes in

   385   HOL.

   386

   387   \item [\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}] represents existing types as

   388   inductive ones, generating the standard infrastructure of derived

   389   concepts (primitive recursion etc.).

   390

   391   \end{descr}

   392

   393   The induction and exhaustion theorems generated provide case names

   394   according to the constructors involved, while parameters are named

   395   after the types (see also \secref{sec:cases-induct}).

   396

   397   See \cite{isabelle-HOL} for more details on datatypes, but beware of

   398   the old-style theory syntax being used there!  Apart from proper

   399   proof methods for case-analysis and induction, there are also

   400   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

   401   to refer directly to the internal structure of subgoals (including

   402   internally bound parameters).%

   403 \end{isamarkuptext}%

   404 \isamarkuptrue%

   405 %

   406 \isamarkupsection{Recursive functions \label{sec:recursion}%

   407 }

   408 \isamarkuptrue%

   409 %

   410 \begin{isamarkuptext}%

   411 \begin{matharray}{rcl}

   412     \indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isarkeep{local{\dsh}theory} \\

   413     \indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isarkeep{local{\dsh}theory} \\

   414     \indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

   415     \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\

   416   \end{matharray}

   417

   418   \begin{rail}

   419     'primrec' target? fixes 'where' equations

   420     ;

   421     equations: (thmdecl? prop + '|')

   422     ;

   423     ('fun' | 'function') target? functionopts? fixes 'where' clauses

   424     ;

   425     clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')

   426     ;

   427     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'

   428     ;

   429     'termination' ( term )?

   430   \end{rail}

   431

   432   \begin{descr}

   433

   434   \item [\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}] defines primitive recursive

   435   functions over datatypes, see also \cite{isabelle-HOL}.

   436

   437   \item [\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}] defines functions by general

   438   wellfounded recursion. A detailed description with examples can be

   439   found in \cite{isabelle-function}. The function is specified by a

   440   set of (possibly conditional) recursive equations with arbitrary

   441   pattern matching. The command generates proof obligations for the

   442   completeness and the compatibility of patterns.

   443

   444   The defined function is considered partial, and the resulting

   445   simplification rules (named \isa{{\isachardoublequote}f{\isachardot}psimps{\isachardoublequote}}) and induction rule

   446   (named \isa{{\isachardoublequote}f{\isachardot}pinduct{\isachardoublequote}}) are guarded by a generated domain

   447   predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}

   448   command can then be used to establish that the function is total.

   449

   450   \item [\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}] is a shorthand notation for

   451   \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by

   452   automated proof attempts regarding pattern matching and termination.

   453   See \cite{isabelle-function} for further details.

   454

   455   \item [\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f}] commences a

   456   termination proof for the previously defined function \isa{f}.  If

   457   this is omitted, the command refers to the most recent function

   458   definition.  After the proof is closed, the recursive equations and

   459   the induction principle is established.

   460

   461   \end{descr}

   462

   463   %FIXME check

   464

   465   Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}

   466   command accommodate

   467   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)

   468   refers to a specific induction rule, with parameters named according

   469   to the user-specified equations.

   470   For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides

   471   with structural recursion on the datatype the recursion is carried

   472   out.

   473   Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of

   474   \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).

   475

   476   The equations provided by these packages may be referred later as

   477   theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)

   478   name of the functions defined.  Individual equations may be named

   479   explicitly as well.

   480

   481   The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following

   482   options.

   483

   484   \begin{descr}

   485

   486   \item [\isa{sequential}] enables a preprocessor which

   487   disambiguates overlapping patterns by making them mutually disjoint.

   488   Earlier equations take precedence over later ones.  This allows to

   489   give the specification in a format very similar to functional

   490   programming.  Note that the resulting simplification and induction

   491   rules correspond to the transformed specification, not the one given

   492   originally. This usually means that each equation given by the user

   493   may result in several theroems.  Also note that this automatic

   494   transformation only works for ML-style datatype patterns.

   495

   496   \item [\isa{domintros}] enables the automated generation of

   497   introduction rules for the domain predicate. While mostly not

   498   needed, they can be helpful in some proofs about partial functions.

   499

   500   \item [\isa{tailrec}] generates the unconstrained recursive

   501   equations even without a termination proof, provided that the

   502   function is tail-recursive. This currently only works

   503

   504   \item [\isa{{\isachardoublequote}default\ d{\isachardoublequote}}] allows to specify a default value for a

   505   (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}}

   506   whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}.

   507

   508   \end{descr}%

   509 \end{isamarkuptext}%

   510 \isamarkuptrue%

   511 %

   512 \isamarkupsubsection{Proof methods related to recursive definitions%

   513 }

   514 \isamarkuptrue%

   515 %

   516 \begin{isamarkuptext}%

   517 \begin{matharray}{rcl}

   518     \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isarmeth \\

   519     \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isarmeth \\

   520     \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isarmeth \\

   521   \end{matharray}

   522

   523   \begin{rail}

   524     'relation' term

   525     ;

   526     'lexicographic\_order' (clasimpmod *)

   527     ;

   528   \end{rail}

   529

   530   \begin{descr}

   531

   532   \item [\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}] is a specialized method to

   533   solve goals regarding the completeness of pattern matching, as

   534   required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\

   535   \cite{isabelle-function}).

   536

   537   \item [\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R}] introduces a termination

   538   proof using the relation \isa{R}.  The resulting proof state will

   539   contain goals expressing that \isa{R} is wellfounded, and that the

   540   arguments of recursive calls decrease with respect to \isa{R}.

   541   Usually, this method is used as the initial proof step of manual

   542   termination proofs.

   543

   544   \item [\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}] attempts a fully

   545   automated termination proof by searching for a lexicographic

   546   combination of size measures on the arguments of the function. The

   547   method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,

   548   which it uses internally to prove local descents.  The same context

   549   modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see

   550   \secref{sec:clasimp}.

   551

   552   In case of failure, extensive information is printed, which can help

   553   to analyse the situation (cf.\ \cite{isabelle-function}).

   554

   555   \end{descr}%

   556 \end{isamarkuptext}%

   557 \isamarkuptrue%

   558 %

   559 \isamarkupsubsection{Old-style recursive function definitions (TFL)%

   560 }

   561 \isamarkuptrue%

   562 %

   563 \begin{isamarkuptext}%

   564 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.

   565

   566   \begin{matharray}{rcl}

   567     \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isartrans{theory}{theory} \\

   568     \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}} & : & \isartrans{theory}{proof(prove)} \\

   569   \end{matharray}

   570

   571   \begin{rail}

   572     'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?

   573     ;

   574     recdeftc thmdecl? tc

   575     ;

   576     hints: '(' 'hints' (recdefmod *) ')'

   577     ;

   578     recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod

   579     ;

   580     tc: nameref ('(' nat ')')?

   581     ;

   582   \end{rail}

   583

   584   \begin{descr}

   585

   586   \item [\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}] defines general well-founded

   587   recursive functions (using the TFL package), see also

   588   \cite{isabelle-HOL}.  The \isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells

   589   TFL to recover from failed proof attempts, returning unfinished

   590   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

   591   automated proof process of TFL.  Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}

   592   declarations (cf.\ \secref{sec:clasimp}) may be given to tune the

   593   context of the Simplifier (cf.\ \secref{sec:simplifier}) and

   594   Classical reasoner (cf.\ \secref{sec:classical}).

   595

   596   \item [\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the

   597   proof for leftover termination condition number \isa{i} (default

   598   1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of

   599   constant \isa{c}.

   600

   601   Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish

   602   its internal proofs without manual intervention.

   603

   604   \end{descr}

   605

   606   \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared

   607   globally, using the following attributes.

   608

   609   \begin{matharray}{rcl}

   610     \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isaratt \\

   611     \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isaratt \\

   612     \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isaratt \\

   613   \end{matharray}

   614

   615   \begin{rail}

   616     ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')

   617     ;

   618   \end{rail}%

   619 \end{isamarkuptext}%

   620 \isamarkuptrue%

   621 %

   622 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%

   623 }

   624 \isamarkuptrue%

   625 %

   626 \begin{isamarkuptext}%

   627 An \textbf{inductive definition} specifies the least predicate (or

   628   set) \isa{R} closed under given rules: applying a rule to elements

   629   of \isa{R} yields a result within \isa{R}.  For example, a

   630   structural operational semantics is an inductive definition of an

   631   evaluation relation.

   632

   633   Dually, a \textbf{coinductive definition} specifies the greatest

   634   predicate~/ set \isa{R} that is consistent with given rules: every

   635   element of \isa{R} can be seen as arising by applying a rule to

   636   elements of \isa{R}.  An important example is using bisimulation

   637   relations to formalise equivalence of processes and infinite data

   638   structures.

   639

   640   \medskip The HOL package is related to the ZF one, which is

   641   described in a separate paper,\footnote{It appeared in CADE

   642   \cite{paulson-CADE}; a longer version is distributed with Isabelle.}

   643   which you should refer to in case of difficulties.  The package is

   644   simpler than that of ZF thanks to implicit type-checking in HOL.

   645   The types of the (co)inductive predicates (or sets) determine the

   646   domain of the fixedpoint definition, and the package does not have

   647   to use inference rules for type-checking.

   648

   649   \begin{matharray}{rcl}

   650     \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isarkeep{local{\dsh}theory} \\

   651     \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\

   652     \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isarkeep{local{\dsh}theory} \\

   653     \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}} & : & \isarkeep{local{\dsh}theory} \\

   654     \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isaratt \\

   655   \end{matharray}

   656

   657   \begin{rail}

   658     ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\

   659     ('where' clauses)? ('monos' thmrefs)?

   660     ;

   661     clauses: (thmdecl? prop + '|')

   662     ;

   663     'mono' (() | 'add' | 'del')

   664     ;

   665   \end{rail}

   666

   667   \begin{descr}

   668

   669   \item [\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}] define (co)inductive predicates from the

   670   introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part.  The

   671   optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the

   672   (co)inductive predicates that remain fixed throughout the

   673   definition.  The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains

   674   \emph{monotonicity theorems}, which are required for each operator

   675   applied to a recursive set in the introduction rules.  There

   676   \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},

   677   for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!

   678

   679   \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,

   680   allowing the definition of (co)inductive sets.

   681

   682   \item [\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}] declares monotonicity rules.  These

   683   rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.

   684

   685   \end{descr}%

   686 \end{isamarkuptext}%

   687 \isamarkuptrue%

   688 %

   689 \isamarkupsubsection{Derived rules%

   690 }

   691 \isamarkuptrue%

   692 %

   693 \begin{isamarkuptext}%

   694 Each (co)inductive definition \isa{R} adds definitions to the

   695   theory and also proves some theorems:

   696

   697   \begin{description}

   698

   699   \item [\isa{R{\isachardot}intros}] is the list of introduction rules as proven

   700   theorems, for the recursive predicates (or sets).  The rules are

   701   also available individually, using the names given them in the

   702   theory file;

   703

   704   \item [\isa{R{\isachardot}cases}] is the case analysis (or elimination) rule;

   705

   706   \item [\isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct}] is the (co)induction

   707   rule.

   708

   709   \end{description}

   710

   711   When several predicates \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardoublequote}} are

   712   defined simultaneously, the list of introduction rules is called

   713   \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}intros{\isachardoublequote}}, the case analysis rules are

   714   called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isachardot}cases{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardot}cases{\isachardoublequote}}, and the list

   715   of mutual induction rules is called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}inducts{\isachardoublequote}}.%

   716 \end{isamarkuptext}%

   717 \isamarkuptrue%

   718 %

   719 \isamarkupsubsection{Monotonicity theorems%

   720 }

   721 \isamarkuptrue%

   722 %

   723 \begin{isamarkuptext}%

   724 Each theory contains a default set of theorems that are used in

   725   monotonicity proofs.  New rules can be added to this set via the

   726   \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute.  The HOL theory \isa{Inductive}

   727   shows how this is done.  In general, the following monotonicity

   728   theorems may be added:

   729

   730   \begin{itemize}

   731

   732   \item Theorems of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, for proving

   733   monotonicity of inductive definitions whose introduction rules have

   734   premises involving terms such as \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}}.

   735

   736   \item Monotonicity theorems for logical operators, which are of the

   737   general form \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isachardoublequote}}.  For example, in

   738   the case of the operator \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, the corresponding theorem is

   739   $  740 \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}}}   741$

   742

   743   \item De Morgan style equations for reasoning about the polarity''

   744   of expressions, e.g.

   745   $  746 \isa{{\isachardoublequote}{\isasymnot}\ {\isasymnot}\ P\ {\isasymlongleftrightarrow}\ P{\isachardoublequote}} \qquad\qquad   747 \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ {\isasymnot}\ Q{\isachardoublequote}}   748$

   749

   750   \item Equations for reducing complex operators to more primitive

   751   ones whose monotonicity can easily be proved, e.g.

   752   $  753 \isa{{\isachardoublequote}{\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ Q{\isachardoublequote}} \qquad\qquad   754 \isa{{\isachardoublequote}Ball\ A\ P\ {\isasymequiv}\ {\isasymforall}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}}   755$

   756

   757   \end{itemize}

   758

   759   %FIXME: Example of an inductive definition%

   760 \end{isamarkuptext}%

   761 \isamarkuptrue%

   762 %

   763 \isamarkupsection{Arithmetic proof support%

   764 }

   765 \isamarkuptrue%

   766 %

   767 \begin{isamarkuptext}%

   768 \begin{matharray}{rcl}

   769     \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isarmeth \\

   770     \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isaratt \\

   771   \end{matharray}

   772

   773   The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems

   774   (on types \isa{nat}, \isa{int}, \isa{real}).  Any current

   775   facts are inserted into the goal before running the procedure.

   776

   777   The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split

   778   rules to be expanded before the arithmetic procedure is invoked.

   779

   780   Note that a simpler (but faster) version of arithmetic reasoning is

   781   already performed by the Simplifier.%

   782 \end{isamarkuptext}%

   783 \isamarkuptrue%

   784 %

   785 \isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%

   786 }

   787 \isamarkuptrue%

   788 %

   789 \begin{isamarkuptext}%

   790 Isabelle/HOL includes a generic \emph{ATP manager} that allows

   791   external automated reasoning tools to crunch a pending goal.

   792   Supported provers include E\footnote{\url{http://www.eprover.org}},

   793   SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire.

   794   There is also a wrapper to invoke provers remotely via the

   795   SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}}

   796   web service.

   797

   798   The problem passed to external provers consists of the goal together

   799   with a smart selection of lemmas from the current theory context.

   800   The result of a successful proof search is some source text that

   801   usually reconstructs the proof within Isabelle, without requiring

   802   external provers again.  The Metis

   803   prover\footnote{\url{http://www.gilith.com/software/metis/}} that is

   804   integrated into Isabelle/HOL is being used here.

   805

   806   In this mode of operation, heavy means of automated reasoning are

   807   used as a strong relevance filter, while the main proof checking

   808   works via explicit inferences going through the Isabelle kernel.

   809   Moreover, rechecking Isabelle proof texts with already specified

   810   auxiliary facts is much faster than performing fully automated

   811   search over and over again.

   812

   813   \begin{matharray}{rcl}

   814     \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\

   815     \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\

   816     \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\

   817     \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\

   818     \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isarmeth \\

   819   \end{matharray}

   820

   821   \begin{rail}

   822   'sledgehammer' (nameref *)

   823   ;

   824

   825   'metis' thmrefs

   826   ;

   827   \end{rail}

   828

   829   \begin{descr}

   830

   831   \item [\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}] invokes the specified automated theorem provers on

   832   the first subgoal.  Provers are run in parallel, the first

   833   successful result is displayed, and the other attempts are

   834   terminated.

   835

   836   Provers are defined in the theory context, see also \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}.  If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as

   837   ATP provers'' preference by the user interface.

   838

   839   There are additional preferences for timeout (default: 60 seconds),

   840   and the maximum number of independent prover processes (default: 5);

   841   excessive provers are automatically terminated.

   842

   843   \item [\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}] prints the list of automated

   844   theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}

   845   command.

   846

   847   \item [\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}] prints information about presently

   848   running provers, including elapsed runtime, and the remaining time

   849   until timeout.

   850

   851   \item [\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}] terminates all presently running

   852   provers.

   853

   854   \item [\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}}] invokes the Metis

   855   prover with the given facts.  Metis is an automated proof tool of

   856   medium strength, but is fully integrated into Isabelle/HOL, with

   857   explicit inferences going through the kernel.  Thus its results are

   858   guaranteed to be correct by construction''.

   859

   860   Note that all facts used with Metis need to be specified as explicit

   861   arguments.  There are no rule declarations as for other Isabelle

   862   provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.

   863

   864   \end{descr}%

   865 \end{isamarkuptext}%

   866 \isamarkuptrue%

   867 %

   868 \isamarkupsection{Unstructured cases analysis and induction \label{sec:hol-induct-tac}%

   869 }

   870 \isamarkuptrue%

   871 %

   872 \begin{isamarkuptext}%

   873 The following tools of Isabelle/HOL support cases analysis and

   874   induction in unstructured tactic scripts; see also

   875   \secref{sec:cases-induct} for proper Isar versions of similar ideas.

   876

   877   \begin{matharray}{rcl}

   878     \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}} & : & \isarmeth \\

   879     \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}} & : & \isarmeth \\

   880     \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}} & : & \isarmeth \\

   881     \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}} & : & \isartrans{theory}{theory} \\

   882   \end{matharray}

   883

   884   \begin{rail}

   885     'case\_tac' goalspec? term rule?

   886     ;

   887     'induct\_tac' goalspec? (insts * 'and') rule?

   888     ;

   889     'ind\_cases' (prop +) ('for' (name +)) ?

   890     ;

   891     'inductive\_cases' (thmdecl? (prop +) + 'and')

   892     ;

   893

   894     rule: ('rule' ':' thmref)

   895     ;

   896   \end{rail}

   897

   898   \begin{descr}

   899

   900   \item [\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}]

   901   admit to reason about inductive types.  Rules are selected according

   902   to the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}} attributes, cf.\ \secref{sec:cases-induct}.  The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.

   903

   904   These unstructured tactics feature both goal addressing and dynamic

   905   instantiation.  Note that named rule cases are \emph{not} provided

   906   as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof

   907   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

   908   statements, only the compact object-logic conclusion of the subgoal

   909   being addressed.

   910

   911   \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

   912   forward manner.

   913

   914   While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the

   915   result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level

   916   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

   917   be generalized before applying the resulting rule.

   918

   919   \end{descr}%

   920 \end{isamarkuptext}%

   921 \isamarkuptrue%

   922 %

   923 \isamarkupsection{Executable code%

   924 }

   925 \isamarkuptrue%

   926 %

   927 \begin{isamarkuptext}%

   928 Isabelle/Pure provides two generic frameworks to support code

   929   generation from executable specifications.  Isabelle/HOL

   930   instantiates these mechanisms in a way that is amenable to end-user

   931   applications.

   932

   933   One framework generates code from both functional and relational

   934   programs to SML.  See \cite{isabelle-HOL} for further information

   935   (this actually covers the new-style theory format as well).

   936

   937   \begin{matharray}{rcl}

   938     \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\

   939     \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isartrans{theory}{theory} \\

   940     \indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isartrans{theory}{theory} \\

   941     \indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\

   942     \indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isartrans{theory}{theory} \\

   943     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\

   944   \end{matharray}

   945

   946   \begin{rail}

   947   'value' term

   948   ;

   949

   950   ( 'code\_module' | 'code\_library' ) modespec ? name ? \\

   951     ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\

   952     'contains' ( ( name '=' term ) + | term + )

   953   ;

   954

   955   modespec: '(' ( name * ) ')'

   956   ;

   957

   958   'consts\_code' (codespec +)

   959   ;

   960

   961   codespec: const template attachment ?

   962   ;

   963

   964   'types\_code' (tycodespec +)

   965   ;

   966

   967   tycodespec: name template attachment ?

   968   ;

   969

   970   const: term

   971   ;

   972

   973   template: '(' string ')'

   974   ;

   975

   976   attachment: 'attach' modespec ? verblbrace text verbrbrace

   977   ;

   978

   979   'code' (name)?

   980   ;

   981   \end{rail}

   982

   983   \begin{descr}

   984

   985   \item [\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t}] evaluates and prints a

   986   term using the code generator.

   987

   988   \end{descr}

   989

   990   \medskip The other framework generates code from functional programs

   991   (including overloading using type classes) to SML \cite{SML}, OCaml

   992   \cite{OCaml} and Haskell \cite{haskell-revised-report}.

   993   Conceptually, code generation is split up in three steps:

   994   \emph{selection} of code theorems, \emph{translation} into an

   995   abstract executable view and \emph{serialization} to a specific

   996   \emph{target language}.  See \cite{isabelle-codegen} for an

   997   introduction on how to use it.

   998

   999   \begin{matharray}{rcl}

  1000     \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}} & : & \isarkeep{theory~|~proof} \\

  1001     \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}} & : & \isarkeep{theory~|~proof} \\

  1002     \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}} & : & \isarkeep{theory~|~proof} \\

  1003     \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isartrans{theory}{theory} \\

  1004     \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isartrans{theory}{theory} \\

  1005     \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isartrans{theory}{theory} \\

  1006     \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isartrans{theory}{theory} \\

  1007     \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isartrans{theory}{theory} \\

  1008     \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isartrans{theory}{theory} \\

  1009     \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isartrans{theory}{theory} \\

  1010     \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isartrans{theory}{theory} \\

  1011     \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isartrans{theory}{theory} \\

  1012     \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isartrans{theory}{theory} \\

  1013     \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}} & : & \isarkeep{theory~|~proof} \\

  1014     \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isaratt \\

  1015   \end{matharray}

  1016

  1017   \begin{rail}

  1018     'export\_code' ( constexpr + ) ? \\

  1019       ( ( 'in' target ( 'module\_name' string ) ? \\

  1020         ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?

  1021     ;

  1022

  1023     'code\_thms' ( constexpr + ) ?

  1024     ;

  1025

  1026     'code\_deps' ( constexpr + ) ?

  1027     ;

  1028

  1029     const: term

  1030     ;

  1031

  1032     constexpr: ( const | 'name.*' | '*' )

  1033     ;

  1034

  1035     typeconstructor: nameref

  1036     ;

  1037

  1038     class: nameref

  1039     ;

  1040

  1041     target: 'OCaml' | 'SML' | 'Haskell'

  1042     ;

  1043

  1044     'code\_datatype' const +

  1045     ;

  1046

  1047     'code\_const' (const + 'and') \\

  1048       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )

  1049     ;

  1050

  1051     'code\_type' (typeconstructor + 'and') \\

  1052       ( ( '(' target ( syntax ? + 'and' ) ')' ) + )

  1053     ;

  1054

  1055     'code\_class' (class + 'and') \\

  1056       ( ( '(' target \\

  1057         ( ( string ('where' \\

  1058           ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )

  1059     ;

  1060

  1061     'code\_instance' (( typeconstructor '::' class ) + 'and') \\

  1062       ( ( '(' target ( '-' ? + 'and' ) ')' ) + )

  1063     ;

  1064

  1065     'code\_monad' const const target

  1066     ;

  1067

  1068     'code\_reserved' target ( string + )

  1069     ;

  1070

  1071     'code\_include' target ( string ( string | '-') )

  1072     ;

  1073

  1074     'code\_modulename' target ( ( string string ) + )

  1075     ;

  1076

  1077     'code\_abort' ( const + )

  1078     ;

  1079

  1080     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string

  1081     ;

  1082

  1083     'code' ( 'inline' ) ? ( 'del' ) ?

  1084     ;

  1085   \end{rail}

  1086

  1087   \begin{descr}

  1088

  1089   \item [\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}] is the canonical interface

  1090   for generating and serializing code: for a given list of constants,

  1091   code is generated for the specified target languages.  Abstract code

  1092   is cached incrementally.  If no constant is given, the currently

  1093   cached code is serialized.  If no serialization instruction is

  1094   given, only abstract code is cached.

  1095

  1096   Constants may be specified by giving them literally, referring to

  1097   all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently

  1098   available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.

  1099

  1100   By default, for each involved theory one corresponding name space

  1101   module is generated.  Alternativly, a module name may be specified

  1102   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is

  1103   placed in this module.

  1104

  1105   For \emph{SML} and \emph{OCaml}, the file specification refers to a

  1106   single file; for \emph{Haskell}, it refers to a whole directory,

  1107   where code is generated in multiple files reflecting the module

  1108   hierarchy.  The file specification \isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard

  1109   output.  For \emph{SML}, omitting the file specification compiles

  1110   code internally in the context of the current ML session.

  1111

  1112   Serializers take an optional list of arguments in parentheses.  For

  1113   \emph{Haskell} a module name prefix may be given using the \isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; \isa{string{\isacharunderscore}classes}'' adds a \verb|deriving (Read, Show)|'' clause to each appropriate datatype

  1114   declaration.

  1115

  1116   \item [\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}] prints a list of theorems

  1117   representing the corresponding program containing all given

  1118   constants; if no constants are given, the currently cached code

  1119   theorems are printed.

  1120

  1121   \item [\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}] visualizes dependencies of

  1122   theorems representing the corresponding program containing all given

  1123   constants; if no constants are given, the currently cached code

  1124   theorems are visualized.

  1125

  1126   \item [\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}] specifies a constructor set

  1127   for a logical type.

  1128

  1129   \item [\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}] associates a list of constants

  1130   with target-specific serializations; omitting a serialization

  1131   deletes an existing serialization.

  1132

  1133   \item [\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}] associates a list of type

  1134   constructors with target-specific serializations; omitting a

  1135   serialization deletes an existing serialization.

  1136

  1137   \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes

  1138   with target-specific class names; in addition, constants associated

  1139   with this class may be given target-specific names used for instance

  1140   declarations; omitting a serialization deletes an existing

  1141   serialization.  This applies only to \emph{Haskell}.

  1142

  1143   \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type

  1144   constructor / class instance relations as already present'' for a

  1145   given target.  Omitting a \isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing

  1146   already present'' declaration.  This applies only to

  1147   \emph{Haskell}.

  1148

  1149   \item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary

  1150   mechanism to generate monadic code for Haskell.

  1151

  1152   \item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as

  1153   reserved for a given target, preventing it to be shadowed by any

  1154   generated code.

  1155

  1156   \item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content

  1157   (include'') to generated code.  A \isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument

  1158   will remove an already added include''.

  1159

  1160   \item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from

  1161   one module name onto another.

  1162

  1163   \item [\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}] declares constants which

  1164   are not required to have a definition by means of defining equations;

  1165   if needed these are implemented by program abort instead.

  1166

  1167   \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or

  1168   with option \isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for

  1169   code generation.  Usually packages introducing defining equations

  1170   provide a reasonable default setup for selection.

  1171

  1172   \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with

  1173   option \isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are

  1174   applied as rewrite rules to any defining equation during

  1175   preprocessing.

  1176

  1177   \item [\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}] gives an overview on

  1178   selected defining equations, code generator datatypes and

  1179   preprocessor setup.

  1180

  1181   \end{descr}%

  1182 \end{isamarkuptext}%

  1183 \isamarkuptrue%

  1184 %

  1185 \isamarkupsection{Definition by specification \label{sec:hol-specification}%

  1186 }

  1187 \isamarkuptrue%

  1188 %

  1189 \begin{isamarkuptext}%

  1190 \begin{matharray}{rcl}

  1191     \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\

  1192     \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\

  1193   \end{matharray}

  1194

  1195   \begin{rail}

  1196   ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)

  1197   ;

  1198   decl: ((name ':')? term '(' 'overloaded' ')'?)

  1199   \end{rail}

  1200

  1201   \begin{descr}

  1202

  1203   \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a

  1204   goal stating the existence of terms with the properties specified to

  1205   hold for the constants given in \isa{decls}.  After finishing the

  1206   proof, the theory will be augmented with definitions for the given

  1207   constants, as well as with theorems stating the properties for these

  1208   constants.

  1209

  1210   \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets

  1211   up a goal stating the existence of terms with the properties

  1212   specified to hold for the constants given in \isa{decls}.  After

  1213   finishing the proof, the theory will be augmented with axioms

  1214   expressing the properties given in the first place.

  1215

  1216   \item [\isa{decl}] declares a constant to be defined by the

  1217   specification given.  The definition for the constant \isa{c} is

  1218   bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in

  1219   the declaration.  Overloaded constants should be declared as such.

  1220

  1221   \end{descr}

  1222

  1223   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

  1224   construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the

  1225   user has explicitly proven it to be safe.  A practical issue must be

  1226   considered, though: After introducing two constants with the same

  1227   properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove

  1228   that the two constants are, in fact, equal.  If this might be a

  1229   problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%

  1230 \end{isamarkuptext}%

  1231 \isamarkuptrue%

  1232 %

  1233 \isadelimtheory

  1234 %

  1235 \endisadelimtheory

  1236 %

  1237 \isatagtheory

  1238 \isacommand{end}\isamarkupfalse%

  1239 %

  1240 \endisatagtheory

  1241 {\isafoldtheory}%

  1242 %

  1243 \isadelimtheory

  1244 %

  1245 \endisadelimtheory

  1246 \isanewline

  1247 \end{isabellebody}%

  1248 %%% Local Variables:

  1249 %%% mode: latex

  1250 %%% TeX-master: "root"

  1251 %%% End: