author | wenzelm |
Wed, 24 Jul 2002 22:13:02 +0200 | |
changeset 13419 | 902ec83c1ca9 |
parent 13383 | 041d78bf9403 |
child 13457 | 7ddcf40a80b3 |
permissions | -rw-r--r-- |
12075 | 1 |
(* Title: HOL/ex/Locales.thy |
2 |
ID: $Id$ |
|
12574 | 3 |
Author: Markus Wenzel, LMU München |
12075 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
*) |
|
6 |
||
12507 | 7 |
header {* Using locales in Isabelle/Isar *} |
12075 | 8 |
|
9 |
theory Locales = Main: |
|
10 |
||
12507 | 11 |
text_raw {* |
12 |
\newcommand{\isasyminv}{\isasyminverse} |
|
13 |
\newcommand{\isasymIN}{\isatext{\isakeyword{in}}} |
|
12965 | 14 |
\newcommand{\isasymINCLUDES}{\isatext{\isakeyword{includes}}} |
12507 | 15 |
*} |
16 |
||
17 |
subsection {* Overview *} |
|
18 |
||
12091 | 19 |
text {* |
12105 | 20 |
Locales provide a mechanism for encapsulating local contexts. The |
12574 | 21 |
original version due to Florian Kammüller \cite{Kamm-et-al:1999} |
12507 | 22 |
refers directly to the raw meta-logic of Isabelle. Semantically, a |
23 |
locale is just a (curried) predicate of the pure meta-logic |
|
24 |
\cite{Paulson:1989}. |
|
25 |
||
26 |
The present version for Isabelle/Isar builds on top of the rich |
|
27 |
infrastructure of proof contexts |
|
28 |
\cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis}, |
|
29 |
achieving a tight integration with Isar proof texts, and a slightly |
|
30 |
more abstract view of the underlying concepts. An Isar proof |
|
31 |
context encapsulates certain language elements that correspond to |
|
32 |
@{text \<And>} (universal quantification), @{text \<Longrightarrow>} (implication), and |
|
33 |
@{text "\<equiv>"} (definitions) of the pure Isabelle framework. Moreover, |
|
34 |
there are extra-logical concepts like term abbreviations or local |
|
35 |
theorem attributes (declarations of simplification rules etc.) that |
|
36 |
are indispensable in realistic applications. |
|
37 |
||
38 |
Locales support concrete syntax, providing a localized version of |
|
39 |
the existing concept of mixfix annotations of Isabelle |
|
40 |
\cite{Paulson:1994:Isabelle}. Furthermore, there is a separate |
|
41 |
concept of ``implicit structures'' that admits to refer to |
|
42 |
particular locale parameters in a casual manner (essentially derived |
|
43 |
from the basic idea of ``anti-quotations'' or generalized de-Bruijn |
|
44 |
indexes demonstrated in \cite[\S13--14]{Wenzel:2001:Isar-examples}). |
|
12105 | 45 |
|
12507 | 46 |
Implicit structures work particular well together with extensible |
47 |
records in HOL \cite{Naraschewski-Wenzel:1998} (the |
|
48 |
``object-oriented'' features discussed there are not required here). |
|
49 |
Thus we shall essentially use record types to represent polymorphic |
|
50 |
signatures of mathematical structures, while locales describe their |
|
51 |
logical properties as a predicate. Due to type inference of |
|
52 |
simply-typed records we are able to give succinct specifications, |
|
53 |
without caring about signature morphisms ourselves. Further |
|
54 |
eye-candy is provided by the independent concept of ``indexed |
|
55 |
concrete syntax'' for record selectors. |
|
56 |
||
57 |
Operations for building up locale contexts from existing definitions |
|
58 |
cover common operations of \emph{merge} (disjunctive union in |
|
59 |
canonical order) and \emph{rename} (of term parameters; types are |
|
60 |
always inferred automatically). |
|
61 |
||
62 |
\medskip Note that the following further concepts are still |
|
63 |
\emph{absent}: |
|
64 |
\begin{itemize} |
|
12099 | 65 |
|
12507 | 66 |
\item Specific language elements for \emph{instantiation} of |
67 |
locales. |
|
68 |
||
69 |
Currently users may simulate this to some extend by having primitive |
|
70 |
Isabelle/Isar operations (@{text of} for substitution and @{text OF} |
|
71 |
for composition, \cite{Wenzel:2001:isar-ref}) act on the |
|
72 |
automatically exported results stemming from different contexts. |
|
73 |
||
74 |
\item Interpretation of locales, analogous to ``functors'' in |
|
75 |
abstract algebra. |
|
76 |
||
77 |
In principle one could directly work with functions over structures |
|
78 |
(extensible records), and predicates being derived from locale |
|
79 |
definitions. |
|
80 |
||
81 |
\end{itemize} |
|
82 |
||
83 |
\medskip Subsequently, we demonstrate some readily available |
|
84 |
concepts of Isabelle/Isar locales by some simple examples of |
|
85 |
abstract algebraic reasoning. |
|
12091 | 86 |
*} |
87 |
||
88 |
subsection {* Local contexts as mathematical structures *} |
|
89 |
||
12099 | 90 |
text {* |
91 |
The following definitions of @{text group} and @{text abelian_group} |
|
12105 | 92 |
merely encapsulate local parameters (with private syntax) and |
12099 | 93 |
assumptions; local definitions may be given as well, but are not |
94 |
shown here. |
|
12075 | 95 |
*} |
96 |
||
12574 | 97 |
locale group_context = |
12075 | 98 |
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70) |
99 |
and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999) |
|
100 |
and one :: 'a ("\<one>") |
|
101 |
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
102 |
and left_inv: "x\<inv> \<cdot> x = \<one>" |
|
103 |
and left_one: "\<one> \<cdot> x = x" |
|
104 |
||
12574 | 105 |
locale abelian_group_context = group_context + |
12075 | 106 |
assumes commute: "x \<cdot> y = y \<cdot> x" |
107 |
||
12099 | 108 |
text {* |
109 |
\medskip We may now prove theorems within a local context, just by |
|
110 |
including a directive ``@{text "(\<IN> name)"}'' in the goal |
|
111 |
specification. The final result will be stored within the named |
|
112 |
locale; a second copy is exported to the enclosing theory context. |
|
113 |
*} |
|
114 |
||
12574 | 115 |
theorem (in group_context) |
12075 | 116 |
right_inv: "x \<cdot> x\<inv> = \<one>" |
117 |
proof - |
|
118 |
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one) |
|
119 |
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc) |
|
120 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv) |
|
121 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc) |
|
122 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv) |
|
123 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc) |
|
124 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one) |
|
125 |
also have "\<dots> = \<one>" by (simp only: left_inv) |
|
126 |
finally show ?thesis . |
|
127 |
qed |
|
128 |
||
12574 | 129 |
theorem (in group_context) |
12075 | 130 |
right_one: "x \<cdot> \<one> = x" |
131 |
proof - |
|
132 |
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv) |
|
133 |
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc) |
|
134 |
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv) |
|
135 |
also have "\<dots> = x" by (simp only: left_one) |
|
136 |
finally show ?thesis . |
|
137 |
qed |
|
138 |
||
12099 | 139 |
text {* |
12105 | 140 |
\medskip Apart from the named context we may also refer to further |
141 |
context elements (parameters, assumptions, etc.) in a casual manner; |
|
142 |
these are discharged when the proof is finished. |
|
12099 | 143 |
*} |
144 |
||
12574 | 145 |
theorem (in group_context) |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset
|
146 |
assumes eq: "e \<cdot> x = x" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset
|
147 |
shows one_equality: "\<one> = e" |
12075 | 148 |
proof - |
149 |
have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv) |
|
150 |
also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq) |
|
151 |
also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc) |
|
152 |
also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv) |
|
153 |
also have "\<dots> = e" by (simp only: right_one) |
|
154 |
finally show ?thesis . |
|
155 |
qed |
|
156 |
||
12574 | 157 |
theorem (in group_context) |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset
|
158 |
assumes eq: "x' \<cdot> x = \<one>" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset
|
159 |
shows inv_equality: "x\<inv> = x'" |
12075 | 160 |
proof - |
161 |
have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one) |
|
162 |
also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq) |
|
163 |
also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc) |
|
164 |
also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv) |
|
165 |
also have "\<dots> = x'" by (simp only: right_one) |
|
166 |
finally show ?thesis . |
|
167 |
qed |
|
168 |
||
12574 | 169 |
theorem (in group_context) |
12075 | 170 |
inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" |
171 |
proof (rule inv_equality) |
|
172 |
show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>" |
|
173 |
proof - |
|
174 |
have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc) |
|
175 |
also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv) |
|
176 |
also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one) |
|
177 |
also have "\<dots> = \<one>" by (simp only: left_inv) |
|
178 |
finally show ?thesis . |
|
179 |
qed |
|
180 |
qed |
|
181 |
||
12099 | 182 |
text {* |
12105 | 183 |
\medskip Established results are automatically propagated through |
184 |
the hierarchy of locales. Below we establish a trivial fact in |
|
185 |
commutative groups, while referring both to theorems of @{text |
|
186 |
group} and the additional assumption of @{text abelian_group}. |
|
12099 | 187 |
*} |
188 |
||
12574 | 189 |
theorem (in abelian_group_context) |
12075 | 190 |
inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>" |
191 |
proof - |
|
192 |
have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod) |
|
193 |
also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute) |
|
194 |
finally show ?thesis . |
|
195 |
qed |
|
196 |
||
12099 | 197 |
text {* |
12507 | 198 |
We see that the initial import of @{text group} within the |
199 |
definition of @{text abelian_group} is actually evaluated |
|
200 |
dynamically. Thus any results in @{text group} are made available |
|
201 |
to the derived context of @{text abelian_group} as well. Note that |
|
12965 | 202 |
the alternative context element @{text \<INCLUDES>} would import |
12507 | 203 |
existing locales in a static fashion, without participating in |
204 |
further facts emerging later on. |
|
205 |
||
206 |
\medskip Some more properties of inversion in general group theory |
|
207 |
follow. |
|
12099 | 208 |
*} |
209 |
||
12574 | 210 |
theorem (in group_context) |
12075 | 211 |
inv_inv: "(x\<inv>)\<inv> = x" |
212 |
proof (rule inv_equality) |
|
213 |
show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv) |
|
214 |
qed |
|
215 |
||
12574 | 216 |
theorem (in group_context) |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset
|
217 |
assumes eq: "x\<inv> = y\<inv>" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset
|
218 |
shows inv_inject: "x = y" |
12075 | 219 |
proof - |
220 |
have "x = x \<cdot> \<one>" by (simp only: right_one) |
|
221 |
also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv) |
|
222 |
also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq) |
|
223 |
also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc) |
|
224 |
also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv) |
|
225 |
also have "\<dots> = y" by (simp only: left_one) |
|
226 |
finally show ?thesis . |
|
227 |
qed |
|
228 |
||
12099 | 229 |
text {* |
230 |
\bigskip We see that this representation of structures as local |
|
231 |
contexts is rather light-weight and convenient to use for abstract |
|
232 |
reasoning. Here the ``components'' (the group operations) have been |
|
233 |
exhibited directly as context parameters; logically this corresponds |
|
13383 | 234 |
to a curried predicate definition: |
235 |
||
13419 | 236 |
@{thm [display] group_context_def [no_vars]} |
237 |
||
238 |
The corresponding introduction rule is as follows: |
|
239 |
||
240 |
@{thm [display] group_context.intro [no_vars]} |
|
13383 | 241 |
|
242 |
Occasionally, this ``externalized'' version of the informal idea of |
|
243 |
classes of tuple structures may cause some inconveniences, |
|
244 |
especially in meta-theoretical studies (involving functors from |
|
245 |
groups to groups, for example). |
|
12091 | 246 |
|
12507 | 247 |
Another minor drawback of the naive approach above is that concrete |
248 |
syntax will get lost on any kind of operation on the locale itself |
|
249 |
(such as renaming, copying, or instantiation). Whenever the |
|
250 |
particular terminology of local parameters is affected the |
|
251 |
associated syntax would have to be changed as well, which is hard to |
|
252 |
achieve formally. |
|
12099 | 253 |
*} |
254 |
||
255 |
||
12105 | 256 |
subsection {* Explicit structures referenced implicitly *} |
12091 | 257 |
|
12099 | 258 |
text {* |
12507 | 259 |
We introduce the same hierarchy of basic group structures as above, |
260 |
this time using extensible record types for the signature part, |
|
261 |
together with concrete syntax for selector functions. |
|
12099 | 262 |
*} |
263 |
||
12507 | 264 |
record 'a semigroup = |
265 |
prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>\<index>" 70) |
|
266 |
||
267 |
record 'a group = "'a semigroup" + |
|
268 |
inv :: "'a \<Rightarrow> 'a" ("(_\<inv>\<index>)" [1000] 999) |
|
269 |
one :: 'a ("\<one>\<index>") |
|
12099 | 270 |
|
271 |
text {* |
|
12507 | 272 |
The mixfix annotations above include a special ``structure index |
12574 | 273 |
indicator'' @{text \<index>} that makes gammer productions dependent on |
12507 | 274 |
certain parameters that have been declared as ``structure'' in a |
275 |
locale context later on. Thus we achieve casual notation as |
|
276 |
encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for |
|
277 |
@{text "prod G x y"}. |
|
12099 | 278 |
|
12507 | 279 |
\medskip The following locale definitions introduce operate on a |
280 |
single parameter declared as ``\isakeyword{structure}''. Type |
|
281 |
inference takes care to fill in the appropriate record type schemes |
|
282 |
internally. |
|
12099 | 283 |
*} |
12091 | 284 |
|
12574 | 285 |
locale semigroup = |
12507 | 286 |
fixes S :: "'a group" (structure) |
287 |
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" |
|
12099 | 288 |
|
12574 | 289 |
locale group = semigroup G + |
12507 | 290 |
assumes left_inv: "x\<inv> \<cdot> x = \<one>" |
12099 | 291 |
and left_one: "\<one> \<cdot> x = x" |
292 |
||
293 |
text {* |
|
12507 | 294 |
Note that we prefer to call the @{text group} record structure |
295 |
@{text G} rather than @{text S} inherited from @{text semigroup}. |
|
296 |
This does not affect our concrete syntax, which is only dependent on |
|
297 |
the \emph{positional} arrangements of currently active structures |
|
298 |
(actually only one above), rather than names. In fact, these |
|
299 |
parameter names rarely occur in the term language at all (due to the |
|
300 |
``indexed syntax'' facility of Isabelle). On the other hand, names |
|
301 |
of locale facts will get qualified accordingly, e.g. @{text S.assoc} |
|
302 |
versus @{text G.assoc}. |
|
303 |
||
12574 | 304 |
\medskip We may now proceed to prove results within @{text group} |
305 |
just as before for @{text group}. The subsequent proof texts are |
|
306 |
exactly the same as despite the more advanced internal arrangement. |
|
12099 | 307 |
*} |
308 |
||
12574 | 309 |
theorem (in group) |
12099 | 310 |
right_inv: "x \<cdot> x\<inv> = \<one>" |
311 |
proof - |
|
312 |
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one) |
|
313 |
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc) |
|
314 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv) |
|
315 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc) |
|
316 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv) |
|
317 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc) |
|
318 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one) |
|
319 |
also have "\<dots> = \<one>" by (simp only: left_inv) |
|
320 |
finally show ?thesis . |
|
321 |
qed |
|
322 |
||
12574 | 323 |
theorem (in group) |
12099 | 324 |
right_one: "x \<cdot> \<one> = x" |
325 |
proof - |
|
326 |
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv) |
|
327 |
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc) |
|
328 |
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv) |
|
329 |
also have "\<dots> = x" by (simp only: left_one) |
|
330 |
finally show ?thesis . |
|
331 |
qed |
|
332 |
||
333 |
text {* |
|
12574 | 334 |
\medskip Several implicit structures may be active at the same time. |
335 |
The concrete syntax facility for locales actually maintains indexed |
|
336 |
structures that may be references implicitly --- via mixfix |
|
337 |
annotations that have been decorated by an ``index argument'' |
|
338 |
(@{text \<index>}). |
|
12099 | 339 |
|
12574 | 340 |
The following synthetic example demonstrates how to refer to several |
341 |
structures of type @{text group} succinctly. We work with two |
|
342 |
versions of the @{text group} locale above. |
|
12099 | 343 |
*} |
12091 | 344 |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset
|
345 |
lemma |
12955 | 346 |
includes group G |
347 |
includes group H |
|
13107 | 348 |
shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" |
349 |
and "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" |
|
350 |
and "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" |
|
351 |
by (rule refl)+ |
|
12574 | 352 |
|
353 |
text {* |
|
354 |
Note that the trivial statements above need to be given as a |
|
355 |
simultaneous goal in order to have type-inference make the implicit |
|
356 |
typing of structures @{text G} and @{text H} agree. |
|
357 |
*} |
|
12091 | 358 |
|
12099 | 359 |
end |