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