3 \def\isabellecontext{HOL{\isaliteral{5F}{\isacharunderscore}}Specific}%
10 \isacommand{theory}\isamarkupfalse%
11 \ HOL{\isaliteral{5F}{\isacharunderscore}}Specific\isanewline
12 \isakeyword{imports}\ Main\isanewline
13 \isakeyword{uses}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2F}{\isacharslash}}antiquote{\isaliteral{5F}{\isacharunderscore}}setup{\isaliteral{2E}{\isachardot}}ML{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
22 \isamarkupchapter{Isabelle/HOL \label{ch:hol}%
26 \isamarkupsection{Typedef axiomatization \label{sec:hol-typedef}%
30 \begin{isamarkuptext}%
31 \begin{matharray}{rcl}
32 \indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
36 \rail@begin{2}{\isa{}}
37 \rail@term{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}}[]
40 \rail@nont{\isa{altname}}[]
42 \rail@nont{\isa{abstype}}[]
43 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
44 \rail@nont{\isa{repset}}[]
46 \rail@begin{3}{\isa{altname}}
47 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
49 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
51 \rail@term{\isa{\isakeyword{open}}}[]
53 \rail@term{\isa{\isakeyword{open}}}[]
54 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
56 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
58 \rail@begin{2}{\isa{abstype}}
59 \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
62 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
65 \rail@begin{2}{\isa{repset}}
66 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
69 \rail@term{\isa{\isakeyword{morphisms}}}[]
70 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
71 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
79 \item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{22}{\isachardoublequote}}}
80 axiomatizes a Gordon/HOL-style type definition in the background
81 theory of the current context, depending on a non-emptiness result
82 of the set \isa{A} (which needs to be proven interactively).
84 The raw type may not depend on parameters or assumptions of the
85 context --- this is logically impossible in Isabelle/HOL --- but the
86 non-emptiness property can be local, potentially resulting in
87 multiple interpretations in target contexts. Thus the established
88 bijection between the representing set \isa{A} and the new type
89 \isa{t} may semantically depend on local assumptions.
91 By default, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t}
92 and a set (term constant) of the same name, unless an alternative
93 base name is given in parentheses, or the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}open{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}''
94 declaration is used to suppress a separate constant definition
95 altogether. The injection from type to set is called \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t},
96 its inverse \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t} --- this may be changed via an explicit
97 \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration.
99 Theorems \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t}, \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse}, and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inverse} provide the most basic characterization as a
100 corresponding injection/surjection pair (in both directions). Rules
101 \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} and \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}inject} provide a slightly
102 more convenient view on the injectivity part, suitable for automated
103 proof tools (e.g.\ in \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}
104 declarations). Rules \isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Rep{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct}, and
105 \isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}cases}/\isa{Abs{\isaliteral{5F}{\isacharunderscore}}t{\isaliteral{5F}{\isacharunderscore}}induct} provide alternative views
106 on surjectivity; these are already declared as set or type rules for
107 the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
109 An alternative name for the set definition (and other derived
110 entities) may be specified in parentheses; the default is to use
111 \isa{t} as indicated before.
117 \isamarkupsection{Adhoc tuples%
121 \begin{isamarkuptext}%
122 \begin{matharray}{rcl}
123 \indexdef{HOL}{attribute}{split\_format}\hypertarget{attribute.HOL.split-format}{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{attribute} \\
127 \rail@begin{2}{\isa{}}
128 \rail@term{\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}}[]
131 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
132 \rail@term{\isa{complete}}[]
133 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
141 \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isaliteral{5F}{\isacharunderscore}}format}}}\ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}complete{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} causes
142 arguments in function applications to be represented canonically
143 according to their tuple type structure.
145 Note that this operation tends to invent funny names for new local
146 parameters introduced.
152 \isamarkupsection{Records \label{sec:hol-record}%
156 \begin{isamarkuptext}%
157 In principle, records merely generalize the concept of tuples, where
158 components may be addressed by labels instead of just position. The
159 logical infrastructure of records in Isabelle/HOL is slightly more
160 advanced, though, supporting truly extensible record schemes. This
161 admits operations that are polymorphic with respect to record
162 extension, yielding ``object-oriented'' effects like (single)
163 inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more
164 details on object-oriented verification and record subtyping in HOL.%
168 \isamarkupsubsection{Basic concepts%
172 \begin{isamarkuptext}%
173 Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
174 at the level of terms and types. The notation is as follows:
177 \begin{tabular}{l|l|l}
178 & record terms & record types \\ \hline
179 fixed & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
180 schematic & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} &
181 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ M{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
185 \noindent The ASCII representation of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{7C}{\isacharbar}}\ x\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}.
187 A fixed record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} has field \isa{x} of value
188 \isa{a} and field \isa{y} of value \isa{b}. The corresponding
189 type is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, assuming that \isa{{\isaliteral{22}{\isachardoublequote}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{22}{\isachardoublequote}}}
190 and \isa{{\isaliteral{22}{\isachardoublequote}}b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{22}{\isachardoublequote}}}.
192 A record scheme like \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} contains fields
193 \isa{x} and \isa{y} as before, but also possibly further fields
194 as indicated by the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' notation (which is actually part
195 of the syntax). The improper field ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' of a record
196 scheme is called the \emph{more part}. Logically it is just a free
197 variable, which is occasionally referred to as ``row variable'' in
198 the literature. The more part of a record scheme may be
199 instantiated by zero or more further components. For example, the
200 previous scheme may get instantiated to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, where \isa{m{\isaliteral{27}{\isacharprime}}} refers to a different more part.
201 Fixed records are special instances of record schemes, where
202 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}'' is properly terminated by the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ unit{\isaliteral{22}{\isachardoublequote}}}
203 element. In fact, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} is just an abbreviation
204 for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
206 \medskip Two key observations make extensible records in a simply
207 typed language like HOL work out:
211 \item the more part is internalized, as a free term or type
214 \item field names are externalized, they cannot be accessed within
215 the logic as first-class values.
219 \medskip In Isabelle/HOL record types have to be defined explicitly,
220 fixing their field names and types, and their (optional) parent
221 record. Afterwards, records may be formed using above syntax, while
222 obeying the canonical order of fields as given by their declaration.
223 The record package provides several standard operations like
224 selectors and updates. The common setup for various generic proof
225 tools enable succinct reasoning patterns. See also the Isabelle/HOL
226 tutorial \cite{isabelle-hol-book} for further instructions on using
227 records in practice.%
231 \isamarkupsubsection{Record specifications%
235 \begin{isamarkuptext}%
236 \begin{matharray}{rcl}
237 \indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
241 \rail@begin{2}{\isa{}}
242 \rail@term{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}}[]
243 \rail@nont{\hyperlink{syntax.typespecsorts}{\mbox{\isa{typespecsorts}}}}[]
244 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
247 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
248 \rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
251 \rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
260 \item \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{2B}{\isacharplus}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} defines extensible record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}},
261 derived from the optional parent record \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} by adding new
262 field components \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} etc.
264 The type variables of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} need to be
265 covered by the (distinct) parameters \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{22}{\isachardoublequote}}}. Type constructor \isa{t} has to be new, while \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} needs to specify an instance of an existing record type. At
266 least one new field \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} has to be specified.
267 Basically, field names need to belong to a unique record. This is
268 not a real restriction in practice, since fields are qualified by
269 the record name internally.
271 The parent record specification \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is optional; if omitted
272 \isa{t} becomes a root record. The hierarchy of all records
273 declared within a theory context forms a forest structure, i.e.\ a
274 set of trees starting with a root record each. There is no way to
275 merge multiple parent records!
277 For convenience, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is made a
278 type abbreviation for the fixed record type \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, likewise is \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{5F}{\isacharunderscore}}scheme{\isaliteral{22}{\isachardoublequote}}} made an abbreviation for
279 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}.
285 \isamarkupsubsection{Record operations%
289 \begin{isamarkuptext}%
290 Any record definition of the form presented above produces certain
291 standard operations. Selectors and updates are provided for any
292 field, including the improper one ``\isa{more}''. There are also
293 cumulative record constructor functions. To simplify the
294 presentation below, we assume for now that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} is a root record with fields \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
296 \medskip \textbf{Selectors} and \textbf{updates} are available for
297 any field (including ``\isa{more}''):
299 \begin{matharray}{lll}
300 \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
301 \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
304 There is special syntax for application of updates: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} abbreviates term \isa{{\isaliteral{22}{\isachardoublequote}}x{\isaliteral{5F}{\isacharunderscore}}update\ a\ r{\isaliteral{22}{\isachardoublequote}}}. Further notation for
305 repeated updates is also available: \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} may be written \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}. Note that
306 because of postfix notation the order of fields shown here is
307 reverse than in the actual term. Since repeated updates are just
308 function applications, fields may be freely permuted in \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ a{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{2C}{\isacharcomma}}\ z\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}}, as far as logical equality is concerned.
309 Thus commutativity of independent updates can be proven within the
310 logic for any two fields, but not as a general theorem.
312 \medskip The \textbf{make} operation provides a cumulative record
313 constructor function:
315 \begin{matharray}{lll}
316 \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
319 \medskip We now reconsider the case of non-root records, which are
320 derived of some parent. In general, the latter may depend on
321 another parent as well, resulting in a list of \emph{ancestor
322 records}. Appending the lists of fields of all ancestors results in
323 a certain field prefix. The record package automatically takes care
324 of this by lifting operations over this context of ancestor fields.
325 Assuming that \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E7375623E}{}\isactrlsub m{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} has ancestor
326 fields \isa{{\isaliteral{22}{\isachardoublequote}}b\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ b\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}},
327 the above record operations will get the following types:
331 \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} \\
332 \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{5F}{\isacharunderscore}}update{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
333 \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C72686F3E}{\isasymrho}}\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
337 \noindent Some further operations address the extension aspect of a
338 derived record scheme specifically: \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} produces a
339 record fragment consisting of exactly the new fields introduced here
340 (the result may serve as a more part elsewhere); \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}
341 takes a fixed record and adds a given more part; \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} restricts a record scheme to a fixed record.
345 \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
346 \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
347 \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7A6574613E}{\isasymzeta}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}\isaliteral{5C3C5E7665633E}{}\isactrlvec b\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C72686F3E}{\isasymrho}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequote}}} \\
351 \noindent Note that \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}} coincide
356 \isamarkupsubsection{Derived rules and proof tools%
360 \begin{isamarkuptext}%
361 The record package proves several results internally, declaring
362 these facts to appropriate proof tools. This enables users to
363 reason about record structures quite conveniently. Assume that
364 \isa{t} is a record type as specified above.
368 \item Standard conversions for selectors or updates applied to
369 record constructor terms are made part of the default Simplifier
370 context; thus proofs by reduction of basic operations merely require
371 the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments. These rules
372 are available as \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, too.
374 \item Selectors applied to updated records are automatically reduced
375 by an internal simplification procedure, which is also part of the
376 standard Simplifier setup.
378 \item Inject equations of a form analogous to \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} are declared to the Simplifier and Classical
379 Reasoner as \hyperlink{attribute.iff}{\mbox{\isa{iff}}} rules. These rules are available as
380 \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}iffs{\isaliteral{22}{\isachardoublequote}}}.
382 \item The introduction rule for record equality analogous to \isa{{\isaliteral{22}{\isachardoublequote}}x\ r\ {\isaliteral{3D}{\isacharequal}}\ x\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ r\ {\isaliteral{3D}{\isacharequal}}\ y\ r{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ r{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequote}}} is declared to the Simplifier,
383 and as the basic rule context as ``\hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}''.
384 The rule is called \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}equality{\isaliteral{22}{\isachardoublequote}}}.
386 \item Representations of arbitrary record expressions as canonical
387 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,
388 \secref{sec:cases-induct}). Several variations are available, for
389 fixed records, record schemes, more parts etc.
391 The generic proof methods are sufficiently smart to pick the most
392 sensible rule according to the type of the indicated record
393 expression: users just need to apply something like ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}cases\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' to a certain proof problem.
395 \item The derived record operations \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}make{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}fields{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}extend{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}truncate{\isaliteral{22}{\isachardoublequote}}} are \emph{not}
396 treated automatically, but usually need to be expanded by hand,
397 using the collective fact \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{2E}{\isachardot}}defs{\isaliteral{22}{\isachardoublequote}}}.
403 \isamarkupsection{Datatypes \label{sec:hol-datatype}%
407 \begin{isamarkuptext}%
408 \begin{matharray}{rcl}
409 \indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
410 \indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
414 \rail@begin{2}{\isa{}}
415 \rail@term{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}}[]
417 \rail@nont{\isa{dtspec}}[]
419 \rail@cterm{\isa{\isakeyword{and}}}[]
422 \rail@begin{3}{\isa{}}
423 \rail@term{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
426 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
428 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
431 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
434 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
438 \rail@begin{2}{\isa{dtspec}}
441 \rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[]
443 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
446 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
448 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
450 \rail@nont{\isa{cons}}[]
452 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
455 \rail@begin{2}{\isa{cons}}
456 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
459 \rail@cnont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
463 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
471 \item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
474 \item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isaliteral{5F}{\isacharunderscore}}datatype}}}} represents existing types as
475 inductive ones, generating the standard infrastructure of derived
476 concepts (primitive recursion etc.).
480 The induction and exhaustion theorems generated provide case names
481 according to the constructors involved, while parameters are named
482 after the types (see also \secref{sec:cases-induct}).
484 See \cite{isabelle-HOL} for more details on datatypes, but beware of
485 the old-style theory syntax being used there! Apart from proper
486 proof methods for case-analysis and induction, there are also
487 emulations of ML tactics \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} available, see \secref{sec:hol-induct-tac}; these admit
488 to refer directly to the internal structure of subgoals (including
489 internally bound parameters).%
493 \isamarkupsection{Functorial structure of types%
497 \begin{isamarkuptext}%
498 \begin{matharray}{rcl}
499 \indexdef{HOL}{command}{enriched\_type}\hypertarget{command.HOL.enriched-type}{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
503 \rail@begin{2}{\isa{}}
504 \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
507 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
508 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
510 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
517 \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}prefix{\isaliteral{3A}{\isacharcolon}}\ m{\isaliteral{22}{\isachardoublequote}}} allows to
518 prove and register properties about the functorial structure of type
519 constructors. These properties then can be used by other packages
520 to deal with those type constructors in certain type constructions.
521 Characteristic theorems are noted in the current local theory. By
522 default, they are prefixed with the base name of the type
523 constructor, an explicit prefix can be given alternatively.
525 The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the
526 corresponding type constructor and must conform to the following
529 \begin{matharray}{lll}
530 \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} &
531 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{29}{\isacharparenright}}\ t{\isaliteral{22}{\isachardoublequote}}} \\
534 \noindent where \isa{t} is the type constructor, \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are distinct
535 type variables free in the local theory and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}},
536 \ldots, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{22}{\isachardoublequote}}} is a subsequence of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \ldots,
537 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}.
543 \isamarkupsection{Recursive functions \label{sec:recursion}%
547 \begin{isamarkuptext}%
548 \begin{matharray}{rcl}
549 \indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
550 \indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
551 \indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
552 \indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
556 \rail@begin{2}{\isa{}}
557 \rail@term{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}}[]
560 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
562 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
563 \rail@term{\isa{\isakeyword{where}}}[]
564 \rail@nont{\isa{equations}}[]
566 \rail@begin{4}{\isa{}}
568 \rail@term{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}}[]
570 \rail@term{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}}[]
574 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
578 \rail@nont{\isa{functionopts}}[]
580 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
582 \rail@term{\isa{\isakeyword{where}}}[]
583 \rail@nont{\isa{equations}}[]
585 \rail@begin{3}{\isa{equations}}
589 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
591 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
593 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
596 \rail@begin{3}{\isa{functionopts}}
597 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
600 \rail@term{\isa{sequential}}[]
602 \rail@term{\isa{domintros}}[]
605 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
607 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
609 \rail@begin{2}{\isa{}}
610 \rail@term{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}}[]
613 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
621 \item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
622 functions over datatypes, see also \cite{isabelle-HOL}.
624 \item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
625 wellfounded recursion. A detailed description with examples can be
626 found in \cite{isabelle-function}. The function is specified by a
627 set of (possibly conditional) recursive equations with arbitrary
628 pattern matching. The command generates proof obligations for the
629 completeness and the compatibility of patterns.
631 The defined function is considered partial, and the resulting
632 simplification rules (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}psimps{\isaliteral{22}{\isachardoublequote}}}) and induction rule
633 (named \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}pinduct{\isaliteral{22}{\isachardoublequote}}}) are guarded by a generated domain
634 predicate \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{5F}{\isacharunderscore}}dom{\isaliteral{22}{\isachardoublequote}}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
635 command can then be used to establish that the function is total.
637 \item \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} is a shorthand notation for ``\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}sequential{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}, followed by automated
638 proof attempts regarding pattern matching and termination. See
639 \cite{isabelle-function} for further details.
641 \item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
642 termination proof for the previously defined function \isa{f}. If
643 this is omitted, the command refers to the most recent function
644 definition. After the proof is closed, the recursive equations and
645 the induction principle is established.
649 Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
651 reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}induct{\isaliteral{22}{\isachardoublequote}}} (where \isa{c} is the name of the function definition)
652 refers to a specific induction rule, with parameters named according
653 to the user-specified equations. Cases are numbered (starting from 1).
655 For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
656 with structural recursion on the datatype the recursion is carried
659 The equations provided by these packages may be referred later as
660 theorem list \isa{{\isaliteral{22}{\isachardoublequote}}f{\isaliteral{2E}{\isachardot}}simps{\isaliteral{22}{\isachardoublequote}}}, where \isa{f} is the (collective)
661 name of the functions defined. Individual equations may be named
664 The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
669 \item \isa{sequential} enables a preprocessor which disambiguates
670 overlapping patterns by making them mutually disjoint. Earlier
671 equations take precedence over later ones. This allows to give the
672 specification in a format very similar to functional programming.
673 Note that the resulting simplification and induction rules
674 correspond to the transformed specification, not the one given
675 originally. This usually means that each equation given by the user
676 may result in several theorems. Also note that this automatic
677 transformation only works for ML-style datatype patterns.
679 \item \isa{domintros} enables the automated generation of
680 introduction rules for the domain predicate. While mostly not
681 needed, they can be helpful in some proofs about partial functions.
687 \isamarkupsubsection{Proof methods related to recursive definitions%
691 \begin{isamarkuptext}%
692 \begin{matharray}{rcl}
693 \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}}} & : & \isa{method} \\
694 \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
695 \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}} & : & \isa{method} \\
696 \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}} & : & \isa{method} \\
700 \rail@begin{1}{\isa{}}
701 \rail@term{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}}[]
702 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
704 \rail@begin{2}{\isa{}}
705 \rail@term{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}}}[]
708 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
711 \rail@begin{2}{\isa{}}
712 \rail@term{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}}}[]
713 \rail@nont{\isa{orders}}[]
716 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
719 \rail@begin{4}{\isa{orders}}
723 \rail@term{\isa{max}}[]
725 \rail@term{\isa{min}}[]
727 \rail@term{\isa{ms}}[]
736 \item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isaliteral{5F}{\isacharunderscore}}completeness}}} is a specialized method to
737 solve goals regarding the completeness of pattern matching, as
738 required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
739 \cite{isabelle-function}).
741 \item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
742 proof using the relation \isa{R}. The resulting proof state will
743 contain goals expressing that \isa{R} is wellfounded, and that the
744 arguments of recursive calls decrease with respect to \isa{R}.
745 Usually, this method is used as the initial proof step of manual
748 \item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isaliteral{5F}{\isacharunderscore}}order}}} attempts a fully
749 automated termination proof by searching for a lexicographic
750 combination of size measures on the arguments of the function. The
751 method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
752 which it uses internally to prove local descents. The same context
753 modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see
754 \secref{sec:clasimp}.
756 In case of failure, extensive information is printed, which can help
757 to analyse the situation (cf.\ \cite{isabelle-function}).
759 \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isaliteral{5F}{\isacharunderscore}}change}}} also works on termination goals,
760 using a variation of the size-change principle, together with a
761 graph decomposition technique (see \cite{krauss_phd} for details).
762 Three kinds of orders are used internally: \isa{max}, \isa{min},
763 and \isa{ms} (multiset), which is only available when the theory
764 \isa{Multiset} is loaded. When no order kinds are given, they are
765 tried in order. The search for a termination proof uses SAT solving
768 For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
774 \isamarkupsubsection{Functions with explicit partiality%
778 \begin{isamarkuptext}%
779 \begin{matharray}{rcl}
780 \indexdef{HOL}{command}{partial\_function}\hypertarget{command.HOL.partial-function}{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
781 \indexdef{HOL}{attribute}{partial\_function\_mono}\hypertarget{attribute.HOL.partial-function-mono}{\hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}}} & : & \isa{attribute} \\
785 \rail@begin{5}{\isa{}}
786 \rail@term{\hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}}[]
789 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
791 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
792 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
793 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
794 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
796 \rail@term{\isa{\isakeyword{where}}}[]
799 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
801 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
808 \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} defines
809 recursive functions based on fixpoints in complete partial
810 orders. No termination proof is required from the user or
811 constructed internally. Instead, the possibility of non-termination
812 is modelled explicitly in the result type, which contains an
813 explicit bottom element.
815 Pattern matching and mutual recursion are currently not supported.
816 Thus, the specification consists of a single function described by a
817 single recursive equation.
819 There are no fixed syntactic restrictions on the body of the
820 function, but the induced functional must be provably monotonic
821 wrt.\ the underlying order. The monotonicitity proof is performed
822 internally, and the definition is rejected when it fails. The proof
823 can be influenced by declaring hints using the
824 \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} attribute.
826 The mandatory \isa{mode} argument specifies the mode of operation
827 of the command, which directly corresponds to a complete partial
828 order on the result type. By default, the following modes are
832 \item \isa{option} defines functions that map into the \isa{option} type. Here, the value \isa{None} is used to model a
833 non-terminating computation. Monotonicity requires that if \isa{None} is returned by a recursive call, then the overall result
834 must also be \isa{None}. This is best achieved through the use of
835 the monadic operator \isa{{\isaliteral{22}{\isachardoublequote}}Option{\isaliteral{2E}{\isachardot}}bind{\isaliteral{22}{\isachardoublequote}}}.
837 \item \isa{tailrec} defines functions with an arbitrary result
838 type and uses the slightly degenerated partial order where \isa{{\isaliteral{22}{\isachardoublequote}}undefined{\isaliteral{22}{\isachardoublequote}}} is the bottom element. Now, monotonicity requires that
839 if \isa{undefined} is returned by a recursive call, then the
840 overall result must also be \isa{undefined}. In practice, this is
841 only satisfied when each recursive call is a tail call, whose result
842 is directly returned. Thus, this mode of operation allows the
843 definition of arbitrary tail-recursive functions.
846 Experienced users may define new modes by instantiating the locale
847 \isa{{\isaliteral{22}{\isachardoublequote}}partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}definitions{\isaliteral{22}{\isachardoublequote}}} appropriately.
849 \item \hyperlink{attribute.HOL.partial-function-mono}{\mbox{\isa{partial{\isaliteral{5F}{\isacharunderscore}}function{\isaliteral{5F}{\isacharunderscore}}mono}}} declares rules for
850 use in the internal monononicity proofs of partial function
857 \isamarkupsubsection{Old-style recursive function definitions (TFL)%
861 \begin{isamarkuptext}%
862 The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\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.
864 \begin{matharray}{rcl}
865 \indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
866 \indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
870 \rail@begin{5}{\isa{}}
871 \rail@term{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}}[]
874 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
875 \rail@term{\isa{\isakeyword{permissive}}}[]
876 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
879 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
880 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
882 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
887 \rail@nont{\isa{hints}}[]
890 \rail@begin{2}{\isa{}}
891 \rail@nont{\isa{recdeftc}}[]
894 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
896 \rail@nont{\isa{tc}}[]
898 \rail@begin{2}{\isa{hints}}
899 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
900 \rail@term{\isa{\isakeyword{hints}}}[]
903 \rail@cnont{\isa{recdefmod}}[]
905 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
907 \rail@begin{4}{\isa{recdefmod}}
910 \rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}[]
912 \rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}[]
914 \rail@term{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}[]
918 \rail@term{\isa{add}}[]
920 \rail@term{\isa{del}}[]
922 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
923 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
925 \rail@nont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
928 \rail@begin{2}{\isa{tc}}
929 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
932 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
933 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
934 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
942 \item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
943 recursive functions (using the TFL package), see also
944 \cite{isabelle-HOL}. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}permissive{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}'' option tells
945 TFL to recover from failed proof attempts, returning unfinished
946 results. The \isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}, \isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}, and \isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf} hints refer to auxiliary rules to be used in the internal
947 automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
948 declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
949 context of the Simplifier (cf.\ \secref{sec:simplifier}) and
950 Classical reasoner (cf.\ \secref{sec:classical}).
952 \item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isaliteral{5F}{\isacharunderscore}}tc}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} recommences the
953 proof for leftover termination condition number \isa{i} (default
954 1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
957 Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
958 its internal proofs without manual intervention.
962 \medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
963 globally, using the following attributes.
965 \begin{matharray}{rcl}
966 \indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}} & : & \isa{attribute} \\
967 \indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}} & : & \isa{attribute} \\
968 \indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}} & : & \isa{attribute} \\
972 \rail@begin{3}{\isa{}}
974 \rail@term{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}simp}}}}[]
976 \rail@term{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}cong}}}}[]
978 \rail@term{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isaliteral{5F}{\isacharunderscore}}wf}}}}[]
982 \rail@term{\isa{add}}[]
984 \rail@term{\isa{del}}[]
991 \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
995 \begin{isamarkuptext}%
996 An \textbf{inductive definition} specifies the least predicate (or
997 set) \isa{R} closed under given rules: applying a rule to elements
998 of \isa{R} yields a result within \isa{R}. For example, a
999 structural operational semantics is an inductive definition of an
1000 evaluation relation.
1002 Dually, a \textbf{coinductive definition} specifies the greatest
1003 predicate~/ set \isa{R} that is consistent with given rules: every
1004 element of \isa{R} can be seen as arising by applying a rule to
1005 elements of \isa{R}. An important example is using bisimulation
1006 relations to formalise equivalence of processes and infinite data
1009 \medskip The HOL package is related to the ZF one, which is
1010 described in a separate paper,\footnote{It appeared in CADE
1011 \cite{paulson-CADE}; a longer version is distributed with Isabelle.}
1012 which you should refer to in case of difficulties. The package is
1013 simpler than that of ZF thanks to implicit type-checking in HOL.
1014 The types of the (co)inductive predicates (or sets) determine the
1015 domain of the fixedpoint definition, and the package does not have
1016 to use inference rules for type-checking.
1018 \begin{matharray}{rcl}
1019 \indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
1020 \indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
1021 \indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
1022 \indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
1023 \indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
1027 \rail@begin{7}{\isa{}}
1029 \rail@term{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}}[]
1031 \rail@term{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1033 \rail@term{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}}[]
1035 \rail@term{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}}}[]
1039 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[]
1041 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1044 \rail@term{\isa{\isakeyword{for}}}[]
1045 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[]
1050 \rail@term{\isa{\isakeyword{where}}}[]
1051 \rail@nont{\isa{clauses}}[]
1055 \rail@term{\isa{\isakeyword{monos}}}[]
1056 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1059 \rail@begin{3}{\isa{clauses}}
1063 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1065 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1067 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
1070 \rail@begin{3}{\isa{}}
1071 \rail@term{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}}[]
1074 \rail@term{\isa{add}}[]
1076 \rail@term{\isa{del}}[]
1084 \item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the
1085 introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The
1086 optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
1087 (co)inductive predicates that remain fixed throughout the
1088 definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains
1089 \emph{monotonicity theorems}, which are required for each operator
1090 applied to a recursive set in the introduction rules. There
1091 \emph{must} be a theorem of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}},
1092 for each premise \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}} in an introduction rule!
1094 \item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isaliteral{5F}{\isacharunderscore}}set}}}} are wrappers for to the previous commands,
1095 allowing the definition of (co)inductive sets.
1097 \item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules. These
1098 rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
1101 \end{isamarkuptext}%
1104 \isamarkupsubsection{Derived rules%
1108 \begin{isamarkuptext}%
1109 Each (co)inductive definition \isa{R} adds definitions to the
1110 theory and also proves some theorems:
1114 \item \isa{R{\isaliteral{2E}{\isachardot}}intros} is the list of introduction rules as proven
1115 theorems, for the recursive predicates (or sets). The rules are
1116 also available individually, using the names given them in the
1119 \item \isa{R{\isaliteral{2E}{\isachardot}}cases} is the case analysis (or elimination) rule;
1121 \item \isa{R{\isaliteral{2E}{\isachardot}}induct} or \isa{R{\isaliteral{2E}{\isachardot}}coinduct} is the (co)induction
1126 When several predicates \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} are
1127 defined simultaneously, the list of introduction rules is called
1128 \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5F}{\isacharunderscore}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}intros{\isaliteral{22}{\isachardoublequote}}}, the case analysis rules are
1129 called \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}cases{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}cases{\isaliteral{22}{\isachardoublequote}}}, and the list
1130 of mutual induction rules is called \isa{{\isaliteral{22}{\isachardoublequote}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5F}{\isacharunderscore}}R\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{2E}{\isachardot}}inducts{\isaliteral{22}{\isachardoublequote}}}.%
1131 \end{isamarkuptext}%
1134 \isamarkupsubsection{Monotonicity theorems%
1138 \begin{isamarkuptext}%
1139 Each theory contains a default set of theorems that are used in
1140 monotonicity proofs. New rules can be added to this set via the
1141 \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. The HOL theory \isa{Inductive}
1142 shows how this is done. In general, the following monotonicity
1143 theorems may be added:
1147 \item Theorems of the form \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ M\ A\ {\isaliteral{5C3C6C653E}{\isasymle}}\ M\ B{\isaliteral{22}{\isachardoublequote}}}, for proving
1148 monotonicity of inductive definitions whose introduction rules have
1149 premises involving terms such as \isa{{\isaliteral{22}{\isachardoublequote}}M\ R\isaliteral{5C3C5E7375623E}{}\isactrlsub i\ t{\isaliteral{22}{\isachardoublequote}}}.
1151 \item Monotonicity theorems for logical operators, which are of the
1152 general form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}. For example, in
1153 the case of the operator \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, the corresponding theorem is
1155 \infer{\isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}}{\isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}P\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}}}
1158 \item De Morgan style equations for reasoning about the ``polarity''
1159 of expressions, e.g.
1161 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ P{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
1162 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ Q{\isaliteral{22}{\isachardoublequote}}}
1165 \item Equations for reducing complex operators to more primitive
1166 ones whose monotonicity can easily be proved, e.g.
1168 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}} \qquad\qquad
1169 \isa{{\isaliteral{22}{\isachardoublequote}}Ball\ A\ P\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequote}}}
1174 %FIXME: Example of an inductive definition%
1175 \end{isamarkuptext}%
1178 \isamarkupsection{Arithmetic proof support%
1182 \begin{isamarkuptext}%
1183 \begin{matharray}{rcl}
1184 \indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\
1185 \indexdef{HOL}{attribute}{arith}\hypertarget{attribute.HOL.arith}{\hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{attribute} \\
1186 \indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}}} & : & \isa{attribute} \\
1189 The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
1190 (on types \isa{nat}, \isa{int}, \isa{real}). Any current
1191 facts are inserted into the goal before running the procedure.
1193 The \hyperlink{attribute.HOL.arith}{\mbox{\isa{arith}}} attribute declares facts that are
1194 always supplied to the arithmetic provers implicitly.
1196 The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isaliteral{5F}{\isacharunderscore}}split}}} attribute declares case split
1197 rules to be expanded before \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} is invoked.
1199 Note that a simpler (but faster) arithmetic prover is
1200 already invoked by the Simplifier.%
1201 \end{isamarkuptext}%
1204 \isamarkupsection{Intuitionistic proof search%
1208 \begin{isamarkuptext}%
1209 \begin{matharray}{rcl}
1210 \indexdef{HOL}{method}{iprover}\hypertarget{method.HOL.iprover}{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}} & : & \isa{method} \\
1214 \rail@begin{2}{\isa{}}
1215 \rail@term{\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}}[]
1218 \rail@cnont{\hyperlink{syntax.rulemod}{\mbox{\isa{rulemod}}}}[]
1224 The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
1225 search, depending on specifically declared rules from the context,
1226 or given as explicit arguments. Chained facts are inserted into the
1227 goal before commencing proof search.
1229 Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
1230 \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
1231 ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' indicator refers to ``safe'' rules, which may be
1232 applied aggressively (without considering back-tracking later).
1233 Rules declared with ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' are ignored in proof search (the
1234 single-step \hyperlink{method.Pure.rule}{\mbox{\isa{rule}}} method still observes these). An
1235 explicit weight annotation may be given as well; otherwise the
1236 number of rule premises will be taken into account here.%
1237 \end{isamarkuptext}%
1240 \isamarkupsection{Coherent Logic%
1244 \begin{isamarkuptext}%
1245 \begin{matharray}{rcl}
1246 \indexdef{HOL}{method}{coherent}\hypertarget{method.HOL.coherent}{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}} & : & \isa{method} \\
1250 \rail@begin{2}{\isa{}}
1251 \rail@term{\hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}}}[]
1254 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1260 The \hyperlink{method.HOL.coherent}{\mbox{\isa{coherent}}} method solves problems of
1261 \emph{Coherent Logic} \cite{Bezem-Coquand:2005}, which covers
1262 applications in confluence theory, lattice theory and projective
1263 geometry. See \verb|~~/src/HOL/ex/Coherent.thy| for some
1265 \end{isamarkuptext}%
1268 \isamarkupsection{Proving propositions%
1272 \begin{isamarkuptext}%
1273 In addition to the standard proof methods, a number of diagnosis
1274 tools search for proofs and provide an Isar proof snippet on success.
1275 These tools are available via the following commands.
1277 \begin{matharray}{rcl}
1278 \indexdef{HOL}{command}{solve\_direct}\hypertarget{command.HOL.solve-direct}{\hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1279 \indexdef{HOL}{command}{try}\hypertarget{command.HOL.try}{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1280 \indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1281 \indexdef{HOL}{command}{sledgehammer\_params}\hypertarget{command.HOL.sledgehammer-params}{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
1285 \rail@begin{6}{\isa{}}
1286 \rail@term{\hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}}}[]
1291 \rail@term{\isa{simp}}[]
1293 \rail@term{\isa{intro}}[]
1295 \rail@term{\isa{elim}}[]
1297 \rail@term{\isa{dest}}[]
1299 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1300 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1306 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1309 \rail@begin{2}{\isa{}}
1310 \rail@term{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}[]
1313 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1314 \rail@nont{\isa{args}}[]
1315 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1319 \rail@nont{\isa{facts}}[]
1323 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1326 \rail@begin{2}{\isa{}}
1327 \rail@term{\hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1330 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1331 \rail@nont{\isa{args}}[]
1332 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1335 \rail@begin{2}{\isa{args}}
1337 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1338 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1339 \rail@nont{\isa{value}}[]
1341 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1344 \rail@begin{5}{\isa{facts}}
1345 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1352 \rail@term{\isa{add}}[]
1354 \rail@term{\isa{del}}[]
1356 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1358 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
1362 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1365 % FIXME try: proper clasimpmod!?
1366 % FIXME check args "value"
1370 \item \hyperlink{command.HOL.solve-direct}{\mbox{\isa{\isacommand{solve{\isaliteral{5F}{\isacharunderscore}}direct}}}} checks whether the current subgoals can
1371 be solved directly by an existing theorem. Duplicate lemmas can be detected
1374 \item \hyperlink{command.HOL.try}{\mbox{\isa{\isacommand{try}}}} attempts to prove a subgoal using a combination
1375 of standard proof methods (\isa{auto}, \isa{simp}, \isa{blast}, etc.).
1376 Additional facts supplied via \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}intro{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}},
1377 \isa{{\isaliteral{22}{\isachardoublequote}}elim{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}, and \isa{{\isaliteral{22}{\isachardoublequote}}dest{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}} are passed to the appropriate proof
1380 \item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} attempts to prove a subgoal using external
1381 automatic provers (resolution provers and SMT solvers). See the Sledgehammer
1382 manual \cite{isabelle-sledgehammer} for details.
1384 \item \hyperlink{command.HOL.sledgehammer-params}{\mbox{\isa{\isacommand{sledgehammer{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1385 \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} configuration options persistently.
1388 \end{isamarkuptext}%
1391 \isamarkupsection{Checking and refuting propositions%
1395 \begin{isamarkuptext}%
1396 Identifying incorrect propositions usually involves evaluation of
1397 particular assignments and systematic counterexample search. This
1398 is supported by the following commands.
1400 \begin{matharray}{rcl}
1401 \indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1402 \indexdef{HOL}{command}{quickcheck}\hypertarget{command.HOL.quickcheck}{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1403 \indexdef{HOL}{command}{refute}\hypertarget{command.HOL.refute}{\hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1404 \indexdef{HOL}{command}{nitpick}\hypertarget{command.HOL.nitpick}{\hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1405 \indexdef{HOL}{command}{quickcheck\_params}\hypertarget{command.HOL.quickcheck-params}{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1406 \indexdef{HOL}{command}{refute\_params}\hypertarget{command.HOL.refute-params}{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1407 \indexdef{HOL}{command}{nitpick\_params}\hypertarget{command.HOL.nitpick-params}{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
1411 \rail@begin{2}{\isa{}}
1412 \rail@term{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}[]
1415 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1416 \rail@nont{\isa{name}}[]
1417 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1421 \rail@nont{\isa{modes}}[]
1423 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1425 \rail@begin{3}{\isa{}}
1427 \rail@term{\hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}}[]
1429 \rail@term{\hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}}}[]
1431 \rail@term{\hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}}}[]
1435 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1436 \rail@nont{\isa{args}}[]
1437 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1441 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
1444 \rail@begin{3}{\isa{}}
1446 \rail@term{\hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1448 \rail@term{\hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1450 \rail@term{\hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}}}[]
1454 \rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
1455 \rail@nont{\isa{args}}[]
1456 \rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
1459 \rail@begin{2}{\isa{modes}}
1460 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1462 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1465 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1467 \rail@begin{2}{\isa{args}}
1469 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1470 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1471 \rail@nont{\isa{value}}[]
1473 \rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
1477 % FIXME check "value"
1481 \item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a
1482 term; optionally \isa{modes} can be specified, which are
1483 appended to the current print mode (see also \cite{isabelle-ref}).
1484 Internally, the evaluation is performed by registered evaluators,
1485 which are invoked sequentially until a result is returned.
1486 Alternatively a specific evaluator can be selected using square
1487 brackets; typical evaluators use the current set of code equations
1488 to normalize and include \isa{simp} for fully symbolic evaluation
1489 using the simplifier, \isa{nbe} for \emph{normalization by evaluation}
1490 and \emph{code} for code generation in SML.
1492 \item \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} tests the current goal for
1493 counterexamples using a series of assignments for its
1494 free variables; by default the first subgoal is tested, an other
1495 can be selected explicitly using an optional goal index.
1496 Assignments can be chosen exhausting the search space upto a given
1497 size or using a fixed number of random assignments in the search space.
1498 By default, quickcheck uses exhaustive testing.
1499 A number of configuration options are supported for
1500 \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}}, notably:
1504 \item[\isa{tester}] specifies how to explore the search space
1505 (e.g. exhaustive or random).
1506 An unknown configuration option is treated as an argument to tester,
1507 making \isa{{\isaliteral{22}{\isachardoublequote}}tester\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{22}{\isachardoublequote}}} optional.
1508 \item[\isa{size}] specifies the maximum size of the search space
1509 for assignment values.
1511 \item[\isa{eval}] takes a term or a list of terms and evaluates
1512 these terms under the variable assignment found by quickcheck.
1514 \item[\isa{iterations}] sets how many sets of assignments are
1515 generated for each particular size.
1517 \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in
1518 structured proofs should be ignored.
1520 \item[\isa{timeout}] sets the time limit in seconds.
1522 \item[\isa{default{\isaliteral{5F}{\isacharunderscore}}type}] sets the type(s) generally used to
1523 instantiate type variables.
1525 \item[\isa{report}] if set quickcheck reports how many tests
1526 fulfilled the preconditions.
1528 \item[\isa{quiet}] if not set quickcheck informs about the
1529 current size for assignment values.
1531 \item[\isa{expect}] can be used to check if the user's
1532 expectation was met (\isa{no{\isaliteral{5F}{\isacharunderscore}}expectation}, \isa{no{\isaliteral{5F}{\isacharunderscore}}counterexample}, or \isa{counterexample}).
1536 These option can be given within square brackets.
1538 \item \hyperlink{command.HOL.quickcheck-params}{\mbox{\isa{\isacommand{quickcheck{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1539 \hyperlink{command.HOL.quickcheck}{\mbox{\isa{\isacommand{quickcheck}}}} configuration options persistently.
1541 \item \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} tests the current goal for
1542 counterexamples using a reduction to SAT. The following configuration
1543 options are supported:
1547 \item[\isa{minsize}] specifies the minimum size (cardinality) of the
1548 models to search for.
1550 \item[\isa{maxsize}] specifies the maximum size (cardinality) of the
1551 models to search for. Nonpositive values mean $\infty$.
1553 \item[\isa{maxvars}] specifies the maximum number of Boolean variables
1554 to use when transforming the term into a propositional formula.
1555 Nonpositive values mean $\infty$.
1557 \item[\isa{satsolver}] specifies the SAT solver to use.
1559 \item[\isa{no{\isaliteral{5F}{\isacharunderscore}}assms}] specifies whether assumptions in
1560 structured proofs should be ignored.
1562 \item[\isa{maxtime}] sets the time limit in seconds.
1564 \item[\isa{expect}] can be used to check if the user's
1565 expectation was met (\isa{genuine}, \isa{potential},
1566 \isa{none}, or \isa{unknown}).
1570 These option can be given within square brackets.
1572 \item \hyperlink{command.HOL.refute-params}{\mbox{\isa{\isacommand{refute{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1573 \hyperlink{command.HOL.refute}{\mbox{\isa{\isacommand{refute}}}} configuration options persistently.
1575 \item \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} tests the current goal for counterexamples
1576 using a reduction to first-order relational logic. See the Nitpick manual
1577 \cite{isabelle-nitpick} for details.
1579 \item \hyperlink{command.HOL.nitpick-params}{\mbox{\isa{\isacommand{nitpick{\isaliteral{5F}{\isacharunderscore}}params}}}} changes
1580 \hyperlink{command.HOL.nitpick}{\mbox{\isa{\isacommand{nitpick}}}} configuration options persistently.
1583 \end{isamarkuptext}%
1586 \isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%
1590 \begin{isamarkuptext}%
1591 The following tools of Isabelle/HOL support cases analysis and
1592 induction in unstructured tactic scripts; see also
1593 \secref{sec:cases-induct} for proper Isar versions of similar ideas.
1595 \begin{matharray}{rcl}
1596 \indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
1597 \indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
1598 \indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
1599 \indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
1603 \rail@begin{2}{\isa{}}
1604 \rail@term{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1607 \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
1609 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1612 \rail@nont{\isa{rule}}[]
1615 \rail@begin{3}{\isa{}}
1616 \rail@term{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}}}[]
1619 \rail@nont{\hyperlink{syntax.goalspec}{\mbox{\isa{goalspec}}}}[]
1624 \rail@nont{\hyperlink{syntax.insts}{\mbox{\isa{insts}}}}[]
1626 \rail@cterm{\isa{\isakeyword{and}}}[]
1631 \rail@nont{\isa{rule}}[]
1634 \rail@begin{3}{\isa{}}
1635 \rail@term{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}}}[]
1637 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1642 \rail@term{\isa{\isakeyword{for}}}[]
1644 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1649 \rail@begin{3}{\isa{}}
1650 \rail@term{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}}}[]
1654 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1657 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
1661 \rail@cterm{\isa{\isakeyword{and}}}[]
1664 \rail@begin{1}{\isa{rule}}
1665 \rail@term{\isa{rule}}[]
1666 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1667 \rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
1674 \item \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} admit
1675 to reason about inductive types. Rules are selected according to
1676 the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}}
1677 attributes, cf.\ \secref{sec:cases-induct}. The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.
1679 These unstructured tactics feature both goal addressing and dynamic
1680 instantiation. Note that named rule cases are \emph{not} provided
1681 as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof
1682 methods (see \secref{sec:cases-induct}). Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isaliteral{5F}{\isacharunderscore}}tac}}} does not handle structured rule
1683 statements, only the compact object-logic conclusion of the subgoal
1686 \item \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}} provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted
1689 While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}} is a proof method to apply the
1690 result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}}}} provides case split theorems at the theory level
1691 for later use. The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isaliteral{5F}{\isacharunderscore}}cases}}} method allows to specify a list of variables that should
1692 be generalized before applying the resulting rule.
1695 \end{isamarkuptext}%
1698 \isamarkupsection{Executable code%
1702 \begin{isamarkuptext}%
1703 For validation purposes, it is often useful to \emph{execute}
1704 specifications. In principle, execution could be simulated by
1705 Isabelle's inference kernel, i.e. by a combination of resolution and
1706 simplification. Unfortunately, this approach is rather inefficient.
1707 A more efficient way of executing specifications is to translate
1708 them into a functional programming language such as ML.
1710 Isabelle provides two generic frameworks to support code generation
1711 from executable specifications. Isabelle/HOL instantiates these
1712 mechanisms in a way that is amenable to end-user applications.%
1713 \end{isamarkuptext}%
1716 \isamarkupsubsection{The new code generator (F. Haftmann)%
1720 \begin{isamarkuptext}%
1721 This framework generates code from functional programs
1722 (including overloading using type classes) to SML \cite{SML}, OCaml
1723 \cite{OCaml}, Haskell \cite{haskell-revised-report} and Scala
1724 \cite{scala-overview-tech-report}. Conceptually, code generation is
1725 split up in three steps: \emph{selection} of code theorems,
1726 \emph{translation} into an abstract executable view and
1727 \emph{serialization} to a specific \emph{target language}.
1728 Inductive specifications can be executed using the predicate
1729 compiler which operates within HOL. See \cite{isabelle-codegen} for
1732 \begin{matharray}{rcl}
1733 \indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1734 \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
1735 \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1736 \indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1737 \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1738 \indexdef{HOL}{attribute}{code\_inline}\hypertarget{attribute.HOL.code-inline}{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}} & : & \isa{attribute} \\
1739 \indexdef{HOL}{attribute}{code\_post}\hypertarget{attribute.HOL.code-post}{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}} & : & \isa{attribute} \\
1740 \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1741 \indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1742 \indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
1743 \indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1744 \indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1745 \indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1746 \indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1747 \indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1748 \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1749 \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1750 \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
1751 \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}}
1755 \rail@begin{11}{\isa{}}
1756 \rail@term{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
1758 \rail@nont{\isa{constexpr}}[]
1765 \rail@term{\isa{\isakeyword{in}}}[]
1766 \rail@nont{\isa{target}}[]
1769 \rail@term{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}[]
1770 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1775 \rail@term{\isa{\isakeyword{file}}}[]
1777 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1779 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
1784 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1785 \rail@nont{\isa{args}}[]
1786 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1792 \rail@begin{1}{\isa{const}}
1793 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1795 \rail@begin{3}{\isa{constexpr}}
1797 \rail@nont{\isa{const}}[]
1799 \rail@term{\isa{name{\isaliteral{2E}{\isachardot}}{\isaliteral{5F}{\isacharunderscore}}}}[]
1801 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
1804 \rail@begin{1}{\isa{typeconstructor}}
1805 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1807 \rail@begin{1}{\isa{class}}
1808 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
1810 \rail@begin{4}{\isa{target}}
1812 \rail@term{\isa{SML}}[]
1814 \rail@term{\isa{OCaml}}[]
1816 \rail@term{\isa{Haskell}}[]
1818 \rail@term{\isa{Scala}}[]
1821 \rail@begin{4}{\isa{}}
1822 \rail@term{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}}[]
1826 \rail@term{\isa{del}}[]
1828 \rail@term{\isa{abstype}}[]
1830 \rail@term{\isa{abstract}}[]
1834 \rail@begin{2}{\isa{}}
1835 \rail@term{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}}}[]
1837 \rail@nont{\isa{const}}[]
1841 \rail@begin{2}{\isa{}}
1842 \rail@term{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}[]
1844 \rail@nont{\isa{const}}[]
1848 \rail@begin{2}{\isa{}}
1849 \rail@term{\hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}}}[]
1852 \rail@term{\isa{del}}[]
1855 \rail@begin{2}{\isa{}}
1856 \rail@term{\hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}}}[]
1859 \rail@term{\isa{del}}[]
1862 \rail@begin{3}{\isa{}}
1863 \rail@term{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
1867 \rail@nont{\isa{constexpr}}[]
1872 \rail@begin{3}{\isa{}}
1873 \rail@term{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
1877 \rail@nont{\isa{constexpr}}[]
1882 \rail@begin{7}{\isa{}}
1883 \rail@term{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}}}[]
1885 \rail@nont{\isa{const}}[]
1887 \rail@cterm{\isa{\isakeyword{and}}}[]
1891 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1892 \rail@nont{\isa{target}}[]
1896 \rail@nont{\isa{syntax}}[]
1899 \rail@cterm{\isa{\isakeyword{and}}}[]
1901 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1905 \rail@begin{7}{\isa{}}
1906 \rail@term{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
1908 \rail@nont{\isa{typeconstructor}}[]
1910 \rail@cterm{\isa{\isakeyword{and}}}[]
1914 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1915 \rail@nont{\isa{target}}[]
1919 \rail@nont{\isa{syntax}}[]
1922 \rail@cterm{\isa{\isakeyword{and}}}[]
1924 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1928 \rail@begin{9}{\isa{}}
1929 \rail@term{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}}}[]
1931 \rail@nont{\isa{class}}[]
1933 \rail@cterm{\isa{\isakeyword{and}}}[]
1937 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1938 \rail@nont{\isa{target}}[]
1943 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1946 \rail@cterm{\isa{\isakeyword{and}}}[]
1948 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1952 \rail@begin{7}{\isa{}}
1953 \rail@term{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}}}[]
1955 \rail@nont{\isa{typeconstructor}}[]
1956 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
1957 \rail@nont{\isa{class}}[]
1959 \rail@cterm{\isa{\isakeyword{and}}}[]
1963 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
1964 \rail@nont{\isa{target}}[]
1968 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
1971 \rail@cterm{\isa{\isakeyword{and}}}[]
1973 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
1977 \rail@begin{2}{\isa{}}
1978 \rail@term{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}}}[]
1979 \rail@nont{\isa{target}}[]
1981 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1985 \rail@begin{1}{\isa{}}
1986 \rail@term{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}}}[]
1987 \rail@nont{\isa{const}}[]
1988 \rail@nont{\isa{const}}[]
1989 \rail@nont{\isa{target}}[]
1991 \rail@begin{2}{\isa{}}
1992 \rail@term{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}}}[]
1993 \rail@nont{\isa{target}}[]
1994 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1996 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
1998 \rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
2001 \rail@begin{2}{\isa{}}
2002 \rail@term{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}}}[]
2003 \rail@nont{\isa{target}}[]
2005 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2006 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2010 \rail@begin{11}{\isa{}}
2011 \rail@term{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}}}[]
2012 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2016 \rail@term{\isa{\isakeyword{datatypes}}}[]
2017 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2018 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
2020 \rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
2024 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2026 \rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
2029 \rail@cterm{\isa{\isakeyword{and}}}[]
2036 \rail@term{\isa{\isakeyword{functions}}}[]
2038 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2044 \rail@term{\isa{\isakeyword{file}}}[]
2045 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2048 \rail@begin{4}{\isa{syntax}}
2050 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2053 \rail@term{\isa{\isakeyword{infix}}}[]
2055 \rail@term{\isa{\isakeyword{infixl}}}[]
2057 \rail@term{\isa{\isakeyword{infixr}}}[]
2059 \rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
2060 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2068 \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isaliteral{5F}{\isacharunderscore}}code}}}} generates code for a given list
2069 of constants in the specified target language(s). If no
2070 serialization instruction is given, only abstract code is generated
2073 Constants may be specified by giving them literally, referring to
2074 all executable contants within a certain theory by giving \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{2E}{\isachardot}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, or referring to \emph{all} executable constants currently
2075 available by giving \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}.
2077 By default, for each involved theory one corresponding name space
2078 module is generated. Alternativly, a module name may be specified
2079 after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isaliteral{5F}{\isacharunderscore}}name}}}} keyword; then \emph{all} code is
2080 placed in this module.
2082 For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
2083 refers to a single file; for \emph{Haskell}, it refers to a whole
2084 directory, where code is generated in multiple files reflecting the
2085 module hierarchy. Omitting the file specification denotes standard
2088 Serializers take an optional list of arguments in parentheses. For
2089 \emph{SML} and \emph{OCaml}, ``\isa{no{\isaliteral{5F}{\isacharunderscore}}signatures}`` omits
2090 explicit module signatures.
2092 For \emph{Haskell} a module name prefix may be given using the
2093 ``\isa{{\isaliteral{22}{\isachardoublequote}}root{\isaliteral{3A}{\isacharcolon}}{\isaliteral{22}{\isachardoublequote}}}'' argument; ``\isa{string{\isaliteral{5F}{\isacharunderscore}}classes}'' adds a
2094 ``\verb|deriving (Read, Show)|'' clause to each appropriate
2095 datatype declaration.
2097 \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
2098 ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' deselects) a code equation for code generation.
2099 Usually packages introducing code equations provide a reasonable
2100 default setup for selection. Variants \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstype{\isaliteral{22}{\isachardoublequote}}} and
2101 \isa{{\isaliteral{22}{\isachardoublequote}}code\ abstract{\isaliteral{22}{\isachardoublequote}}} declare abstract datatype certificates or
2102 code equations on abstract datatype representations respectively.
2104 \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}abort}}}} declares constants which are not
2105 required to have a definition by means of code equations; if needed
2106 these are implemented by program abort instead.
2108 \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}} specifies a constructor set
2111 \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}} gives an overview on
2112 selected code equations and code generator datatypes.
2114 \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}inline}}} declares (or with option
2115 ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) inlining theorems which are applied as
2116 rewrite rules to any code equation during preprocessing.
2118 \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isaliteral{5F}{\isacharunderscore}}post}}} declares (or with option ``\isa{{\isaliteral{22}{\isachardoublequote}}del{\isaliteral{22}{\isachardoublequote}}}'' removes) theorems which are applied as rewrite rules to any
2119 result of an evaluation.
2121 \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codeproc}}}} prints the setup of the code
2122 generator preprocessor.
2124 \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}thms}}}} prints a list of theorems
2125 representing the corresponding program containing all given
2126 constants after preprocessing.
2128 \item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}deps}}}} visualizes dependencies of
2129 theorems representing the corresponding program containing all given
2130 constants after preprocessing.
2132 \item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}const}}}} associates a list of constants
2133 with target-specific serializations; omitting a serialization
2134 deletes an existing serialization.
2136 \item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}type}}}} associates a list of type
2137 constructors with target-specific serializations; omitting a
2138 serialization deletes an existing serialization.
2140 \item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}class}}}} associates a list of classes
2141 with target-specific class names; omitting a serialization deletes
2142 an existing serialization. This applies only to \emph{Haskell}.
2144 \item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}instance}}}} declares a list of type
2145 constructor / class instance relations as ``already present'' for a
2146 given target. Omitting a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' deletes an existing
2147 ``already present'' declaration. This applies only to
2150 \item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reserved}}}} declares a list of names as
2151 reserved for a given target, preventing it to be shadowed by any
2154 \item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}monad}}}} provides an auxiliary mechanism
2155 to generate monadic code for Haskell.
2157 \item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}include}}}} adds arbitrary named content
2158 (``include'') to generated code. A ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' as last argument
2159 will remove an already added ``include''.
2161 \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}modulename}}}} declares aliasings from one
2162 module name onto another.
2164 \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} without a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}''
2165 argument compiles code into the system runtime environment and
2166 modifies the code generator setup that future invocations of system
2167 runtime code generation referring to one of the ``\isa{{\isaliteral{22}{\isachardoublequote}}datatypes{\isaliteral{22}{\isachardoublequote}}}'' or ``\isa{{\isaliteral{22}{\isachardoublequote}}functions{\isaliteral{22}{\isachardoublequote}}}'' entities use these precompiled
2168 entities. With a ``\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}'' argument, the corresponding code
2169 is generated into that specified file without modifying the code
2173 \end{isamarkuptext}%
2176 \isamarkupsubsection{The old code generator (S. Berghofer)%
2180 \begin{isamarkuptext}%
2181 This framework generates code from both functional and
2182 relational programs to SML, as explained below.
2184 \begin{matharray}{rcl}
2185 \indexdef{}{command}{code\_module}\hypertarget{command.code-module}{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2186 \indexdef{}{command}{code\_library}\hypertarget{command.code-library}{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2187 \indexdef{}{command}{consts\_code}\hypertarget{command.consts-code}{\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2188 \indexdef{}{command}{types\_code}\hypertarget{command.types-code}{\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
2189 \indexdef{}{attribute}{code}\hypertarget{attribute.code}{\hyperlink{attribute.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
2193 \rail@begin{11}{\isa{}}
2195 \rail@term{\hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}}[]
2197 \rail@term{\hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}}[]
2201 \rail@nont{\isa{modespec}}[]
2205 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2210 \rail@term{\isa{\isakeyword{file}}}[]
2211 \rail@nont{\isa{name}}[]
2215 \rail@term{\isa{\isakeyword{imports}}}[]
2217 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2222 \rail@term{\isa{\isakeyword{contains}}}[]
2225 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2226 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
2227 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2232 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2237 \rail@begin{2}{\isa{modespec}}
2238 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
2241 \rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2243 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
2245 \rail@begin{2}{\isa{}}
2246 \rail@term{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
2248 \rail@nont{\isa{codespec}}[]
2252 \rail@begin{2}{\isa{codespec}}
2253 \rail@nont{\isa{const}}[]
2254 \rail@nont{\isa{template}}[]
2257 \rail@nont{\isa{attachment}}[]
2260 \rail@begin{2}{\isa{}}
2261 \rail@term{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}}}[]
2263 \rail@nont{\isa{tycodespec}}[]
2267 \rail@begin{2}{\isa{tycodespec}}
2268 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2269 \rail@nont{\isa{template}}[]
2272 \rail@nont{\isa{attachment}}[]
2275 \rail@begin{1}{\isa{const}}
2276 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2278 \rail@begin{1}{\isa{template}}
2279 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
2280 \rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
2281 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
2283 \rail@begin{2}{\isa{attachment}}
2284 \rail@term{\isa{attach}}[]
2287 \rail@nont{\isa{modespec}}[]
2289 \rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]
2290 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
2291 \rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
2293 \rail@begin{2}{\isa{}}
2294 \rail@term{\hyperlink{attribute.code}{\mbox{\isa{code}}}}[]
2297 \rail@nont{\isa{name}}[]
2301 \end{isamarkuptext}%
2304 \isamarkupsubsubsection{Invoking the code generator%
2308 \begin{isamarkuptext}%
2309 The code generator is invoked via the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}}
2310 and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}} commands, which correspond to
2311 \emph{incremental} and \emph{modular} code generation, respectively.
2315 \item [Modular] For each theory, an ML structure is generated,
2316 containing the code generated from the constants defined in this
2319 \item [Incremental] All the generated code is emitted into the same
2320 structure. This structure may import code from previously generated
2321 structures, which can be specified via \hyperlink{keyword.imports}{\mbox{\isa{\isakeyword{imports}}}}.
2322 Moreover, the generated structure may also be referred to in later
2323 invocations of the code generator.
2327 After the \hyperlink{command.code-module}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}}}} and \hyperlink{command.code-library}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}library}}}}
2328 keywords, the user may specify an optional list of ``modes'' in
2329 parentheses. These can be used to instruct the code generator to
2330 emit additional code for special purposes, e.g.\ functions for
2331 converting elements of generated datatypes to Isabelle terms, or
2332 test data generators. The list of modes is followed by a module
2333 name. The module name is optional for modular code generation, but
2334 must be specified for incremental code generation.
2336 The code can either be written to a file, in which case a file name
2337 has to be specified after the \hyperlink{keyword.file}{\mbox{\isa{\isakeyword{file}}}} keyword, or be loaded
2338 directly into Isabelle's ML environment. In the latter case, the
2339 \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} theory command can be used to inspect the results
2340 interactively, for example.
2342 The terms from which to generate code can be specified after the
2343 \hyperlink{keyword.contains}{\mbox{\isa{\isakeyword{contains}}}} keyword, either as a list of bindings, or just
2344 as a list of terms. In the latter case, the code generator just
2345 produces code for all constants and types occuring in the term, but
2346 does not bind the compiled terms to ML identifiers.
2348 Here is an example:%
2349 \end{isamarkuptext}%
2351 \isacommand{code{\isaliteral{5F}{\isacharunderscore}}module}\isamarkupfalse%
2353 \ \ \isakeyword{contains}\ test\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}foldl\ op\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{3}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{4}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{5}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
2354 \begin{isamarkuptext}%
2355 \noindent This binds the result of compiling the given term to
2356 the ML identifier \verb|Test.test|.%
2357 \end{isamarkuptext}%
2365 \isacommand{ML}\isamarkupfalse%
2366 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\ %
2370 \ {\isaliteral{28}{\isacharparenleft}}Test{\isaliteral{2E}{\isachardot}}test\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
2378 \isamarkupsubsubsection{Configuring the code generator%
2382 \begin{isamarkuptext}%
2383 When generating code for a complex term, the code generator
2384 recursively calls itself for all subterms. When it arrives at a
2385 constant, the default strategy of the code generator is to look up
2386 its definition and try to generate code for it. Constants which
2387 have no definitions that are immediately executable, may be
2388 associated with a piece of ML code manually using the \indexref{}{command}{consts\_code}\hyperlink{command.consts-code}{\mbox{\isa{\isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}}}} command. It takes a list whose elements consist of a
2389 constant (given in usual term syntax -- an explicit type constraint
2390 accounts for overloading), and a mixfix template describing the ML
2391 code. The latter is very much the same as the mixfix templates used
2392 when declaring new constants. The most notable difference is that
2393 terms may be included in the ML template using antiquotation
2394 brackets \verb|{|\verb|*|~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}~\verb|*|\verb|}|.
2396 A similar mechanism is available for types: \indexref{}{command}{types\_code}\hyperlink{command.types-code}{\mbox{\isa{\isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}}}} associates type constructors with specific ML code.
2398 For example, the following declarations copied from \verb|~~/src/HOL/Product_Type.thy| describe how the product type of
2399 Isabelle/HOL should be compiled to ML.%
2400 \end{isamarkuptext}%
2402 \isacommand{typedecl}\isamarkupfalse%
2403 \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod\isanewline
2404 \isacommand{consts}\isamarkupfalse%
2405 \ Pair\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ prod{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2407 \isacommand{types{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
2408 \ prod\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
2409 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
2410 \ Pair\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{2F}{\isacharslash}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
2411 \begin{isamarkuptext}%
2412 Sometimes, the code associated with a constant or type may
2413 need to refer to auxiliary functions, which have to be emitted when
2414 the constant is used. Code for such auxiliary functions can be
2415 declared using \hyperlink{keyword.attach}{\mbox{\isa{\isakeyword{attach}}}}. For example, the \isa{wfrec}
2416 function can be implemented as follows:%
2417 \end{isamarkuptext}%
2419 \isacommand{consts{\isaliteral{5F}{\isacharunderscore}}code}\isamarkupfalse%
2420 \ wfrec\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}wfrec{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ \ \isanewline
2421 \ \ \isakeyword{attach}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\ fun\ wfrec\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}wfrec\ f{\isaliteral{29}{\isacharparenright}}\ x\ {\isaliteral{2A7D}{\isacharverbatimclose}}%
2422 \begin{isamarkuptext}%
2423 If the code containing a call to \isa{wfrec} resides in an
2424 ML structure different from the one containing the function
2425 definition attached to \isa{wfrec}, the name of the ML structure
2426 (followed by a ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2E}{\isachardot}}{\isaliteral{22}{\isachardoublequote}}}'') is inserted in place of ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6D6F64756C653E}{\isasymmodule}}{\isaliteral{22}{\isachardoublequote}}}'' in the above template. The ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}{\isaliteral{22}{\isachardoublequote}}}'' means that
2427 the code generator should ignore the first argument of \isa{wfrec}, i.e.\ the termination relation, which is usually not
2430 \medskip Another possibility of configuring the code generator is to
2431 register theorems to be used for code generation. Theorems can be
2432 registered via the \hyperlink{attribute.code}{\mbox{\isa{code}}} attribute. It takes an optional
2433 name as an argument, which indicates the format of the
2434 theorem. Currently supported formats are equations (this is the
2435 default when no name is specified) and horn clauses (this is
2436 indicated by the name \texttt{ind}). The left-hand sides of
2437 equations may only contain constructors and distinct variables,
2438 whereas horn clauses must have the same format as introduction rules
2439 of inductive definitions.
2441 The following example specifies three equations from which to
2442 generate code for \isa{{\isaliteral{22}{\isachardoublequote}}op\ {\isaliteral{3C}{\isacharless}}{\isaliteral{22}{\isachardoublequote}}} on natural numbers (see also
2443 \verb|~~/src/HOL/Nat.thy|).%
2444 \end{isamarkuptext}%
2446 \isacommand{lemma}\isamarkupfalse%
2447 \ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}Suc\ m\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{3C}{\isacharless}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2448 \ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}n{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
2449 \ \ \isakeyword{and}\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}%
2455 \isacommand{by}\isamarkupfalse%
2456 \ simp{\isaliteral{5F}{\isacharunderscore}}all%
2464 \isamarkupsubsubsection{Specific HOL code generators%
2468 \begin{isamarkuptext}%
2469 The basic code generator framework offered by Isabelle/Pure
2470 has already been extended with additional code generators for
2471 specific HOL constructs. These include datatypes, recursive
2472 functions and inductive relations. The code generator for inductive
2473 relations can handle expressions of the form \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ t\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ r{\isaliteral{22}{\isachardoublequote}}}, where \isa{{\isaliteral{22}{\isachardoublequote}}r{\isaliteral{22}{\isachardoublequote}}} is an inductively defined relation. If at
2474 least one of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} is a dummy pattern ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{22}{\isachardoublequote}}}'',
2475 the above expression evaluates to a sequence of possible answers. If
2476 all of the \isa{{\isaliteral{22}{\isachardoublequote}}t\isaliteral{5C3C5E7375623E}{}\isactrlsub i{\isaliteral{22}{\isachardoublequote}}} are proper terms, the expression evaluates
2481 % theory Test = Lambda:
2485 % test1 = "Abs (Var 0) \(\circ\) Var 0 -> Var 0"
2486 % test2 = "Abs (Abs (Var 0 \(\circ\) Var 0) \(\circ\) (Abs (Var 0) \(\circ\) Var 0)) -> _"
2488 %In the above example, \texttt{Test.test1} evaluates to the boolean
2489 %value \texttt{true}, whereas \texttt{Test.test2} is a sequence whose
2490 %elements can be inspected using \texttt{Seq.pull} or similar functions.
2492 %ML \{* Seq.pull Test.test2 *\} -- \{* This is the first answer *\}
2493 %ML \{* Seq.pull (snd (the it)) *\} -- \{* This is the second answer *\}
2496 \medskip The theory underlying the HOL code generator is described
2497 more detailed in \cite{Berghofer-Nipkow:2002}. More examples that
2498 illustrate the usage of the code generator can be found e.g.\ in
2499 \verb|~~/src/HOL/MicroJava/J/JListExample.thy| and \verb|~~/src/HOL/MicroJava/JVM/JVMListExample.thy|.%
2500 \end{isamarkuptext}%
2503 \isamarkupsection{Definition by specification \label{sec:hol-specification}%
2507 \begin{isamarkuptext}%
2508 \begin{matharray}{rcl}
2509 \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
2510 \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
2514 \rail@begin{6}{\isa{}}
2516 \rail@term{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}}[]
2518 \rail@term{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}}[]
2520 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
2522 \rail@nont{\isa{decl}}[]
2525 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
2530 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
2532 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[]
2536 \rail@begin{2}{\isa{decl}}
2539 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2540 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
2542 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2543 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
2544 \rail@term{\isa{\isakeyword{overloaded}}}[]
2547 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
2555 \item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}decls\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} sets up a
2556 goal stating the existence of terms with the properties specified to
2557 hold for the constants given in \isa{decls}. After finishing the
2558 proof, the theory will be augmented with definitions for the given
2559 constants, as well as with theorems stating the properties for these
2562 \item \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}decls\ {\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{22}{\isachardoublequote}}} sets up
2563 a goal stating the existence of terms with the properties specified
2564 to hold for the constants given in \isa{decls}. After finishing
2565 the proof, the theory will be augmented with axioms expressing the
2566 properties given in the first place.
2568 \item \isa{decl} declares a constant to be defined by the
2569 specification given. The definition for the constant \isa{c} is
2570 bound to the name \isa{c{\isaliteral{5F}{\isacharunderscore}}def} unless a theorem name is given in
2571 the declaration. Overloaded constants should be declared as such.
2575 Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\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
2576 construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}} does introduce axioms, but only after the
2577 user has explicitly proven it to be safe. A practical issue must be
2578 considered, though: After introducing two constants with the same
2579 properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
2580 that the two constants are, in fact, equal. If this might be a
2581 problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isaliteral{5F}{\isacharunderscore}}specification}}}}.%
2582 \end{isamarkuptext}%
2590 \isacommand{end}\isamarkupfalse%
2600 %%% Local Variables:
2602 %%% TeX-master: "root"