author | wenzelm |
Sat, 11 Jun 2016 16:41:11 +0200 | |
changeset 63285 | e9c777bfd78c |
parent 63282 | 7c509ddf29a5 |
child 63531 | 847eefdca90d |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
2 |
||
26869 | 3 |
theory Spec |
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61665
diff
changeset
|
4 |
imports Base Main |
26869 | 5 |
begin |
6 |
||
58618 | 7 |
chapter \<open>Specifications\<close> |
26869 | 8 |
|
61664 | 9 |
text \<open> |
10 |
The Isabelle/Isar theory format integrates specifications and proofs, with |
|
11 |
support for interactive development by continuous document editing. There is |
|
12 |
a separate document preparation system (see \chref{ch:document-prep}), for |
|
13 |
typesetting formal developments together with informal text. The resulting |
|
14 |
hyper-linked PDF documents can be used both for WWW presentation and printed |
|
15 |
copies. |
|
29745 | 16 |
|
61664 | 17 |
The Isar proof language (see \chref{ch:proofs}) is embedded into the theory |
18 |
language as a proper sub-language. Proof mode is entered by stating some |
|
61665 | 19 |
\<^theory_text>\<open>theorem\<close> or \<^theory_text>\<open>lemma\<close> at the theory level, and left again with the final |
20 |
conclusion (e.g.\ via \<^theory_text>\<open>qed\<close>). |
|
58618 | 21 |
\<close> |
29745 | 22 |
|
23 |
||
58618 | 24 |
section \<open>Defining theories \label{sec:begin-thy}\<close> |
26870 | 25 |
|
58618 | 26 |
text \<open> |
26870 | 27 |
\begin{matharray}{rcl} |
61493 | 28 |
@{command_def "theory"} & : & \<open>toplevel \<rightarrow> theory\<close> \\ |
29 |
@{command_def (global) "end"} & : & \<open>theory \<rightarrow> toplevel\<close> \\ |
|
30 |
@{command_def "thy_deps"}\<open>\<^sup>*\<close> & : & \<open>theory \<rightarrow>\<close> \\ |
|
26870 | 31 |
\end{matharray} |
32 |
||
59781 | 33 |
Isabelle/Isar theories are defined via theory files, which consist of an |
34 |
outermost sequence of definition--statement--proof elements. Some |
|
61665 | 35 |
definitions are self-sufficient (e.g.\ \<^theory_text>\<open>fun\<close> in Isabelle/HOL), with |
61664 | 36 |
foundational proofs performed internally. Other definitions require an |
61665 | 37 |
explicit proof as justification (e.g.\ \<^theory_text>\<open>function\<close> and \<^theory_text>\<open>termination\<close> in |
38 |
Isabelle/HOL). Plain statements like \<^theory_text>\<open>theorem\<close> or \<^theory_text>\<open>lemma\<close> are merely a |
|
39 |
special case of that, defining a theorem from a given proposition and its |
|
40 |
proof. |
|
26870 | 41 |
|
61664 | 42 |
The theory body may be sub-structured by means of \<^emph>\<open>local theory targets\<close>, |
61706 | 43 |
such as \<^theory_text>\<open>locale\<close> and \<^theory_text>\<open>class\<close>. It is also possible to use \<^theory_text>\<open>context begin \<dots> |
44 |
end\<close> blocks to delimited a local theory context: a \<^emph>\<open>named context\<close> to |
|
45 |
augment a locale or class specification, or an \<^emph>\<open>unnamed context\<close> to refer |
|
46 |
to local parameters and assumptions that are discharged later. See |
|
47 |
\secref{sec:target} for more details. |
|
28745 | 48 |
|
61421 | 49 |
\<^medskip> |
61665 | 50 |
A theory is commenced by the \<^theory_text>\<open>theory\<close> command, which indicates imports of |
51 |
previous theories, according to an acyclic foundational order. Before the |
|
52 |
initial \<^theory_text>\<open>theory\<close> command, there may be optional document header material |
|
53 |
(like \<^theory_text>\<open>section\<close> or \<^theory_text>\<open>text\<close>, see \secref{sec:markup}). The document header |
|
54 |
is outside of the formal theory context, though. |
|
59781 | 55 |
|
61664 | 56 |
A theory is concluded by a final @{command (global) "end"} command, one that |
57 |
does not belong to a local theory target. No further commands may follow |
|
58 |
such a global @{command (global) "end"}. |
|
26870 | 59 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
60 |
@{rail \<open> |
59781 | 61 |
@@{command theory} @{syntax name} imports? keywords? \<newline> @'begin' |
26870 | 62 |
; |
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
63 |
imports: @'imports' (@{syntax name} +) |
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
64 |
; |
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
65 |
keywords: @'keywords' (keyword_decls + @'and') |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
66 |
; |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
67 |
keyword_decls: (@{syntax string} +) |
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
68 |
('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})? |
60093 | 69 |
; |
70 |
@@{command thy_deps} (thy_bounds thy_bounds?)? |
|
71 |
; |
|
72 |
thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')' |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
73 |
\<close>} |
26870 | 74 |
|
61665 | 75 |
\<^descr> \<^theory_text>\<open>theory A imports B\<^sub>1 \<dots> B\<^sub>n begin\<close> starts a new theory \<open>A\<close> based on the |
76 |
merge of existing theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>. Due to the possibility to import |
|
77 |
more than one ancestor, the resulting theory structure of an Isabelle |
|
78 |
session forms a directed acyclic graph (DAG). Isabelle takes care that |
|
79 |
sources contributing to the development graph are always up-to-date: changed |
|
80 |
files are automatically rechecked whenever a theory header specification is |
|
81 |
processed. |
|
47114
7c9e31ffcd9e
updated theory header syntax and related details;
wenzelm
parents:
46999
diff
changeset
|
82 |
|
59781 | 83 |
Empty imports are only allowed in the bootstrap process of the special |
84 |
theory @{theory Pure}, which is the start of any other formal development |
|
61664 | 85 |
based on Isabelle. Regular user theories usually refer to some more complex |
86 |
entry point, such as theory @{theory Main} in Isabelle/HOL. |
|
59781 | 87 |
|
61664 | 88 |
The optional @{keyword_def "keywords"} specification declares outer syntax |
89 |
(\chref{ch:outer-syntax}) that is introduced in this theory later on (rare |
|
90 |
in end-user applications). Both minor keywords and major keywords of the |
|
91 |
Isar command language need to be specified, in order to make parsing of |
|
92 |
proof documents work properly. Command keywords need to be classified |
|
93 |
according to their structural role in the formal text. Examples may be seen |
|
94 |
in Isabelle/HOL sources itself, such as @{keyword "keywords"}~\<^verbatim>\<open>"typedef"\<close> |
|
95 |
\<open>:: thy_goal\<close> or @{keyword "keywords"}~\<^verbatim>\<open>"datatype"\<close> \<open>:: thy_decl\<close> for |
|
96 |
theory-level declarations with and without proof, respectively. Additional |
|
97 |
@{syntax tags} provide defaults for document preparation |
|
98 |
(\secref{sec:tags}). |
|
50128
599c935aac82
alternative completion for outer syntax keywords;
wenzelm
parents:
49243
diff
changeset
|
99 |
|
61664 | 100 |
It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>, while |
101 |
the default is the corresponding keyword name. |
|
26870 | 102 |
|
61664 | 103 |
\<^descr> @{command (global) "end"} concludes the current theory definition. Note |
61665 | 104 |
that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close> |
105 |
may involve a \<^theory_text>\<open>begin\<close> that needs to be matched by @{command (local) "end"}, |
|
106 |
according to the usual rules for nested blocks. |
|
27040 | 107 |
|
61665 | 108 |
\<^descr> \<^theory_text>\<open>thy_deps\<close> visualizes the theory hierarchy as a directed acyclic graph. |
109 |
By default, all imported theories are shown, taking the base session as a |
|
110 |
starting point. Alternatively, it is possibly to restrict the full theory |
|
111 |
graph by giving bounds, analogously to @{command_ref class_deps}. |
|
58618 | 112 |
\<close> |
27040 | 113 |
|
114 |
||
58618 | 115 |
section \<open>Local theory targets \label{sec:target}\<close> |
27040 | 116 |
|
58618 | 117 |
text \<open> |
47483 | 118 |
\begin{matharray}{rcll} |
61493 | 119 |
@{command_def "context"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ |
120 |
@{command_def (local) "end"} & : & \<open>local_theory \<rightarrow> theory\<close> \\ |
|
59926 | 121 |
@{keyword_def "private"} \\ |
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset
|
122 |
@{keyword_def "qualified"} \\ |
47483 | 123 |
\end{matharray} |
124 |
||
61664 | 125 |
A local theory target is a specification context that is managed separately |
126 |
within the enclosing theory. Contexts may introduce parameters (fixed |
|
127 |
variables) and assumptions (hypotheses). Definitions and theorems depending |
|
128 |
on the context may be added incrementally later on. |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
129 |
|
61664 | 130 |
\<^emph>\<open>Named contexts\<close> refer to locales (cf.\ \secref{sec:locale}) or type |
131 |
classes (cf.\ \secref{sec:class}); the name ``\<open>-\<close>'' signifies the global |
|
132 |
theory context. |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
133 |
|
61664 | 134 |
\<^emph>\<open>Unnamed contexts\<close> may introduce additional parameters and assumptions, and |
135 |
results produced in the context are generalized accordingly. Such auxiliary |
|
61665 | 136 |
contexts may be nested within other targets, like \<^theory_text>\<open>locale\<close>, \<^theory_text>\<open>class\<close>, |
137 |
\<^theory_text>\<open>instantiation\<close>, \<^theory_text>\<open>overloading\<close>. |
|
27040 | 138 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
139 |
@{rail \<open> |
62969 | 140 |
@@{command context} @{syntax name} @'begin' |
27040 | 141 |
; |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
142 |
@@{command context} @{syntax_ref "includes"}? (@{syntax context_elem} * ) @'begin' |
47484 | 143 |
; |
62969 | 144 |
@{syntax_def target}: '(' @'in' @{syntax name} ')' |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
145 |
\<close>} |
27040 | 146 |
|
61665 | 147 |
\<^descr> \<^theory_text>\<open>context c begin\<close> opens a named context, by recommencing an existing |
148 |
locale or class \<open>c\<close>. Note that locale and class definitions allow to include |
|
149 |
the \<^theory_text>\<open>begin\<close> keyword as well, in order to continue the local theory |
|
150 |
immediately after the initial specification. |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47114
diff
changeset
|
151 |
|
61665 | 152 |
\<^descr> \<^theory_text>\<open>context bundles elements begin\<close> opens an unnamed context, by extending |
153 |
the enclosing global or local theory target by the given declaration bundles |
|
154 |
(\secref{sec:bundle}) and context elements (\<^theory_text>\<open>fixes\<close>, \<^theory_text>\<open>assumes\<close> etc.). This |
|
155 |
means any results stemming from definitions and proofs in the extended |
|
156 |
context will be exported into the enclosing target by lifting over extra |
|
157 |
parameters and premises. |
|
61664 | 158 |
|
159 |
\<^descr> @{command (local) "end"} concludes the current local theory, according to |
|
160 |
the nesting of contexts. Note that a global @{command (global) "end"} has a |
|
161 |
different meaning: it concludes the theory itself (\secref{sec:begin-thy}). |
|
27040 | 162 |
|
61665 | 163 |
\<^descr> \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> may be given as modifiers before any local |
164 |
theory command. This restricts name space accesses to the local scope, as |
|
165 |
determined by the enclosing \<^theory_text>\<open>context begin \<dots> end\<close> block. Outside its scope, |
|
166 |
a \<^theory_text>\<open>private\<close> name is inaccessible, and a \<^theory_text>\<open>qualified\<close> name is only |
|
61664 | 167 |
accessible with some qualification. |
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59926
diff
changeset
|
168 |
|
61665 | 169 |
Neither a global \<^theory_text>\<open>theory\<close> nor a \<^theory_text>\<open>locale\<close> target provides a local scope by |
170 |
itself: an extra unnamed context is required to use \<^theory_text>\<open>private\<close> or |
|
171 |
\<^theory_text>\<open>qualified\<close> here. |
|
59926 | 172 |
|
61664 | 173 |
\<^descr> \<open>(\<close>@{keyword_def "in"}~\<open>c)\<close> given after any local theory command specifies |
61665 | 174 |
an immediate target, e.g.\ ``\<^theory_text>\<open>definition (in c)\<close>'' or |
175 |
``\<^theory_text>\<open>theorem (in c)\<close>''. This works both in a local or global theory context; |
|
176 |
the current target context will be suspended for this command only. Note |
|
177 |
that ``\<^theory_text>\<open>(in -)\<close>'' will always produce a global result independently of the |
|
178 |
current target context. |
|
27040 | 179 |
|
180 |
||
61664 | 181 |
Any specification element that operates on \<open>local_theory\<close> according to this |
61665 | 182 |
manual implicitly allows the above target syntax \<^theory_text>\<open>(in c)\<close>, but individual |
183 |
syntax diagrams omit that aspect for clarity. |
|
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
184 |
|
61421 | 185 |
\<^medskip> |
61664 | 186 |
The exact meaning of results produced within a local theory context depends |
187 |
on the underlying target infrastructure (locale, type class etc.). The |
|
188 |
general idea is as follows, considering a context named \<open>c\<close> with parameter |
|
189 |
\<open>x\<close> and assumption \<open>A[x]\<close>. |
|
27040 | 190 |
|
61664 | 191 |
Definitions are exported by introducing a global version with additional |
192 |
arguments; a syntactic abbreviation links the long form with the abstract |
|
193 |
version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv> |
|
194 |
t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local |
|
195 |
abbreviation \<open>c \<equiv> c.a x\<close> in the target context (for the fixed parameter |
|
196 |
\<open>x\<close>). |
|
27040 | 197 |
|
61664 | 198 |
Theorems are exported by discharging the assumptions and generalizing the |
199 |
parameters of the context. For example, \<open>a: B[x]\<close> becomes \<open>c.a: A[?x] \<Longrightarrow> |
|
200 |
B[?x]\<close>, again for arbitrary \<open>?x\<close>. |
|
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
201 |
\<close> |
27040 | 202 |
|
203 |
||
58618 | 204 |
section \<open>Bundled declarations \label{sec:bundle}\<close> |
47484 | 205 |
|
58618 | 206 |
text \<open> |
47484 | 207 |
\begin{matharray}{rcl} |
61493 | 208 |
@{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
63273 | 209 |
@{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ |
61494 | 210 |
@{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
61493 | 211 |
@{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
212 |
@{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\ |
|
47484 | 213 |
@{keyword_def "includes"} & : & syntax \\ |
214 |
\end{matharray} |
|
215 |
||
216 |
The outer syntax of fact expressions (\secref{sec:syn-att}) involves |
|
61664 | 217 |
theorems and attributes, which are evaluated in the context and applied to |
218 |
it. Attributes may declare theorems to the context, as in \<open>this_rule [intro] |
|
219 |
that_rule [elim]\<close> for example. Configuration options (\secref{sec:config}) |
|
220 |
are special declaration attributes that operate on the context without a |
|
221 |
theorem, as in \<open>[[show_types = false]]\<close> for example. |
|
47484 | 222 |
|
61664 | 223 |
Expressions of this form may be defined as \<^emph>\<open>bundled declarations\<close> in the |
224 |
context, and included in other situations later on. Including declaration |
|
225 |
bundles augments a local context casually without logical dependencies, |
|
226 |
which is in contrast to locales and locale interpretation |
|
227 |
(\secref{sec:locale}). |
|
47484 | 228 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
229 |
@{rail \<open> |
63273 | 230 |
@@{command bundle} @{syntax name} |
231 |
( '=' @{syntax thms} @{syntax for_fixes} | @'begin') |
|
63272 | 232 |
; |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59905
diff
changeset
|
233 |
@@{command print_bundles} ('!'?) |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59905
diff
changeset
|
234 |
; |
62969 | 235 |
(@@{command include} | @@{command including}) (@{syntax name}+) |
47484 | 236 |
; |
62969 | 237 |
@{syntax_def "includes"}: @'includes' (@{syntax name}+) |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
238 |
\<close>} |
47484 | 239 |
|
61665 | 240 |
\<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current |
241 |
context. The RHS is similar to the one of the \<^theory_text>\<open>declare\<close> command. Bundles |
|
242 |
defined in local theory targets are subject to transformations via |
|
243 |
morphisms, when moved into different application contexts; this works |
|
244 |
analogously to any other local theory specification. |
|
47484 | 245 |
|
63273 | 246 |
\<^descr> \<^theory_text>\<open>bundle b begin body end\<close> defines a bundle of declarations from the |
247 |
\<open>body\<close> of local theory specifications. It may consist of commands that are |
|
248 |
technically equivalent to \<^theory_text>\<open>declare\<close> or \<^theory_text>\<open>declaration\<close>, which also includes |
|
249 |
\<^theory_text>\<open>notation\<close>, for example. Named fact declarations like ``\<^theory_text>\<open>lemmas a [simp] = |
|
250 |
b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name |
|
251 |
bindings are not recorded in the bundle. |
|
63272 | 252 |
|
61665 | 253 |
\<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the |
254 |
current context; the ``\<open>!\<close>'' option indicates extra verbosity. |
|
47484 | 255 |
|
63282 | 256 |
\<^descr> \<^theory_text>\<open>unbundle b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles in |
257 |
the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close> |
|
258 |
(\secref{sec:theorems}) with the expanded bundles. |
|
259 |
||
260 |
\<^descr> \<^theory_text>\<open>include\<close> is similar to \<^theory_text>\<open>unbundle\<close>, but works in a proof body (forward |
|
261 |
mode). This is analogous to \<^theory_text>\<open>note\<close> (\secref{sec:proof-facts}) with the |
|
262 |
expanded bundles. |
|
47484 | 263 |
|
61665 | 264 |
\<^descr> \<^theory_text>\<open>including\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof refinement |
265 |
(backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts}) |
|
266 |
with the expanded bundles. |
|
267 |
||
268 |
\<^descr> \<^theory_text>\<open>includes b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>include\<close>, but works in situations |
|
269 |
where a specification context is constructed, notably for \<^theory_text>\<open>context\<close> and |
|
270 |
long statements of \<^theory_text>\<open>theorem\<close> etc. |
|
47484 | 271 |
|
272 |
||
61664 | 273 |
Here is an artificial example of bundling various configuration options: |
61458 | 274 |
\<close> |
47484 | 275 |
|
59905 | 276 |
(*<*)experiment begin(*>*) |
53536
69c943125fd3
do not expose internal flags to attribute name space;
wenzelm
parents:
53370
diff
changeset
|
277 |
bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]] |
47484 | 278 |
|
279 |
lemma "x = x" |
|
280 |
including trace by metis |
|
59905 | 281 |
(*<*)end(*>*) |
47484 | 282 |
|
283 |
||
58618 | 284 |
section \<open>Term definitions \label{sec:term-definitions}\<close> |
27040 | 285 |
|
58618 | 286 |
text \<open> |
27040 | 287 |
\begin{matharray}{rcll} |
61493 | 288 |
@{command_def "definition"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
289 |
@{attribute_def "defn"} & : & \<open>attribute\<close> \\ |
|
61494 | 290 |
@{command_def "print_defn_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
61493 | 291 |
@{command_def "abbreviation"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
61494 | 292 |
@{command_def "print_abbrevs"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
27040 | 293 |
\end{matharray} |
294 |
||
61664 | 295 |
Term definitions may either happen within the logic (as equational axioms of |
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
296 |
a certain form (see also \secref{sec:overloading}), or outside of it as |
57487 | 297 |
rewrite system on abstract syntax. The second form is called |
298 |
``abbreviation''. |
|
27040 | 299 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
300 |
@{rail \<open> |
63180 | 301 |
@@{command definition} decl? definition |
27040 | 302 |
; |
63180 | 303 |
@@{command abbreviation} @{syntax mode}? decl? abbreviation |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59905
diff
changeset
|
304 |
; |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59905
diff
changeset
|
305 |
@@{command print_abbrevs} ('!'?) |
63180 | 306 |
; |
307 |
decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where' |
|
308 |
; |
|
63182 | 309 |
definition: @{syntax thmdecl}? @{syntax prop} |
310 |
@{syntax spec_prems} @{syntax for_fixes} |
|
63180 | 311 |
; |
312 |
abbreviation: @{syntax prop} @{syntax for_fixes} |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
313 |
\<close>} |
27040 | 314 |
|
61665 | 315 |
\<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according |
316 |
to the specification given as \<open>eq\<close>, which is then turned into a proven fact. |
|
317 |
The given proposition may deviate from internal meta-level equality |
|
318 |
according to the rewrite rules declared as @{attribute defn} by the |
|
61664 | 319 |
object-logic. This usually covers object-level equality \<open>x = y\<close> and |
61665 | 320 |
equivalence \<open>A \<longleftrightarrow> B\<close>. End-users normally need not change the @{attribute |
61664 | 321 |
defn} setup. |
27040 | 322 |
|
61664 | 323 |
Definitions may be presented with explicit arguments on the LHS, as well as |
324 |
additional conditions, e.g.\ \<open>f x y = t\<close> instead of \<open>f \<equiv> \<lambda>x y. t\<close> and \<open>y \<noteq> 0 |
|
325 |
\<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>. |
|
51585 | 326 |
|
61665 | 327 |
\<^descr> \<^theory_text>\<open>print_defn_rules\<close> prints the definitional rewrite rules declared via |
328 |
@{attribute defn} in the current context. |
|
51585 | 329 |
|
61665 | 330 |
\<^descr> \<^theory_text>\<open>abbreviation c where eq\<close> introduces a syntactic constant which is |
331 |
associated with a certain term according to the meta-level equality \<open>eq\<close>. |
|
27040 | 332 |
|
61664 | 333 |
Abbreviations participate in the usual type-inference process, but are |
334 |
expanded before the logic ever sees them. Pretty printing of terms involves |
|
335 |
higher-order rewriting with rules stemming from reverted abbreviations. This |
|
336 |
needs some care to avoid overlapping or looping syntactic replacements! |
|
27040 | 337 |
|
61664 | 338 |
The optional \<open>mode\<close> specification restricts output to a particular print |
339 |
mode; using ``\<open>input\<close>'' here achieves the effect of one-way abbreviations. |
|
61665 | 340 |
The mode may also include an ``\<^theory_text>\<open>output\<close>'' qualifier that affects the |
341 |
concrete syntax declared for abbreviations, cf.\ \<^theory_text>\<open>syntax\<close> in |
|
27040 | 342 |
\secref{sec:syn-trans}. |
343 |
||
61665 | 344 |
\<^descr> \<^theory_text>\<open>print_abbrevs\<close> prints all constant abbreviations of the current context; |
345 |
the ``\<open>!\<close>'' option indicates extra verbosity. |
|
58618 | 346 |
\<close> |
27040 | 347 |
|
348 |
||
58618 | 349 |
section \<open>Axiomatizations \label{sec:axiomatizations}\<close> |
57487 | 350 |
|
58618 | 351 |
text \<open> |
57487 | 352 |
\begin{matharray}{rcll} |
61493 | 353 |
@{command_def "axiomatization"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\ |
57487 | 354 |
\end{matharray} |
355 |
||
356 |
@{rail \<open> |
|
63285 | 357 |
@@{command axiomatization} @{syntax vars}? (@'where' axiomatization)? |
57487 | 358 |
; |
63178 | 359 |
axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and') |
63182 | 360 |
@{syntax spec_prems} @{syntax for_fixes} |
57487 | 361 |
\<close>} |
362 |
||
61665 | 363 |
\<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants |
364 |
simultaneously and states axiomatic properties for these. The constants are |
|
365 |
marked as being specified once and for all, which prevents additional |
|
366 |
specifications for the same constants later on, but it is always possible do |
|
367 |
emit axiomatizations without referring to particular constants. Note that |
|
368 |
lack of precise dependency tracking of axiomatizations may disrupt the |
|
369 |
well-formedness of an otherwise definitional theory. |
|
57487 | 370 |
|
371 |
Axiomatization is restricted to a global theory context: support for local |
|
372 |
theory targets \secref{sec:target} would introduce an extra dimension of |
|
373 |
uncertainty what the written specifications really are, and make it |
|
374 |
infeasible to argue why they are correct. |
|
375 |
||
376 |
Axiomatic specifications are required when declaring a new logical system |
|
377 |
within Isabelle/Pure, but in an application environment like Isabelle/HOL |
|
61664 | 378 |
the user normally stays within definitional mechanisms provided by the logic |
379 |
and its libraries. |
|
58618 | 380 |
\<close> |
57487 | 381 |
|
382 |
||
58618 | 383 |
section \<open>Generic declarations\<close> |
27040 | 384 |
|
58618 | 385 |
text \<open> |
47483 | 386 |
\begin{matharray}{rcl} |
61493 | 387 |
@{command_def "declaration"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
388 |
@{command_def "syntax_declaration"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
389 |
@{command_def "declare"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
47483 | 390 |
\end{matharray} |
391 |
||
61664 | 392 |
Arbitrary operations on the background context may be wrapped-up as generic |
393 |
declaration elements. Since the underlying concept of local theories may be |
|
394 |
subject to later re-interpretation, there is an additional dependency on a |
|
395 |
morphism that tells the difference of the original declaration context wrt.\ |
|
396 |
the application context encountered later on. A fact declaration is an |
|
397 |
important special case: it consists of a theorem which is applied to the |
|
398 |
context by means of an attribute. |
|
27040 | 399 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
400 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
401 |
(@@{command declaration} | @@{command syntax_declaration}) |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
402 |
('(' @'pervasive' ')')? \<newline> @{syntax text} |
27040 | 403 |
; |
62969 | 404 |
@@{command declare} (@{syntax thms} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
405 |
\<close>} |
27040 | 406 |
|
61665 | 407 |
\<^descr> \<^theory_text>\<open>declaration d\<close> adds the declaration function \<open>d\<close> of ML type @{ML_type |
408 |
declaration}, to the current local theory under construction. In later |
|
409 |
application contexts, the function is transformed according to the morphisms |
|
410 |
being involved in the interpretation hierarchy. |
|
27040 | 411 |
|
61665 | 412 |
If the \<^theory_text>\<open>(pervasive)\<close> option is given, the corresponding declaration is |
61664 | 413 |
applied to all possible contexts involved, including the global background |
414 |
theory. |
|
33516 | 415 |
|
61665 | 416 |
\<^descr> \<^theory_text>\<open>syntax_declaration\<close> is similar to \<^theory_text>\<open>declaration\<close>, but is meant to affect |
417 |
only ``syntactic'' tools by convention (such as notation and type-checking |
|
418 |
information). |
|
40784 | 419 |
|
61665 | 420 |
\<^descr> \<^theory_text>\<open>declare thms\<close> declares theorems to the current local theory context. No |
421 |
theorem binding is involved here, unlike \<^theory_text>\<open>lemmas\<close> (cf.\ |
|
422 |
\secref{sec:theorems}), so \<^theory_text>\<open>declare\<close> only has the effect of applying |
|
423 |
attributes as included in the theorem specification. |
|
58618 | 424 |
\<close> |
27040 | 425 |
|
426 |
||
58618 | 427 |
section \<open>Locales \label{sec:locale}\<close> |
27040 | 428 |
|
58618 | 429 |
text \<open> |
54049 | 430 |
A locale is a functor that maps parameters (including implicit type |
61664 | 431 |
parameters) and a specification to a list of declarations. The syntax of |
432 |
locales is modeled after the Isar proof context commands (cf.\ |
|
433 |
\secref{sec:proof-context}). |
|
54049 | 434 |
|
61664 | 435 |
Locale hierarchies are supported by maintaining a graph of dependencies |
436 |
between locale instances in the global theory. Dependencies may be |
|
437 |
introduced through import (where a locale is defined as sublocale of the |
|
438 |
imported instances) or by proving that an existing locale is a sublocale of |
|
439 |
one or several locale instances. |
|
54049 | 440 |
|
441 |
A locale may be opened with the purpose of appending to its list of |
|
61664 | 442 |
declarations (cf.\ \secref{sec:target}). When opening a locale declarations |
443 |
from all dependencies are collected and are presented as a local theory. In |
|
444 |
this process, which is called \<^emph>\<open>roundup\<close>, redundant locale instances are |
|
445 |
omitted. A locale instance is redundant if it is subsumed by an instance |
|
446 |
encountered earlier. A more detailed description of this process is |
|
447 |
available elsewhere @{cite Ballarin2014}. |
|
58618 | 448 |
\<close> |
27040 | 449 |
|
450 |
||
58618 | 451 |
subsection \<open>Locale expressions \label{sec:locale-expr}\<close> |
33846 | 452 |
|
58618 | 453 |
text \<open> |
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
454 |
A \<^emph>\<open>locale expression\<close> denotes a context composed of instances of existing |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
455 |
locales. The context consists of the declaration elements from the locale |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
456 |
instances. Redundant locale instances are omitted according to roundup. |
33846 | 457 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
458 |
@{rail \<open> |
59785 | 459 |
@{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes} |
33846 | 460 |
; |
62969 | 461 |
instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) |
33846 | 462 |
; |
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
463 |
qualifier: @{syntax name} ('?')? |
33846 | 464 |
; |
42617 | 465 |
pos_insts: ('_' | @{syntax term})* |
33846 | 466 |
; |
42617 | 467 |
named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
468 |
\<close>} |
33846 | 469 |
|
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
470 |
A locale instance consists of a reference to a locale and either positional |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
471 |
or named parameter instantiations. Identical instantiations (that is, those |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
472 |
that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>'' |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
473 |
enables to omit the instantiation for a parameter inside a positional |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
474 |
instantiation. |
33846 | 475 |
|
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
476 |
Terms in instantiations are from the context the locale expressions is |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
477 |
declared in. Local names may be added to this context with the optional |
61665 | 478 |
\<^theory_text>\<open>for\<close> clause. This is useful for shadowing names bound in outer contexts, |
479 |
and for declaring syntax. In addition, syntax declarations from one instance |
|
480 |
are effective when parsing subsequent instances of the same expression. |
|
33846 | 481 |
|
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
482 |
Instances have an optional qualifier which applies to names in declarations. |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
483 |
Names include local definitions and theorem names. If present, the qualifier |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
484 |
itself is either mandatory (default) or non-mandatory (when followed by |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
485 |
``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input. |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
486 |
Qualifiers only affect name spaces; they play no role in determining whether |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61566
diff
changeset
|
487 |
one locale instance subsumes another. |
58618 | 488 |
\<close> |
33846 | 489 |
|
490 |
||
58618 | 491 |
subsection \<open>Locale declarations\<close> |
27040 | 492 |
|
58618 | 493 |
text \<open> |
27040 | 494 |
\begin{matharray}{rcl} |
61493 | 495 |
@{command_def "locale"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ |
496 |
@{command_def "experiment"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ |
|
497 |
@{command_def "print_locale"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
498 |
@{command_def "print_locales"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
499 |
@{command_def "locale_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
500 |
@{method_def intro_locales} & : & \<open>method\<close> \\ |
|
501 |
@{method_def unfold_locales} & : & \<open>method\<close> \\ |
|
27040 | 502 |
\end{matharray} |
503 |
||
504 |
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes} |
|
28787 | 505 |
\indexisarelem{defines}\indexisarelem{notes} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
506 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
507 |
@@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'? |
27040 | 508 |
; |
59901 | 509 |
@@{command experiment} (@{syntax context_elem}*) @'begin' |
510 |
; |
|
62969 | 511 |
@@{command print_locale} '!'? @{syntax name} |
27040 | 512 |
; |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59905
diff
changeset
|
513 |
@@{command print_locales} ('!'?) |
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59905
diff
changeset
|
514 |
; |
42617 | 515 |
@{syntax_def locale}: @{syntax context_elem}+ | |
516 |
@{syntax locale_expr} ('+' (@{syntax context_elem}+))? |
|
27040 | 517 |
; |
42617 | 518 |
@{syntax_def context_elem}: |
63285 | 519 |
@'fixes' @{syntax vars} | |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
520 |
@'constrains' (@{syntax name} '::' @{syntax type} + @'and') | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
521 |
@'assumes' (@{syntax props} + @'and') | |
42705 | 522 |
@'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') | |
62969 | 523 |
@'notes' (@{syntax thmdef}? @{syntax thms} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
524 |
\<close>} |
27040 | 525 |
|
61665 | 526 |
\<^descr> \<^theory_text>\<open>locale loc = import + body\<close> defines a new locale \<open>loc\<close> as a context |
527 |
consisting of a certain view of existing locales (\<open>import\<close>) plus some |
|
528 |
additional elements (\<open>body\<close>). Both \<open>import\<close> and \<open>body\<close> are optional; the |
|
529 |
degenerate form \<^theory_text>\<open>locale loc\<close> defines an empty locale, which may still be |
|
530 |
useful to collect declarations of facts later on. Type-inference on locale |
|
531 |
expressions automatically takes care of the most general typing that the |
|
532 |
combined context elements may acquire. |
|
27040 | 533 |
|
61664 | 534 |
The \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context} |
61665 | 535 |
above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<close>. These are |
536 |
parameters of the defined locale. Locale parameters whose instantiation is |
|
537 |
omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> clause: they are |
|
538 |
inserted at its beginning. This means that these parameters may be referred |
|
539 |
to from within the expression and also in the subsequent context elements |
|
540 |
and provides a notational convenience for the inheritance of parameters in |
|
541 |
locale declarations. |
|
27040 | 542 |
|
61493 | 543 |
The \<open>body\<close> consists of context elements. |
27040 | 544 |
|
61664 | 545 |
\<^descr> @{element "fixes"}~\<open>x :: \<tau> (mx)\<close> declares a local parameter of type \<open>\<tau>\<close> |
546 |
and mixfix annotation \<open>mx\<close> (both are optional). The special syntax |
|
547 |
declaration ``\<open>(\<close>@{keyword_ref "structure"}\<open>)\<close>'' means that \<open>x\<close> may be |
|
548 |
referenced implicitly in this context. |
|
27040 | 549 |
|
61664 | 550 |
\<^descr> @{element "constrains"}~\<open>x :: \<tau>\<close> introduces a type constraint \<open>\<tau>\<close> on the |
551 |
local parameter \<open>x\<close>. This element is deprecated. The type constraint |
|
61665 | 552 |
should be introduced in the \<^theory_text>\<open>for\<close> clause or the relevant @{element |
553 |
"fixes"} element. |
|
27040 | 554 |
|
61664 | 555 |
\<^descr> @{element "assumes"}~\<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces local premises, similar |
61665 | 556 |
to \<^theory_text>\<open>assume\<close> within a proof (cf.\ \secref{sec:proof-context}). |
27040 | 557 |
|
61664 | 558 |
\<^descr> @{element "defines"}~\<open>a: x \<equiv> t\<close> defines a previously declared parameter. |
63039 | 559 |
This is similar to \<^theory_text>\<open>define\<close> within a proof (cf.\ |
560 |
\secref{sec:proof-context}), but @{element "defines"} is restricted to |
|
561 |
Pure equalities and the defined variable needs to be declared beforehand |
|
562 |
via @{element "fixes"}. The left-hand side of the equation may have |
|
563 |
additional arguments, e.g.\ ``@{element "defines"}~\<open>f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t\<close>'', |
|
564 |
which need to be free in the context. |
|
27040 | 565 |
|
61664 | 566 |
\<^descr> @{element "notes"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> reconsiders facts within a local |
567 |
context. Most notably, this may include arbitrary declarations in any |
|
568 |
attribute specifications included here, e.g.\ a local @{attribute simp} |
|
569 |
rule. |
|
27040 | 570 |
|
61664 | 571 |
Both @{element "assumes"} and @{element "defines"} elements contribute to |
572 |
the locale specification. When defining an operation derived from the |
|
61665 | 573 |
parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is usually more |
574 |
appropriate. |
|
27040 | 575 |
|
61665 | 576 |
Note that ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syntax of @{element |
61664 | 577 |
"assumes"} and @{element "defines"} above are illegal in locale definitions. |
578 |
In the long goal format of \secref{sec:goals}, term bindings may be included |
|
579 |
as expected, though. |
|
27040 | 580 |
|
61421 | 581 |
\<^medskip> |
61664 | 582 |
Locale specifications are ``closed up'' by turning the given text into a |
583 |
predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as |
|
584 |
local lemmas (modulo local definitions). The predicate statement covers only |
|
585 |
the newly specified assumptions, omitting the content of included locale |
|
586 |
expressions. The full cumulative view is only provided on export, involving |
|
587 |
another predicate \<open>loc\<close> that refers to the complete specification text. |
|
27040 | 588 |
|
61664 | 589 |
In any case, the predicate arguments are those locale parameters that |
590 |
actually occur in the respective piece of text. Also these predicates |
|
591 |
operate at the meta-level in theory, but the locale packages attempts to |
|
592 |
internalize statements according to the object-logic setup (e.g.\ replacing |
|
593 |
\<open>\<And>\<close> by \<open>\<forall>\<close>, and \<open>\<Longrightarrow>\<close> by \<open>\<longrightarrow>\<close> in HOL; see also \secref{sec:object-logic}). |
|
594 |
Separate introduction rules \<open>loc_axioms.intro\<close> and \<open>loc.intro\<close> are provided |
|
595 |
as well. |
|
59901 | 596 |
|
61665 | 597 |
\<^descr> \<^theory_text>\<open>experiment exprs begin\<close> opens an anonymous locale context with private |
598 |
naming policy. Specifications in its body are inaccessible from outside. |
|
599 |
This is useful to perform experiments, without polluting the name space. |
|
59901 | 600 |
|
61665 | 601 |
\<^descr> \<^theory_text>\<open>print_locale locale\<close> prints the contents of the named locale. The |
602 |
command omits @{element "notes"} elements by default. Use \<^theory_text>\<open>print_locale!\<close> |
|
603 |
to have them included. |
|
27040 | 604 |
|
61665 | 605 |
\<^descr> \<^theory_text>\<open>print_locales\<close> prints the names of all locales of the current theory; |
606 |
the ``\<open>!\<close>'' option indicates extra verbosity. |
|
27040 | 607 |
|
61665 | 608 |
\<^descr> \<^theory_text>\<open>locale_deps\<close> visualizes all locales and their relations as a Hasse |
609 |
diagram. This includes locales defined as type classes (\secref{sec:class}). |
|
610 |
See also \<^theory_text>\<open>print_dependencies\<close> below. |
|
50716 | 611 |
|
61664 | 612 |
\<^descr> @{method intro_locales} and @{method unfold_locales} repeatedly expand all |
613 |
introduction rules of locale predicates of the theory. While @{method |
|
614 |
intro_locales} only applies the \<open>loc.intro\<close> introduction rules and therefore |
|
615 |
does not descend to assumptions, @{method unfold_locales} is more aggressive |
|
616 |
and applies \<open>loc_axioms.intro\<close> as well. Both methods are aware of locale |
|
617 |
specifications entailed by the context, both from target statements, and |
|
618 |
from interpretations (see below). New goals that are entailed by the current |
|
619 |
context are discharged automatically. |
|
58618 | 620 |
\<close> |
27040 | 621 |
|
622 |
||
58618 | 623 |
subsection \<open>Locale interpretation\<close> |
27040 | 624 |
|
58618 | 625 |
text \<open> |
27040 | 626 |
\begin{matharray}{rcl} |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
627 |
@{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\ |
61493 | 628 |
@{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\ |
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
629 |
@{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\ |
61493 | 630 |
@{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\ |
631 |
@{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
632 |
@{command_def "print_interps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
27040 | 633 |
\end{matharray} |
634 |
||
61664 | 635 |
Locales may be instantiated, and the resulting instantiated declarations |
636 |
added to the current context. This requires proof (of the instantiated |
|
61706 | 637 |
specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is |
638 |
possible within arbitrary local theories (\<^theory_text>\<open>interpretation\<close>), within proof |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
639 |
bodies (\<^theory_text>\<open>interpret\<close>), into global theories (\<^theory_text>\<open>global_interpretation\<close>) and |
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
640 |
into locales (\<^theory_text>\<open>sublocale\<close>). |
47483 | 641 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
642 |
@{rail \<open> |
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
643 |
@@{command interpretation} @{syntax locale_expr} equations? |
27040 | 644 |
; |
42617 | 645 |
@@{command interpret} @{syntax locale_expr} equations? |
27040 | 646 |
; |
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
647 |
@@{command global_interpretation} @{syntax locale_expr} \<newline> |
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
648 |
definitions? equations? |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
649 |
; |
62969 | 650 |
@@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline> |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
651 |
definitions? equations? |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
652 |
; |
42617 | 653 |
@@{command print_dependencies} '!'? @{syntax locale_expr} |
27040 | 654 |
; |
62969 | 655 |
@@{command print_interps} @{syntax name} |
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
656 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
657 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
658 |
definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline> |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
659 |
@{syntax mixfix}? @'=' @{syntax term} + @'and'); |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
660 |
|
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
661 |
equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
662 |
\<close>} |
27040 | 663 |
|
61706 | 664 |
The core of each interpretation command is a locale expression \<open>expr\<close>; the |
665 |
command generates proof obligations for the instantiated specifications. |
|
666 |
Once these are discharged by the user, instantiated declarations (in |
|
667 |
particular, facts) are added to the context in a post-processing phase, in a |
|
668 |
manner specific to each command. |
|
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
669 |
|
61706 | 670 |
Interpretation commands are aware of interpretations that are already |
671 |
active: post-processing is achieved through a variant of roundup that takes |
|
61664 | 672 |
interpretations of the current global or local theory into account. In order |
673 |
to simplify the proof obligations according to existing interpretations use |
|
674 |
methods @{method intro_locales} or @{method unfold_locales}. |
|
53368
92b9965f479d
Clarifies documentation of interpretation in local theories.
ballarin
parents:
53015
diff
changeset
|
675 |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
676 |
Given equations \<open>eqns\<close> amend the morphism through which \<open>expr\<close> is |
61706 | 677 |
interpreted, adding rewrite rules. This is particularly useful for |
678 |
interpreting concepts introduced through definitions. The equations must be |
|
679 |
proved the user. |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
680 |
|
61706 | 681 |
Given definitions \<open>defs\<close> produce corresponding definitions in the local |
682 |
theory's underlying target \<^emph>\<open>and\<close> amend the morphism with the equations |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
683 |
stemming from the symmetric of those definitions. Hence these need not be |
61706 | 684 |
proved explicitly the user. Such rewrite definitions are a even more useful |
685 |
device for interpreting concepts introduced through definitions, but they |
|
686 |
are only supported for interpretation commands operating in a local theory |
|
61823 | 687 |
whose implementing target actually supports this. Note that despite |
688 |
the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close> |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
689 |
are processed sequentially without mutual recursion. |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
690 |
|
61706 | 691 |
\<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory |
692 |
such that its lifetime is limited to the current context block (e.g. a |
|
693 |
locale or unnamed context). At the closing @{command end} of the block the |
|
694 |
interpretation and its declarations disappear. Hence facts based on |
|
695 |
interpretation can be established without creating permanent links to the |
|
696 |
interpreted locale instances, as would be the case with @{command |
|
697 |
sublocale}. |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
698 |
|
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
699 |
When used on the level of a global theory, there is no end of a current |
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
700 |
context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to |
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
701 |
\<^theory_text>\<open>global_interpretation\<close> then. |
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
702 |
|
61706 | 703 |
\<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets \<open>expr\<close> into a proof context: |
704 |
the interpretation and its declarations disappear when closing the current |
|
705 |
proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly |
|
706 |
universally quantified. |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
707 |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
708 |
\<^descr> \<^theory_text>\<open>global_interpretation defines defs rewrites eqns\<close> interprets \<open>expr\<close> |
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
709 |
into a global theory. |
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
710 |
|
53369
b4bcac7d065b
Clarifies that interpretation does not only apply to facts, but to declaratoins in general.
ballarin
parents:
53368
diff
changeset
|
711 |
When adding declarations to locales, interpreted versions of these |
61664 | 712 |
declarations are added to the global theory for all interpretations in the |
61891
76189756ff65
documentation on last state of the art concerning interpretation
haftmann
parents:
61853
diff
changeset
|
713 |
global theory as well. That is, interpretations into global theories |
61664 | 714 |
dynamically participate in any declarations added to locales. |
54049 | 715 |
|
61664 | 716 |
Free variables in the interpreted expression are allowed. They are turned |
717 |
into schematic variables in the generated declarations. In order to use a |
|
718 |
free variable whose name is already bound in the context --- for example, |
|
61665 | 719 |
because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause. |
48824
45d0e40b07af
Clarification: free variables allowed in interpreted locale instances.
ballarin
parents:
47484
diff
changeset
|
720 |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
721 |
\<^descr> \<^theory_text>\<open>sublocale name \<subseteq> defines defs expr rewrites eqns\<close> interprets \<open>expr\<close> |
61706 | 722 |
into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the |
723 |
specification of \<open>expr\<close> is required. As in the localized version of the |
|
724 |
theorem command, the proof is in the context of \<open>name\<close>. After the proof |
|
725 |
obligation has been discharged, the locale hierarchy is changed as if \<open>name\<close> |
|
726 |
imported \<open>expr\<close> (hence the name \<^theory_text>\<open>sublocale\<close>). When the context of \<open>name\<close> is |
|
727 |
subsequently entered, traversing the locale hierarchy will involve the |
|
728 |
locale instances of \<open>expr\<close>, and their declarations will be added to the |
|
729 |
context. This makes \<^theory_text>\<open>sublocale\<close> dynamic: extensions of a locale that is |
|
730 |
instantiated in \<open>expr\<close> may take place after the \<^theory_text>\<open>sublocale\<close> declaration and |
|
731 |
still become available in the context. Circular \<^theory_text>\<open>sublocale\<close> declarations |
|
732 |
are allowed as long as they do not lead to infinite chains. |
|
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
733 |
|
61664 | 734 |
If interpretations of \<open>name\<close> exist in the current global theory, the command |
735 |
adds interpretations for \<open>expr\<close> as well, with the same qualifier, although |
|
736 |
only for fragments of \<open>expr\<close> that are not interpreted in the theory already. |
|
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41249
diff
changeset
|
737 |
|
61706 | 738 |
Using equations \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break infinite |
739 |
chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations. |
|
27040 | 740 |
|
61665 | 741 |
In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the |
742 |
locale argument must be omitted. The command then refers to the locale (or |
|
743 |
class) target of the context block. |
|
51747 | 744 |
|
61665 | 745 |
\<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an |
746 |
interpretation of \<open>expr\<close> in the current context. It lists all locale |
|
747 |
instances for which interpretations would be added to the current context. |
|
748 |
Variant \<^theory_text>\<open>print_dependencies!\<close> does not generalize parameters and assumes an |
|
749 |
empty context --- that is, it prints all locale instances that would be |
|
750 |
considered for interpretation. The latter is useful for understanding the |
|
751 |
dependencies of a locale expression. |
|
41435 | 752 |
|
61665 | 753 |
\<^descr> \<^theory_text>\<open>print_interps locale\<close> lists all interpretations of \<open>locale\<close> in the |
754 |
current theory or proof context, including those due to a combination of an |
|
755 |
\<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close> |
|
756 |
declarations. |
|
33867 | 757 |
|
27040 | 758 |
\begin{warn} |
61664 | 759 |
If a global theory inherits declarations (body elements) for a locale from |
760 |
one parent and an interpretation of that locale from another parent, the |
|
761 |
interpretation will not be applied to the declarations. |
|
54049 | 762 |
\end{warn} |
763 |
||
764 |
\begin{warn} |
|
61664 | 765 |
Since attributes are applied to interpreted theorems, interpretation may |
766 |
modify the context of common proof tools, e.g.\ the Simplifier or |
|
61665 | 767 |
Classical Reasoner. As the behaviour of such tools is \<^emph>\<open>not\<close> stable under |
61664 | 768 |
interpretation morphisms, manual declarations might have to be added to |
769 |
the target context of the interpretation to revert such declarations. |
|
27040 | 770 |
\end{warn} |
771 |
||
772 |
\begin{warn} |
|
51747 | 773 |
An interpretation in a local theory or proof context may subsume previous |
61664 | 774 |
interpretations. This happens if the same specification fragment is |
775 |
interpreted twice and the instantiation of the second interpretation is |
|
776 |
more general than the interpretation of the first. The locale package does |
|
777 |
not attempt to remove subsumed interpretations. |
|
27040 | 778 |
\end{warn} |
779 |
||
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
780 |
\begin{warn} |
61823 | 781 |
Due to a technical limitation, the specific context of a interpretation |
782 |
given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and |
|
783 |
\<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using |
|
784 |
explicit sort constraints and quantified term variables. |
|
785 |
\end{warn} |
|
786 |
||
787 |
\begin{warn} |
|
61673
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
788 |
While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
789 |
its result is discarded immediately. |
fd4ac1530d63
represent both algebraic and local-theory views on locale interpretation in interfaces
haftmann
parents:
61671
diff
changeset
|
790 |
\end{warn} |
59003
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
791 |
\<close> |
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
792 |
|
16d92d37a8a1
documentation stubs about permanent_interpretation
haftmann
parents:
58724
diff
changeset
|
793 |
|
58618 | 794 |
section \<open>Classes \label{sec:class}\<close> |
27040 | 795 |
|
58618 | 796 |
text \<open> |
27040 | 797 |
\begin{matharray}{rcl} |
61493 | 798 |
@{command_def "class"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ |
799 |
@{command_def "instantiation"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ |
|
800 |
@{command_def "instance"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
801 |
@{command "instance"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\ |
|
802 |
@{command_def "subclass"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
803 |
@{command_def "print_classes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
804 |
@{command_def "class_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
805 |
@{method_def intro_classes} & : & \<open>method\<close> \\ |
|
27040 | 806 |
\end{matharray} |
807 |
||
61664 | 808 |
A class is a particular locale with \<^emph>\<open>exactly one\<close> type variable \<open>\<alpha>\<close>. Beyond |
809 |
the underlying locale, a corresponding type class is established which is |
|
810 |
interpreted logically as axiomatic type class @{cite "Wenzel:1997:TPHOL"} |
|
811 |
whose logical content are the assumptions of the locale. Thus, classes |
|
812 |
provide the full generality of locales combined with the commodity of type |
|
813 |
classes (notably type-inference). See @{cite "isabelle-classes"} for a short |
|
47483 | 814 |
tutorial. |
815 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
816 |
@{rail \<open> |
42704 | 817 |
@@{command class} class_spec @'begin'? |
818 |
; |
|
819 |
class_spec: @{syntax name} '=' |
|
62969 | 820 |
((@{syntax name} '+' (@{syntax context_elem}+)) | |
821 |
@{syntax name} | (@{syntax context_elem}+)) |
|
27040 | 822 |
; |
62969 | 823 |
@@{command instantiation} (@{syntax name} + @'and') '::' @{syntax arity} @'begin' |
27040 | 824 |
; |
62969 | 825 |
@@{command instance} (() | (@{syntax name} + @'and') '::' @{syntax arity} | |
826 |
@{syntax name} ('<' | '\<subseteq>') @{syntax name} ) |
|
31681 | 827 |
; |
62969 | 828 |
@@{command subclass} @{syntax name} |
58202 | 829 |
; |
60091 | 830 |
@@{command class_deps} (class_bounds class_bounds?)? |
60090 | 831 |
; |
60091 | 832 |
class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')' |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
833 |
\<close>} |
27040 | 834 |
|
61665 | 835 |
\<^descr> \<^theory_text>\<open>class c = superclasses + body\<close> defines a new class \<open>c\<close>, inheriting from |
836 |
\<open>superclasses\<close>. This introduces a locale \<open>c\<close> with import of all locales |
|
837 |
\<open>superclasses\<close>. |
|
27040 | 838 |
|
61664 | 839 |
Any @{element "fixes"} in \<open>body\<close> are lifted to the global theory level |
840 |
(\<^emph>\<open>class operations\<close> \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close> of class \<open>c\<close>), mapping the local type |
|
841 |
parameter \<open>\<alpha>\<close> to a schematic type variable \<open>?\<alpha> :: c\<close>. |
|
27040 | 842 |
|
61664 | 843 |
Likewise, @{element "assumes"} in \<open>body\<close> are also lifted, mapping each local |
844 |
parameter \<open>f :: \<tau>[\<alpha>]\<close> to its corresponding global constant \<open>f :: \<tau>[?\<alpha> :: |
|
845 |
c]\<close>. The corresponding introduction rule is provided as |
|
846 |
\<open>c_class_axioms.intro\<close>. This rule should be rarely needed directly --- the |
|
847 |
@{method intro_classes} method takes care of the details of class membership |
|
848 |
proofs. |
|
27040 | 849 |
|
61665 | 850 |
\<^descr> \<^theory_text>\<open>instantiation t :: (s\<^sub>1, \<dots>, s\<^sub>n)s begin\<close> opens a target (cf.\ |
851 |
\secref{sec:target}) which allows to specify class operations \<open>f\<^sub>1, \<dots>, f\<^sub>n\<close> |
|
852 |
corresponding to sort \<open>s\<close> at the particular type instance \<open>(\<alpha>\<^sub>1 :: s\<^sub>1, \<dots>, |
|
853 |
\<alpha>\<^sub>n :: s\<^sub>n) t\<close>. A plain \<^theory_text>\<open>instance\<close> command in the target body poses a goal |
|
854 |
stating these type arities. The target is concluded by an @{command_ref |
|
855 |
(local) "end"} command. |
|
27040 | 856 |
|
61664 | 857 |
Note that a list of simultaneous type constructors may be given; this |
858 |
corresponds nicely to mutually recursive type definitions, e.g.\ in |
|
859 |
Isabelle/HOL. |
|
27040 | 860 |
|
61665 | 861 |
\<^descr> \<^theory_text>\<open>instance\<close> in an instantiation target body sets up a goal stating the |
862 |
type arities claimed at the opening \<^theory_text>\<open>instantiation\<close>. The proof would |
|
863 |
usually proceed by @{method intro_classes}, and then establish the |
|
864 |
characteristic theorems of the type classes involved. After finishing the |
|
865 |
proof, the background theory will be augmented by the proven type arities. |
|
31681 | 866 |
|
61665 | 867 |
On the theory level, \<^theory_text>\<open>instance t :: (s\<^sub>1, \<dots>, s\<^sub>n)s\<close> provides a convenient |
868 |
way to instantiate a type class with no need to specify operations: one can |
|
869 |
continue with the instantiation proof immediately. |
|
27040 | 870 |
|
61665 | 871 |
\<^descr> \<^theory_text>\<open>subclass c\<close> in a class context for class \<open>d\<close> sets up a goal stating that |
872 |
class \<open>c\<close> is logically contained in class \<open>d\<close>. After finishing the proof, |
|
873 |
class \<open>d\<close> is proven to be subclass \<open>c\<close> and the locale \<open>c\<close> is interpreted |
|
874 |
into \<open>d\<close> simultaneously. |
|
31681 | 875 |
|
61664 | 876 |
A weakened form of this is available through a further variant of @{command |
61665 | 877 |
instance}: \<^theory_text>\<open>instance c\<^sub>1 \<subseteq> c\<^sub>2\<close> opens a proof that class \<open>c\<^sub>2\<close> implies |
878 |
\<open>c\<^sub>1\<close> without reference to the underlying locales; this is useful if the |
|
879 |
properties to prove the logical connection are not sufficient on the locale |
|
880 |
level but on the theory level. |
|
61664 | 881 |
|
61665 | 882 |
\<^descr> \<^theory_text>\<open>print_classes\<close> prints all classes in the current theory. |
27040 | 883 |
|
61665 | 884 |
\<^descr> \<^theory_text>\<open>class_deps\<close> visualizes classes and their subclass relations as a |
885 |
directed acyclic graph. By default, all classes from the current theory |
|
61664 | 886 |
context are show. This may be restricted by optional bounds as follows: |
61665 | 887 |
\<^theory_text>\<open>class_deps upper\<close> or \<^theory_text>\<open>class_deps upper lower\<close>. A class is visualized, iff |
888 |
it is a subclass of some sort from \<open>upper\<close> and a superclass of some sort |
|
889 |
from \<open>lower\<close>. |
|
29706 | 890 |
|
61664 | 891 |
\<^descr> @{method intro_classes} repeatedly expands all class introduction rules of |
892 |
this theory. Note that this method usually needs not be named explicitly, as |
|
61665 | 893 |
it is already included in the default proof step (e.g.\ of \<^theory_text>\<open>proof\<close>). In |
894 |
particular, instantiation of trivial (syntactic) classes may be performed by |
|
895 |
a single ``\<^theory_text>\<open>..\<close>'' proof step. |
|
58618 | 896 |
\<close> |
26870 | 897 |
|
27040 | 898 |
|
58618 | 899 |
subsection \<open>The class target\<close> |
27040 | 900 |
|
58618 | 901 |
text \<open> |
27040 | 902 |
%FIXME check |
903 |
||
61664 | 904 |
A named context may refer to a locale (cf.\ \secref{sec:target}). If this |
905 |
locale is also a class \<open>c\<close>, apart from the common locale target behaviour |
|
906 |
the following happens. |
|
27040 | 907 |
|
61664 | 908 |
\<^item> Local constant declarations \<open>g[\<alpha>]\<close> referring to the local type parameter |
909 |
\<open>\<alpha>\<close> and local parameters \<open>f[\<alpha>]\<close> are accompanied by theory-level constants |
|
910 |
\<open>g[?\<alpha> :: c]\<close> referring to theory-level class operations \<open>f[?\<alpha> :: c]\<close>. |
|
27040 | 911 |
|
61664 | 912 |
\<^item> Local theorem bindings are lifted as are assumptions. |
27040 | 913 |
|
61664 | 914 |
\<^item> Local syntax refers to local operations \<open>g[\<alpha>]\<close> and global operations |
915 |
\<open>g[?\<alpha> :: c]\<close> uniformly. Type inference resolves ambiguities. In rare |
|
916 |
cases, manual type annotations are needed. |
|
58618 | 917 |
\<close> |
27040 | 918 |
|
919 |
||
58618 | 920 |
subsection \<open>Co-regularity of type classes and arities\<close> |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
921 |
|
61664 | 922 |
text \<open> |
923 |
The class relation together with the collection of type-constructor arities |
|
924 |
must obey the principle of \<^emph>\<open>co-regularity\<close> as defined below. |
|
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
925 |
|
61421 | 926 |
\<^medskip> |
61664 | 927 |
For the subsequent formulation of co-regularity we assume that the class |
928 |
relation is closed by transitivity and reflexivity. Moreover the collection |
|
929 |
of arities \<open>t :: (\<^vec>s)c\<close> is completed such that \<open>t :: (\<^vec>s)c\<close> and |
|
930 |
\<open>c \<subseteq> c'\<close> implies \<open>t :: (\<^vec>s)c'\<close> for all such declarations. |
|
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
931 |
|
61664 | 932 |
Treating sorts as finite sets of classes (meaning the intersection), the |
933 |
class relation \<open>c\<^sub>1 \<subseteq> c\<^sub>2\<close> is extended to sorts as follows: |
|
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
934 |
\[ |
61493 | 935 |
\<open>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\<close> |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
936 |
\] |
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
937 |
|
61664 | 938 |
This relation on sorts is further extended to tuples of sorts (of the same |
939 |
length) in the component-wise way. |
|
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
940 |
|
61421 | 941 |
\<^medskip> |
61664 | 942 |
Co-regularity of the class relation together with the arities relation |
943 |
means: |
|
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
944 |
\[ |
61493 | 945 |
\<open>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\<close> |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
946 |
\] |
61664 | 947 |
for all such arities. In other words, whenever the result classes of some |
948 |
type-constructor arities are related, then the argument sorts need to be |
|
949 |
related in the same way. |
|
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
950 |
|
61421 | 951 |
\<^medskip> |
61664 | 952 |
Co-regularity is a very fundamental property of the order-sorted algebra of |
953 |
types. For example, it entails principle types and most general unifiers, |
|
954 |
e.g.\ see @{cite "nipkow-prehofer"}. |
|
58618 | 955 |
\<close> |
37768
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
956 |
|
e86221f3bac7
moved co-regularity to class section; avoid duplicated class_deps
haftmann
parents:
37112
diff
changeset
|
957 |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
958 |
section \<open>Overloaded constant definitions \label{sec:overloading}\<close> |
27040 | 959 |
|
58618 | 960 |
text \<open> |
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
961 |
Definitions essentially express abbreviations within the logic. The simplest |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
962 |
form of a definition is \<open>c :: \<sigma> \<equiv> t\<close>, where \<open>c\<close> is a new constant and \<open>t\<close> is |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
963 |
a closed term that does not mention \<open>c\<close>. Moreover, so-called \<^emph>\<open>hidden |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
964 |
polymorphism\<close> is excluded: all type variables in \<open>t\<close> need to occur in its |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
965 |
type \<open>\<sigma>\<close>. |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
966 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
967 |
\<^emph>\<open>Overloading\<close> means that a constant being declared as \<open>c :: \<alpha> decl\<close> may be |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
968 |
defined separately on type instances \<open>c :: (\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n)\<kappa> decl\<close> for each |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
969 |
type constructor \<open>\<kappa>\<close>. At most occasions overloading will be used in a |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
970 |
Haskell-like fashion together with type classes by means of \<^theory_text>\<open>instantiation\<close> |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
971 |
(see \secref{sec:class}). Sometimes low-level overloading is desirable; this |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
972 |
is supported by \<^theory_text>\<open>consts\<close> and \<^theory_text>\<open>overloading\<close> explained below. |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
973 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
974 |
The right-hand side of overloaded definitions may mention overloaded |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
975 |
constants recursively at type instances corresponding to the immediate |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
976 |
argument types \<open>\<beta>\<^sub>1, \<dots>, \<beta>\<^sub>n\<close>. Incomplete specification patterns impose |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
977 |
global constraints on all occurrences. E.g.\ \<open>d :: \<alpha> \<times> \<alpha>\<close> on the left-hand |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
978 |
side means that all corresponding occurrences on some right-hand side need |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
979 |
to be an instance of this, and general \<open>d :: \<alpha> \<times> \<beta>\<close> will be disallowed. Full |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
980 |
details are given by Kun\v{c}ar @{cite "Kuncar:2015"}. |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
981 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
982 |
\<^medskip> |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
983 |
The \<^theory_text>\<open>consts\<close> command and the \<^theory_text>\<open>overloading\<close> target provide a convenient |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
984 |
interface for end-users. Regular specification elements such as @{command |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
985 |
definition}, @{command inductive}, @{command function} may be used in the |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
986 |
body. It is also possible to use \<^theory_text>\<open>consts c :: \<sigma>\<close> with later \<^theory_text>\<open>overloading c |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
987 |
\<equiv> c :: \<sigma>\<close> to keep the declaration and definition of a constant separate. |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
988 |
|
47483 | 989 |
\begin{matharray}{rcl} |
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
990 |
@{command_def "consts"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
61493 | 991 |
@{command_def "overloading"} & : & \<open>theory \<rightarrow> local_theory\<close> \\ |
47483 | 992 |
\end{matharray} |
993 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
994 |
@{rail \<open> |
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
995 |
@@{command consts} ((@{syntax name} '::' @{syntax type} @{syntax mixfix}?) +) |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
996 |
; |
42704 | 997 |
@@{command overloading} ( spec + ) @'begin' |
998 |
; |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
999 |
spec: @{syntax name} ( '\<equiv>' | '==' ) @{syntax term} ( '(' @'unchecked' ')' )? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1000 |
\<close>} |
27040 | 1001 |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1002 |
\<^descr> \<^theory_text>\<open>consts c :: \<sigma>\<close> declares constant \<open>c\<close> to have any instance of type scheme |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1003 |
\<open>\<sigma>\<close>. The optional mixfix annotations may attach concrete syntax to the |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1004 |
constants declared. |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1005 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1006 |
\<^descr> \<^theory_text>\<open>overloading x\<^sub>1 \<equiv> c\<^sub>1 :: \<tau>\<^sub>1 \<dots> x\<^sub>n \<equiv> c\<^sub>n :: \<tau>\<^sub>n begin \<dots> end\<close> defines |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1007 |
a theory target (cf.\ \secref{sec:target}) which allows to specify already |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1008 |
declared constants via definitions in the body. These are identified by an |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1009 |
explicitly given mapping from variable names \<open>x\<^sub>i\<close> to constants \<open>c\<^sub>i\<close> at |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1010 |
particular type instances. The definitions themselves are established using |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1011 |
common specification tools, using the names \<open>x\<^sub>i\<close> as reference to the |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1012 |
corresponding constants. |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1013 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1014 |
Option \<^theory_text>\<open>(unchecked)\<close> disables global dependency checks for the |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1015 |
corresponding definition, which is occasionally useful for exotic |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1016 |
overloading; this is a form of axiomatic specification. It is at the |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1017 |
discretion of the user to avoid malformed theory specifications! |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1018 |
\<close> |
27040 | 1019 |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1020 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1021 |
subsubsection \<open>Example\<close> |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1022 |
|
62173 | 1023 |
consts Length :: "'a \<Rightarrow> nat" |
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1024 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1025 |
overloading |
62173 | 1026 |
Length\<^sub>0 \<equiv> "Length :: unit \<Rightarrow> nat" |
1027 |
Length\<^sub>1 \<equiv> "Length :: 'a \<times> unit \<Rightarrow> nat" |
|
1028 |
Length\<^sub>2 \<equiv> "Length :: 'a \<times> 'b \<times> unit \<Rightarrow> nat" |
|
1029 |
Length\<^sub>3 \<equiv> "Length :: 'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1030 |
begin |
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1031 |
|
62173 | 1032 |
fun Length\<^sub>0 :: "unit \<Rightarrow> nat" where "Length\<^sub>0 () = 0" |
1033 |
fun Length\<^sub>1 :: "'a \<times> unit \<Rightarrow> nat" where "Length\<^sub>1 (a, ()) = 1" |
|
1034 |
fun Length\<^sub>2 :: "'a \<times> 'b \<times> unit \<Rightarrow> nat" where "Length\<^sub>2 (a, b, ()) = 2" |
|
1035 |
fun Length\<^sub>3 :: "'a \<times> 'b \<times> 'c \<times> unit \<Rightarrow> nat" where "Length\<^sub>3 (a, b, c, ()) = 3" |
|
62172
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1036 |
|
7eaeae127955
updated section on "Overloaded constant definitions";
wenzelm
parents:
61891
diff
changeset
|
1037 |
end |
27040 | 1038 |
|
62173 | 1039 |
lemma "Length (a, b, c, ()) = 3" by simp |
1040 |
lemma "Length ((a, b), (c, d), ()) = 2" by simp |
|
1041 |
lemma "Length ((a, b, c, d, e), ()) = 1" by simp |
|
1042 |
||
27040 | 1043 |
|
58618 | 1044 |
section \<open>Incorporating ML code \label{sec:ML}\<close> |
27040 | 1045 |
|
58618 | 1046 |
text \<open> |
27040 | 1047 |
\begin{matharray}{rcl} |
62862 | 1048 |
@{command_def "SML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
62903 | 1049 |
@{command_def "SML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1050 |
@{command_def "SML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
61493 | 1051 |
@{command_def "ML_file"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
62903 | 1052 |
@{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1053 |
@{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
61493 | 1054 |
@{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1055 |
@{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\ |
|
1056 |
@{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\ |
|
1057 |
@{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\ |
|
1058 |
@{command_def "setup"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1059 |
@{command_def "local_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
1060 |
@{command_def "attribute_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1061 |
\end{matharray} |
57478 | 1062 |
\begin{tabular}{rcll} |
61493 | 1063 |
@{attribute_def ML_print_depth} & : & \<open>attribute\<close> & default 10 \\ |
1064 |
@{attribute_def ML_source_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
|
62903 | 1065 |
@{attribute_def ML_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
61493 | 1066 |
@{attribute_def ML_exception_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
62903 | 1067 |
@{attribute_def ML_exception_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
57478 | 1068 |
\end{tabular} |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28758
diff
changeset
|
1069 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1070 |
@{rail \<open> |
62903 | 1071 |
(@@{command SML_file} | |
1072 |
@@{command SML_file_debug} | |
|
1073 |
@@{command SML_file_no_debug} | |
|
1074 |
@@{command ML_file} | |
|
1075 |
@@{command ML_file_debug} | |
|
62969 | 1076 |
@@{command ML_file_no_debug}) @{syntax name} ';'? |
27040 | 1077 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1078 |
(@@{command ML} | @@{command ML_prf} | @@{command ML_val} | |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1079 |
@@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} |
27040 | 1080 |
; |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59781
diff
changeset
|
1081 |
@@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1082 |
\<close>} |
27040 | 1083 |
|
61665 | 1084 |
\<^descr> \<^theory_text>\<open>SML_file name\<close> reads and evaluates the given Standard ML file. Top-level |
62862 | 1085 |
SML bindings are stored within the (global or local) theory context; the |
1086 |
initial environment is restricted to the Standard ML implementation of |
|
1087 |
Poly/ML, without the many add-ons of Isabelle/ML. Multiple \<^theory_text>\<open>SML_file\<close> |
|
1088 |
commands may be used to build larger Standard ML projects, independently of |
|
1089 |
the regular Isabelle/ML environment. |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
55837
diff
changeset
|
1090 |
|
61665 | 1091 |
\<^descr> \<^theory_text>\<open>ML_file name\<close> reads and evaluates the given ML file. The current theory |
1092 |
context is passed down to the ML toplevel and may be modified, using @{ML |
|
1093 |
"Context.>>"} or derived ML commands. Top-level ML bindings are stored |
|
1094 |
within the (global or local) theory context. |
|
62903 | 1095 |
|
1096 |
\<^descr> \<^theory_text>\<open>SML_file_debug\<close>, \<^theory_text>\<open>SML_file_no_debug\<close>, \<^theory_text>\<open>ML_file_debug\<close>, and |
|
1097 |
\<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while |
|
1098 |
the given file is compiled. |
|
1099 |
||
61665 | 1100 |
\<^descr> \<^theory_text>\<open>ML text\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given |
1101 |
\<open>text\<close>. Top-level ML bindings are stored within the (global or local) theory |
|
1102 |
context. |
|
28281 | 1103 |
|
61665 | 1104 |
\<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context. |
1105 |
Top-level ML bindings are stored within the proof context in a purely |
|
1106 |
sequential fashion, disregarding the nested proof structure. ML bindings |
|
1107 |
introduced by \<^theory_text>\<open>ML_prf\<close> are discarded at the end of the proof. |
|
27040 | 1108 |
|
61665 | 1109 |
\<^descr> \<^theory_text>\<open>ML_val\<close> and \<^theory_text>\<open>ML_command\<close> are diagnostic versions of \<^theory_text>\<open>ML\<close>, which means |
1110 |
that the context may not be updated. \<^theory_text>\<open>ML_val\<close> echos the bindings produced |
|
1111 |
at the ML toplevel, but \<^theory_text>\<open>ML_command\<close> is silent. |
|
27040 | 1112 |
|
61665 | 1113 |
\<^descr> \<^theory_text>\<open>setup "text"\<close> changes the current theory context by applying \<open>text\<close>, |
1114 |
which refers to an ML expression of type @{ML_type "theory -> theory"}. This |
|
1115 |
enables to initialize any object-logic specific tools and packages written |
|
1116 |
in ML, for example. |
|
30461 | 1117 |
|
61665 | 1118 |
\<^descr> \<^theory_text>\<open>local_setup\<close> is similar to \<^theory_text>\<open>setup\<close> for a local theory context, and an |
1119 |
ML expression of type @{ML_type "local_theory -> local_theory"}. This allows |
|
1120 |
to invoke local theory specification packages without going through concrete |
|
1121 |
outer syntax, for example. |
|
28758 | 1122 |
|
61665 | 1123 |
\<^descr> \<^theory_text>\<open>attribute_setup name = "text" description\<close> defines an attribute in the |
1124 |
current context. The given \<open>text\<close> has to be an ML expression of type |
|
1125 |
@{ML_type "attribute context_parser"}, cf.\ basic parsers defined in |
|
1126 |
structure @{ML_structure Args} and @{ML_structure Attrib}. |
|
30526 | 1127 |
|
1128 |
In principle, attributes can operate both on a given theorem and the |
|
61664 | 1129 |
implicit context, although in practice only one is modified and the other |
1130 |
serves as parameter. Here are examples for these two cases: |
|
58618 | 1131 |
\<close> |
30526 | 1132 |
|
59905 | 1133 |
(*<*)experiment begin(*>*) |
62903 | 1134 |
attribute_setup my_rule = |
1135 |
\<open>Attrib.thms >> (fn ths => |
|
1136 |
Thm.rule_attribute ths |
|
1137 |
(fn context: Context.generic => fn th: thm => |
|
1138 |
let val th' = th OF ths |
|
1139 |
in th' end))\<close> |
|
30526 | 1140 |
|
62903 | 1141 |
attribute_setup my_declaration = |
1142 |
\<open>Attrib.thms >> (fn ths => |
|
1143 |
Thm.declaration_attribute |
|
1144 |
(fn th: thm => fn context: Context.generic => |
|
1145 |
let val context' = context |
|
1146 |
in context' end))\<close> |
|
59905 | 1147 |
(*<*)end(*>*) |
30526 | 1148 |
|
58618 | 1149 |
text \<open> |
61664 | 1150 |
\<^descr> @{attribute ML_print_depth} controls the printing depth of the ML toplevel |
62903 | 1151 |
pretty printer. Typically the limit should be less than 10. Bigger values |
1152 |
such as 100--1000 are occasionally useful for debugging. |
|
57478 | 1153 |
|
61664 | 1154 |
\<^descr> @{attribute ML_source_trace} indicates whether the source text that is |
1155 |
given to the ML compiler should be output: it shows the raw Standard ML |
|
57478 | 1156 |
after expansion of Isabelle/ML antiquotations. |
1157 |
||
62903 | 1158 |
\<^descr> @{attribute ML_debugger} controls compilation of sources with or without |
1159 |
debugging information. The global system option @{system_option_ref |
|
1160 |
ML_debugger} does the same when building a session image. It is also |
|
1161 |
possible use commands like \<^theory_text>\<open>ML_file_debug\<close> etc. The ML debugger is |
|
1162 |
explained further in @{cite "isabelle-jedit"}. |
|
1163 |
||
61664 | 1164 |
\<^descr> @{attribute ML_exception_trace} indicates whether the ML run-time system |
1165 |
should print a detailed stack trace on exceptions. The result is dependent |
|
62903 | 1166 |
on various ML compiler optimizations. The boundary for the exception trace |
1167 |
is the current Isar command transactions: it is occasionally better to |
|
1168 |
insert the combinator @{ML Runtime.exn_trace} into ML code for debugging |
|
1169 |
@{cite "isabelle-implementation"}, closer to the point where it actually |
|
1170 |
happens. |
|
57478 | 1171 |
|
62903 | 1172 |
\<^descr> @{attribute ML_exception_debugger} controls detailed exception trace via |
1173 |
the Poly/ML debugger, at the cost of extra compile-time and run-time |
|
1174 |
overhead. Relevant ML modules need to be compiled beforehand with debugging |
|
1175 |
enabled, see @{attribute ML_debugger} above. |
|
58618 | 1176 |
\<close> |
57478 | 1177 |
|
27040 | 1178 |
|
58618 | 1179 |
section \<open>Primitive specification elements\<close> |
27040 | 1180 |
|
58618 | 1181 |
subsection \<open>Sorts\<close> |
27040 | 1182 |
|
58618 | 1183 |
text \<open> |
27040 | 1184 |
\begin{matharray}{rcll} |
61493 | 1185 |
@{command_def "default_sort"} & : & \<open>local_theory \<rightarrow> local_theory\<close> |
27040 | 1186 |
\end{matharray} |
1187 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1188 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1189 |
@@{command default_sort} @{syntax sort} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1190 |
\<close>} |
27040 | 1191 |
|
61665 | 1192 |
\<^descr> \<^theory_text>\<open>default_sort s\<close> makes sort \<open>s\<close> the new default sort for any type |
1193 |
variable that is given explicitly in the text, but lacks a sort constraint |
|
1194 |
(wrt.\ the current context). Type variables generated by type inference are |
|
1195 |
not affected. |
|
28767 | 1196 |
|
61664 | 1197 |
Usually the default sort is only changed when defining a new object-logic. |
1198 |
For example, the default sort in Isabelle/HOL is @{class type}, the class of |
|
1199 |
all HOL types. |
|
28767 | 1200 |
|
61664 | 1201 |
When merging theories, the default sorts of the parents are logically |
1202 |
intersected, i.e.\ the representations as lists of classes are joined. |
|
58618 | 1203 |
\<close> |
27040 | 1204 |
|
1205 |
||
58618 | 1206 |
subsection \<open>Types \label{sec:types-pure}\<close> |
27040 | 1207 |
|
58618 | 1208 |
text \<open> |
27040 | 1209 |
\begin{matharray}{rcll} |
61493 | 1210 |
@{command_def "type_synonym"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1211 |
@{command_def "typedecl"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
27040 | 1212 |
\end{matharray} |
1213 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1214 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1215 |
@@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?) |
27040 | 1216 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1217 |
@@{command typedecl} @{syntax typespec} @{syntax mixfix}? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1218 |
\<close>} |
27040 | 1219 |
|
61665 | 1220 |
\<^descr> \<^theory_text>\<open>type_synonym (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t = \<tau>\<close> introduces a \<^emph>\<open>type synonym\<close> \<open>(\<alpha>\<^sub>1, \<dots>, |
1221 |
\<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in |
|
1222 |
Isabelle/HOL, type synonyms are merely syntactic abbreviations without any |
|
1223 |
logical significance. Internally, type synonyms are fully expanded. |
|
27040 | 1224 |
|
61665 | 1225 |
\<^descr> \<^theory_text>\<open>typedecl (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor \<open>t\<close>. If the |
1226 |
object-logic defines a base sort \<open>s\<close>, then the constructor is declared to |
|
1227 |
operate on that, via the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>. |
|
27040 | 1228 |
|
57487 | 1229 |
|
1230 |
\begin{warn} |
|
61664 | 1231 |
If you introduce a new type axiomatically, i.e.\ via @{command_ref |
1232 |
typedecl} and @{command_ref axiomatization} |
|
1233 |
(\secref{sec:axiomatizations}), the minimum requirement is that it has a |
|
1234 |
non-empty model, to avoid immediate collapse of the logical environment. |
|
1235 |
Moreover, one needs to demonstrate that the interpretation of such |
|
1236 |
free-form axiomatizations can coexist with other axiomatization schemes |
|
1237 |
for types, notably @{command_def typedef} in Isabelle/HOL |
|
1238 |
(\secref{sec:hol-typedef}), or any other extension that people might have |
|
1239 |
introduced elsewhere. |
|
57487 | 1240 |
\end{warn} |
58618 | 1241 |
\<close> |
27040 | 1242 |
|
1243 |
||
58618 | 1244 |
section \<open>Naming existing theorems \label{sec:theorems}\<close> |
27040 | 1245 |
|
58618 | 1246 |
text \<open> |
27040 | 1247 |
\begin{matharray}{rcll} |
61493 | 1248 |
@{command_def "lemmas"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1249 |
@{command_def "named_theorems"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
27040 | 1250 |
\end{matharray} |
1251 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1252 |
@{rail \<open> |
62969 | 1253 |
@@{command lemmas} (@{syntax thmdef}? @{syntax thms} + @'and') |
59785 | 1254 |
@{syntax for_fixes} |
57946
6a26aa5fa65e
updated documentation concerning 'named_theorems';
wenzelm
parents:
57941
diff
changeset
|
1255 |
; |
59785 | 1256 |
@@{command named_theorems} (@{syntax name} @{syntax text}? + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1257 |
\<close>} |
27040 | 1258 |
|
61665 | 1259 |
\<^descr> \<^theory_text>\<open>lemmas a = b\<^sub>1 \<dots> b\<^sub>n\<close>~@{keyword_def "for"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close> evaluates given |
1260 |
facts (with attributes) in the current context, which may be augmented by |
|
1261 |
local variables. Results are standardized before being stored, i.e.\ |
|
1262 |
schematic variables are renamed to enforce index \<open>0\<close> uniformly. |
|
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
42936
diff
changeset
|
1263 |
|
61665 | 1264 |
\<^descr> \<^theory_text>\<open>named_theorems name description\<close> declares a dynamic fact within the |
1265 |
context. The same \<open>name\<close> is used to define an attribute with the usual |
|
1266 |
\<open>add\<close>/\<open>del\<close> syntax (e.g.\ see \secref{sec:simp-rules}) to maintain the |
|
61664 | 1267 |
content incrementally, in canonical declaration order of the text structure. |
58618 | 1268 |
\<close> |
27040 | 1269 |
|
1270 |
||
58618 | 1271 |
section \<open>Oracles\<close> |
27040 | 1272 |
|
58618 | 1273 |
text \<open> |
47483 | 1274 |
\begin{matharray}{rcll} |
61493 | 1275 |
@{command_def "oracle"} & : & \<open>theory \<rightarrow> theory\<close> & (axiomatic!) \\ |
47483 | 1276 |
\end{matharray} |
1277 |
||
61664 | 1278 |
Oracles allow Isabelle to take advantage of external reasoners such as |
1279 |
arithmetic decision procedures, model checkers, fast tautology checkers or |
|
1280 |
computer algebra systems. Invoked as an oracle, an external reasoner can |
|
1281 |
create arbitrary Isabelle theorems. |
|
28756 | 1282 |
|
61664 | 1283 |
It is the responsibility of the user to ensure that the external reasoner is |
1284 |
as trustworthy as the application requires. Another typical source of errors |
|
1285 |
is the linkup between Isabelle and the external tool, not just its concrete |
|
1286 |
implementation, but also the required translation between two different |
|
1287 |
logical environments. |
|
28756 | 1288 |
|
1289 |
Isabelle merely guarantees well-formedness of the propositions being |
|
61664 | 1290 |
asserted, and records within the internal derivation object how presumed |
1291 |
theorems depend on unproven suppositions. |
|
28756 | 1292 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1293 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1294 |
@@{command oracle} @{syntax name} '=' @{syntax text} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1295 |
\<close>} |
27040 | 1296 |
|
61665 | 1297 |
\<^descr> \<^theory_text>\<open>oracle name = "text"\<close> turns the given ML expression \<open>text\<close> of type |
1298 |
@{ML_text "'a -> cterm"} into an ML function of type @{ML_text "'a -> thm"}, |
|
1299 |
which is bound to the global identifier @{ML_text name}. This acts like an |
|
1300 |
infinitary specification of axioms! Invoking the oracle only works within |
|
1301 |
the scope of the resulting theory. |
|
27040 | 1302 |
|
28756 | 1303 |
|
61664 | 1304 |
See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of defining |
1305 |
a new primitive rule as oracle, and turning it into a proof method. |
|
58618 | 1306 |
\<close> |
27040 | 1307 |
|
1308 |
||
58618 | 1309 |
section \<open>Name spaces\<close> |
27040 | 1310 |
|
58618 | 1311 |
text \<open> |
27040 | 1312 |
\begin{matharray}{rcl} |
61493 | 1313 |
@{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1314 |
@{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1315 |
@{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1316 |
@{command_def "hide_fact"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
27040 | 1317 |
\end{matharray} |
1318 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1319 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
41435
diff
changeset
|
1320 |
( @{command hide_class} | @{command hide_type} | |
62969 | 1321 |
@{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + ) |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1322 |
\<close>} |
27040 | 1323 |
|
61664 | 1324 |
Isabelle organizes any kind of name declarations (of types, constants, |
1325 |
theorems etc.) by separate hierarchically structured name spaces. Normally |
|
61665 | 1326 |
the user does not have to control the behaviour of name spaces by hand, yet |
61664 | 1327 |
the following commands provide some way to do so. |
27040 | 1328 |
|
61665 | 1329 |
\<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name |
1330 |
space; with the \<open>(open)\<close> option, only the unqualified base name is hidden. |
|
36177
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
35681
diff
changeset
|
1331 |
|
61664 | 1332 |
Note that hiding name space accesses has no impact on logical declarations |
1333 |
--- they remain valid internally. Entities that are no longer accessible to |
|
1334 |
the user are printed with the special qualifier ``\<open>??\<close>'' prefixed to the |
|
1335 |
full internal name. |
|
27040 | 1336 |
|
61665 | 1337 |
\<^descr> \<^theory_text>\<open>hide_type\<close>, \<^theory_text>\<open>hide_const\<close>, and \<^theory_text>\<open>hide_fact\<close> are similar to |
1338 |
\<^theory_text>\<open>hide_class\<close>, but hide types, constants, and facts, respectively. |
|
58618 | 1339 |
\<close> |
27040 | 1340 |
|
26869 | 1341 |
end |