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}}}
|
|
14 |
\newcommand{\isasymUSES}{\isatext{\isakeyword{uses}}}
|
|
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)
|
12075
|
146 |
(assumes eq: "e \<cdot> x = x")
|
|
147 |
one_equality: "\<one> = e"
|
|
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)
|
12075
|
158 |
(assumes eq: "x' \<cdot> x = \<one>")
|
|
159 |
inv_equality: "x\<inv> = x'"
|
|
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
|
|
202 |
the alternative context element @{text \<USES>} would import
|
|
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)
|
12075
|
217 |
(assumes eq: "x\<inv> = y\<inv>")
|
|
218 |
inv_inject: "x = y"
|
|
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
|
|
234 |
to a curried predicate definition. Occasionally, this
|
|
235 |
``externalized'' version of the informal idea of classes of tuple
|
|
236 |
structures may cause some inconveniences, especially in
|
|
237 |
meta-theoretical studies (involving functors from groups to groups,
|
|
238 |
for example).
|
12091
|
239 |
|
12507
|
240 |
Another minor drawback of the naive approach above is that concrete
|
|
241 |
syntax will get lost on any kind of operation on the locale itself
|
|
242 |
(such as renaming, copying, or instantiation). Whenever the
|
|
243 |
particular terminology of local parameters is affected the
|
|
244 |
associated syntax would have to be changed as well, which is hard to
|
|
245 |
achieve formally.
|
12099
|
246 |
*}
|
|
247 |
|
|
248 |
|
12105
|
249 |
subsection {* Explicit structures referenced implicitly *}
|
12091
|
250 |
|
12099
|
251 |
text {*
|
12507
|
252 |
We introduce the same hierarchy of basic group structures as above,
|
|
253 |
this time using extensible record types for the signature part,
|
|
254 |
together with concrete syntax for selector functions.
|
12099
|
255 |
*}
|
|
256 |
|
12507
|
257 |
record 'a semigroup =
|
|
258 |
prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>\<index>" 70)
|
|
259 |
|
|
260 |
record 'a group = "'a semigroup" +
|
|
261 |
inv :: "'a \<Rightarrow> 'a" ("(_\<inv>\<index>)" [1000] 999)
|
|
262 |
one :: 'a ("\<one>\<index>")
|
12099
|
263 |
|
|
264 |
text {*
|
12507
|
265 |
The mixfix annotations above include a special ``structure index
|
12574
|
266 |
indicator'' @{text \<index>} that makes gammer productions dependent on
|
12507
|
267 |
certain parameters that have been declared as ``structure'' in a
|
|
268 |
locale context later on. Thus we achieve casual notation as
|
|
269 |
encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for
|
|
270 |
@{text "prod G x y"}.
|
12099
|
271 |
|
12507
|
272 |
\medskip The following locale definitions introduce operate on a
|
|
273 |
single parameter declared as ``\isakeyword{structure}''. Type
|
|
274 |
inference takes care to fill in the appropriate record type schemes
|
|
275 |
internally.
|
12099
|
276 |
*}
|
12091
|
277 |
|
12574
|
278 |
locale semigroup =
|
12507
|
279 |
fixes S :: "'a group" (structure)
|
|
280 |
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
|
12099
|
281 |
|
12574
|
282 |
locale group = semigroup G +
|
12507
|
283 |
assumes left_inv: "x\<inv> \<cdot> x = \<one>"
|
12099
|
284 |
and left_one: "\<one> \<cdot> x = x"
|
|
285 |
|
|
286 |
text {*
|
12507
|
287 |
Note that we prefer to call the @{text group} record structure
|
|
288 |
@{text G} rather than @{text S} inherited from @{text semigroup}.
|
|
289 |
This does not affect our concrete syntax, which is only dependent on
|
|
290 |
the \emph{positional} arrangements of currently active structures
|
|
291 |
(actually only one above), rather than names. In fact, these
|
|
292 |
parameter names rarely occur in the term language at all (due to the
|
|
293 |
``indexed syntax'' facility of Isabelle). On the other hand, names
|
|
294 |
of locale facts will get qualified accordingly, e.g. @{text S.assoc}
|
|
295 |
versus @{text G.assoc}.
|
|
296 |
|
12574
|
297 |
\medskip We may now proceed to prove results within @{text group}
|
|
298 |
just as before for @{text group}. The subsequent proof texts are
|
|
299 |
exactly the same as despite the more advanced internal arrangement.
|
12099
|
300 |
*}
|
|
301 |
|
12574
|
302 |
theorem (in group)
|
12099
|
303 |
right_inv: "x \<cdot> x\<inv> = \<one>"
|
|
304 |
proof -
|
|
305 |
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
|
|
306 |
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
|
|
307 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
|
|
308 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
|
|
309 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
|
|
310 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
|
|
311 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
|
|
312 |
also have "\<dots> = \<one>" by (simp only: left_inv)
|
|
313 |
finally show ?thesis .
|
|
314 |
qed
|
|
315 |
|
12574
|
316 |
theorem (in group)
|
12099
|
317 |
right_one: "x \<cdot> \<one> = x"
|
|
318 |
proof -
|
|
319 |
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
|
|
320 |
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
|
|
321 |
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
|
|
322 |
also have "\<dots> = x" by (simp only: left_one)
|
|
323 |
finally show ?thesis .
|
|
324 |
qed
|
|
325 |
|
|
326 |
text {*
|
12574
|
327 |
\medskip Several implicit structures may be active at the same time.
|
|
328 |
The concrete syntax facility for locales actually maintains indexed
|
|
329 |
structures that may be references implicitly --- via mixfix
|
|
330 |
annotations that have been decorated by an ``index argument''
|
|
331 |
(@{text \<index>}).
|
12099
|
332 |
|
12574
|
333 |
The following synthetic example demonstrates how to refer to several
|
|
334 |
structures of type @{text group} succinctly. We work with two
|
|
335 |
versions of the @{text group} locale above.
|
12099
|
336 |
*}
|
12091
|
337 |
|
12574
|
338 |
lemma (uses group G + group H)
|
|
339 |
"x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
|
|
340 |
"x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
|
|
341 |
"x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
|
|
342 |
|
|
343 |
text {*
|
|
344 |
Note that the trivial statements above need to be given as a
|
|
345 |
simultaneous goal in order to have type-inference make the implicit
|
|
346 |
typing of structures @{text G} and @{text H} agree.
|
|
347 |
*}
|
12091
|
348 |
|
12099
|
349 |
end
|