26840
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{HOL{\isacharunderscore}Specific}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
\isanewline
|
|
7 |
\isanewline
|
|
8 |
%
|
|
9 |
\endisadelimtheory
|
|
10 |
%
|
|
11 |
\isatagtheory
|
|
12 |
\isacommand{theory}\isamarkupfalse%
|
|
13 |
\ HOL{\isacharunderscore}Specific\isanewline
|
26849
|
14 |
\isakeyword{imports}\ Main\isanewline
|
|
15 |
\isakeyword{begin}%
|
|
16 |
\endisatagtheory
|
|
17 |
{\isafoldtheory}%
|
|
18 |
%
|
|
19 |
\isadelimtheory
|
|
20 |
%
|
|
21 |
\endisadelimtheory
|
|
22 |
%
|
26852
|
23 |
\isamarkupchapter{Isabelle/HOL \label{ch:hol}%
|
26849
|
24 |
}
|
|
25 |
\isamarkuptrue%
|
|
26 |
%
|
|
27 |
\isamarkupsection{Primitive types \label{sec:hol-typedef}%
|
|
28 |
}
|
|
29 |
\isamarkuptrue%
|
|
30 |
%
|
|
31 |
\begin{isamarkuptext}%
|
|
32 |
\begin{matharray}{rcl}
|
28788
|
33 |
\indexdef{HOL}{command}{typedecl}\hypertarget{command.HOL.typedecl}{\hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
34 |
\indexdef{HOL}{command}{typedef}\hypertarget{command.HOL.typedef}{\hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
|
26849
|
35 |
\end{matharray}
|
|
36 |
|
|
37 |
\begin{rail}
|
|
38 |
'typedecl' typespec infix?
|
|
39 |
;
|
|
40 |
'typedef' altname? abstype '=' repset
|
|
41 |
;
|
|
42 |
|
|
43 |
altname: '(' (name | 'open' | 'open' name) ')'
|
|
44 |
;
|
|
45 |
abstype: typespec infix?
|
|
46 |
;
|
|
47 |
repset: term ('morphisms' name name)?
|
|
48 |
;
|
|
49 |
\end{rail}
|
|
50 |
|
28788
|
51 |
\begin{description}
|
26849
|
52 |
|
28788
|
53 |
\item \hyperlink{command.HOL.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} is similar
|
|
54 |
to the original \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}} of Isabelle/Pure (see
|
|
55 |
\secref{sec:types-pure}), but also declares type arity \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ type{\isacharparenright}\ type{\isachardoublequote}}, making \isa{t} an actual HOL type
|
|
56 |
constructor. %FIXME check, update
|
26849
|
57 |
|
28788
|
58 |
\item \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ A{\isachardoublequote}} sets up
|
|
59 |
a goal stating non-emptiness of the set \isa{A}. After finishing
|
|
60 |
the proof, the theory will be augmented by a Gordon/HOL-style type
|
|
61 |
definition, which establishes a bijection between the representing
|
|
62 |
set \isa{A} and the new type \isa{t}.
|
26849
|
63 |
|
26902
|
64 |
Technically, \hyperlink{command.HOL.typedef}{\mbox{\isa{\isacommand{typedef}}}} defines both a type \isa{t} and a set (term constant) of the same name (an alternative base
|
26849
|
65 |
name may be given in parentheses). The injection from type to set
|
|
66 |
is called \isa{Rep{\isacharunderscore}t}, its inverse \isa{Abs{\isacharunderscore}t} (this may be
|
26902
|
67 |
changed via an explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} declaration).
|
26849
|
68 |
|
|
69 |
Theorems \isa{Rep{\isacharunderscore}t}, \isa{Rep{\isacharunderscore}t{\isacharunderscore}inverse}, and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inverse} provide the most basic characterization as a
|
|
70 |
corresponding injection/surjection pair (in both directions). Rules
|
|
71 |
\isa{Rep{\isacharunderscore}t{\isacharunderscore}inject} and \isa{Abs{\isacharunderscore}t{\isacharunderscore}inject} provide a slightly
|
|
72 |
more convenient view on the injectivity part, suitable for automated
|
26902
|
73 |
proof tools (e.g.\ in \hyperlink{attribute.simp}{\mbox{\isa{simp}}} or \hyperlink{attribute.iff}{\mbox{\isa{iff}}}
|
26895
|
74 |
declarations). Rules \isa{Rep{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Rep{\isacharunderscore}t{\isacharunderscore}induct}, and
|
|
75 |
\isa{Abs{\isacharunderscore}t{\isacharunderscore}cases}/\isa{Abs{\isacharunderscore}t{\isacharunderscore}induct} provide alternative views
|
|
76 |
on surjectivity; these are already declared as set or type rules for
|
26902
|
77 |
the generic \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} methods.
|
26849
|
78 |
|
|
79 |
An alternative name may be specified in parentheses; the default is
|
|
80 |
to use \isa{t} as indicated before. The ``\isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}''
|
|
81 |
declaration suppresses a separate constant definition for the
|
|
82 |
representing set.
|
|
83 |
|
28788
|
84 |
\end{description}
|
26849
|
85 |
|
|
86 |
Note that raw type declarations are rarely used in practice; the
|
|
87 |
main application is with experimental (or even axiomatic!) theory
|
|
88 |
fragments. Instead of primitive HOL type definitions, user-level
|
26902
|
89 |
theories usually refer to higher-level packages such as \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}} (see \secref{sec:hol-record}) or \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} (see \secref{sec:hol-datatype}).%
|
26849
|
90 |
\end{isamarkuptext}%
|
|
91 |
\isamarkuptrue%
|
|
92 |
%
|
|
93 |
\isamarkupsection{Adhoc tuples%
|
|
94 |
}
|
|
95 |
\isamarkuptrue%
|
|
96 |
%
|
|
97 |
\begin{isamarkuptext}%
|
|
98 |
\begin{matharray}{rcl}
|
28788
|
99 |
\hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{attribute} \\
|
26849
|
100 |
\end{matharray}
|
|
101 |
|
|
102 |
\begin{rail}
|
|
103 |
'split\_format' (((name *) + 'and') | ('(' 'complete' ')'))
|
|
104 |
;
|
|
105 |
\end{rail}
|
|
106 |
|
28788
|
107 |
\begin{description}
|
26849
|
108 |
|
28788
|
109 |
\item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}} puts expressions of low-level tuple types into
|
|
110 |
canonical form as specified by the arguments given; the \isa{i}-th
|
|
111 |
collection of arguments refers to occurrences in premise \isa{i}
|
|
112 |
of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all}
|
|
113 |
arguments in function applications to be represented canonically
|
|
114 |
according to their tuple type structure.
|
26849
|
115 |
|
|
116 |
Note that these operations tend to invent funny names for new local
|
|
117 |
parameters to be introduced.
|
|
118 |
|
28788
|
119 |
\end{description}%
|
26849
|
120 |
\end{isamarkuptext}%
|
|
121 |
\isamarkuptrue%
|
|
122 |
%
|
|
123 |
\isamarkupsection{Records \label{sec:hol-record}%
|
|
124 |
}
|
|
125 |
\isamarkuptrue%
|
|
126 |
%
|
|
127 |
\begin{isamarkuptext}%
|
|
128 |
In principle, records merely generalize the concept of tuples, where
|
|
129 |
components may be addressed by labels instead of just position. The
|
|
130 |
logical infrastructure of records in Isabelle/HOL is slightly more
|
|
131 |
advanced, though, supporting truly extensible record schemes. This
|
|
132 |
admits operations that are polymorphic with respect to record
|
|
133 |
extension, yielding ``object-oriented'' effects like (single)
|
|
134 |
inheritance. See also \cite{NaraschewskiW-TPHOLs98} for more
|
|
135 |
details on object-oriented verification and record subtyping in HOL.%
|
|
136 |
\end{isamarkuptext}%
|
|
137 |
\isamarkuptrue%
|
|
138 |
%
|
|
139 |
\isamarkupsubsection{Basic concepts%
|
|
140 |
}
|
|
141 |
\isamarkuptrue%
|
|
142 |
%
|
|
143 |
\begin{isamarkuptext}%
|
|
144 |
Isabelle/HOL supports both \emph{fixed} and \emph{schematic} records
|
|
145 |
at the level of terms and types. The notation is as follows:
|
|
146 |
|
|
147 |
\begin{center}
|
|
148 |
\begin{tabular}{l|l|l}
|
|
149 |
& record terms & record types \\ \hline
|
|
150 |
fixed & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}} \\
|
|
151 |
schematic & \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} &
|
|
152 |
\isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ M{\isasymrparr}{\isachardoublequote}} \\
|
|
153 |
\end{tabular}
|
|
154 |
\end{center}
|
|
155 |
|
|
156 |
\noindent The ASCII representation of \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} is \isa{{\isachardoublequote}{\isacharparenleft}{\isacharbar}\ x\ {\isacharequal}\ a\ {\isacharbar}{\isacharparenright}{\isachardoublequote}}.
|
|
157 |
|
|
158 |
A fixed record \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} has field \isa{x} of value
|
|
159 |
\isa{a} and field \isa{y} of value \isa{b}. The corresponding
|
|
160 |
type is \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharcolon}\ A{\isacharcomma}\ y\ {\isacharcolon}{\isacharcolon}\ B{\isasymrparr}{\isachardoublequote}}, assuming that \isa{{\isachardoublequote}a\ {\isacharcolon}{\isacharcolon}\ A{\isachardoublequote}}
|
|
161 |
and \isa{{\isachardoublequote}b\ {\isacharcolon}{\isacharcolon}\ B{\isachardoublequote}}.
|
|
162 |
|
|
163 |
A record scheme like \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isasymrparr}{\isachardoublequote}} contains fields
|
|
164 |
\isa{x} and \isa{y} as before, but also possibly further fields
|
|
165 |
as indicated by the ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' notation (which is actually part
|
|
166 |
of the syntax). The improper field ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' of a record
|
|
167 |
scheme is called the \emph{more part}. Logically it is just a free
|
|
168 |
variable, which is occasionally referred to as ``row variable'' in
|
|
169 |
the literature. The more part of a record scheme may be
|
|
170 |
instantiated by zero or more further components. For example, the
|
26852
|
171 |
previous scheme may get instantiated to \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ z\ {\isacharequal}\ c{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ m{\isacharprime}{\isasymrparr}{\isachardoublequote}}, where \isa{m{\isacharprime}} refers to a different more part.
|
26849
|
172 |
Fixed records are special instances of record schemes, where
|
|
173 |
``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' is properly terminated by the \isa{{\isachardoublequote}{\isacharparenleft}{\isacharparenright}\ {\isacharcolon}{\isacharcolon}\ unit{\isachardoublequote}}
|
|
174 |
element. In fact, \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isasymrparr}{\isachardoublequote}} is just an abbreviation
|
|
175 |
for \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharequal}\ a{\isacharcomma}\ y\ {\isacharequal}\ b{\isacharcomma}\ {\isasymdots}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenright}{\isasymrparr}{\isachardoublequote}}.
|
|
176 |
|
|
177 |
\medskip Two key observations make extensible records in a simply
|
|
178 |
typed language like HOL work out:
|
|
179 |
|
|
180 |
\begin{enumerate}
|
|
181 |
|
|
182 |
\item the more part is internalized, as a free term or type
|
|
183 |
variable,
|
|
184 |
|
26852
|
185 |
\item field names are externalized, they cannot be accessed within
|
|
186 |
the logic as first-class values.
|
26849
|
187 |
|
|
188 |
\end{enumerate}
|
|
189 |
|
|
190 |
\medskip In Isabelle/HOL record types have to be defined explicitly,
|
|
191 |
fixing their field names and types, and their (optional) parent
|
|
192 |
record. Afterwards, records may be formed using above syntax, while
|
|
193 |
obeying the canonical order of fields as given by their declaration.
|
|
194 |
The record package provides several standard operations like
|
|
195 |
selectors and updates. The common setup for various generic proof
|
|
196 |
tools enable succinct reasoning patterns. See also the Isabelle/HOL
|
|
197 |
tutorial \cite{isabelle-hol-book} for further instructions on using
|
|
198 |
records in practice.%
|
|
199 |
\end{isamarkuptext}%
|
|
200 |
\isamarkuptrue%
|
|
201 |
%
|
|
202 |
\isamarkupsubsection{Record specifications%
|
|
203 |
}
|
|
204 |
\isamarkuptrue%
|
|
205 |
%
|
|
206 |
\begin{isamarkuptext}%
|
|
207 |
\begin{matharray}{rcl}
|
28788
|
208 |
\indexdef{HOL}{command}{record}\hypertarget{command.HOL.record}{\hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
26849
|
209 |
\end{matharray}
|
|
210 |
|
|
211 |
\begin{rail}
|
|
212 |
'record' typespec '=' (type '+')? (constdecl +)
|
|
213 |
;
|
|
214 |
\end{rail}
|
|
215 |
|
28788
|
216 |
\begin{description}
|
26849
|
217 |
|
28788
|
218 |
\item \hyperlink{command.HOL.record}{\mbox{\isa{\isacommand{record}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}\ {\isacharplus}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}} defines extensible record type \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}},
|
26849
|
219 |
derived from the optional parent record \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} by adding new
|
|
220 |
field components \isa{{\isachardoublequote}c\isactrlsub i\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} etc.
|
|
221 |
|
|
222 |
The type variables of \isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i{\isachardoublequote}} need to be
|
|
223 |
covered by the (distinct) parameters \isa{{\isachardoublequote}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isachardoublequote}}. Type constructor \isa{t} has to be new, while \isa{{\isasymtau}} needs to specify an instance of an existing record type. At
|
|
224 |
least one new field \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} has to be specified.
|
|
225 |
Basically, field names need to belong to a unique record. This is
|
|
226 |
not a real restriction in practice, since fields are qualified by
|
|
227 |
the record name internally.
|
|
228 |
|
|
229 |
The parent record specification \isa{{\isasymtau}} is optional; if omitted
|
|
230 |
\isa{t} becomes a root record. The hierarchy of all records
|
|
231 |
declared within a theory context forms a forest structure, i.e.\ a
|
|
232 |
set of trees starting with a root record each. There is no way to
|
|
233 |
merge multiple parent records!
|
|
234 |
|
|
235 |
For convenience, \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is made a
|
|
236 |
type abbreviation for the fixed record type \isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isasymrparr}{\isachardoublequote}}, likewise is \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharcomma}\ {\isasymzeta}{\isacharparenright}\ t{\isacharunderscore}scheme{\isachardoublequote}} made an abbreviation for
|
|
237 |
\isa{{\isachardoublequote}{\isasymlparr}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}}.
|
|
238 |
|
28788
|
239 |
\end{description}%
|
26849
|
240 |
\end{isamarkuptext}%
|
|
241 |
\isamarkuptrue%
|
|
242 |
%
|
|
243 |
\isamarkupsubsection{Record operations%
|
|
244 |
}
|
|
245 |
\isamarkuptrue%
|
|
246 |
%
|
|
247 |
\begin{isamarkuptext}%
|
|
248 |
Any record definition of the form presented above produces certain
|
|
249 |
standard operations. Selectors and updates are provided for any
|
|
250 |
field, including the improper one ``\isa{more}''. There are also
|
|
251 |
cumulative record constructor functions. To simplify the
|
|
252 |
presentation below, we assume for now that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} is a root record with fields \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\isactrlsub n{\isachardoublequote}}.
|
|
253 |
|
|
254 |
\medskip \textbf{Selectors} and \textbf{updates} are available for
|
|
255 |
any field (including ``\isa{more}''):
|
|
256 |
|
|
257 |
\begin{matharray}{lll}
|
26852
|
258 |
\isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
|
|
259 |
\isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
|
26849
|
260 |
\end{matharray}
|
|
261 |
|
|
262 |
There is special syntax for application of updates: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isachardoublequote}} abbreviates term \isa{{\isachardoublequote}x{\isacharunderscore}update\ a\ r{\isachardoublequote}}. Further notation for
|
|
263 |
repeated updates is also available: \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isasymrparr}{\isasymlparr}y\ {\isacharcolon}{\isacharequal}\ b{\isasymrparr}{\isasymlparr}z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}} may be written \isa{{\isachardoublequote}r{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}. Note that
|
|
264 |
because of postfix notation the order of fields shown here is
|
|
265 |
reverse than in the actual term. Since repeated updates are just
|
|
266 |
function applications, fields may be freely permuted in \isa{{\isachardoublequote}{\isasymlparr}x\ {\isacharcolon}{\isacharequal}\ a{\isacharcomma}\ y\ {\isacharcolon}{\isacharequal}\ b{\isacharcomma}\ z\ {\isacharcolon}{\isacharequal}\ c{\isasymrparr}{\isachardoublequote}}, as far as logical equality is concerned.
|
|
267 |
Thus commutativity of independent updates can be proven within the
|
|
268 |
logic for any two fields, but not as a general theorem.
|
|
269 |
|
|
270 |
\medskip The \textbf{make} operation provides a cumulative record
|
|
271 |
constructor function:
|
|
272 |
|
|
273 |
\begin{matharray}{lll}
|
26852
|
274 |
\isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
|
26849
|
275 |
\end{matharray}
|
|
276 |
|
|
277 |
\medskip We now reconsider the case of non-root records, which are
|
|
278 |
derived of some parent. In general, the latter may depend on
|
|
279 |
another parent as well, resulting in a list of \emph{ancestor
|
|
280 |
records}. Appending the lists of fields of all ancestors results in
|
|
281 |
a certain field prefix. The record package automatically takes care
|
|
282 |
of this by lifting operations over this context of ancestor fields.
|
|
283 |
Assuming that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub m{\isacharparenright}\ t{\isachardoublequote}} has ancestor
|
|
284 |
fields \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k\ {\isacharcolon}{\isacharcolon}\ {\isasymrho}\isactrlsub k{\isachardoublequote}},
|
|
285 |
the above record operations will get the following types:
|
|
286 |
|
26852
|
287 |
\medskip
|
|
288 |
\begin{tabular}{lll}
|
|
289 |
\isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub i{\isachardoublequote}} \\
|
|
290 |
\isa{{\isachardoublequote}c\isactrlsub i{\isacharunderscore}update{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub i\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
|
|
291 |
\isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymrho}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymrho}\isactrlsub k\ {\isasymRightarrow}\ {\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
|
|
292 |
\end{tabular}
|
|
293 |
\medskip
|
26849
|
294 |
|
26852
|
295 |
\noindent Some further operations address the extension aspect of a
|
26849
|
296 |
derived record scheme specifically: \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} produces a
|
|
297 |
record fragment consisting of exactly the new fields introduced here
|
|
298 |
(the result may serve as a more part elsewhere); \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}
|
|
299 |
takes a fixed record and adds a given more part; \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} restricts a record scheme to a fixed record.
|
|
300 |
|
26852
|
301 |
\medskip
|
|
302 |
\begin{tabular}{lll}
|
|
303 |
\isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymsigma}\isactrlsub {\isadigit{1}}\ {\isasymRightarrow}\ {\isasymdots}\ {\isasymsigma}\isactrlsub n\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
|
|
304 |
\isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymzeta}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}{\isachardoublequote}} \\
|
|
305 |
\isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} & \isa{{\isachardoublequote}{\isacharcolon}{\isacharcolon}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isacharcomma}\ {\isasymdots}\ {\isacharcolon}{\isacharcolon}\ {\isasymzeta}{\isasymrparr}\ {\isasymRightarrow}\ {\isasymlparr}\isactrlvec b\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymrho}{\isacharcomma}\ \isactrlvec c\ {\isacharcolon}{\isacharcolon}\ \isactrlvec {\isasymsigma}{\isasymrparr}{\isachardoublequote}} \\
|
|
306 |
\end{tabular}
|
|
307 |
\medskip
|
26849
|
308 |
|
|
309 |
\noindent Note that \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}} and \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}} coincide
|
|
310 |
for root records.%
|
|
311 |
\end{isamarkuptext}%
|
|
312 |
\isamarkuptrue%
|
|
313 |
%
|
|
314 |
\isamarkupsubsection{Derived rules and proof tools%
|
|
315 |
}
|
|
316 |
\isamarkuptrue%
|
|
317 |
%
|
|
318 |
\begin{isamarkuptext}%
|
|
319 |
The record package proves several results internally, declaring
|
|
320 |
these facts to appropriate proof tools. This enables users to
|
|
321 |
reason about record structures quite conveniently. Assume that
|
|
322 |
\isa{t} is a record type as specified above.
|
|
323 |
|
|
324 |
\begin{enumerate}
|
|
325 |
|
|
326 |
\item Standard conversions for selectors or updates applied to
|
|
327 |
record constructor terms are made part of the default Simplifier
|
|
328 |
context; thus proofs by reduction of basic operations merely require
|
26902
|
329 |
the \hyperlink{method.simp}{\mbox{\isa{simp}}} method without further arguments. These rules
|
26849
|
330 |
are available as \isa{{\isachardoublequote}t{\isachardot}simps{\isachardoublequote}}, too.
|
|
331 |
|
|
332 |
\item Selectors applied to updated records are automatically reduced
|
|
333 |
by an internal simplification procedure, which is also part of the
|
|
334 |
standard Simplifier setup.
|
|
335 |
|
|
336 |
\item Inject equations of a form analogous to \isa{{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x{\isacharprime}{\isacharcomma}\ y{\isacharprime}{\isacharparenright}\ {\isasymequiv}\ x\ {\isacharequal}\ x{\isacharprime}\ {\isasymand}\ y\ {\isacharequal}\ y{\isacharprime}{\isachardoublequote}} are declared to the Simplifier and Classical
|
26902
|
337 |
Reasoner as \hyperlink{attribute.iff}{\mbox{\isa{iff}}} rules. These rules are available as
|
26849
|
338 |
\isa{{\isachardoublequote}t{\isachardot}iffs{\isachardoublequote}}.
|
|
339 |
|
|
340 |
\item The introduction rule for record equality analogous to \isa{{\isachardoublequote}x\ r\ {\isacharequal}\ x\ r{\isacharprime}\ {\isasymLongrightarrow}\ y\ r\ {\isacharequal}\ y\ r{\isacharprime}\ {\isasymdots}\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ r{\isacharprime}{\isachardoublequote}} is declared to the Simplifier,
|
26902
|
341 |
and as the basic rule context as ``\hyperlink{attribute.intro}{\mbox{\isa{intro}}}\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}''.
|
26849
|
342 |
The rule is called \isa{{\isachardoublequote}t{\isachardot}equality{\isachardoublequote}}.
|
|
343 |
|
|
344 |
\item Representations of arbitrary record expressions as canonical
|
26902
|
345 |
constructor terms are provided both in \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} format (cf.\ the generic proof methods of the same name,
|
26849
|
346 |
\secref{sec:cases-induct}). Several variations are available, for
|
|
347 |
fixed records, record schemes, more parts etc.
|
|
348 |
|
|
349 |
The generic proof methods are sufficiently smart to pick the most
|
|
350 |
sensible rule according to the type of the indicated record
|
|
351 |
expression: users just need to apply something like ``\isa{{\isachardoublequote}{\isacharparenleft}cases\ r{\isacharparenright}{\isachardoublequote}}'' to a certain proof problem.
|
|
352 |
|
|
353 |
\item The derived record operations \isa{{\isachardoublequote}t{\isachardot}make{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}fields{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}extend{\isachardoublequote}}, \isa{{\isachardoublequote}t{\isachardot}truncate{\isachardoublequote}} are \emph{not}
|
|
354 |
treated automatically, but usually need to be expanded by hand,
|
|
355 |
using the collective fact \isa{{\isachardoublequote}t{\isachardot}defs{\isachardoublequote}}.
|
|
356 |
|
|
357 |
\end{enumerate}%
|
|
358 |
\end{isamarkuptext}%
|
|
359 |
\isamarkuptrue%
|
|
360 |
%
|
|
361 |
\isamarkupsection{Datatypes \label{sec:hol-datatype}%
|
|
362 |
}
|
|
363 |
\isamarkuptrue%
|
|
364 |
%
|
|
365 |
\begin{isamarkuptext}%
|
|
366 |
\begin{matharray}{rcl}
|
28788
|
367 |
\indexdef{HOL}{command}{datatype}\hypertarget{command.HOL.datatype}{\hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
368 |
\indexdef{HOL}{command}{rep\_datatype}\hypertarget{command.HOL.rep-datatype}{\hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
|
26849
|
369 |
\end{matharray}
|
|
370 |
|
|
371 |
\begin{rail}
|
|
372 |
'datatype' (dtspec + 'and')
|
|
373 |
;
|
27452
|
374 |
'rep\_datatype' ('(' (name +) ')')? (term +)
|
26849
|
375 |
;
|
|
376 |
|
|
377 |
dtspec: parname? typespec infix? '=' (cons + '|')
|
|
378 |
;
|
|
379 |
cons: name (type *) mixfix?
|
|
380 |
\end{rail}
|
|
381 |
|
28788
|
382 |
\begin{description}
|
26849
|
383 |
|
28788
|
384 |
\item \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} defines inductive datatypes in
|
26849
|
385 |
HOL.
|
|
386 |
|
28788
|
387 |
\item \hyperlink{command.HOL.rep-datatype}{\mbox{\isa{\isacommand{rep{\isacharunderscore}datatype}}}} represents existing types as
|
26849
|
388 |
inductive ones, generating the standard infrastructure of derived
|
|
389 |
concepts (primitive recursion etc.).
|
|
390 |
|
28788
|
391 |
\end{description}
|
26849
|
392 |
|
|
393 |
The induction and exhaustion theorems generated provide case names
|
|
394 |
according to the constructors involved, while parameters are named
|
|
395 |
after the types (see also \secref{sec:cases-induct}).
|
|
396 |
|
|
397 |
See \cite{isabelle-HOL} for more details on datatypes, but beware of
|
|
398 |
the old-style theory syntax being used there! Apart from proper
|
|
399 |
proof methods for case-analysis and induction, there are also
|
26907
|
400 |
emulations of ML tactics \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} available, see \secref{sec:hol-induct-tac}; these admit
|
26849
|
401 |
to refer directly to the internal structure of subgoals (including
|
|
402 |
internally bound parameters).%
|
|
403 |
\end{isamarkuptext}%
|
|
404 |
\isamarkuptrue%
|
|
405 |
%
|
|
406 |
\isamarkupsection{Recursive functions \label{sec:recursion}%
|
|
407 |
}
|
|
408 |
\isamarkuptrue%
|
|
409 |
%
|
|
410 |
\begin{isamarkuptext}%
|
|
411 |
\begin{matharray}{rcl}
|
28788
|
412 |
\indexdef{HOL}{command}{primrec}\hypertarget{command.HOL.primrec}{\hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
|
|
413 |
\indexdef{HOL}{command}{fun}\hypertarget{command.HOL.fun}{\hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
|
|
414 |
\indexdef{HOL}{command}{function}\hypertarget{command.HOL.function}{\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
|
|
415 |
\indexdef{HOL}{command}{termination}\hypertarget{command.HOL.termination}{\hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
|
26849
|
416 |
\end{matharray}
|
|
417 |
|
|
418 |
\begin{rail}
|
|
419 |
'primrec' target? fixes 'where' equations
|
|
420 |
;
|
|
421 |
equations: (thmdecl? prop + '|')
|
|
422 |
;
|
26987
|
423 |
('fun' | 'function') target? functionopts? fixes 'where' clauses
|
26849
|
424 |
;
|
|
425 |
clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
|
|
426 |
;
|
26987
|
427 |
functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
|
26849
|
428 |
;
|
|
429 |
'termination' ( term )?
|
|
430 |
\end{rail}
|
|
431 |
|
28788
|
432 |
\begin{description}
|
26849
|
433 |
|
28788
|
434 |
\item \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} defines primitive recursive
|
26849
|
435 |
functions over datatypes, see also \cite{isabelle-HOL}.
|
|
436 |
|
28788
|
437 |
\item \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} defines functions by general
|
26849
|
438 |
wellfounded recursion. A detailed description with examples can be
|
|
439 |
found in \cite{isabelle-function}. The function is specified by a
|
|
440 |
set of (possibly conditional) recursive equations with arbitrary
|
|
441 |
pattern matching. The command generates proof obligations for the
|
|
442 |
completeness and the compatibility of patterns.
|
|
443 |
|
|
444 |
The defined function is considered partial, and the resulting
|
|
445 |
simplification rules (named \isa{{\isachardoublequote}f{\isachardot}psimps{\isachardoublequote}}) and induction rule
|
|
446 |
(named \isa{{\isachardoublequote}f{\isachardot}pinduct{\isachardoublequote}}) are guarded by a generated domain
|
26902
|
447 |
predicate \isa{{\isachardoublequote}f{\isacharunderscore}dom{\isachardoublequote}}. The \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}
|
26849
|
448 |
command can then be used to establish that the function is total.
|
|
449 |
|
28788
|
450 |
\item \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} is a shorthand notation for ``\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}~\isa{{\isachardoublequote}{\isacharparenleft}sequential{\isacharparenright}{\isachardoublequote}}, followed by automated
|
|
451 |
proof attempts regarding pattern matching and termination. See
|
|
452 |
\cite{isabelle-function} for further details.
|
26849
|
453 |
|
28788
|
454 |
\item \hyperlink{command.HOL.termination}{\mbox{\isa{\isacommand{termination}}}}~\isa{f} commences a
|
26849
|
455 |
termination proof for the previously defined function \isa{f}. If
|
|
456 |
this is omitted, the command refers to the most recent function
|
|
457 |
definition. After the proof is closed, the recursive equations and
|
|
458 |
the induction principle is established.
|
|
459 |
|
28788
|
460 |
\end{description}
|
26849
|
461 |
|
|
462 |
%FIXME check
|
|
463 |
|
27452
|
464 |
Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
|
|
465 |
command accommodate
|
26849
|
466 |
reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isachardoublequote}c{\isachardot}induct{\isachardoublequote}} (where \isa{c} is the name of the function definition)
|
|
467 |
refers to a specific induction rule, with parameters named according
|
27452
|
468 |
to the user-specified equations.
|
|
469 |
For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
|
|
470 |
with structural recursion on the datatype the recursion is carried
|
|
471 |
out.
|
|
472 |
Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
|
26902
|
473 |
\hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
|
26849
|
474 |
|
|
475 |
The equations provided by these packages may be referred later as
|
|
476 |
theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)
|
|
477 |
name of the functions defined. Individual equations may be named
|
|
478 |
explicitly as well.
|
|
479 |
|
26902
|
480 |
The \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} command accepts the following
|
26849
|
481 |
options.
|
|
482 |
|
28788
|
483 |
\begin{description}
|
26849
|
484 |
|
28788
|
485 |
\item \isa{sequential} enables a preprocessor which disambiguates
|
|
486 |
overlapping patterns by making them mutually disjoint. Earlier
|
|
487 |
equations take precedence over later ones. This allows to give the
|
|
488 |
specification in a format very similar to functional programming.
|
|
489 |
Note that the resulting simplification and induction rules
|
|
490 |
correspond to the transformed specification, not the one given
|
26849
|
491 |
originally. This usually means that each equation given by the user
|
|
492 |
may result in several theroems. Also note that this automatic
|
|
493 |
transformation only works for ML-style datatype patterns.
|
|
494 |
|
28788
|
495 |
\item \isa{domintros} enables the automated generation of
|
26849
|
496 |
introduction rules for the domain predicate. While mostly not
|
|
497 |
needed, they can be helpful in some proofs about partial functions.
|
|
498 |
|
28788
|
499 |
\item \isa{tailrec} generates the unconstrained recursive
|
26849
|
500 |
equations even without a termination proof, provided that the
|
|
501 |
function is tail-recursive. This currently only works
|
|
502 |
|
28788
|
503 |
\item \isa{{\isachardoublequote}default\ d{\isachardoublequote}} allows to specify a default value for a
|
26849
|
504 |
(partial) function, which will ensure that \isa{{\isachardoublequote}f\ x\ {\isacharequal}\ d\ x{\isachardoublequote}}
|
|
505 |
whenever \isa{{\isachardoublequote}x\ {\isasymnotin}\ f{\isacharunderscore}dom{\isachardoublequote}}.
|
|
506 |
|
28788
|
507 |
\end{description}%
|
26849
|
508 |
\end{isamarkuptext}%
|
|
509 |
\isamarkuptrue%
|
|
510 |
%
|
|
511 |
\isamarkupsubsection{Proof methods related to recursive definitions%
|
|
512 |
}
|
|
513 |
\isamarkuptrue%
|
|
514 |
%
|
|
515 |
\begin{isamarkuptext}%
|
|
516 |
\begin{matharray}{rcl}
|
28788
|
517 |
\indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
|
|
518 |
\indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
|
|
519 |
\indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
|
26849
|
520 |
\end{matharray}
|
|
521 |
|
|
522 |
\begin{rail}
|
|
523 |
'relation' term
|
|
524 |
;
|
|
525 |
'lexicographic\_order' (clasimpmod *)
|
|
526 |
;
|
|
527 |
\end{rail}
|
|
528 |
|
28788
|
529 |
\begin{description}
|
26849
|
530 |
|
28788
|
531 |
\item \hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}} is a specialized method to
|
26849
|
532 |
solve goals regarding the completeness of pattern matching, as
|
26902
|
533 |
required by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} package (cf.\
|
26849
|
534 |
\cite{isabelle-function}).
|
|
535 |
|
28788
|
536 |
\item \hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}~\isa{R} introduces a termination
|
26849
|
537 |
proof using the relation \isa{R}. The resulting proof state will
|
|
538 |
contain goals expressing that \isa{R} is wellfounded, and that the
|
|
539 |
arguments of recursive calls decrease with respect to \isa{R}.
|
|
540 |
Usually, this method is used as the initial proof step of manual
|
|
541 |
termination proofs.
|
|
542 |
|
28788
|
543 |
\item \hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}} attempts a fully
|
26849
|
544 |
automated termination proof by searching for a lexicographic
|
|
545 |
combination of size measures on the arguments of the function. The
|
26902
|
546 |
method accepts the same arguments as the \hyperlink{method.auto}{\mbox{\isa{auto}}} method,
|
26849
|
547 |
which it uses internally to prove local descents. The same context
|
26902
|
548 |
modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see
|
26849
|
549 |
\secref{sec:clasimp}.
|
|
550 |
|
|
551 |
In case of failure, extensive information is printed, which can help
|
|
552 |
to analyse the situation (cf.\ \cite{isabelle-function}).
|
|
553 |
|
28788
|
554 |
\end{description}%
|
26849
|
555 |
\end{isamarkuptext}%
|
|
556 |
\isamarkuptrue%
|
|
557 |
%
|
|
558 |
\isamarkupsubsection{Old-style recursive function definitions (TFL)%
|
|
559 |
}
|
|
560 |
\isamarkuptrue%
|
|
561 |
%
|
|
562 |
\begin{isamarkuptext}%
|
26907
|
563 |
The old TFL commands \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} and \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}} for defining recursive are mostly obsolete; \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} or \hyperlink{command.HOL.fun}{\mbox{\isa{\isacommand{fun}}}} should be used instead.
|
26849
|
564 |
|
|
565 |
\begin{matharray}{rcl}
|
28788
|
566 |
\indexdef{HOL}{command}{recdef}\hypertarget{command.HOL.recdef}{\hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isacharparenright}{\isachardoublequote}} \\
|
|
567 |
\indexdef{HOL}{command}{recdef\_tc}\hypertarget{command.HOL.recdef-tc}{\hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
|
26849
|
568 |
\end{matharray}
|
|
569 |
|
|
570 |
\begin{rail}
|
|
571 |
'recdef' ('(' 'permissive' ')')? \\ name term (prop +) hints?
|
|
572 |
;
|
|
573 |
recdeftc thmdecl? tc
|
|
574 |
;
|
|
575 |
hints: '(' 'hints' (recdefmod *) ')'
|
|
576 |
;
|
|
577 |
recdefmod: (('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del') ':' thmrefs) | clasimpmod
|
|
578 |
;
|
|
579 |
tc: nameref ('(' nat ')')?
|
|
580 |
;
|
|
581 |
\end{rail}
|
|
582 |
|
28788
|
583 |
\begin{description}
|
26849
|
584 |
|
28788
|
585 |
\item \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} defines general well-founded
|
26849
|
586 |
recursive functions (using the TFL package), see also
|
|
587 |
\cite{isabelle-HOL}. The ``\isa{{\isachardoublequote}{\isacharparenleft}permissive{\isacharparenright}{\isachardoublequote}}'' option tells
|
|
588 |
TFL to recover from failed proof attempts, returning unfinished
|
|
589 |
results. The \isa{recdef{\isacharunderscore}simp}, \isa{recdef{\isacharunderscore}cong}, and \isa{recdef{\isacharunderscore}wf} hints refer to auxiliary rules to be used in the internal
|
26902
|
590 |
automated proof process of TFL. Additional \hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}
|
26849
|
591 |
declarations (cf.\ \secref{sec:clasimp}) may be given to tune the
|
|
592 |
context of the Simplifier (cf.\ \secref{sec:simplifier}) and
|
|
593 |
Classical reasoner (cf.\ \secref{sec:classical}).
|
|
594 |
|
28788
|
595 |
\item \hyperlink{command.HOL.recdef-tc}{\mbox{\isa{\isacommand{recdef{\isacharunderscore}tc}}}}~\isa{{\isachardoublequote}c\ {\isacharparenleft}i{\isacharparenright}{\isachardoublequote}} recommences the
|
26849
|
596 |
proof for leftover termination condition number \isa{i} (default
|
26902
|
597 |
1) as generated by a \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} definition of
|
26849
|
598 |
constant \isa{c}.
|
|
599 |
|
26902
|
600 |
Note that in most cases, \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} is able to finish
|
26849
|
601 |
its internal proofs without manual intervention.
|
|
602 |
|
28788
|
603 |
\end{description}
|
26849
|
604 |
|
26902
|
605 |
\medskip Hints for \hyperlink{command.HOL.recdef}{\mbox{\isa{\isacommand{recdef}}}} may be also declared
|
26849
|
606 |
globally, using the following attributes.
|
|
607 |
|
|
608 |
\begin{matharray}{rcl}
|
28788
|
609 |
\indexdef{HOL}{attribute}{recdef\_simp}\hypertarget{attribute.HOL.recdef-simp}{\hyperlink{attribute.HOL.recdef-simp}{\mbox{\isa{recdef{\isacharunderscore}simp}}}} & : & \isa{attribute} \\
|
|
610 |
\indexdef{HOL}{attribute}{recdef\_cong}\hypertarget{attribute.HOL.recdef-cong}{\hyperlink{attribute.HOL.recdef-cong}{\mbox{\isa{recdef{\isacharunderscore}cong}}}} & : & \isa{attribute} \\
|
|
611 |
\indexdef{HOL}{attribute}{recdef\_wf}\hypertarget{attribute.HOL.recdef-wf}{\hyperlink{attribute.HOL.recdef-wf}{\mbox{\isa{recdef{\isacharunderscore}wf}}}} & : & \isa{attribute} \\
|
26849
|
612 |
\end{matharray}
|
|
613 |
|
|
614 |
\begin{rail}
|
|
615 |
('recdef\_simp' | 'recdef\_cong' | 'recdef\_wf') (() | 'add' | 'del')
|
|
616 |
;
|
|
617 |
\end{rail}%
|
|
618 |
\end{isamarkuptext}%
|
|
619 |
\isamarkuptrue%
|
|
620 |
%
|
|
621 |
\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
|
|
622 |
}
|
|
623 |
\isamarkuptrue%
|
|
624 |
%
|
|
625 |
\begin{isamarkuptext}%
|
|
626 |
An \textbf{inductive definition} specifies the least predicate (or
|
|
627 |
set) \isa{R} closed under given rules: applying a rule to elements
|
|
628 |
of \isa{R} yields a result within \isa{R}. For example, a
|
|
629 |
structural operational semantics is an inductive definition of an
|
|
630 |
evaluation relation.
|
|
631 |
|
|
632 |
Dually, a \textbf{coinductive definition} specifies the greatest
|
|
633 |
predicate~/ set \isa{R} that is consistent with given rules: every
|
|
634 |
element of \isa{R} can be seen as arising by applying a rule to
|
|
635 |
elements of \isa{R}. An important example is using bisimulation
|
|
636 |
relations to formalise equivalence of processes and infinite data
|
|
637 |
structures.
|
|
638 |
|
|
639 |
\medskip The HOL package is related to the ZF one, which is
|
|
640 |
described in a separate paper,\footnote{It appeared in CADE
|
|
641 |
\cite{paulson-CADE}; a longer version is distributed with Isabelle.}
|
|
642 |
which you should refer to in case of difficulties. The package is
|
|
643 |
simpler than that of ZF thanks to implicit type-checking in HOL.
|
|
644 |
The types of the (co)inductive predicates (or sets) determine the
|
|
645 |
domain of the fixedpoint definition, and the package does not have
|
|
646 |
to use inference rules for type-checking.
|
|
647 |
|
|
648 |
\begin{matharray}{rcl}
|
28788
|
649 |
\indexdef{HOL}{command}{inductive}\hypertarget{command.HOL.inductive}{\hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
|
|
650 |
\indexdef{HOL}{command}{inductive\_set}\hypertarget{command.HOL.inductive-set}{\hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
|
|
651 |
\indexdef{HOL}{command}{coinductive}\hypertarget{command.HOL.coinductive}{\hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
|
|
652 |
\indexdef{HOL}{command}{coinductive\_set}\hypertarget{command.HOL.coinductive-set}{\hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
|
|
653 |
\indexdef{HOL}{attribute}{mono}\hypertarget{attribute.HOL.mono}{\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}}} & : & \isa{attribute} \\
|
26849
|
654 |
\end{matharray}
|
|
655 |
|
|
656 |
\begin{rail}
|
|
657 |
('inductive' | 'inductive\_set' | 'coinductive' | 'coinductive\_set') target? fixes ('for' fixes)? \\
|
|
658 |
('where' clauses)? ('monos' thmrefs)?
|
|
659 |
;
|
|
660 |
clauses: (thmdecl? prop + '|')
|
|
661 |
;
|
|
662 |
'mono' (() | 'add' | 'del')
|
|
663 |
;
|
|
664 |
\end{rail}
|
|
665 |
|
28788
|
666 |
\begin{description}
|
26849
|
667 |
|
28788
|
668 |
\item \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}} and \hyperlink{command.HOL.coinductive}{\mbox{\isa{\isacommand{coinductive}}}} define (co)inductive predicates from the
|
26902
|
669 |
introduction rules given in the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} part. The
|
|
670 |
optional \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} part contains a list of parameters of the
|
26849
|
671 |
(co)inductive predicates that remain fixed throughout the
|
26902
|
672 |
definition. The optional \hyperlink{keyword.monos}{\mbox{\isa{\isakeyword{monos}}}} section contains
|
26849
|
673 |
\emph{monotonicity theorems}, which are required for each operator
|
|
674 |
applied to a recursive set in the introduction rules. There
|
|
675 |
\emph{must} be a theorem of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}},
|
|
676 |
for each premise \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}} in an introduction rule!
|
|
677 |
|
28788
|
678 |
\item \hyperlink{command.HOL.inductive-set}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}set}}}} and \hyperlink{command.HOL.coinductive-set}{\mbox{\isa{\isacommand{coinductive{\isacharunderscore}set}}}} are wrappers for to the previous commands,
|
26849
|
679 |
allowing the definition of (co)inductive sets.
|
|
680 |
|
28788
|
681 |
\item \hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} declares monotonicity rules. These
|
26902
|
682 |
rule are involved in the automated monotonicity proof of \hyperlink{command.HOL.inductive}{\mbox{\isa{\isacommand{inductive}}}}.
|
26849
|
683 |
|
28788
|
684 |
\end{description}%
|
26849
|
685 |
\end{isamarkuptext}%
|
|
686 |
\isamarkuptrue%
|
|
687 |
%
|
|
688 |
\isamarkupsubsection{Derived rules%
|
|
689 |
}
|
|
690 |
\isamarkuptrue%
|
|
691 |
%
|
|
692 |
\begin{isamarkuptext}%
|
|
693 |
Each (co)inductive definition \isa{R} adds definitions to the
|
|
694 |
theory and also proves some theorems:
|
|
695 |
|
|
696 |
\begin{description}
|
|
697 |
|
28788
|
698 |
\item \isa{R{\isachardot}intros} is the list of introduction rules as proven
|
26849
|
699 |
theorems, for the recursive predicates (or sets). The rules are
|
|
700 |
also available individually, using the names given them in the
|
|
701 |
theory file;
|
|
702 |
|
28788
|
703 |
\item \isa{R{\isachardot}cases} is the case analysis (or elimination) rule;
|
26849
|
704 |
|
28788
|
705 |
\item \isa{R{\isachardot}induct} or \isa{R{\isachardot}coinduct} is the (co)induction
|
26849
|
706 |
rule.
|
|
707 |
|
|
708 |
\end{description}
|
|
709 |
|
|
710 |
When several predicates \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardoublequote}} are
|
|
711 |
defined simultaneously, the list of introduction rules is called
|
|
712 |
\isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}intros{\isachardoublequote}}, the case analysis rules are
|
|
713 |
called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isachardot}cases{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ R\isactrlsub n{\isachardot}cases{\isachardoublequote}}, and the list
|
|
714 |
of mutual induction rules is called \isa{{\isachardoublequote}R\isactrlsub {\isadigit{1}}{\isacharunderscore}{\isasymdots}{\isacharunderscore}R\isactrlsub n{\isachardot}inducts{\isachardoublequote}}.%
|
|
715 |
\end{isamarkuptext}%
|
|
716 |
\isamarkuptrue%
|
|
717 |
%
|
|
718 |
\isamarkupsubsection{Monotonicity theorems%
|
|
719 |
}
|
|
720 |
\isamarkuptrue%
|
|
721 |
%
|
|
722 |
\begin{isamarkuptext}%
|
|
723 |
Each theory contains a default set of theorems that are used in
|
|
724 |
monotonicity proofs. New rules can be added to this set via the
|
26902
|
725 |
\hyperlink{attribute.HOL.mono}{\mbox{\isa{mono}}} attribute. The HOL theory \isa{Inductive}
|
26849
|
726 |
shows how this is done. In general, the following monotonicity
|
|
727 |
theorems may be added:
|
|
728 |
|
|
729 |
\begin{itemize}
|
|
730 |
|
|
731 |
\item Theorems of the form \isa{{\isachardoublequote}A\ {\isasymle}\ B\ {\isasymLongrightarrow}\ M\ A\ {\isasymle}\ M\ B{\isachardoublequote}}, for proving
|
|
732 |
monotonicity of inductive definitions whose introduction rules have
|
|
733 |
premises involving terms such as \isa{{\isachardoublequote}M\ R\isactrlsub i\ t{\isachardoublequote}}.
|
|
734 |
|
|
735 |
\item Monotonicity theorems for logical operators, which are of the
|
|
736 |
general form \isa{{\isachardoublequote}{\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isacharparenleft}{\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymlongrightarrow}\ {\isasymdots}{\isachardoublequote}}. For example, in
|
|
737 |
the case of the operator \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, the corresponding theorem is
|
|
738 |
\[
|
|
739 |
\infer{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymor}\ P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}\ {\isasymor}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}}{\isa{{\isachardoublequote}P\isactrlsub {\isadigit{1}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \isa{{\isachardoublequote}P\isactrlsub {\isadigit{2}}\ {\isasymlongrightarrow}\ Q\isactrlsub {\isadigit{2}}{\isachardoublequote}}}
|
|
740 |
\]
|
|
741 |
|
|
742 |
\item De Morgan style equations for reasoning about the ``polarity''
|
|
743 |
of expressions, e.g.
|
|
744 |
\[
|
|
745 |
\isa{{\isachardoublequote}{\isasymnot}\ {\isasymnot}\ P\ {\isasymlongleftrightarrow}\ P{\isachardoublequote}} \qquad\qquad
|
|
746 |
\isa{{\isachardoublequote}{\isasymnot}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ {\isasymnot}\ Q{\isachardoublequote}}
|
|
747 |
\]
|
|
748 |
|
|
749 |
\item Equations for reducing complex operators to more primitive
|
|
750 |
ones whose monotonicity can easily be proved, e.g.
|
|
751 |
\[
|
|
752 |
\isa{{\isachardoublequote}{\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isasymlongleftrightarrow}\ {\isasymnot}\ P\ {\isasymor}\ Q{\isachardoublequote}} \qquad\qquad
|
|
753 |
\isa{{\isachardoublequote}Ball\ A\ P\ {\isasymequiv}\ {\isasymforall}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymlongrightarrow}\ P\ x{\isachardoublequote}}
|
|
754 |
\]
|
|
755 |
|
|
756 |
\end{itemize}
|
|
757 |
|
|
758 |
%FIXME: Example of an inductive definition%
|
|
759 |
\end{isamarkuptext}%
|
|
760 |
\isamarkuptrue%
|
|
761 |
%
|
|
762 |
\isamarkupsection{Arithmetic proof support%
|
|
763 |
}
|
|
764 |
\isamarkuptrue%
|
|
765 |
%
|
|
766 |
\begin{isamarkuptext}%
|
|
767 |
\begin{matharray}{rcl}
|
28788
|
768 |
\indexdef{HOL}{method}{arith}\hypertarget{method.HOL.arith}{\hyperlink{method.HOL.arith}{\mbox{\isa{arith}}}} & : & \isa{method} \\
|
|
769 |
\indexdef{HOL}{attribute}{arith\_split}\hypertarget{attribute.HOL.arith-split}{\hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}}} & : & \isa{attribute} \\
|
26849
|
770 |
\end{matharray}
|
|
771 |
|
26902
|
772 |
The \hyperlink{method.HOL.arith}{\mbox{\isa{arith}}} method decides linear arithmetic problems
|
26849
|
773 |
(on types \isa{nat}, \isa{int}, \isa{real}). Any current
|
|
774 |
facts are inserted into the goal before running the procedure.
|
|
775 |
|
26907
|
776 |
The \hyperlink{attribute.HOL.arith-split}{\mbox{\isa{arith{\isacharunderscore}split}}} attribute declares case split
|
26895
|
777 |
rules to be expanded before the arithmetic procedure is invoked.
|
26849
|
778 |
|
|
779 |
Note that a simpler (but faster) version of arithmetic reasoning is
|
|
780 |
already performed by the Simplifier.%
|
|
781 |
\end{isamarkuptext}%
|
|
782 |
\isamarkuptrue%
|
|
783 |
%
|
28603
|
784 |
\isamarkupsection{Invoking automated reasoning tools -- The Sledgehammer%
|
|
785 |
}
|
|
786 |
\isamarkuptrue%
|
|
787 |
%
|
|
788 |
\begin{isamarkuptext}%
|
|
789 |
Isabelle/HOL includes a generic \emph{ATP manager} that allows
|
|
790 |
external automated reasoning tools to crunch a pending goal.
|
|
791 |
Supported provers include E\footnote{\url{http://www.eprover.org}},
|
|
792 |
SPASS\footnote{\url{http://www.spass-prover.org/}}, and Vampire.
|
|
793 |
There is also a wrapper to invoke provers remotely via the
|
|
794 |
SystemOnTPTP\footnote{\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}}
|
|
795 |
web service.
|
|
796 |
|
|
797 |
The problem passed to external provers consists of the goal together
|
|
798 |
with a smart selection of lemmas from the current theory context.
|
|
799 |
The result of a successful proof search is some source text that
|
|
800 |
usually reconstructs the proof within Isabelle, without requiring
|
|
801 |
external provers again. The Metis
|
|
802 |
prover\footnote{\url{http://www.gilith.com/software/metis/}} that is
|
|
803 |
integrated into Isabelle/HOL is being used here.
|
|
804 |
|
|
805 |
In this mode of operation, heavy means of automated reasoning are
|
|
806 |
used as a strong relevance filter, while the main proof checking
|
|
807 |
works via explicit inferences going through the Isabelle kernel.
|
|
808 |
Moreover, rechecking Isabelle proof texts with already specified
|
|
809 |
auxiliary facts is much faster than performing fully automated
|
|
810 |
search over and over again.
|
|
811 |
|
|
812 |
\begin{matharray}{rcl}
|
28788
|
813 |
\indexdef{HOL}{command}{sledgehammer}\hypertarget{command.HOL.sledgehammer}{\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
814 |
\indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
815 |
\indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
816 |
\indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
|
29113
|
817 |
\indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
|
28788
|
818 |
\indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
|
28603
|
819 |
\end{matharray}
|
|
820 |
|
|
821 |
\begin{rail}
|
|
822 |
'sledgehammer' (nameref *)
|
|
823 |
;
|
29113
|
824 |
'atp\_messages' ('(' nat ')')?
|
28603
|
825 |
|
|
826 |
'metis' thmrefs
|
|
827 |
;
|
|
828 |
\end{rail}
|
|
829 |
|
28788
|
830 |
\begin{description}
|
28603
|
831 |
|
28788
|
832 |
\item \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}~\isa{{\isachardoublequote}prover\isactrlsub {\isadigit{1}}\ {\isasymdots}\ prover\isactrlsub n{\isachardoublequote}}
|
|
833 |
invokes the specified automated theorem provers on the first
|
|
834 |
subgoal. Provers are run in parallel, the first successful result
|
|
835 |
is displayed, and the other attempts are terminated.
|
28603
|
836 |
|
|
837 |
Provers are defined in the theory context, see also \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}. If no provers are given as arguments to \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}, the system refers to the default defined as
|
|
838 |
``ATP provers'' preference by the user interface.
|
|
839 |
|
|
840 |
There are additional preferences for timeout (default: 60 seconds),
|
|
841 |
and the maximum number of independent prover processes (default: 5);
|
|
842 |
excessive provers are automatically terminated.
|
|
843 |
|
28788
|
844 |
\item \hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}} prints the list of automated
|
28603
|
845 |
theorem provers available to the \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}}
|
|
846 |
command.
|
|
847 |
|
28788
|
848 |
\item \hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}} prints information about presently
|
28603
|
849 |
running provers, including elapsed runtime, and the remaining time
|
|
850 |
until timeout.
|
|
851 |
|
28788
|
852 |
\item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
|
28603
|
853 |
provers.
|
|
854 |
|
29113
|
855 |
\item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
|
|
856 |
by automated theorem provers. This allows to examine results that
|
|
857 |
might have got lost due to the asynchronous nature of default
|
|
858 |
\hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output.
|
|
859 |
|
28788
|
860 |
\item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
|
|
861 |
with the given facts. Metis is an automated proof tool of medium
|
|
862 |
strength, but is fully integrated into Isabelle/HOL, with explicit
|
|
863 |
inferences going through the kernel. Thus its results are
|
28603
|
864 |
guaranteed to be ``correct by construction''.
|
|
865 |
|
|
866 |
Note that all facts used with Metis need to be specified as explicit
|
|
867 |
arguments. There are no rule declarations as for other Isabelle
|
|
868 |
provers, like \hyperlink{method.blast}{\mbox{\isa{blast}}} or \hyperlink{method.fast}{\mbox{\isa{fast}}}.
|
|
869 |
|
28788
|
870 |
\end{description}%
|
28603
|
871 |
\end{isamarkuptext}%
|
|
872 |
\isamarkuptrue%
|
|
873 |
%
|
28788
|
874 |
\isamarkupsection{Unstructured case analysis and induction \label{sec:hol-induct-tac}%
|
26849
|
875 |
}
|
|
876 |
\isamarkuptrue%
|
|
877 |
%
|
|
878 |
\begin{isamarkuptext}%
|
27124
|
879 |
The following tools of Isabelle/HOL support cases analysis and
|
|
880 |
induction in unstructured tactic scripts; see also
|
|
881 |
\secref{sec:cases-induct} for proper Isar versions of similar ideas.
|
26849
|
882 |
|
|
883 |
\begin{matharray}{rcl}
|
28788
|
884 |
\indexdef{HOL}{method}{case\_tac}\hypertarget{method.HOL.case-tac}{\hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
|
|
885 |
\indexdef{HOL}{method}{induct\_tac}\hypertarget{method.HOL.induct-tac}{\hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
|
|
886 |
\indexdef{HOL}{method}{ind\_cases}\hypertarget{method.HOL.ind-cases}{\hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{method} \\
|
|
887 |
\indexdef{HOL}{command}{inductive\_cases}\hypertarget{command.HOL.inductive-cases}{\hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
|
26849
|
888 |
\end{matharray}
|
|
889 |
|
|
890 |
\begin{rail}
|
|
891 |
'case\_tac' goalspec? term rule?
|
|
892 |
;
|
|
893 |
'induct\_tac' goalspec? (insts * 'and') rule?
|
|
894 |
;
|
|
895 |
'ind\_cases' (prop +) ('for' (name +)) ?
|
|
896 |
;
|
|
897 |
'inductive\_cases' (thmdecl? (prop +) + 'and')
|
|
898 |
;
|
|
899 |
|
|
900 |
rule: ('rule' ':' thmref)
|
|
901 |
;
|
|
902 |
\end{rail}
|
|
903 |
|
28788
|
904 |
\begin{description}
|
26849
|
905 |
|
28788
|
906 |
\item \hyperlink{method.HOL.case-tac}{\mbox{\isa{case{\isacharunderscore}tac}}} and \hyperlink{method.HOL.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} admit
|
|
907 |
to reason about inductive types. Rules are selected according to
|
|
908 |
the declarations by the \hyperlink{attribute.cases}{\mbox{\isa{cases}}} and \hyperlink{attribute.induct}{\mbox{\isa{induct}}}
|
|
909 |
attributes, cf.\ \secref{sec:cases-induct}. The \hyperlink{command.HOL.datatype}{\mbox{\isa{\isacommand{datatype}}}} package already takes care of this.
|
27124
|
910 |
|
|
911 |
These unstructured tactics feature both goal addressing and dynamic
|
26849
|
912 |
instantiation. Note that named rule cases are \emph{not} provided
|
27124
|
913 |
as would be by the proper \hyperlink{method.cases}{\mbox{\isa{cases}}} and \hyperlink{method.induct}{\mbox{\isa{induct}}} proof
|
|
914 |
methods (see \secref{sec:cases-induct}). Unlike the \hyperlink{method.induct}{\mbox{\isa{induct}}} method, \hyperlink{method.induct-tac}{\mbox{\isa{induct{\isacharunderscore}tac}}} does not handle structured rule
|
|
915 |
statements, only the compact object-logic conclusion of the subgoal
|
|
916 |
being addressed.
|
26849
|
917 |
|
28788
|
918 |
\item \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} and \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provide an interface to the internal \verb|mk_cases| operation. Rules are simplified in an unrestricted
|
26861
|
919 |
forward manner.
|
26849
|
920 |
|
26907
|
921 |
While \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} is a proof method to apply the
|
|
922 |
result immediately as elimination rules, \hyperlink{command.HOL.inductive-cases}{\mbox{\isa{\isacommand{inductive{\isacharunderscore}cases}}}} provides case split theorems at the theory level
|
|
923 |
for later use. The \hyperlink{keyword.for}{\mbox{\isa{\isakeyword{for}}}} argument of the \hyperlink{method.HOL.ind-cases}{\mbox{\isa{ind{\isacharunderscore}cases}}} method allows to specify a list of variables that should
|
26849
|
924 |
be generalized before applying the resulting rule.
|
|
925 |
|
28788
|
926 |
\end{description}%
|
26849
|
927 |
\end{isamarkuptext}%
|
|
928 |
\isamarkuptrue%
|
|
929 |
%
|
|
930 |
\isamarkupsection{Executable code%
|
|
931 |
}
|
|
932 |
\isamarkuptrue%
|
|
933 |
%
|
|
934 |
\begin{isamarkuptext}%
|
|
935 |
Isabelle/Pure provides two generic frameworks to support code
|
|
936 |
generation from executable specifications. Isabelle/HOL
|
|
937 |
instantiates these mechanisms in a way that is amenable to end-user
|
|
938 |
applications.
|
|
939 |
|
|
940 |
One framework generates code from both functional and relational
|
|
941 |
programs to SML. See \cite{isabelle-HOL} for further information
|
|
942 |
(this actually covers the new-style theory format as well).
|
|
943 |
|
|
944 |
\begin{matharray}{rcl}
|
28788
|
945 |
\indexdef{HOL}{command}{value}\hypertarget{command.HOL.value}{\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
946 |
\indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
947 |
\indexdef{HOL}{command}{code\_library}\hypertarget{command.HOL.code-library}{\hyperlink{command.HOL.code-library}{\mbox{\isa{\isacommand{code{\isacharunderscore}library}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
948 |
\indexdef{HOL}{command}{consts\_code}\hypertarget{command.HOL.consts-code}{\hyperlink{command.HOL.consts-code}{\mbox{\isa{\isacommand{consts{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
949 |
\indexdef{HOL}{command}{types\_code}\hypertarget{command.HOL.types-code}{\hyperlink{command.HOL.types-code}{\mbox{\isa{\isacommand{types{\isacharunderscore}code}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
950 |
\indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
|
26849
|
951 |
\end{matharray}
|
|
952 |
|
|
953 |
\begin{rail}
|
|
954 |
'value' term
|
|
955 |
;
|
|
956 |
|
|
957 |
( 'code\_module' | 'code\_library' ) modespec ? name ? \\
|
|
958 |
( 'file' name ) ? ( 'imports' ( name + ) ) ? \\
|
|
959 |
'contains' ( ( name '=' term ) + | term + )
|
|
960 |
;
|
|
961 |
|
|
962 |
modespec: '(' ( name * ) ')'
|
|
963 |
;
|
|
964 |
|
|
965 |
'consts\_code' (codespec +)
|
|
966 |
;
|
|
967 |
|
|
968 |
codespec: const template attachment ?
|
|
969 |
;
|
|
970 |
|
|
971 |
'types\_code' (tycodespec +)
|
|
972 |
;
|
|
973 |
|
|
974 |
tycodespec: name template attachment ?
|
|
975 |
;
|
|
976 |
|
|
977 |
const: term
|
|
978 |
;
|
|
979 |
|
|
980 |
template: '(' string ')'
|
|
981 |
;
|
|
982 |
|
|
983 |
attachment: 'attach' modespec ? verblbrace text verbrbrace
|
|
984 |
;
|
|
985 |
|
|
986 |
'code' (name)?
|
|
987 |
;
|
|
988 |
\end{rail}
|
|
989 |
|
28788
|
990 |
\begin{description}
|
26849
|
991 |
|
28788
|
992 |
\item \hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}~\isa{t} evaluates and prints a term
|
|
993 |
using the code generator.
|
26849
|
994 |
|
28788
|
995 |
\end{description}
|
26849
|
996 |
|
|
997 |
\medskip The other framework generates code from functional programs
|
|
998 |
(including overloading using type classes) to SML \cite{SML}, OCaml
|
|
999 |
\cite{OCaml} and Haskell \cite{haskell-revised-report}.
|
|
1000 |
Conceptually, code generation is split up in three steps:
|
|
1001 |
\emph{selection} of code theorems, \emph{translation} into an
|
|
1002 |
abstract executable view and \emph{serialization} to a specific
|
|
1003 |
\emph{target language}. See \cite{isabelle-codegen} for an
|
|
1004 |
introduction on how to use it.
|
|
1005 |
|
|
1006 |
\begin{matharray}{rcl}
|
28788
|
1007 |
\indexdef{HOL}{command}{export\_code}\hypertarget{command.HOL.export-code}{\hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
1008 |
\indexdef{HOL}{command}{code\_thms}\hypertarget{command.HOL.code-thms}{\hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
1009 |
\indexdef{HOL}{command}{code\_deps}\hypertarget{command.HOL.code-deps}{\hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
1010 |
\indexdef{HOL}{command}{code\_datatype}\hypertarget{command.HOL.code-datatype}{\hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1011 |
\indexdef{HOL}{command}{code\_const}\hypertarget{command.HOL.code-const}{\hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1012 |
\indexdef{HOL}{command}{code\_type}\hypertarget{command.HOL.code-type}{\hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1013 |
\indexdef{HOL}{command}{code\_class}\hypertarget{command.HOL.code-class}{\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1014 |
\indexdef{HOL}{command}{code\_instance}\hypertarget{command.HOL.code-instance}{\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1015 |
\indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1016 |
\indexdef{HOL}{command}{code\_reserved}\hypertarget{command.HOL.code-reserved}{\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1017 |
\indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1018 |
\indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1019 |
\indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
|
|
1020 |
\indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
|
|
1021 |
\indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
|
26849
|
1022 |
\end{matharray}
|
|
1023 |
|
|
1024 |
\begin{rail}
|
|
1025 |
'export\_code' ( constexpr + ) ? \\
|
|
1026 |
( ( 'in' target ( 'module\_name' string ) ? \\
|
|
1027 |
( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
|
|
1028 |
;
|
|
1029 |
|
|
1030 |
'code\_thms' ( constexpr + ) ?
|
|
1031 |
;
|
|
1032 |
|
|
1033 |
'code\_deps' ( constexpr + ) ?
|
|
1034 |
;
|
|
1035 |
|
|
1036 |
const: term
|
|
1037 |
;
|
|
1038 |
|
|
1039 |
constexpr: ( const | 'name.*' | '*' )
|
|
1040 |
;
|
|
1041 |
|
|
1042 |
typeconstructor: nameref
|
|
1043 |
;
|
|
1044 |
|
|
1045 |
class: nameref
|
|
1046 |
;
|
|
1047 |
|
|
1048 |
target: 'OCaml' | 'SML' | 'Haskell'
|
|
1049 |
;
|
|
1050 |
|
|
1051 |
'code\_datatype' const +
|
|
1052 |
;
|
|
1053 |
|
|
1054 |
'code\_const' (const + 'and') \\
|
|
1055 |
( ( '(' target ( syntax ? + 'and' ) ')' ) + )
|
|
1056 |
;
|
|
1057 |
|
|
1058 |
'code\_type' (typeconstructor + 'and') \\
|
|
1059 |
( ( '(' target ( syntax ? + 'and' ) ')' ) + )
|
|
1060 |
;
|
|
1061 |
|
|
1062 |
'code\_class' (class + 'and') \\
|
28687
|
1063 |
( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
|
26849
|
1064 |
;
|
|
1065 |
|
|
1066 |
'code\_instance' (( typeconstructor '::' class ) + 'and') \\
|
|
1067 |
( ( '(' target ( '-' ? + 'and' ) ')' ) + )
|
|
1068 |
;
|
|
1069 |
|
|
1070 |
'code\_monad' const const target
|
|
1071 |
;
|
|
1072 |
|
|
1073 |
'code\_reserved' target ( string + )
|
|
1074 |
;
|
|
1075 |
|
|
1076 |
'code\_include' target ( string ( string | '-') )
|
|
1077 |
;
|
|
1078 |
|
|
1079 |
'code\_modulename' target ( ( string string ) + )
|
|
1080 |
;
|
|
1081 |
|
27452
|
1082 |
'code\_abort' ( const + )
|
26849
|
1083 |
;
|
|
1084 |
|
|
1085 |
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
|
|
1086 |
;
|
|
1087 |
|
28562
|
1088 |
'code' ( 'inline' ) ? ( 'del' ) ?
|
26849
|
1089 |
;
|
|
1090 |
\end{rail}
|
|
1091 |
|
28788
|
1092 |
\begin{description}
|
26849
|
1093 |
|
28788
|
1094 |
\item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} is the canonical interface for
|
|
1095 |
generating and serializing code: for a given list of constants, code
|
|
1096 |
is generated for the specified target languages. Abstract code is
|
|
1097 |
cached incrementally. If no constant is given, the currently cached
|
|
1098 |
code is serialized. If no serialization instruction is given, only
|
|
1099 |
abstract code is cached.
|
26849
|
1100 |
|
|
1101 |
Constants may be specified by giving them literally, referring to
|
|
1102 |
all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
|
|
1103 |
available by giving \isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}.
|
|
1104 |
|
|
1105 |
By default, for each involved theory one corresponding name space
|
|
1106 |
module is generated. Alternativly, a module name may be specified
|
26907
|
1107 |
after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
|
26849
|
1108 |
placed in this module.
|
|
1109 |
|
|
1110 |
For \emph{SML} and \emph{OCaml}, the file specification refers to a
|
|
1111 |
single file; for \emph{Haskell}, it refers to a whole directory,
|
|
1112 |
where code is generated in multiple files reflecting the module
|
|
1113 |
hierarchy. The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
|
|
1114 |
output. For \emph{SML}, omitting the file specification compiles
|
|
1115 |
code internally in the context of the current ML session.
|
|
1116 |
|
|
1117 |
Serializers take an optional list of arguments in parentheses. For
|
|
1118 |
\emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
|
|
1119 |
declaration.
|
|
1120 |
|
28788
|
1121 |
\item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
|
26849
|
1122 |
representing the corresponding program containing all given
|
|
1123 |
constants; if no constants are given, the currently cached code
|
|
1124 |
theorems are printed.
|
|
1125 |
|
28788
|
1126 |
\item \hyperlink{command.HOL.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} visualizes dependencies of
|
26849
|
1127 |
theorems representing the corresponding program containing all given
|
|
1128 |
constants; if no constants are given, the currently cached code
|
|
1129 |
theorems are visualized.
|
|
1130 |
|
28788
|
1131 |
\item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
|
26849
|
1132 |
for a logical type.
|
|
1133 |
|
28788
|
1134 |
\item \hyperlink{command.HOL.code-const}{\mbox{\isa{\isacommand{code{\isacharunderscore}const}}}} associates a list of constants
|
26849
|
1135 |
with target-specific serializations; omitting a serialization
|
|
1136 |
deletes an existing serialization.
|
|
1137 |
|
28788
|
1138 |
\item \hyperlink{command.HOL.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}} associates a list of type
|
26849
|
1139 |
constructors with target-specific serializations; omitting a
|
|
1140 |
serialization deletes an existing serialization.
|
|
1141 |
|
28788
|
1142 |
\item \hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}} associates a list of classes
|
|
1143 |
with target-specific class names; omitting a serialization deletes
|
|
1144 |
an existing serialization. This applies only to \emph{Haskell}.
|
26849
|
1145 |
|
28788
|
1146 |
\item \hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}} declares a list of type
|
26849
|
1147 |
constructor / class instance relations as ``already present'' for a
|
|
1148 |
given target. Omitting a ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' deletes an existing
|
|
1149 |
``already present'' declaration. This applies only to
|
|
1150 |
\emph{Haskell}.
|
|
1151 |
|
28788
|
1152 |
\item \hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}} provides an auxiliary mechanism
|
|
1153 |
to generate monadic code for Haskell.
|
26849
|
1154 |
|
28788
|
1155 |
\item \hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}} declares a list of names as
|
26849
|
1156 |
reserved for a given target, preventing it to be shadowed by any
|
|
1157 |
generated code.
|
|
1158 |
|
28788
|
1159 |
\item \hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}} adds arbitrary named content
|
27834
|
1160 |
(``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
|
26849
|
1161 |
will remove an already added ``include''.
|
|
1162 |
|
28788
|
1163 |
\item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
|
|
1164 |
module name onto another.
|
26849
|
1165 |
|
28788
|
1166 |
\item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
|
|
1167 |
required to have a definition by means of defining equations; if
|
|
1168 |
needed these are implemented by program abort instead.
|
26849
|
1169 |
|
28788
|
1170 |
\item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
|
|
1171 |
``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for code
|
|
1172 |
generation. Usually packages introducing defining equations provide
|
|
1173 |
a reasonable default setup for selection.
|
26849
|
1174 |
|
28788
|
1175 |
\item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
|
28562
|
1176 |
option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
|
26849
|
1177 |
applied as rewrite rules to any defining equation during
|
|
1178 |
preprocessing.
|
|
1179 |
|
28788
|
1180 |
\item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
|
26849
|
1181 |
selected defining equations, code generator datatypes and
|
|
1182 |
preprocessor setup.
|
|
1183 |
|
28788
|
1184 |
\end{description}%
|
26849
|
1185 |
\end{isamarkuptext}%
|
|
1186 |
\isamarkuptrue%
|
|
1187 |
%
|
27047
|
1188 |
\isamarkupsection{Definition by specification \label{sec:hol-specification}%
|
|
1189 |
}
|
|
1190 |
\isamarkuptrue%
|
|
1191 |
%
|
|
1192 |
\begin{isamarkuptext}%
|
|
1193 |
\begin{matharray}{rcl}
|
28788
|
1194 |
\indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
|
|
1195 |
\indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
|
27047
|
1196 |
\end{matharray}
|
|
1197 |
|
|
1198 |
\begin{rail}
|
|
1199 |
('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
|
|
1200 |
;
|
|
1201 |
decl: ((name ':')? term '(' 'overloaded' ')'?)
|
|
1202 |
\end{rail}
|
|
1203 |
|
28788
|
1204 |
\begin{description}
|
27047
|
1205 |
|
28788
|
1206 |
\item \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up a
|
27047
|
1207 |
goal stating the existence of terms with the properties specified to
|
|
1208 |
hold for the constants given in \isa{decls}. After finishing the
|
|
1209 |
proof, the theory will be augmented with definitions for the given
|
|
1210 |
constants, as well as with theorems stating the properties for these
|
|
1211 |
constants.
|
|
1212 |
|
28788
|
1213 |
\item \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}} sets up
|
|
1214 |
a goal stating the existence of terms with the properties specified
|
|
1215 |
to hold for the constants given in \isa{decls}. After finishing
|
|
1216 |
the proof, the theory will be augmented with axioms expressing the
|
|
1217 |
properties given in the first place.
|
27047
|
1218 |
|
28788
|
1219 |
\item \isa{decl} declares a constant to be defined by the
|
27047
|
1220 |
specification given. The definition for the constant \isa{c} is
|
|
1221 |
bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
|
|
1222 |
the declaration. Overloaded constants should be declared as such.
|
|
1223 |
|
28788
|
1224 |
\end{description}
|
27047
|
1225 |
|
|
1226 |
Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style. \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
|
|
1227 |
construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
|
|
1228 |
user has explicitly proven it to be safe. A practical issue must be
|
|
1229 |
considered, though: After introducing two constants with the same
|
|
1230 |
properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
|
|
1231 |
that the two constants are, in fact, equal. If this might be a
|
|
1232 |
problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
|
|
1233 |
\end{isamarkuptext}%
|
|
1234 |
\isamarkuptrue%
|
|
1235 |
%
|
26849
|
1236 |
\isadelimtheory
|
|
1237 |
%
|
|
1238 |
\endisadelimtheory
|
|
1239 |
%
|
|
1240 |
\isatagtheory
|
26840
|
1241 |
\isacommand{end}\isamarkupfalse%
|
|
1242 |
%
|
|
1243 |
\endisatagtheory
|
|
1244 |
{\isafoldtheory}%
|
|
1245 |
%
|
|
1246 |
\isadelimtheory
|
|
1247 |
%
|
|
1248 |
\endisadelimtheory
|
26849
|
1249 |
\isanewline
|
26840
|
1250 |
\end{isabellebody}%
|
|
1251 |
%%% Local Variables:
|
|
1252 |
%%% mode: latex
|
|
1253 |
%%% TeX-master: "root"
|
|
1254 |
%%% End:
|