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