3 \def\isabellecontext{HOL{\isacharunderscore}Specific}%
12 \isacommand{theory}\isamarkupfalse%
13 \ HOL{\isacharunderscore}Specific\isanewline
14 \isakeyword{imports}\ Main\isanewline
23 \isamarkupchapter{Isabelle/HOL \label{ch:hol}%
27 \isamarkupsection{Primitive types \label{sec:hol-typedef}%
31 \begin{isamarkuptext}%
32 \begin{matharray}{rcl}
33 \indexdef{HOL}{command}{typedecl}\mbox{\isa{\isacommand{typedecl}}} & : & \isartrans{theory}{theory} \\
34 \indexdef{HOL}{command}{typedef}\mbox{\isa{\isacommand{typedef}}} & : & \isartrans{theory}{proof(prove)} \\
38 'typedecl' typespec infix?
40 'typedef' altname? abstype '=' repset
43 altname: '(' (name | 'open' | 'open' name) ')'
45 abstype: typespec infix?
47 repset: term ('morphisms' name name)?
53 \item [\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 \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
58 \item [\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}.
63 Technically, \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 \mbox{\isa{\isakeyword{morphisms}}} declaration).
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 \mbox{\isa{simp}} or \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 \mbox{\isa{cases}} and \mbox{\isa{induct}} methods.
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
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 \mbox{\isa{\isacommand{record}}} (see \secref{sec:hol-record}) or \mbox{\isa{\isacommand{datatype}}} (see \secref{sec:hol-datatype}).%
92 \isamarkupsection{Adhoc tuples%
96 \begin{isamarkuptext}%
97 \begin{matharray}{rcl}
98 \mbox{\isa{split{\isacharunderscore}format}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isaratt \\
102 'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
108 \item [\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
115 Note that these operations tend to invent funny names for new local
116 parameters to be introduced.
122 \isamarkupsection{Records \label{sec:hol-record}%
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.%
138 \isamarkupsubsection{Basic concepts%
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:
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}} \\
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}}.
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}}.
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}}.
176 \medskip Two key observations make extensible records in a simply
177 typed language like HOL work out:
181 \item the more part is internalized, as a free term or type
184 \item field names are externalized, they cannot be accessed within
185 the logic as first-class values.
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.%
201 \isamarkupsubsection{Record specifications%
205 \begin{isamarkuptext}%
206 \begin{matharray}{rcl}
207 \indexdef{HOL}{command}{record}\mbox{\isa{\isacommand{record}}} & : & \isartrans{theory}{theory} \\
211 'record' typespec '=' (type '+')? (constdecl +)
217 \item [\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.
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.
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!
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}}.
243 \isamarkupsubsection{Record operations%
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}}.
254 \medskip \textbf{Selectors} and \textbf{updates} are available for
255 any field (including ``\isa{more}''):
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}} \\
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.
270 \medskip The \textbf{make} operation provides a cumulative record
271 constructor function:
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}} \\
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:
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}} \\
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.
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}} \\
309 \noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide
314 \isamarkupsubsection{Derived rules and proof tools%
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.
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 \mbox{\isa{simp}} method without further arguments. These rules
330 are available as \isa{{\isachardoublequote}t{\isachardot}simps{\isachardoublequote}}, too.
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.
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 \mbox{\isa{iff}} rules. These rules are available as
338 \isa{{\isachardoublequote}t{\isachardot}iffs{\isachardoublequote}}.
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 ``\mbox{\isa{intro}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''.
342 The rule is called \isa{{\isachardoublequote}t{\isachardot}equality{\isachardoublequote}}.
344 \item Representations of arbitrary record expressions as canonical
345 constructor terms are provided both in \mbox{\isa{cases}} and \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.
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.
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}}.
361 \isamarkupsection{Datatypes \label{sec:hol-datatype}%
365 \begin{isamarkuptext}%
366 \begin{matharray}{rcl}
367 \indexdef{HOL}{command}{datatype}\mbox{\isa{\isacommand{datatype}}} & : & \isartrans{theory}{theory} \\
368 \indexdef{HOL}{command}{rep\_datatype}\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
372 'datatype' (dtspec + 'and')
374 'rep\_datatype' (name *) dtrules
377 dtspec: parname? typespec infix? '=' (cons + '|')
379 cons: name (type *) mixfix?
381 dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
386 \item [\mbox{\isa{\isacommand{datatype}}}] defines inductive datatypes in
389 \item [\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}] represents existing types as
390 inductive ones, generating the standard infrastructure of derived
391 concepts (primitive recursion etc.).
395 The induction and exhaustion theorems generated provide case names
396 according to the constructors involved, while parameters are named
397 after the types (see also \secref{sec:cases-induct}).
399 See \cite{isabelle-HOL} for more details on datatypes, but beware of
400 the old-style theory syntax being used there! Apart from proper
401 proof methods for case-analysis and induction, there are also
402 emulations of ML tactics \mbox{\isa{case{\isacharunderscore}tac}} and \mbox{\isa{induct{\isacharunderscore}tac}} available, see \secref{sec:hol-induct-tac}; these admit
403 to refer directly to the internal structure of subgoals (including
404 internally bound parameters).%
408 \isamarkupsection{Recursive functions \label{sec:recursion}%
412 \begin{isamarkuptext}%
413 \begin{matharray}{rcl}
414 \indexdef{HOL}{command}{primrec}\mbox{\isa{\isacommand{primrec}}} & : & \isarkeep{local{\dsh}theory} \\
415 \indexdef{HOL}{command}{fun}\mbox{\isa{\isacommand{fun}}} & : & \isarkeep{local{\dsh}theory} \\
416 \indexdef{HOL}{command}{function}\mbox{\isa{\isacommand{function}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
417 \indexdef{HOL}{command}{termination}\mbox{\isa{\isacommand{termination}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
420 \railalias{funopts}{function\_opts} %FIXME ??
423 'primrec' target? fixes 'where' equations
425 equations: (thmdecl? prop + '|')
427 ('fun' | 'function') (funopts)? fixes 'where' clauses
429 clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
431 funopts: '(' (('sequential' | 'in' name | 'domintros' | 'tailrec' |
432 'default' term) + ',') ')'
434 'termination' ( term )?
439 \item [\mbox{\isa{\isacommand{primrec}}}] defines primitive recursive
440 functions over datatypes, see also \cite{isabelle-HOL}.
442 \item [\mbox{\isa{\isacommand{function}}}] defines functions by general
443 wellfounded recursion. A detailed description with examples can be
444 found in \cite{isabelle-function}. The function is specified by a
445 set of (possibly conditional) recursive equations with arbitrary
446 pattern matching. The command generates proof obligations for the
447 completeness and the compatibility of patterns.
449 The defined function is considered partial, and the resulting
450 simplification rules (named \isa{{\isachardoublequote}f{\isachardot}psimps{\isachardoublequote}}) and induction rule
451 (named \isa{{\isachardoublequote}f{\isachardot}pinduct{\isachardoublequote}}) are guarded by a generated domain
452 predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \mbox{\isa{\isacommand{termination}}}
453 command can then be used to establish that the function is total.
455 \item [\mbox{\isa{\isacommand{fun}}}] is a shorthand notation for
456 ``\mbox{\isa{\isacommand{function}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by
457 automated proof attempts regarding pattern matching and termination.
458 See \cite{isabelle-function} for further details.
460 \item [\mbox{\isa{\isacommand{termination}}}~\isa{f}] commences a
461 termination proof for the previously defined function \isa{f}. If
462 this is omitted, the command refers to the most recent function
463 definition. After the proof is closed, the recursive equations and
464 the induction principle is established.
470 Recursive definitions introduced by both the \mbox{\isa{\isacommand{primrec}}} and the \mbox{\isa{\isacommand{function}}} command accommodate
471 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)
472 refers to a specific induction rule, with parameters named according
473 to the user-specified equations. Case names of \mbox{\isa{\isacommand{primrec}}} are that of the datatypes involved, while those of
474 \mbox{\isa{\isacommand{function}}} are numbered (starting from 1).
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
481 The \mbox{\isa{\isacommand{function}}} command accepts the following
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.
496 \item [\isa{{\isachardoublequote}{\isasymIN}\ name{\isachardoublequote}}] gives the target for the definition.
499 \item [\isa{domintros}] enables the automated generation of
500 introduction rules for the domain predicate. While mostly not
501 needed, they can be helpful in some proofs about partial functions.
503 \item [\isa{tailrec}] generates the unconstrained recursive
504 equations even without a termination proof, provided that the
505 function is tail-recursive. This currently only works
507 \item [\isa{{\isachardoublequote}default\ d{\isachardoublequote}}] allows to specify a default value for a
508 (partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}}
509 whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}.
515 \isamarkupsubsection{Proof methods related to recursive definitions%
519 \begin{isamarkuptext}%
520 \begin{matharray}{rcl}
521 \indexdef{HOL}{method}{pat\_completeness}\mbox{\isa{pat{\isacharunderscore}completeness}} & : & \isarmeth \\
522 \indexdef{HOL}{method}{relation}\mbox{\isa{relation}} & : & \isarmeth \\
523 \indexdef{HOL}{method}{lexicographic\_order}\mbox{\isa{lexicographic{\isacharunderscore}order}} & : & \isarmeth \\
529 'lexicographic\_order' (clasimpmod *)
535 \item [\mbox{\isa{pat{\isacharunderscore}completeness}}] is a specialized method to
536 solve goals regarding the completeness of pattern matching, as
537 required by the \mbox{\isa{\isacommand{function}}} package (cf.\
538 \cite{isabelle-function}).
540 \item [\mbox{\isa{relation}}~\isa{R}] introduces a termination
541 proof using the relation \isa{R}. The resulting proof state will
542 contain goals expressing that \isa{R} is wellfounded, and that the
543 arguments of recursive calls decrease with respect to \isa{R}.
544 Usually, this method is used as the initial proof step of manual
547 \item [\mbox{\isa{lexicographic{\isacharunderscore}order}}] attempts a fully
548 automated termination proof by searching for a lexicographic
549 combination of size measures on the arguments of the function. The
550 method accepts the same arguments as the \mbox{\isa{auto}} method,
551 which it uses internally to prove local descents. The same context
552 modifiers as for \mbox{\isa{auto}} are accepted, see
553 \secref{sec:clasimp}.
555 In case of failure, extensive information is printed, which can help
556 to analyse the situation (cf.\ \cite{isabelle-function}).
562 \isamarkupsubsection{Old-style recursive function definitions (TFL)%
566 \begin{isamarkuptext}%
567 The old TFL commands \mbox{\isa{\isacommand{recdef}}} and \mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}} for defining recursive are mostly obsolete; \mbox{\isa{\isacommand{function}}} or \mbox{\isa{\isacommand{fun}}} should be used instead.
569 \begin{matharray}{rcl}
570 \indexdef{HOL}{command}{recdef}\mbox{\isa{\isacommand{recdef}}} & : & \isartrans{theory}{theory} \\
571 \indexdef{HOL}{command}{recdef\_tc}\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{theory}{proof(prove)} \\
575 'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
579 hints: '(' 'hints' (recdefmod *) ')'
581 recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
583 tc: nameref ('(' nat ')')?
589 \item [\mbox{\isa{\isacommand{recdef}}}] defines general well-founded
590 recursive functions (using the TFL package), see also
591 \cite{isabelle-HOL}. The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells
592 TFL to recover from failed proof attempts, returning unfinished
593 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
594 automated proof process of TFL. Additional \mbox{\isa{clasimpmod}}
595 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
596 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
597 Classical reasoner (cf.\ \secref{sec:classical}).
599 \item [\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}}] recommences the
600 proof for leftover termination condition number \isa{i} (default
601 1) as generated by a \mbox{\isa{\isacommand{recdef}}} definition of
604 Note that in most cases, \mbox{\isa{\isacommand{recdef}}} is able to finish
605 its internal proofs without manual intervention.
609 \medskip Hints for \mbox{\isa{\isacommand{recdef}}} may be also declared
610 globally, using the following attributes.
612 \begin{matharray}{rcl}
613 \indexdef{HOL}{attribute}{recdef\_simp}\mbox{\isa{recdef{\isacharunderscore}simp}} & : & \isaratt \\
614 \indexdef{HOL}{attribute}{recdef\_cong}\mbox{\isa{recdef{\isacharunderscore}cong}} & : & \isaratt \\
615 \indexdef{HOL}{attribute}{recdef\_wf}\mbox{\isa{recdef{\isacharunderscore}wf}} & : & \isaratt \\
619 ('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
625 \isamarkupsection{Definition by specification \label{sec:hol-specification}%
629 \begin{isamarkuptext}%
630 \begin{matharray}{rcl}
631 \indexdef{HOL}{command}{specification}\mbox{\isa{\isacommand{specification}}} & : & \isartrans{theory}{proof(prove)} \\
632 \indexdef{HOL}{command}{ax\_specification}\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} & : & \isartrans{theory}{proof(prove)} \\
636 ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
638 decl: ((name ':')? term '(' 'overloaded' ')'?)
643 \item [\mbox{\isa{\isacommand{specification}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
644 goal stating the existence of terms with the properties specified to
645 hold for the constants given in \isa{decls}. After finishing the
646 proof, the theory will be augmented with definitions for the given
647 constants, as well as with theorems stating the properties for these
650 \item [\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
651 up a goal stating the existence of terms with the properties
652 specified to hold for the constants given in \isa{decls}. After
653 finishing the proof, the theory will be augmented with axioms
654 expressing the properties given in the first place.
656 \item [\isa{decl}] declares a constant to be defined by the
657 specification given. The definition for the constant \isa{c} is
658 bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
659 the declaration. Overloaded constants should be declared as such.
663 Whether to use \mbox{\isa{\isacommand{specification}}} or \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} is to some extent a matter of style. \mbox{\isa{\isacommand{specification}}} introduces no new axioms, and so by
664 construction cannot introduce inconsistencies, whereas \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}} does introduce axioms, but only after the
665 user has explicitly proven it to be safe. A practical issue must be
666 considered, though: After introducing two constants with the same
667 properties using \mbox{\isa{\isacommand{specification}}}, one can prove
668 that the two constants are, in fact, equal. If this might be a
669 problem, one should use \mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}.%
673 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
677 \begin{isamarkuptext}%
678 An \textbf{inductive definition} specifies the least predicate (or
679 set) \isa{R} closed under given rules: applying a rule to elements
680 of \isa{R} yields a result within \isa{R}. For example, a
681 structural operational semantics is an inductive definition of an
684 Dually, a \textbf{coinductive definition} specifies the greatest
685 predicate~/ set \isa{R} that is consistent with given rules: every
686 element of \isa{R} can be seen as arising by applying a rule to
687 elements of \isa{R}. An important example is using bisimulation
688 relations to formalise equivalence of processes and infinite data
691 \medskip The HOL package is related to the ZF one, which is
692 described in a separate paper,\footnote{It appeared in CADE
693 \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
694 which you should refer to in case of difficulties. The package is
695 simpler than that of ZF thanks to implicit type-checking in HOL.
696 The types of the (co)inductive predicates (or sets) determine the
697 domain of the fixedpoint definition, and the package does not have
698 to use inference rules for type-checking.
700 \begin{matharray}{rcl}
701 \indexdef{HOL}{command}{inductive}\mbox{\isa{\isacommand{inductive}}} & : & \isarkeep{local{\dsh}theory} \\
702 \indexdef{HOL}{command}{inductive\_set}\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
703 \indexdef{HOL}{command}{coinductive}\mbox{\isa{\isacommand{coinductive}}} & : & \isarkeep{local{\dsh}theory} \\
704 \indexdef{HOL}{command}{coinductive\_set}\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}} & : & \isarkeep{local{\dsh}theory} \\
705 \indexdef{HOL}{attribute}{mono}\mbox{\isa{mono}} & : & \isaratt \\
709 ('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
710 ('where' clauses)? ('monos' thmrefs)?
712 clauses: (thmdecl? prop + '|')
714 'mono' (() | 'add' | 'del')
720 \item [\mbox{\isa{\isacommand{inductive}}} and \mbox{\isa{\isacommand{coinductive}}}] define (co)inductive predicates from the
721 introduction rules given in the \mbox{\isa{\isakeyword{where}}} part. The
722 optional \mbox{\isa{\isakeyword{for}}} part contains a list of parameters of the
723 (co)inductive predicates that remain fixed throughout the
724 definition. The optional \mbox{\isa{\isakeyword{monos}}} section contains
725 \emph{monotonicity theorems}, which are required for each operator
726 applied to a recursive set in the introduction rules. There
727 \emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
728 for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
730 \item [\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}} and \mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}] are wrappers for to the previous commands,
731 allowing the definition of (co)inductive sets.
733 \item [\mbox{\isa{mono}}] declares monotonicity rules. These
734 rule are involved in the automated monotonicity proof of \mbox{\isa{\isacommand{inductive}}}.
740 \isamarkupsubsection{Derived rules%
744 \begin{isamarkuptext}%
745 Each (co)inductive definition \isa{R} adds definitions to the
746 theory and also proves some theorems:
750 \item [\isa{R{\isachardot}intros}] is the list of introduction rules as proven
751 theorems, for the recursive predicates (or sets). The rules are
752 also available individually, using the names given them in the
755 \item [\isa{R{\isachardot}cases}] is the case analysis (or elimination) rule;
757 \item [\isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct}] is the (co)induction
762 When several predicates \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardoublequote}} are
763 defined simultaneously, the list of introduction rules is called
764 \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}intros{\isachardoublequote}}, the case analysis rules are
765 called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isachardot}cases{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardot}cases{\isachardoublequote}}, and the list
766 of mutual induction rules is called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}inducts{\isachardoublequote}}.%
770 \isamarkupsubsection{Monotonicity theorems%
774 \begin{isamarkuptext}%
775 Each theory contains a default set of theorems that are used in
776 monotonicity proofs. New rules can be added to this set via the
777 \mbox{\isa{mono}} attribute. The HOL theory \isa{Inductive}
778 shows how this is done. In general, the following monotonicity
779 theorems may be added:
783 \item Theorems of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, for proving
784 monotonicity of inductive definitions whose introduction rules have
785 premises involving terms such as \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}}.
787 \item Monotonicity theorems for logical operators, which are of the
788 general form \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isachardoublequote}}. For example, in
789 the case of the operator \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, the corresponding theorem is
791 \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}}}
794 \item De Morgan style equations for reasoning about the ``polarity''
797 \isa{{\isachardoublequote}{\isasymnot}\ {\isasymnot}\ P\ {\isasymlongleftrightarrow}\ P{\isachardoublequote}} \qquad\qquad
798 \isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ {\isasymnot}\ Q{\isachardoublequote}}
801 \item Equations for reducing complex operators to more primitive
802 ones whose monotonicity can easily be proved, e.g.
804 \isa{{\isachardoublequote}{\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ Q{\isachardoublequote}} \qquad\qquad
805 \isa{{\isachardoublequote}Ball\ A\ P\ {\isasymequiv}\ {\isasymforall}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}}
810 %FIXME: Example of an inductive definition%
814 \isamarkupsection{Arithmetic proof support%
818 \begin{isamarkuptext}%
819 \begin{matharray}{rcl}
820 \indexdef{HOL}{method}{arith}\mbox{\isa{arith}} & : & \isarmeth \\
821 \indexdef{HOL}{attribute}{arith\_split}\mbox{\isa{arith{\isacharunderscore}split}} & : & \isaratt \\
824 The \mbox{\isa{arith}} method decides linear arithmetic problems
825 (on types \isa{nat}, \isa{int}, \isa{real}). Any current
826 facts are inserted into the goal before running the procedure.
828 The \mbox{\isa{arith{\isacharunderscore}split}} attribute declares case split
829 rules to be expanded before the arithmetic procedure is invoked.
831 Note that a simpler (but faster) version of arithmetic reasoning is
832 already performed by the Simplifier.%
836 \isamarkupsection{Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac}%
840 \begin{isamarkuptext}%
841 The following important tactical tools of Isabelle/HOL have been
842 ported to Isar. These should be never used in proper proof texts!
844 \begin{matharray}{rcl}
845 \indexdef{HOL}{method}{case\_tac}\mbox{\isa{case{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
846 \indexdef{HOL}{method}{induct\_tac}\mbox{\isa{induct{\isacharunderscore}tac}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
847 \indexdef{HOL}{method}{ind\_cases}\mbox{\isa{ind{\isacharunderscore}cases}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
848 \indexdef{HOL}{command}{inductive\_cases}\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} & : & \isartrans{theory}{theory} \\
852 'case\_tac' goalspec? term rule?
854 'induct\_tac' goalspec? (insts * 'and') rule?
856 'ind\_cases' (prop +) ('for' (name +)) ?
858 'inductive\_cases' (thmdecl? (prop +) + 'and')
861 rule: ('rule' ':' thmref)
867 \item [\mbox{\isa{case{\isacharunderscore}tac}} and \mbox{\isa{induct{\isacharunderscore}tac}}]
868 admit to reason about inductive datatypes only (unless an
869 alternative rule is given explicitly). Furthermore, \mbox{\isa{case{\isacharunderscore}tac}} does a classical case split on booleans; \mbox{\isa{induct{\isacharunderscore}tac}} allows only variables to be given as instantiation.
870 These tactic emulations feature both goal addressing and dynamic
871 instantiation. Note that named rule cases are \emph{not} provided
872 as would be by the proper \mbox{\isa{induct}} and \mbox{\isa{cases}} proof
873 methods (see \secref{sec:cases-induct}).
875 \item [\mbox{\isa{ind{\isacharunderscore}cases}} and \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}] provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted
878 While \mbox{\isa{ind{\isacharunderscore}cases}} is a proof method to apply the
879 result immediately as elimination rules, \mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}} provides case split theorems at the theory level
880 for later use. The \mbox{\isa{\isakeyword{for}}} argument of the \mbox{\isa{ind{\isacharunderscore}cases}} method allows to specify a list of variables that should
881 be generalized before applying the resulting rule.
887 \isamarkupsection{Executable code%
891 \begin{isamarkuptext}%
892 Isabelle/Pure provides two generic frameworks to support code
893 generation from executable specifications. Isabelle/HOL
894 instantiates these mechanisms in a way that is amenable to end-user
897 One framework generates code from both functional and relational
898 programs to SML. See \cite{isabelle-HOL} for further information
899 (this actually covers the new-style theory format as well).
901 \begin{matharray}{rcl}
902 \indexdef{HOL}{command}{value}\mbox{\isa{\isacommand{value}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
903 \indexdef{HOL}{command}{code\_module}\mbox{\isa{\isacommand{code{\isacharunderscore}module}}} & : & \isartrans{theory}{theory} \\
904 \indexdef{HOL}{command}{code\_library}\mbox{\isa{\isacommand{code{\isacharunderscore}library}}} & : & \isartrans{theory}{theory} \\
905 \indexdef{HOL}{command}{consts\_code}\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
906 \indexdef{HOL}{command}{types\_code}\mbox{\isa{\isacommand{types{\isacharunderscore}code}}} & : & \isartrans{theory}{theory} \\
907 \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
914 ( 'code\_module' | 'code\_library' ) modespec ? name ? \\
915 ( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
916 'contains' ( ( name '=' term ) + | term + )
919 modespec: '(' ( name * ) ')'
922 'consts\_code' (codespec +)
925 codespec: const template attachment ?
928 'types\_code' (tycodespec +)
931 tycodespec: name template attachment ?
937 template: '(' string ')'
940 attachment: 'attach' modespec ? verblbrace text verbrbrace
949 \item [\mbox{\isa{\isacommand{value}}}~\isa{t}] evaluates and prints a
950 term using the code generator.
954 \medskip The other framework generates code from functional programs
955 (including overloading using type classes) to SML \cite{SML}, OCaml
956 \cite{OCaml} and Haskell \cite{haskell-revised-report}.
957 Conceptually, code generation is split up in three steps:
958 \emph{selection} of code theorems, \emph{translation} into an
959 abstract executable view and \emph{serialization} to a specific
960 \emph{target language}. See \cite{isabelle-codegen} for an
961 introduction on how to use it.
963 \begin{matharray}{rcl}
964 \indexdef{HOL}{command}{export\_code}\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
965 \indexdef{HOL}{command}{code\_thms}\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
966 \indexdef{HOL}{command}{code\_deps}\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
967 \indexdef{HOL}{command}{code\_datatype}\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}} & : & \isartrans{theory}{theory} \\
968 \indexdef{HOL}{command}{code\_const}\mbox{\isa{\isacommand{code{\isacharunderscore}const}}} & : & \isartrans{theory}{theory} \\
969 \indexdef{HOL}{command}{code\_type}\mbox{\isa{\isacommand{code{\isacharunderscore}type}}} & : & \isartrans{theory}{theory} \\
970 \indexdef{HOL}{command}{code\_class}\mbox{\isa{\isacommand{code{\isacharunderscore}class}}} & : & \isartrans{theory}{theory} \\
971 \indexdef{HOL}{command}{code\_instance}\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}} & : & \isartrans{theory}{theory} \\
972 \indexdef{HOL}{command}{code\_monad}\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}} & : & \isartrans{theory}{theory} \\
973 \indexdef{HOL}{command}{code\_reserved}\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}} & : & \isartrans{theory}{theory} \\
974 \indexdef{HOL}{command}{code\_include}\mbox{\isa{\isacommand{code{\isacharunderscore}include}}} & : & \isartrans{theory}{theory} \\
975 \indexdef{HOL}{command}{code\_modulename}\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}} & : & \isartrans{theory}{theory} \\
976 \indexdef{HOL}{command}{code\_exception}\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}} & : & \isartrans{theory}{theory} \\
977 \indexdef{HOL}{command}{print\_codesetup}\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
978 \indexdef{HOL}{attribute}{code}\mbox{\isa{code}} & : & \isaratt \\
982 'export\_code' ( constexpr + ) ? \\
983 ( ( 'in' target ( 'module\_name' string ) ? \\
984 ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
987 'code\_thms' ( constexpr + ) ?
990 'code\_deps' ( constexpr + ) ?
996 constexpr: ( const | 'name.*' | '*' )
999 typeconstructor: nameref
1005 target: 'OCaml' | 'SML' | 'Haskell'
1008 'code\_datatype' const +
1011 'code\_const' (const + 'and') \\
1012 ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1015 'code\_type' (typeconstructor + 'and') \\
1016 ( ( '(' target ( syntax ? + 'and' ) ')' ) + )
1019 'code\_class' (class + 'and') \\
1021 ( ( string ('where' \\
1022 ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
1025 'code\_instance' (( typeconstructor '::' class ) + 'and') \\
1026 ( ( '(' target ( '-' ? + 'and' ) ')' ) + )
1029 'code\_monad' const const target
1032 'code\_reserved' target ( string + )
1035 'code\_include' target ( string ( string | '-') )
1038 'code\_modulename' target ( ( string string ) + )
1041 'code\_exception' ( const + )
1044 syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
1047 'code' ('func' | 'inline') ( 'del' )?
1053 \item [\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}] is the canonical interface
1054 for generating and serializing code: for a given list of constants,
1055 code is generated for the specified target languages. Abstract code
1056 is cached incrementally. If no constant is given, the currently
1057 cached code is serialized. If no serialization instruction is
1058 given, only abstract code is cached.
1060 Constants may be specified by giving them literally, referring to
1061 all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
1062 available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
1064 By default, for each involved theory one corresponding name space
1065 module is generated. Alternativly, a module name may be specified
1066 after the \mbox{\isa{\isakeyword{module{\isacharunderscore}name}}} keyword; then \emph{all} code is
1067 placed in this module.
1069 For \emph{SML} and \emph{OCaml}, the file specification refers to a
1070 single file; for \emph{Haskell}, it refers to a whole directory,
1071 where code is generated in multiple files reflecting the module
1072 hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
1073 output. For \emph{SML}, omitting the file specification compiles
1074 code internally in the context of the current ML session.
1076 Serializers take an optional list of arguments in parentheses. For
1077 \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
1080 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}] prints a list of theorems
1081 representing the corresponding program containing all given
1082 constants; if no constants are given, the currently cached code
1083 theorems are printed.
1085 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}] visualizes dependencies of
1086 theorems representing the corresponding program containing all given
1087 constants; if no constants are given, the currently cached code
1088 theorems are visualized.
1090 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}] specifies a constructor set
1093 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}] associates a list of constants
1094 with target-specific serializations; omitting a serialization
1095 deletes an existing serialization.
1097 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}] associates a list of type
1098 constructors with target-specific serializations; omitting a
1099 serialization deletes an existing serialization.
1101 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}] associates a list of classes
1102 with target-specific class names; in addition, constants associated
1103 with this class may be given target-specific names used for instance
1104 declarations; omitting a serialization deletes an existing
1105 serialization. This applies only to \emph{Haskell}.
1107 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}] declares a list of type
1108 constructor / class instance relations as ``already present'' for a
1109 given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
1110 ``already present'' declaration. This applies only to
1113 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}] provides an auxiliary
1114 mechanism to generate monadic code.
1116 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}] declares a list of names as
1117 reserved for a given target, preventing it to be shadowed by any
1120 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}] adds arbitrary named content
1121 (``include'') to generated code. A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}''
1122 will remove an already added ``include''.
1124 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}] declares aliasings from
1125 one module name onto another.
1127 \item [\mbox{\isa{\isacommand{code{\isacharunderscore}exception}}}] declares constants which
1128 are not required to have a definition by a defining equations; these
1129 are mapped on exceptions instead.
1131 \item [\mbox{\isa{code}}~\isa{func}] explicitly selects (or
1132 with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
1133 code generation. Usually packages introducing defining equations
1134 provide a resonable default setup for selection.
1136 \item [\mbox{\isa{code}}\isa{inline}] declares (or with
1137 option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
1138 applied as rewrite rules to any defining equation during
1141 \item [\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}] gives an overview on
1142 selected defining equations, code generator datatypes and
1146 \end{isamarkuptext}%
1154 \isacommand{end}\isamarkupfalse%
1165 %%% Local Variables:
1167 %%% TeX-master: "root"