author | wenzelm |
Thu, 13 Nov 2008 22:45:12 +0100 | |
changeset 28788 | ff9d8a8932e4 |
parent 28728 | 08314d96246b |
child 29560 | fa6c5d62adf5 |
permissions | -rw-r--r-- |
26869 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Spec}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
\isanewline |
|
7 |
\isanewline |
|
8 |
% |
|
9 |
\endisadelimtheory |
|
10 |
% |
|
11 |
\isatagtheory |
|
12 |
\isacommand{theory}\isamarkupfalse% |
|
13 |
\ Spec\isanewline |
|
14 |
\isakeyword{imports}\ Main\isanewline |
|
15 |
\isakeyword{begin}% |
|
16 |
\endisatagtheory |
|
17 |
{\isafoldtheory}% |
|
18 |
% |
|
19 |
\isadelimtheory |
|
20 |
% |
|
21 |
\endisadelimtheory |
|
22 |
% |
|
27047 | 23 |
\isamarkupchapter{Theory specifications% |
26869 | 24 |
} |
25 |
\isamarkuptrue% |
|
26 |
% |
|
26870 | 27 |
\isamarkupsection{Defining theories \label{sec:begin-thy}% |
28 |
} |
|
29 |
\isamarkuptrue% |
|
30 |
% |
|
31 |
\begin{isamarkuptext}% |
|
32 |
\begin{matharray}{rcl} |
|
28788 | 33 |
\indexdef{}{command}{theory}\hypertarget{command.theory}{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}} & : & \isa{{\isachardoublequote}toplevel\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
34 |
\indexdef{global}{command}{end}\hypertarget{command.global.end}{\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ toplevel{\isachardoublequote}} \\ |
|
26870 | 35 |
\end{matharray} |
36 |
||
28788 | 37 |
Isabelle/Isar theories are defined via theory files, which may |
38 |
contain both specifications and proofs; occasionally definitional |
|
39 |
mechanisms also require some explicit proof. The theory body may be |
|
40 |
sub-structured by means of \emph{local theory targets}, such as |
|
41 |
\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}. |
|
26870 | 42 |
|
28788 | 43 |
The first proper command of a theory is \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}, which |
44 |
indicates imports of previous theories and optional dependencies on |
|
45 |
other source files (usually in ML). Just preceding the initial |
|
46 |
\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}} command there may be an optional \hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}} declaration, which is only relevant to document |
|
47 |
preparation: see also the other section markup commands in |
|
48 |
\secref{sec:markup}. |
|
49 |
||
50 |
A theory is concluded by a final \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} command, |
|
51 |
one that does not belong to a local theory target. No further |
|
52 |
commands may follow such a global \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}}, |
|
53 |
although some user-interfaces might pretend that trailing input is |
|
54 |
admissible. |
|
26870 | 55 |
|
56 |
\begin{rail} |
|
57 |
'theory' name 'imports' (name +) uses? 'begin' |
|
58 |
; |
|
59 |
||
60 |
uses: 'uses' ((name | parname) +); |
|
61 |
\end{rail} |
|
62 |
||
28788 | 63 |
\begin{description} |
26870 | 64 |
|
28788 | 65 |
\item \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}} |
66 |
starts a new theory \isa{A} based on the merge of existing |
|
67 |
theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}. |
|
26870 | 68 |
|
28788 | 69 |
Due to the possibility to import more than one ancestor, the |
70 |
resulting theory structure of an Isabelle session forms a directed |
|
71 |
acyclic graph (DAG). Isabelle's theory loader ensures that the |
|
72 |
sources contributing to the development graph are always up-to-date: |
|
73 |
changed files are automatically reloaded whenever a theory header |
|
74 |
specification is processed. |
|
26870 | 75 |
|
26902 | 76 |
The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional |
26870 | 77 |
dependencies on extra files (usually ML sources). Files will be |
28788 | 78 |
loaded immediately (as ML), unless the name is parenthesized. The |
79 |
latter case records a dependency that needs to be resolved later in |
|
80 |
the text, usually via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} for ML files; |
|
81 |
other file formats require specific load commands defined by the |
|
82 |
corresponding tools or packages. |
|
26870 | 83 |
|
28788 | 84 |
\item \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} concludes the current theory |
85 |
definition. Note that local theory targets involve a local |
|
86 |
\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, which is clear from the nesting. |
|
27042 | 87 |
|
28788 | 88 |
\end{description}% |
27042 | 89 |
\end{isamarkuptext}% |
90 |
\isamarkuptrue% |
|
91 |
% |
|
92 |
\isamarkupsection{Local theory targets \label{sec:target}% |
|
93 |
} |
|
94 |
\isamarkuptrue% |
|
95 |
% |
|
96 |
\begin{isamarkuptext}% |
|
97 |
A local theory target is a context managed separately within the |
|
98 |
enclosing theory. Contexts may introduce parameters (fixed |
|
99 |
variables) and assumptions (hypotheses). Definitions and theorems |
|
100 |
depending on the context may be added incrementally later on. Named |
|
101 |
contexts refer to locales (cf.\ \secref{sec:locale}) or type classes |
|
102 |
(cf.\ \secref{sec:class}); the name ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' signifies the |
|
103 |
global theory context. |
|
104 |
||
105 |
\begin{matharray}{rcll} |
|
28788 | 106 |
\indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
107 |
\indexdef{local}{command}{end}\hypertarget{command.local.end}{\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
27042 | 108 |
\end{matharray} |
109 |
||
110 |
\indexouternonterm{target} |
|
111 |
\begin{rail} |
|
112 |
'context' name 'begin' |
|
113 |
; |
|
114 |
||
115 |
target: '(' 'in' name ')' |
|
116 |
; |
|
117 |
\end{rail} |
|
118 |
||
28788 | 119 |
\begin{description} |
27042 | 120 |
|
28788 | 121 |
\item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isachardoublequote}c\ {\isasymBEGIN}{\isachardoublequote}} recommences an |
27042 | 122 |
existing locale or class context \isa{c}. Note that locale and |
27052 | 123 |
class definitions allow to include the \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as |
124 |
well, in order to continue the local theory immediately after the |
|
125 |
initial specification. |
|
27042 | 126 |
|
28788 | 127 |
\item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory |
27042 | 128 |
and continues the enclosing global theory. Note that a global |
129 |
\hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the |
|
130 |
theory itself (\secref{sec:begin-thy}). |
|
131 |
||
28788 | 132 |
\item \isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}{\isachardoublequote}} given after any local theory command |
27042 | 133 |
specifies an immediate target, e.g.\ ``\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}'' or ``\hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ c{\isacharparenright}\ {\isasymdots}{\isachardoublequote}}''. This works both in a local or |
134 |
global theory context; the current target context will be suspended |
|
135 |
for this command only. Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIN}\ {\isacharminus}{\isacharparenright}{\isachardoublequote}}'' will |
|
136 |
always produce a global result independently of the current target |
|
137 |
context. |
|
138 |
||
28788 | 139 |
\end{description} |
27042 | 140 |
|
141 |
The exact meaning of results produced within a local theory context |
|
142 |
depends on the underlying target infrastructure (locale, type class |
|
143 |
etc.). The general idea is as follows, considering a context named |
|
144 |
\isa{c} with parameter \isa{x} and assumption \isa{{\isachardoublequote}A{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}}. |
|
145 |
||
146 |
Definitions are exported by introducing a global version with |
|
147 |
additional arguments; a syntactic abbreviation links the long form |
|
148 |
with the abstract version of the target context. For example, |
|
149 |
\isa{{\isachardoublequote}a\ {\isasymequiv}\ t{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a\ {\isacharquery}x\ {\isasymequiv}\ t{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}} at the theory |
|
150 |
level (for arbitrary \isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}), together with a local |
|
151 |
abbreviation \isa{{\isachardoublequote}c\ {\isasymequiv}\ c{\isachardot}a\ x{\isachardoublequote}} in the target context (for the |
|
152 |
fixed parameter \isa{x}). |
|
153 |
||
154 |
Theorems are exported by discharging the assumptions and |
|
155 |
generalizing the parameters of the context. For example, \isa{{\isachardoublequote}a{\isacharcolon}\ B{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} becomes \isa{{\isachardoublequote}c{\isachardot}a{\isacharcolon}\ A{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}\ {\isasymLongrightarrow}\ B{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}{\isachardoublequote}}, again for arbitrary |
|
156 |
\isa{{\isachardoublequote}{\isacharquery}x{\isachardoublequote}}.% |
|
157 |
\end{isamarkuptext}% |
|
158 |
\isamarkuptrue% |
|
159 |
% |
|
160 |
\isamarkupsection{Basic specification elements% |
|
161 |
} |
|
162 |
\isamarkuptrue% |
|
163 |
% |
|
164 |
\begin{isamarkuptext}% |
|
165 |
\begin{matharray}{rcll} |
|
28788 | 166 |
\indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!)\\ |
167 |
\indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
168 |
\indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\ |
|
169 |
\indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
170 |
\indexdef{}{command}{print\_abbrevs}\hypertarget{command.print-abbrevs}{\hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}\ {\isachardoublequote}} \\ |
|
27042 | 171 |
\end{matharray} |
172 |
||
173 |
These specification mechanisms provide a slightly more abstract view |
|
174 |
than the underlying primitives of \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}, \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}} (see \secref{sec:consts}), and \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}} (see |
|
175 |
\secref{sec:axms-thms}). In particular, type-inference is commonly |
|
176 |
available, and result names need not be given. |
|
177 |
||
178 |
\begin{rail} |
|
179 |
'axiomatization' target? fixes? ('where' specs)? |
|
180 |
; |
|
181 |
'definition' target? (decl 'where')? thmdecl? prop |
|
182 |
; |
|
183 |
'abbreviation' target? mode? (decl 'where')? prop |
|
184 |
; |
|
185 |
||
186 |
fixes: ((name ('::' type)? mixfix? | vars) + 'and') |
|
187 |
; |
|
188 |
specs: (thmdecl? props + 'and') |
|
189 |
; |
|
190 |
decl: name ('::' type)? mixfix? |
|
191 |
; |
|
192 |
\end{rail} |
|
193 |
||
28788 | 194 |
\begin{description} |
27042 | 195 |
|
28788 | 196 |
\item \hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymdots}\ c\isactrlsub m\ {\isasymWHERE}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} |
197 |
introduces several constants simultaneously and states axiomatic |
|
198 |
properties for these. The constants are marked as being specified |
|
199 |
once and for all, which prevents additional specifications being |
|
200 |
issued later on. |
|
27042 | 201 |
|
202 |
Note that axiomatic specifications are only appropriate when |
|
28110 | 203 |
declaring a new logical system; axiomatic specifications are |
204 |
restricted to global theory contexts. Normal applications should |
|
205 |
only use definitional mechanisms! |
|
27042 | 206 |
|
28788 | 207 |
\item \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}} produces an |
27042 | 208 |
internal definition \isa{{\isachardoublequote}c\ {\isasymequiv}\ t{\isachardoublequote}} according to the specification |
209 |
given as \isa{eq}, which is then turned into a proven fact. The |
|
210 |
given proposition may deviate from internal meta-level equality |
|
211 |
according to the rewrite rules declared as \hyperlink{attribute.defn}{\mbox{\isa{defn}}} by the |
|
212 |
object-logic. This usually covers object-level equality \isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}} and equivalence \isa{{\isachardoublequote}A\ {\isasymleftrightarrow}\ B{\isachardoublequote}}. End-users normally need not |
|
213 |
change the \hyperlink{attribute.defn}{\mbox{\isa{defn}}} setup. |
|
214 |
||
215 |
Definitions may be presented with explicit arguments on the LHS, as |
|
216 |
well as additional conditions, e.g.\ \isa{{\isachardoublequote}f\ x\ y\ {\isacharequal}\ t{\isachardoublequote}} instead of |
|
217 |
\isa{{\isachardoublequote}f\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} and \isa{{\isachardoublequote}y\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ g\ x\ y\ {\isacharequal}\ u{\isachardoublequote}} instead of an |
|
218 |
unrestricted \isa{{\isachardoublequote}g\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ u{\isachardoublequote}}. |
|
219 |
||
28788 | 220 |
\item \hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}~\isa{{\isachardoublequote}c\ {\isasymWHERE}\ eq{\isachardoublequote}} introduces a |
221 |
syntactic constant which is associated with a certain term according |
|
222 |
to the meta-level equality \isa{eq}. |
|
27042 | 223 |
|
224 |
Abbreviations participate in the usual type-inference process, but |
|
225 |
are expanded before the logic ever sees them. Pretty printing of |
|
226 |
terms involves higher-order rewriting with rules stemming from |
|
227 |
reverted abbreviations. This needs some care to avoid overlapping |
|
228 |
or looping syntactic replacements! |
|
229 |
||
230 |
The optional \isa{mode} specification restricts output to a |
|
231 |
particular print mode; using ``\isa{input}'' here achieves the |
|
232 |
effect of one-way abbreviations. The mode may also include an |
|
233 |
``\hyperlink{keyword.output}{\mbox{\isa{\isakeyword{output}}}}'' qualifier that affects the concrete syntax |
|
234 |
declared for abbreviations, cf.\ \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} in |
|
235 |
\secref{sec:syn-trans}. |
|
236 |
||
28788 | 237 |
\item \hyperlink{command.print-abbrevs}{\mbox{\isa{\isacommand{print{\isacharunderscore}abbrevs}}}} prints all constant abbreviations |
27042 | 238 |
of the current context. |
239 |
||
28788 | 240 |
\end{description}% |
27042 | 241 |
\end{isamarkuptext}% |
242 |
\isamarkuptrue% |
|
243 |
% |
|
244 |
\isamarkupsection{Generic declarations% |
|
245 |
} |
|
246 |
\isamarkuptrue% |
|
247 |
% |
|
248 |
\begin{isamarkuptext}% |
|
249 |
Arbitrary operations on the background context may be wrapped-up as |
|
250 |
generic declaration elements. Since the underlying concept of local |
|
251 |
theories may be subject to later re-interpretation, there is an |
|
252 |
additional dependency on a morphism that tells the difference of the |
|
253 |
original declaration context wrt.\ the application context |
|
254 |
encountered later on. A fact declaration is an important special |
|
255 |
case: it consists of a theorem which is applied to the context by |
|
256 |
means of an attribute. |
|
257 |
||
258 |
\begin{matharray}{rcl} |
|
28788 | 259 |
\indexdef{}{command}{declaration}\hypertarget{command.declaration}{\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
260 |
\indexdef{}{command}{declare}\hypertarget{command.declare}{\hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
27042 | 261 |
\end{matharray} |
262 |
||
263 |
\begin{rail} |
|
264 |
'declaration' target? text |
|
265 |
; |
|
266 |
'declare' target? (thmrefs + 'and') |
|
267 |
; |
|
268 |
\end{rail} |
|
269 |
||
28788 | 270 |
\begin{description} |
27042 | 271 |
|
28788 | 272 |
\item \hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}~\isa{d} adds the declaration |
27042 | 273 |
function \isa{d} of ML type \verb|declaration|, to the current |
274 |
local theory under construction. In later application contexts, the |
|
275 |
function is transformed according to the morphisms being involved in |
|
276 |
the interpretation hierarchy. |
|
277 |
||
28788 | 278 |
\item \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}}~\isa{thms} declares theorems to the |
27042 | 279 |
current local theory context. No theorem binding is involved here, |
280 |
unlike \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} or \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}} (cf.\ |
|
281 |
\secref{sec:axms-thms}), so \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} only has the effect |
|
282 |
of applying attributes as included in the theorem specification. |
|
283 |
||
28788 | 284 |
\end{description}% |
27042 | 285 |
\end{isamarkuptext}% |
286 |
\isamarkuptrue% |
|
287 |
% |
|
288 |
\isamarkupsection{Locales \label{sec:locale}% |
|
289 |
} |
|
290 |
\isamarkuptrue% |
|
291 |
% |
|
292 |
\begin{isamarkuptext}% |
|
293 |
Locales are named local contexts, consisting of a list of |
|
294 |
declaration elements that are modeled after the Isar proof context |
|
295 |
commands (cf.\ \secref{sec:proof-context}).% |
|
296 |
\end{isamarkuptext}% |
|
297 |
\isamarkuptrue% |
|
298 |
% |
|
299 |
\isamarkupsubsection{Locale specifications% |
|
300 |
} |
|
301 |
\isamarkuptrue% |
|
302 |
% |
|
303 |
\begin{isamarkuptext}% |
|
304 |
\begin{matharray}{rcl} |
|
28788 | 305 |
\indexdef{}{command}{locale}\hypertarget{command.locale}{\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
306 |
\indexdef{}{command}{print\_locale}\hypertarget{command.print-locale}{\hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
307 |
\indexdef{}{command}{print\_locales}\hypertarget{command.print-locales}{\hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
308 |
\indexdef{}{method}{intro\_locales}\hypertarget{method.intro-locales}{\hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}}} & : & \isa{method} \\ |
|
309 |
\indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isa{method} \\ |
|
27042 | 310 |
\end{matharray} |
311 |
||
312 |
\indexouternonterm{contextexpr}\indexouternonterm{contextelem} |
|
313 |
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
|
28788 | 314 |
\indexisarelem{defines}\indexisarelem{notes} |
27042 | 315 |
\begin{rail} |
27834 | 316 |
'locale' name ('=' localeexpr)? 'begin'? |
27042 | 317 |
; |
318 |
'print\_locale' '!'? localeexpr |
|
319 |
; |
|
320 |
localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+)) |
|
321 |
; |
|
322 |
||
323 |
contextexpr: nameref | '(' contextexpr ')' | |
|
324 |
(contextexpr (name mixfix? +)) | (contextexpr + '+') |
|
325 |
; |
|
326 |
contextelem: fixes | constrains | assumes | defines | notes |
|
327 |
; |
|
328 |
fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and') |
|
329 |
; |
|
330 |
constrains: 'constrains' (name '::' type + 'and') |
|
331 |
; |
|
332 |
assumes: 'assumes' (thmdecl? props + 'and') |
|
333 |
; |
|
334 |
defines: 'defines' (thmdecl? prop proppat? + 'and') |
|
335 |
; |
|
336 |
notes: 'notes' (thmdef? thmrefs + 'and') |
|
337 |
; |
|
338 |
\end{rail} |
|
339 |
||
28788 | 340 |
\begin{description} |
27042 | 341 |
|
28788 | 342 |
\item \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{{\isachardoublequote}loc\ {\isacharequal}\ import\ {\isacharplus}\ body{\isachardoublequote}} defines a |
27042 | 343 |
new locale \isa{loc} as a context consisting of a certain view of |
344 |
existing locales (\isa{import}) plus some additional elements |
|
345 |
(\isa{body}). Both \isa{import} and \isa{body} are optional; |
|
346 |
the degenerate form \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}~\isa{loc} defines an empty |
|
347 |
locale, which may still be useful to collect declarations of facts |
|
348 |
later on. Type-inference on locale expressions automatically takes |
|
349 |
care of the most general typing that the combined context elements |
|
350 |
may acquire. |
|
351 |
||
352 |
The \isa{import} consists of a structured context expression, |
|
353 |
consisting of references to existing locales, renamed contexts, or |
|
354 |
merged contexts. Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed |
|
355 |
parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that |
|
356 |
position. Renaming by default deletes concrete syntax, but new |
|
357 |
syntax may by specified with a mixfix annotation. An exeption of |
|
358 |
this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it |
|
359 |
be changed. Merging proceeds from left-to-right, suppressing any |
|
360 |
duplicates stemming from different paths through the import |
|
361 |
hierarchy. |
|
362 |
||
363 |
The \isa{body} consists of basic context elements, further context |
|
364 |
expressions may be included as well. |
|
365 |
||
28788 | 366 |
\begin{description} |
27042 | 367 |
|
28788 | 368 |
\item \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\ {\isacharparenleft}mx{\isacharparenright}{\isachardoublequote}} declares a local |
27042 | 369 |
parameter of type \isa{{\isasymtau}} and mixfix annotation \isa{mx} (both |
370 |
are optional). The special syntax declaration ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' means that \isa{x} may be referenced |
|
371 |
implicitly in this context. |
|
372 |
||
28788 | 373 |
\item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type |
27042 | 374 |
constraint \isa{{\isasymtau}} on the local parameter \isa{x}. |
375 |
||
28788 | 376 |
\item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} |
27042 | 377 |
introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a |
378 |
proof (cf.\ \secref{sec:proof-context}). |
|
379 |
||
28788 | 380 |
\item \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} defines a previously |
27042 | 381 |
declared parameter. This is similar to \hyperlink{command.def}{\mbox{\isa{\isacommand{def}}}} within a |
382 |
proof (cf.\ \secref{sec:proof-context}), but \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} |
|
383 |
takes an equational proposition instead of variable-term pair. The |
|
384 |
left-hand side of the equation may have additional arguments, e.g.\ |
|
385 |
``\hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}}~\isa{{\isachardoublequote}f\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ t{\isachardoublequote}}''. |
|
386 |
||
28788 | 387 |
\item \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} |
27042 | 388 |
reconsiders facts within a local context. Most notably, this may |
389 |
include arbitrary declarations in any attribute specifications |
|
390 |
included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule. |
|
391 |
||
28788 | 392 |
The initial \isa{import} specification of a locale expression |
393 |
maintains a dynamic relation to the locales being referenced |
|
394 |
(benefiting from any later fact declarations in the obvious manner). |
|
27042 | 395 |
|
28788 | 396 |
\end{description} |
27042 | 397 |
|
398 |
Note that ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}'' patterns given |
|
399 |
in the syntax of \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} and \hyperlink{element.defines}{\mbox{\isa{\isakeyword{defines}}}} above |
|
400 |
are illegal in locale definitions. In the long goal format of |
|
401 |
\secref{sec:goals}, term bindings may be included as expected, |
|
402 |
though. |
|
403 |
||
404 |
\medskip By default, locale specifications are ``closed up'' by |
|
405 |
turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas |
|
406 |
(modulo local definitions). The predicate statement covers only the |
|
407 |
newly specified assumptions, omitting the content of included locale |
|
408 |
expressions. The full cumulative view is only provided on export, |
|
409 |
involving another predicate \isa{loc} that refers to the complete |
|
410 |
specification text. |
|
411 |
||
412 |
In any case, the predicate arguments are those locale parameters |
|
413 |
that actually occur in the respective piece of text. Also note that |
|
414 |
these predicates operate at the meta-level in theory, but the locale |
|
415 |
packages attempts to internalize statements according to the |
|
416 |
object-logic setup (e.g.\ replacing \isa{{\isasymAnd}} by \isa{{\isasymforall}}, and |
|
417 |
\isa{{\isachardoublequote}{\isasymLongrightarrow}{\isachardoublequote}} by \isa{{\isachardoublequote}{\isasymlongrightarrow}{\isachardoublequote}} in HOL; see also |
|
418 |
\secref{sec:object-logic}). Separate introduction rules \isa{loc{\isacharunderscore}axioms{\isachardot}intro} and \isa{loc{\isachardot}intro} are provided as well. |
|
419 |
||
28788 | 420 |
\item \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{{\isachardoublequote}import\ {\isacharplus}\ body{\isachardoublequote}} prints the |
27042 | 421 |
specified locale expression in a flattened form. The notable |
422 |
special case \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}~\isa{loc} just prints the |
|
423 |
contents of the named locale, but keep in mind that type-inference |
|
424 |
will normalize type variables according to the usual alphabetical |
|
425 |
order. The command omits \hyperlink{element.notes}{\mbox{\isa{\isakeyword{notes}}}} elements by default. |
|
426 |
Use \hyperlink{command.print-locale}{\mbox{\isa{\isacommand{print{\isacharunderscore}locale}}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}} to get them included. |
|
427 |
||
28788 | 428 |
\item \hyperlink{command.print-locales}{\mbox{\isa{\isacommand{print{\isacharunderscore}locales}}}} prints the names of all locales |
27042 | 429 |
of the current theory. |
430 |
||
28788 | 431 |
\item \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} and \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} |
27042 | 432 |
repeatedly expand all introduction rules of locale predicates of the |
433 |
theory. While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to |
|
434 |
assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies |
|
435 |
\isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well. Both methods are aware of locale |
|
28728 | 436 |
specifications entailed by the context, both from target statements, |
437 |
and from interpretations (see below). New goals that are entailed |
|
438 |
by the current context are discharged automatically. |
|
27042 | 439 |
|
28788 | 440 |
\end{description}% |
27042 | 441 |
\end{isamarkuptext}% |
442 |
\isamarkuptrue% |
|
443 |
% |
|
444 |
\isamarkupsubsection{Interpretation of locales% |
|
445 |
} |
|
446 |
\isamarkuptrue% |
|
447 |
% |
|
448 |
\begin{isamarkuptext}% |
|
449 |
Locale expressions (more precisely, \emph{context expressions}) may |
|
450 |
be instantiated, and the instantiated facts added to the current |
|
451 |
context. This requires a proof of the instantiated specification |
|
452 |
and is called \emph{locale interpretation}. Interpretation is |
|
453 |
possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}). |
|
454 |
||
455 |
\begin{matharray}{rcl} |
|
28788 | 456 |
\indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\ |
457 |
\indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\ |
|
458 |
\indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
27042 | 459 |
\end{matharray} |
460 |
||
461 |
\indexouternonterm{interp} |
|
462 |
\begin{rail} |
|
463 |
'interpretation' (interp | name ('<' | subseteq) contextexpr) |
|
464 |
; |
|
465 |
'interpret' interp |
|
466 |
; |
|
467 |
'print\_interps' '!'? name |
|
468 |
; |
|
469 |
instantiation: ('[' (inst+) ']')? |
|
470 |
; |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
471 |
interp: (name ':')? \\ (contextexpr instantiation | |
27042 | 472 |
name instantiation 'where' (thmdecl? prop + 'and')) |
473 |
; |
|
474 |
\end{rail} |
|
475 |
||
28788 | 476 |
\begin{description} |
27042 | 477 |
|
28788 | 478 |
\item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}} |
27042 | 479 |
|
480 |
The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory. The instantiation is given as a list of terms |
|
481 |
\isa{insts} and is positional. All parameters must receive an |
|
482 |
instantiation term --- with the exception of defined parameters. |
|
483 |
These are, if omitted, derived from the defining equation and other |
|
484 |
instantiations. Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term. |
|
485 |
||
486 |
The command generates proof obligations for the instantiated |
|
487 |
specifications (assumes and defines elements). Once these are |
|
488 |
discharged by the user, instantiated facts are added to the theory |
|
489 |
in a post-processing phase. |
|
490 |
||
491 |
Additional equations, which are unfolded in facts during |
|
492 |
post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}. |
|
493 |
This is useful for interpreting concepts introduced through |
|
494 |
definition specification elements. The equations must be proved. |
|
495 |
Note that if equations are present, the context expression is |
|
496 |
restricted to a locale name. |
|
497 |
||
498 |
The command is aware of interpretations already active in the |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
499 |
theory, but does not simplify the goal automatically. In order to |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
500 |
simplify the proof obligations use methods \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
501 |
or \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}. Post-processing is not applied to |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
502 |
facts of interpretations that are already active. This avoids |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
503 |
duplication of interpreted facts, in particular. Note that, in the |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
504 |
case of a locale with import, parts of the interpretation may |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
505 |
already be active. The command will only process facts for new |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
506 |
parts. |
27042 | 507 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
508 |
The context expression may be preceded by a name, which takes effect |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
509 |
in the post-processing of facts. It is used to prefix fact names, |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
27834
diff
changeset
|
510 |
for example to avoid accidental hiding of other facts. |
27042 | 511 |
|
512 |
Adding facts to locales has the effect of adding interpreted facts |
|
513 |
to the theory for all active interpretations also. That is, |
|
514 |
interpretations dynamically participate in any facts added to |
|
515 |
locales. |
|
516 |
||
28788 | 517 |
\item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}} |
27042 | 518 |
|
519 |
This form of the command interprets \isa{expr} in the locale |
|
520 |
\isa{name}. It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}. As in the |
|
521 |
localized version of the theorem command, the proof is in the |
|
522 |
context of \isa{name}. After the proof obligation has been |
|
523 |
dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the |
|
524 |
context \isa{name} is subsequently entered. Note that, like |
|
525 |
import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}. |
|
526 |
Like facts of renamed context elements, facts obtained by |
|
527 |
interpretation may be accessed by prefixing with the parameter |
|
528 |
renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}''). |
|
529 |
||
530 |
Unlike interpretation in theories, instantiation is confined to the |
|
531 |
renaming of parameters, which may be specified as part of the |
|
532 |
context expression \isa{expr}. Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though. |
|
533 |
||
534 |
Only specification fragments of \isa{expr} that are not already |
|
535 |
part of \isa{name} (be it imported, derived or a derived fragment |
|
536 |
of the import) are considered by interpretation. This enables |
|
537 |
circular interpretations. |
|
538 |
||
539 |
If interpretations of \isa{name} exist in the current theory, the |
|
540 |
command adds interpretations for \isa{expr} as well, with the same |
|
541 |
prefix and attributes, although only for fragments of \isa{expr} |
|
542 |
that are not interpreted in the theory already. |
|
543 |
||
28788 | 544 |
\item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}} |
27042 | 545 |
interprets \isa{expr} in the proof context and is otherwise |
546 |
similar to interpretation in theories. |
|
547 |
||
28788 | 548 |
\item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}~\isa{loc} prints the |
27042 | 549 |
interpretations of a particular locale \isa{loc} that are active |
550 |
in the current context, either theory or proof context. The |
|
551 |
exclamation point argument triggers printing of \emph{witness} |
|
552 |
theorems justifying interpretations. These are normally omitted |
|
553 |
from the output. |
|
554 |
||
28788 | 555 |
\end{description} |
27042 | 556 |
|
557 |
\begin{warn} |
|
558 |
Since attributes are applied to interpreted theorems, |
|
559 |
interpretation may modify the context of common proof tools, e.g.\ |
|
560 |
the Simplifier or Classical Reasoner. Since the behavior of such |
|
561 |
automated reasoning tools is \emph{not} stable under |
|
562 |
interpretation morphisms, manual declarations might have to be |
|
563 |
issued. |
|
564 |
\end{warn} |
|
565 |
||
566 |
\begin{warn} |
|
567 |
An interpretation in a theory may subsume previous |
|
568 |
interpretations. This happens if the same specification fragment |
|
569 |
is interpreted twice and the instantiation of the second |
|
570 |
interpretation is more general than the interpretation of the |
|
571 |
first. A warning is issued, since it is likely that these could |
|
572 |
have been generalized in the first place. The locale package does |
|
573 |
not attempt to remove subsumed interpretations. |
|
574 |
\end{warn}% |
|
575 |
\end{isamarkuptext}% |
|
576 |
\isamarkuptrue% |
|
577 |
% |
|
578 |
\isamarkupsection{Classes \label{sec:class}% |
|
579 |
} |
|
580 |
\isamarkuptrue% |
|
581 |
% |
|
582 |
\begin{isamarkuptext}% |
|
583 |
A class is a particular locale with \emph{exactly one} type variable |
|
584 |
\isa{{\isasymalpha}}. Beyond the underlying locale, a corresponding type class |
|
585 |
is established which is interpreted logically as axiomatic type |
|
586 |
class \cite{Wenzel:1997:TPHOL} whose logical content are the |
|
587 |
assumptions of the locale. Thus, classes provide the full |
|
588 |
generality of locales combined with the commodity of type classes |
|
589 |
(notably type-inference). See \cite{isabelle-classes} for a short |
|
590 |
tutorial. |
|
591 |
||
592 |
\begin{matharray}{rcl} |
|
28788 | 593 |
\indexdef{}{command}{class}\hypertarget{command.class}{\hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
594 |
\indexdef{}{command}{instantiation}\hypertarget{command.instantiation}{\hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
595 |
\indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
596 |
\indexdef{}{command}{subclass}\hypertarget{command.subclass}{\hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
597 |
\indexdef{}{command}{print\_classes}\hypertarget{command.print-classes}{\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
598 |
\indexdef{}{method}{intro\_classes}\hypertarget{method.intro-classes}{\hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}} & : & \isa{method} \\ |
|
27042 | 599 |
\end{matharray} |
600 |
||
601 |
\begin{rail} |
|
602 |
'class' name '=' ((superclassexpr '+' (contextelem+)) | superclassexpr | (contextelem+)) \\ |
|
603 |
'begin'? |
|
604 |
; |
|
605 |
'instantiation' (nameref + 'and') '::' arity 'begin' |
|
606 |
; |
|
607 |
'instance' |
|
608 |
; |
|
609 |
'subclass' target? nameref |
|
610 |
; |
|
611 |
'print\_classes' |
|
612 |
; |
|
613 |
||
614 |
superclassexpr: nameref | (nameref '+' superclassexpr) |
|
615 |
; |
|
616 |
\end{rail} |
|
617 |
||
28788 | 618 |
\begin{description} |
27042 | 619 |
|
28788 | 620 |
\item \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}~\isa{{\isachardoublequote}c\ {\isacharequal}\ superclasses\ {\isacharplus}\ body{\isachardoublequote}} defines |
27042 | 621 |
a new class \isa{c}, inheriting from \isa{superclasses}. This |
622 |
introduces a locale \isa{c} with import of all locales \isa{superclasses}. |
|
623 |
||
624 |
Any \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} in \isa{body} are lifted to the global |
|
625 |
theory level (\emph{class operations} \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} of class \isa{c}), mapping the local type parameter |
|
626 |
\isa{{\isasymalpha}} to a schematic type variable \isa{{\isachardoublequote}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isachardoublequote}}. |
|
627 |
||
628 |
Likewise, \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} in \isa{body} are also lifted, |
|
629 |
mapping each local parameter \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} to its |
|
630 |
corresponding global constant \isa{{\isachardoublequote}f\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. The |
|
631 |
corresponding introduction rule is provided as \isa{c{\isacharunderscore}class{\isacharunderscore}axioms{\isachardot}intro}. This rule should be rarely needed directly |
|
632 |
--- the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method takes care of the details of |
|
633 |
class membership proofs. |
|
634 |
||
28788 | 635 |
\item \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s\ {\isasymBEGIN}{\isachardoublequote}} opens a theory target (cf.\ \secref{sec:target}) which |
636 |
allows to specify class operations \isa{{\isachardoublequote}f\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ f\isactrlsub n{\isachardoublequote}} corresponding |
|
637 |
to sort \isa{s} at the particular type instance \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ s\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}}. A plain \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command in the |
|
638 |
target body poses a goal stating these type arities. The target is |
|
639 |
concluded by an \indexref{local}{command}{end}\hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} command. |
|
27042 | 640 |
|
641 |
Note that a list of simultaneous type constructors may be given; |
|
642 |
this corresponds nicely to mutual recursive type definitions, e.g.\ |
|
643 |
in Isabelle/HOL. |
|
644 |
||
28788 | 645 |
\item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} in an instantiation target body sets |
27042 | 646 |
up a goal stating the type arities claimed at the opening \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of |
647 |
the type classes involved. After finishing the proof, the |
|
648 |
background theory will be augmented by the proven type arities. |
|
649 |
||
28788 | 650 |
\item \hyperlink{command.subclass}{\mbox{\isa{\isacommand{subclass}}}}~\isa{c} in a class context for class |
27042 | 651 |
\isa{d} sets up a goal stating that class \isa{c} is logically |
652 |
contained in class \isa{d}. After finishing the proof, class |
|
653 |
\isa{d} is proven to be subclass \isa{c} and the locale \isa{c} is interpreted into \isa{d} simultaneously. |
|
654 |
||
28788 | 655 |
\item \hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}} prints all classes in the current |
27042 | 656 |
theory. |
657 |
||
28788 | 658 |
\item \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} repeatedly expands all class |
27042 | 659 |
introduction rules of this theory. Note that this method usually |
660 |
needs not be named explicitly, as it is already included in the |
|
661 |
default proof step (e.g.\ of \hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}). In particular, |
|
662 |
instantiation of trivial (syntactic) classes may be performed by a |
|
663 |
single ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof step. |
|
26870 | 664 |
|
28788 | 665 |
\end{description}% |
26870 | 666 |
\end{isamarkuptext}% |
667 |
\isamarkuptrue% |
|
668 |
% |
|
27042 | 669 |
\isamarkupsubsection{The class target% |
670 |
} |
|
671 |
\isamarkuptrue% |
|
672 |
% |
|
673 |
\begin{isamarkuptext}% |
|
674 |
%FIXME check |
|
675 |
||
676 |
A named context may refer to a locale (cf.\ \secref{sec:target}). |
|
677 |
If this locale is also a class \isa{c}, apart from the common |
|
678 |
locale target behaviour the following happens. |
|
679 |
||
680 |
\begin{itemize} |
|
681 |
||
682 |
\item Local constant declarations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} referring to the |
|
683 |
local type parameter \isa{{\isasymalpha}} and local parameters \isa{{\isachardoublequote}f{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} |
|
684 |
are accompanied by theory-level constants \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} |
|
685 |
referring to theory-level class operations \isa{{\isachardoublequote}f{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}}. |
|
686 |
||
687 |
\item Local theorem bindings are lifted as are assumptions. |
|
688 |
||
689 |
\item Local syntax refers to local operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isasymalpha}{\isacharbrackright}{\isachardoublequote}} and |
|
690 |
global operations \isa{{\isachardoublequote}g{\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isacharcolon}{\isacharcolon}\ c{\isacharbrackright}{\isachardoublequote}} uniformly. Type inference |
|
691 |
resolves ambiguities. In rare cases, manual type annotations are |
|
692 |
needed. |
|
693 |
||
694 |
\end{itemize}% |
|
695 |
\end{isamarkuptext}% |
|
696 |
\isamarkuptrue% |
|
697 |
% |
|
27054 | 698 |
\isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}% |
27042 | 699 |
} |
700 |
\isamarkuptrue% |
|
701 |
% |
|
702 |
\begin{isamarkuptext}% |
|
27054 | 703 |
\begin{matharray}{rcl} |
28788 | 704 |
\indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
705 |
\indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\ |
|
27042 | 706 |
\end{matharray} |
707 |
||
708 |
Axiomatic type classes are Isabelle/Pure's primitive |
|
709 |
\emph{definitional} interface to type classes. For practical |
|
710 |
applications, you should consider using classes |
|
711 |
(cf.~\secref{sec:classes}) which provide high level interface. |
|
712 |
||
713 |
\begin{rail} |
|
714 |
'axclass' classdecl (axmdecl prop +) |
|
715 |
; |
|
716 |
'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity) |
|
717 |
; |
|
718 |
\end{rail} |
|
719 |
||
28788 | 720 |
\begin{description} |
27042 | 721 |
|
28788 | 722 |
\item \hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n\ axms{\isachardoublequote}} defines an |
723 |
axiomatic type class as the intersection of existing classes, with |
|
724 |
additional axioms holding. Class axioms may not contain more than |
|
725 |
one type variable. The class axioms (with implicit sort constraints |
|
726 |
added) are bound to the given names. Furthermore a class |
|
727 |
introduction rule is generated (being bound as \isa{c{\isacharunderscore}class{\isachardot}intro}); this rule is employed by method \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} to support instantiation proofs of this class. |
|
27042 | 728 |
|
28788 | 729 |
The ``class axioms'' (which are derived from the internal class |
730 |
definition) are stored as theorems according to the given name |
|
731 |
specifications; the name space prefix \isa{{\isachardoublequote}c{\isacharunderscore}class{\isachardoublequote}} is added |
|
732 |
here. The full collection of these facts is also stored as \isa{c{\isacharunderscore}class{\isachardot}axioms}. |
|
27042 | 733 |
|
28788 | 734 |
\item \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} and \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} setup a goal stating a class |
735 |
relation or type arity. The proof would usually proceed by \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}}, and then establish the characteristic theorems of |
|
736 |
the type classes involved. After finishing the proof, the theory |
|
737 |
will be augmented by a type signature declaration corresponding to |
|
738 |
the resulting theorem. |
|
27042 | 739 |
|
28788 | 740 |
\end{description}% |
27042 | 741 |
\end{isamarkuptext}% |
742 |
\isamarkuptrue% |
|
743 |
% |
|
744 |
\isamarkupsection{Unrestricted overloading% |
|
745 |
} |
|
746 |
\isamarkuptrue% |
|
747 |
% |
|
748 |
\begin{isamarkuptext}% |
|
749 |
Isabelle/Pure's definitional schemes support certain forms of |
|
750 |
overloading (see \secref{sec:consts}). At most occassions |
|
751 |
overloading will be used in a Haskell-like fashion together with |
|
752 |
type classes by means of \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} (see |
|
753 |
\secref{sec:class}). Sometimes low-level overloading is desirable. |
|
754 |
The \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}} target provides a convenient view for |
|
755 |
end-users. |
|
756 |
||
757 |
\begin{matharray}{rcl} |
|
28788 | 758 |
\indexdef{}{command}{overloading}\hypertarget{command.overloading}{\hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
27042 | 759 |
\end{matharray} |
760 |
||
761 |
\begin{rail} |
|
762 |
'overloading' \\ |
|
763 |
( string ( '==' | equiv ) term ( '(' 'unchecked' ')' )? + ) 'begin' |
|
764 |
\end{rail} |
|
765 |
||
28788 | 766 |
\begin{description} |
27042 | 767 |
|
28788 | 768 |
\item \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymequiv}\ c\isactrlsub {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isasymequiv}\ c\isactrlsub n\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}} |
27042 | 769 |
opens a theory target (cf.\ \secref{sec:target}) which allows to |
770 |
specify constants with overloaded definitions. These are identified |
|
28788 | 771 |
by an explicitly given mapping from variable names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} to |
772 |
constants \isa{{\isachardoublequote}c\isactrlsub i{\isachardoublequote}} at particular type instances. The |
|
773 |
definitions themselves are established using common specification |
|
774 |
tools, using the names \isa{{\isachardoublequote}x\isactrlsub i{\isachardoublequote}} as reference to the |
|
775 |
corresponding constants. The target is concluded by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}. |
|
27042 | 776 |
|
777 |
A \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks for |
|
778 |
the corresponding definition, which is occasionally useful for |
|
779 |
exotic overloading. It is at the discretion of the user to avoid |
|
780 |
malformed theory specifications! |
|
781 |
||
28788 | 782 |
\end{description}% |
27042 | 783 |
\end{isamarkuptext}% |
784 |
\isamarkuptrue% |
|
785 |
% |
|
786 |
\isamarkupsection{Incorporating ML code \label{sec:ML}% |
|
787 |
} |
|
788 |
\isamarkuptrue% |
|
789 |
% |
|
790 |
\begin{isamarkuptext}% |
|
791 |
\begin{matharray}{rcl} |
|
28788 | 792 |
\indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
793 |
\indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
794 |
\indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isa{{\isachardoublequote}proof\ {\isasymrightarrow}\ proof{\isachardoublequote}} \\ |
|
795 |
\indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
796 |
\indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
797 |
\indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
27042 | 798 |
\end{matharray} |
799 |
||
28788 | 800 |
\begin{mldecls} |
801 |
\indexml{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\ |
|
802 |
\indexml{bind\_thm}\verb|bind_thm: string * thm -> unit| \\ |
|
803 |
\end{mldecls} |
|
804 |
||
27042 | 805 |
\begin{rail} |
806 |
'use' name |
|
807 |
; |
|
28788 | 808 |
('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text |
27042 | 809 |
; |
810 |
\end{rail} |
|
811 |
||
28788 | 812 |
\begin{description} |
27042 | 813 |
|
28788 | 814 |
\item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isachardoublequote}file{\isachardoublequote}} reads and executes ML |
27042 | 815 |
commands from \isa{{\isachardoublequote}file{\isachardoublequote}}. The current theory context is passed |
28788 | 816 |
down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with |
27042 | 817 |
the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory |
818 |
header (see also \secref{sec:begin-thy}). |
|
28281 | 819 |
|
820 |
Top-level ML bindings are stored within the (global or local) theory |
|
821 |
context. |
|
27042 | 822 |
|
28788 | 823 |
\item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, |
824 |
but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}. |
|
825 |
Top-level ML bindings are stored within the (global or local) theory |
|
826 |
context. |
|
28281 | 827 |
|
28788 | 828 |
\item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works |
829 |
within a proof context. |
|
28281 | 830 |
|
831 |
Top-level ML bindings are stored within the proof context in a |
|
832 |
purely sequential fashion, disregarding the nested proof structure. |
|
833 |
ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} are discarded at the |
|
834 |
end of the proof. |
|
27042 | 835 |
|
28788 | 836 |
\item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are diagnostic |
837 |
versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be |
|
838 |
updated. \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} echos the bindings produced at the ML |
|
839 |
toplevel, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent. |
|
27042 | 840 |
|
28788 | 841 |
\item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory |
27042 | 842 |
context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression |
28788 | 843 |
of type \verb|theory -> theory|. This enables |
844 |
to initialize any object-logic specific tools and packages written |
|
845 |
in ML, for example. |
|
27042 | 846 |
|
28788 | 847 |
\item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of |
848 |
theorems produced in ML both in the theory context and the ML |
|
849 |
toplevel, associating it with the provided name. Theorems are put |
|
850 |
into a global ``standard'' format before being stored. |
|
27042 | 851 |
|
28788 | 852 |
\item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a |
853 |
singleton theorem. |
|
854 |
||
855 |
\end{description}% |
|
27042 | 856 |
\end{isamarkuptext}% |
857 |
\isamarkuptrue% |
|
858 |
% |
|
859 |
\isamarkupsection{Primitive specification elements% |
|
860 |
} |
|
861 |
\isamarkuptrue% |
|
862 |
% |
|
863 |
\isamarkupsubsection{Type classes and sorts \label{sec:classes}% |
|
864 |
} |
|
865 |
\isamarkuptrue% |
|
866 |
% |
|
867 |
\begin{isamarkuptext}% |
|
868 |
\begin{matharray}{rcll} |
|
28788 | 869 |
\indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
870 |
\indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\ |
|
871 |
\indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
872 |
\indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
27042 | 873 |
\end{matharray} |
874 |
||
875 |
\begin{rail} |
|
876 |
'classes' (classdecl +) |
|
877 |
; |
|
878 |
'classrel' (nameref ('<' | subseteq) nameref + 'and') |
|
879 |
; |
|
880 |
'defaultsort' sort |
|
881 |
; |
|
882 |
\end{rail} |
|
883 |
||
28788 | 884 |
\begin{description} |
27042 | 885 |
|
28788 | 886 |
\item \hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}~\isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}} declares class |
887 |
\isa{c} to be a subclass of existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n{\isachardoublequote}}. |
|
888 |
Isabelle implicitly maintains the transitive closure of the class |
|
889 |
hierarchy. Cyclic class structures are not permitted. |
|
890 |
||
891 |
\item \hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}~\isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} states subclass |
|
892 |
relations between existing classes \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}{\isachardoublequote}} and \isa{{\isachardoublequote}c\isactrlsub {\isadigit{2}}{\isachardoublequote}}. |
|
893 |
This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} command |
|
894 |
(see \secref{sec:axclass}) provides a way to introduce proven class |
|
895 |
relations. |
|
27042 | 896 |
|
28788 | 897 |
\item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the |
898 |
new default sort for any type variable that is given explicitly in |
|
899 |
the text, but lacks a sort constraint (wrt.\ the current context). |
|
900 |
Type variables generated by type inference are not affected. |
|
27042 | 901 |
|
28788 | 902 |
Usually the default sort is only changed when defining a new |
903 |
object-logic. For example, the default sort in Isabelle/HOL is |
|
904 |
\isa{type}, the class of all HOL types. %FIXME sort antiq? |
|
27042 | 905 |
|
28788 | 906 |
When merging theories, the default sorts of the parents are |
907 |
logically intersected, i.e.\ the representations as lists of classes |
|
908 |
are joined. |
|
909 |
||
910 |
\item \hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}} visualizes the subclass relation, |
|
27042 | 911 |
using Isabelle's graph browser tool (see also \cite{isabelle-sys}). |
912 |
||
28788 | 913 |
\end{description}% |
27042 | 914 |
\end{isamarkuptext}% |
915 |
\isamarkuptrue% |
|
916 |
% |
|
917 |
\isamarkupsubsection{Types and type abbreviations \label{sec:types-pure}% |
|
918 |
} |
|
919 |
\isamarkuptrue% |
|
920 |
% |
|
921 |
\begin{isamarkuptext}% |
|
922 |
\begin{matharray}{rcll} |
|
28788 | 923 |
\indexdef{}{command}{types}\hypertarget{command.types}{\hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
924 |
\indexdef{}{command}{typedecl}\hypertarget{command.typedecl}{\hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
925 |
\indexdef{}{command}{arities}\hypertarget{command.arities}{\hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\ |
|
27042 | 926 |
\end{matharray} |
927 |
||
928 |
\begin{rail} |
|
929 |
'types' (typespec '=' type infix? +) |
|
930 |
; |
|
931 |
'typedecl' typespec infix? |
|
932 |
; |
|
933 |
'arities' (nameref '::' arity +) |
|
934 |
; |
|
935 |
\end{rail} |
|
936 |
||
28788 | 937 |
\begin{description} |
27042 | 938 |
|
28788 | 939 |
\item \hyperlink{command.types}{\mbox{\isa{\isacommand{types}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}{\isachardoublequote}} introduces a |
940 |
\emph{type synonym} \isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} for the existing type |
|
941 |
\isa{{\isachardoublequote}{\isasymtau}{\isachardoublequote}}. Unlike actual type definitions, as are available in |
|
942 |
Isabelle/HOL for example, type synonyms are merely syntactic |
|
943 |
abbreviations without any logical significance. Internally, type |
|
944 |
synonyms are fully expanded. |
|
27042 | 945 |
|
28788 | 946 |
\item \hyperlink{command.typedecl}{\mbox{\isa{\isacommand{typedecl}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t{\isachardoublequote}} declares a new |
947 |
type constructor \isa{t}. If the object-logic defines a base sort |
|
948 |
\isa{s}, then the constructor is declared to operate on that, via |
|
949 |
the axiomatic specification \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s{\isacharparenright}s{\isachardoublequote}}. |
|
950 |
||
951 |
\item \hyperlink{command.arities}{\mbox{\isa{\isacommand{arities}}}}~\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}s{\isachardoublequote}} augments |
|
952 |
Isabelle's order-sorted signature of types by new type constructor |
|
953 |
arities. This is done axiomatically! The \indexref{}{command}{instance}\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} |
|
954 |
command (see \secref{sec:axclass}) provides a way to introduce |
|
955 |
proven type arities. |
|
956 |
||
957 |
\end{description}% |
|
958 |
\end{isamarkuptext}% |
|
959 |
\isamarkuptrue% |
|
960 |
% |
|
961 |
\isamarkupsubsection{Co-regularity of type classes and arities% |
|
962 |
} |
|
963 |
\isamarkuptrue% |
|
964 |
% |
|
965 |
\begin{isamarkuptext}% |
|
966 |
The class relation together with the collection of |
|
967 |
type-constructor arities must obey the principle of |
|
968 |
\emph{co-regularity} as defined below. |
|
27042 | 969 |
|
28788 | 970 |
\medskip For the subsequent formulation of co-regularity we assume |
971 |
that the class relation is closed by transitivity and reflexivity. |
|
972 |
Moreover the collection of arities \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} is |
|
973 |
completed such that \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isachardoublequote}} and \isa{{\isachardoublequote}c\ {\isasymsubseteq}\ c{\isacharprime}{\isachardoublequote}} |
|
974 |
implies \isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s{\isacharparenright}c{\isacharprime}{\isachardoublequote}} for all such declarations. |
|
975 |
||
976 |
Treating sorts as finite sets of classes (meaning the intersection), |
|
977 |
the class relation \isa{{\isachardoublequote}c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} is extended to sorts as |
|
978 |
follows: |
|
979 |
\[ |
|
980 |
\isa{{\isachardoublequote}s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ s\isactrlsub {\isadigit{2}}\ {\isasymequiv}\ {\isasymforall}c\isactrlsub {\isadigit{2}}\ {\isasymin}\ s\isactrlsub {\isadigit{2}}{\isachardot}\ {\isasymexists}c\isactrlsub {\isadigit{1}}\ {\isasymin}\ s\isactrlsub {\isadigit{1}}{\isachardot}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}{\isachardoublequote}} |
|
981 |
\] |
|
27042 | 982 |
|
28788 | 983 |
This relation on sorts is further extended to tuples of sorts (of |
984 |
the same length) in the component-wise way. |
|
27042 | 985 |
|
28788 | 986 |
\smallskip Co-regularity of the class relation together with the |
987 |
arities relation means: |
|
988 |
\[ |
|
989 |
\isa{{\isachardoublequote}t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{1}}{\isacharparenright}c\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}\isactrlvec s\isactrlsub {\isadigit{2}}{\isacharparenright}c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}\ {\isasymLongrightarrow}\ \isactrlvec s\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ \isactrlvec s\isactrlsub {\isadigit{2}}{\isachardoublequote}} |
|
990 |
\] |
|
991 |
\noindent for all such arities. In other words, whenever the result |
|
992 |
classes of some type-constructor arities are related, then the |
|
993 |
argument sorts need to be related in the same way. |
|
994 |
||
995 |
\medskip Co-regularity is a very fundamental property of the |
|
996 |
order-sorted algebra of types. For example, it entails principle |
|
997 |
types and most general unifiers, e.g.\ see \cite{nipkow-prehofer}.% |
|
27042 | 998 |
\end{isamarkuptext}% |
999 |
\isamarkuptrue% |
|
1000 |
% |
|
1001 |
\isamarkupsubsection{Constants and definitions \label{sec:consts}% |
|
1002 |
} |
|
1003 |
\isamarkuptrue% |
|
1004 |
% |
|
1005 |
\begin{isamarkuptext}% |
|
1006 |
Definitions essentially express abbreviations within the logic. The |
|
1007 |
simplest form of a definition is \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t{\isachardoublequote}}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms |
|
1008 |
where the arguments of \isa{c} appear on the left, abbreviating a |
|
1009 |
prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{{\isachardoublequote}c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t{\isachardoublequote}} may be |
|
1010 |
written more conveniently as \isa{{\isachardoublequote}c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. Moreover, |
|
1011 |
definitions may be weakened by adding arbitrary pre-conditions: |
|
1012 |
\isa{{\isachardoublequote}A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t{\isachardoublequote}}. |
|
1013 |
||
1014 |
\medskip The built-in well-formedness conditions for definitional |
|
1015 |
specifications are: |
|
1016 |
||
1017 |
\begin{itemize} |
|
1018 |
||
1019 |
\item Arguments (on the left-hand side) must be distinct variables. |
|
1020 |
||
1021 |
\item All variables on the right-hand side must also appear on the |
|
1022 |
left-hand side. |
|
1023 |
||
1024 |
\item All type variables on the right-hand side must also appear on |
|
1025 |
the left-hand side; this prohibits \isa{{\isachardoublequote}{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}{\isachardoublequote}} for example. |
|
1026 |
||
1027 |
\item The definition must not be recursive. Most object-logics |
|
1028 |
provide definitional principles that can be used to express |
|
1029 |
recursion safely. |
|
1030 |
||
1031 |
\end{itemize} |
|
1032 |
||
1033 |
Overloading means that a constant being declared as \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl{\isachardoublequote}} may be defined separately on type instances \isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl{\isachardoublequote}} for each type constructor \isa{t}. The right-hand side may mention overloaded constants |
|
1034 |
recursively at type instances corresponding to the immediate |
|
1035 |
argument types \isa{{\isachardoublequote}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isachardoublequote}}. Incomplete |
|
1036 |
specification patterns impose global constraints on all occurrences, |
|
1037 |
e.g.\ \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}{\isachardoublequote}} on the left-hand side means that all |
|
1038 |
corresponding occurrences on some right-hand side need to be an |
|
1039 |
instance of this, general \isa{{\isachardoublequote}d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}{\isachardoublequote}} will be disallowed. |
|
1040 |
||
1041 |
\begin{matharray}{rcl} |
|
28788 | 1042 |
\indexdef{}{command}{consts}\hypertarget{command.consts}{\hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1043 |
\indexdef{}{command}{defs}\hypertarget{command.defs}{\hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
1044 |
\indexdef{}{command}{constdefs}\hypertarget{command.constdefs}{\hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
27042 | 1045 |
\end{matharray} |
1046 |
||
1047 |
\begin{rail} |
|
1048 |
'consts' ((name '::' type mixfix?) +) |
|
1049 |
; |
|
1050 |
'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) |
|
1051 |
; |
|
1052 |
\end{rail} |
|
1053 |
||
1054 |
\begin{rail} |
|
1055 |
'constdefs' structs? (constdecl? constdef +) |
|
1056 |
; |
|
1057 |
||
1058 |
structs: '(' 'structure' (vars + 'and') ')' |
|
1059 |
; |
|
1060 |
constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' |
|
1061 |
; |
|
1062 |
constdef: thmdecl? prop |
|
1063 |
; |
|
1064 |
\end{rail} |
|
1065 |
||
28788 | 1066 |
\begin{description} |
27042 | 1067 |
|
28788 | 1068 |
\item \hyperlink{command.consts}{\mbox{\isa{\isacommand{consts}}}}~\isa{{\isachardoublequote}c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}{\isachardoublequote}} declares constant \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The optional |
1069 |
mixfix annotations may attach concrete syntax to the constants |
|
1070 |
declared. |
|
27042 | 1071 |
|
28788 | 1072 |
\item \hyperlink{command.defs}{\mbox{\isa{\isacommand{defs}}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ eqn{\isachardoublequote}} introduces \isa{eqn} |
27042 | 1073 |
as a definitional axiom for some existing constant. |
1074 |
||
1075 |
The \isa{{\isachardoublequote}{\isacharparenleft}unchecked{\isacharparenright}{\isachardoublequote}} option disables global dependency checks |
|
1076 |
for this definition, which is occasionally useful for exotic |
|
1077 |
overloading. It is at the discretion of the user to avoid malformed |
|
1078 |
theory specifications! |
|
1079 |
||
1080 |
The \isa{{\isachardoublequote}{\isacharparenleft}overloaded{\isacharparenright}{\isachardoublequote}} option declares definitions to be |
|
1081 |
potentially overloaded. Unless this option is given, a warning |
|
1082 |
message would be issued for any definitional equation with a more |
|
1083 |
special type than that of the corresponding constant declaration. |
|
1084 |
||
28788 | 1085 |
\item \hyperlink{command.constdefs}{\mbox{\isa{\isacommand{constdefs}}}} combines constant declarations and |
1086 |
definitions, with type-inference taking care of the most general |
|
1087 |
typing of the given specification (the optional type constraint may |
|
1088 |
refer to type-inference dummies ``\isa{{\isacharunderscore}}'' as usual). The |
|
1089 |
resulting type declaration needs to agree with that of the |
|
1090 |
specification; overloading is \emph{not} supported here! |
|
27042 | 1091 |
|
1092 |
The constant name may be omitted altogether, if neither type nor |
|
1093 |
syntax declarations are given. The canonical name of the |
|
1094 |
definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def}, |
|
1095 |
unless specified otherwise. Also note that the given list of |
|
1096 |
specifications is processed in a strictly sequential manner, with |
|
1097 |
type-checking being performed independently. |
|
1098 |
||
1099 |
An optional initial context of \isa{{\isachardoublequote}{\isacharparenleft}structure{\isacharparenright}{\isachardoublequote}} declarations |
|
1100 |
admits use of indexed syntax, using the special symbol \verb|\<index>| (printed as ``\isa{{\isachardoublequote}{\isasymindex}{\isachardoublequote}}''). The latter concept is |
|
28788 | 1101 |
particularly useful with locales (see also \secref{sec:locale}). |
27042 | 1102 |
|
28788 | 1103 |
\end{description}% |
27042 | 1104 |
\end{isamarkuptext}% |
1105 |
\isamarkuptrue% |
|
1106 |
% |
|
1107 |
\isamarkupsection{Axioms and theorems \label{sec:axms-thms}% |
|
1108 |
} |
|
1109 |
\isamarkuptrue% |
|
1110 |
% |
|
1111 |
\begin{isamarkuptext}% |
|
1112 |
\begin{matharray}{rcll} |
|
28788 | 1113 |
\indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\ |
1114 |
\indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
1115 |
\indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\ |
|
27042 | 1116 |
\end{matharray} |
1117 |
||
1118 |
\begin{rail} |
|
1119 |
'axioms' (axmdecl prop +) |
|
1120 |
; |
|
1121 |
('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') |
|
1122 |
; |
|
1123 |
\end{rail} |
|
1124 |
||
28788 | 1125 |
\begin{description} |
27042 | 1126 |
|
28788 | 1127 |
\item \hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} introduces arbitrary |
27042 | 1128 |
statements as axioms of the meta-logic. In fact, axioms are |
1129 |
``axiomatic theorems'', and may be referred later just as any other |
|
1130 |
theorem. |
|
1131 |
||
1132 |
Axioms are usually only introduced when declaring new logical |
|
1133 |
systems. Everyday work is typically done the hard way, with proper |
|
1134 |
definitions and proven theorems. |
|
1135 |
||
28788 | 1136 |
\item \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} retrieves and stores |
1137 |
existing facts in the theory context, or the specified target |
|
1138 |
context (see also \secref{sec:target}). Typical applications would |
|
1139 |
also involve attributes, to declare Simplifier rules, for example. |
|
27042 | 1140 |
|
28788 | 1141 |
\item \hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}} is essentially the same as \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}, but marks the result as a different kind of facts. |
27042 | 1142 |
|
28788 | 1143 |
\end{description}% |
27042 | 1144 |
\end{isamarkuptext}% |
1145 |
\isamarkuptrue% |
|
1146 |
% |
|
1147 |
\isamarkupsection{Oracles% |
|
1148 |
} |
|
1149 |
\isamarkuptrue% |
|
1150 |
% |
|
1151 |
\begin{isamarkuptext}% |
|
28788 | 1152 |
Oracles allow Isabelle to take advantage of external reasoners |
1153 |
such as arithmetic decision procedures, model checkers, fast |
|
1154 |
tautology checkers or computer algebra systems. Invoked as an |
|
1155 |
oracle, an external reasoner can create arbitrary Isabelle theorems. |
|
27042 | 1156 |
|
28788 | 1157 |
It is the responsibility of the user to ensure that the external |
1158 |
reasoner is as trustworthy as the application requires. Another |
|
1159 |
typical source of errors is the linkup between Isabelle and the |
|
1160 |
external tool, not just its concrete implementation, but also the |
|
1161 |
required translation between two different logical environments. |
|
1162 |
||
1163 |
Isabelle merely guarantees well-formedness of the propositions being |
|
1164 |
asserted, and records within the internal derivation object how |
|
1165 |
presumed theorems depend on unproven suppositions. |
|
1166 |
||
1167 |
\begin{matharray}{rcl} |
|
1168 |
\indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
1169 |
\end{matharray} |
|
27042 | 1170 |
|
1171 |
\begin{rail} |
|
28291 | 1172 |
'oracle' name '=' text |
27042 | 1173 |
; |
1174 |
\end{rail} |
|
1175 |
||
28788 | 1176 |
\begin{description} |
27042 | 1177 |
|
28788 | 1178 |
\item \hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}} turns the given ML |
28291 | 1179 |
expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an |
1180 |
ML function of type \verb|'a -> thm|, which is bound to the |
|
28788 | 1181 |
global identifier \verb|name|. This acts like an infinitary |
1182 |
specification of axioms! Invoking the oracle only works within the |
|
1183 |
scope of the resulting theory. |
|
27042 | 1184 |
|
28788 | 1185 |
\end{description} |
1186 |
||
1187 |
See \hyperlink{file.~~/src/FOL/ex/IffOracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}IffOracle{\isachardot}thy}}}} for a worked example of |
|
1188 |
defining a new primitive rule as oracle, and turning it into a proof |
|
1189 |
method.% |
|
27042 | 1190 |
\end{isamarkuptext}% |
1191 |
\isamarkuptrue% |
|
1192 |
% |
|
1193 |
\isamarkupsection{Name spaces% |
|
1194 |
} |
|
1195 |
\isamarkuptrue% |
|
1196 |
% |
|
1197 |
\begin{isamarkuptext}% |
|
1198 |
\begin{matharray}{rcl} |
|
28788 | 1199 |
\indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
1200 |
\indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
1201 |
\indexdef{}{command}{hide}\hypertarget{command.hide}{\hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\ |
|
27042 | 1202 |
\end{matharray} |
1203 |
||
1204 |
\begin{rail} |
|
1205 |
'hide' ('(open)')? name (nameref + ) |
|
1206 |
; |
|
1207 |
\end{rail} |
|
1208 |
||
1209 |
Isabelle organizes any kind of name declarations (of types, |
|
1210 |
constants, theorems etc.) by separate hierarchically structured name |
|
1211 |
spaces. Normally the user does not have to control the behavior of |
|
1212 |
name spaces by hand, yet the following commands provide some way to |
|
1213 |
do so. |
|
1214 |
||
28788 | 1215 |
\begin{description} |
27042 | 1216 |
|
28788 | 1217 |
\item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current |
1218 |
name declaration mode. Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by |
|
1219 |
the theory name. Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all |
|
1220 |
names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again. |
|
27042 | 1221 |
|
1222 |
Note that global names are prone to get hidden accidently later, |
|
1223 |
when qualified names of the same base name are introduced. |
|
1224 |
||
28788 | 1225 |
\item \hyperlink{command.hide}{\mbox{\isa{\isacommand{hide}}}}~\isa{{\isachardoublequote}space\ names{\isachardoublequote}} fully removes |
27042 | 1226 |
declarations from a given name space (which may be \isa{{\isachardoublequote}class{\isachardoublequote}}, |
1227 |
\isa{{\isachardoublequote}type{\isachardoublequote}}, \isa{{\isachardoublequote}const{\isachardoublequote}}, or \isa{{\isachardoublequote}fact{\isachardoublequote}}); with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}} option, only the base name is hidden. Global |
|
1228 |
(unqualified) names may never be hidden. |
|
1229 |
||
1230 |
Note that hiding name space accesses has no impact on logical |
|
28788 | 1231 |
declarations --- they remain valid internally. Entities that are no |
27042 | 1232 |
longer accessible to the user are printed with the special qualifier |
1233 |
``\isa{{\isachardoublequote}{\isacharquery}{\isacharquery}{\isachardoublequote}}'' prefixed to the full internal name. |
|
1234 |
||
28788 | 1235 |
\end{description}% |
27042 | 1236 |
\end{isamarkuptext}% |
1237 |
\isamarkuptrue% |
|
1238 |
% |
|
26869 | 1239 |
\isadelimtheory |
1240 |
% |
|
1241 |
\endisadelimtheory |
|
1242 |
% |
|
1243 |
\isatagtheory |
|
1244 |
\isacommand{end}\isamarkupfalse% |
|
1245 |
% |
|
1246 |
\endisatagtheory |
|
1247 |
{\isafoldtheory}% |
|
1248 |
% |
|
1249 |
\isadelimtheory |
|
1250 |
% |
|
1251 |
\endisadelimtheory |
|
1252 |
\isanewline |
|
1253 |
\end{isabellebody}% |
|
1254 |
%%% Local Variables: |
|
1255 |
%%% mode: latex |
|
1256 |
%%% TeX-master: "root" |
|
1257 |
%%% End: |