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