12075
|
1 |
(* Title: HOL/ex/Locales.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, LMU Muenchen
|
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
5 |
*)
|
|
6 |
|
12099
|
7 |
header {* Basic use of locales in Isabelle/Isar *}
|
12075
|
8 |
|
|
9 |
theory Locales = Main:
|
|
10 |
|
12091
|
11 |
text {*
|
12099
|
12 |
Locales provide a mechanism for encapsulating local contexts. While
|
|
13 |
the original version by Florian Kamm\"uller refers to the raw
|
|
14 |
meta-logic, the present one of Isabelle/Isar builds on top of the
|
|
15 |
rich infrastructure of Isar proof contexts. Subsequently, we
|
|
16 |
demonstrate basic use of locales to model mathematical structures
|
|
17 |
(by the inevitable group theory example).
|
|
18 |
*}
|
|
19 |
|
|
20 |
text_raw {*
|
|
21 |
\newcommand{\isasyminv}{\isasyminverse}
|
|
22 |
\newcommand{\isasymone}{\isamath{1}}
|
|
23 |
\newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
|
12091
|
24 |
*}
|
|
25 |
|
|
26 |
|
|
27 |
subsection {* Local contexts as mathematical structures *}
|
|
28 |
|
12099
|
29 |
text {*
|
|
30 |
The following definitions of @{text group} and @{text abelian_group}
|
|
31 |
simply encapsulate local parameters (with private syntax) and
|
|
32 |
assumptions; local definitions may be given as well, but are not
|
|
33 |
shown here.
|
12075
|
34 |
*}
|
|
35 |
|
|
36 |
locale group =
|
|
37 |
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)
|
|
38 |
and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
|
|
39 |
and one :: 'a ("\<one>")
|
|
40 |
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
|
|
41 |
and left_inv: "x\<inv> \<cdot> x = \<one>"
|
|
42 |
and left_one: "\<one> \<cdot> x = x"
|
|
43 |
|
|
44 |
locale abelian_group = group +
|
|
45 |
assumes commute: "x \<cdot> y = y \<cdot> x"
|
|
46 |
|
12099
|
47 |
text {*
|
|
48 |
\medskip We may now prove theorems within a local context, just by
|
|
49 |
including a directive ``@{text "(\<IN> name)"}'' in the goal
|
|
50 |
specification. The final result will be stored within the named
|
|
51 |
locale; a second copy is exported to the enclosing theory context.
|
|
52 |
*}
|
|
53 |
|
12075
|
54 |
theorem (in group)
|
|
55 |
right_inv: "x \<cdot> x\<inv> = \<one>"
|
|
56 |
proof -
|
|
57 |
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
|
|
58 |
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
|
|
59 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
|
|
60 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
|
|
61 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
|
|
62 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
|
|
63 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
|
|
64 |
also have "\<dots> = \<one>" by (simp only: left_inv)
|
|
65 |
finally show ?thesis .
|
|
66 |
qed
|
|
67 |
|
|
68 |
theorem (in group)
|
|
69 |
right_one: "x \<cdot> \<one> = x"
|
|
70 |
proof -
|
|
71 |
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
|
|
72 |
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
|
|
73 |
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
|
|
74 |
also have "\<dots> = x" by (simp only: left_one)
|
|
75 |
finally show ?thesis .
|
|
76 |
qed
|
|
77 |
|
12099
|
78 |
text {*
|
|
79 |
\medskip Apart from the named locale context we may also refer to
|
|
80 |
further ad-hoc elements (parameters, assumptions, etc.); these are
|
|
81 |
discharged when the proof is finished.
|
|
82 |
*}
|
|
83 |
|
12075
|
84 |
theorem (in group)
|
|
85 |
(assumes eq: "e \<cdot> x = x")
|
|
86 |
one_equality: "\<one> = e"
|
|
87 |
proof -
|
|
88 |
have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
|
|
89 |
also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
|
|
90 |
also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
|
|
91 |
also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)
|
|
92 |
also have "\<dots> = e" by (simp only: right_one)
|
|
93 |
finally show ?thesis .
|
|
94 |
qed
|
|
95 |
|
|
96 |
theorem (in group)
|
|
97 |
(assumes eq: "x' \<cdot> x = \<one>")
|
|
98 |
inv_equality: "x\<inv> = x'"
|
|
99 |
proof -
|
|
100 |
have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
|
|
101 |
also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
|
|
102 |
also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)
|
|
103 |
also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)
|
|
104 |
also have "\<dots> = x'" by (simp only: right_one)
|
|
105 |
finally show ?thesis .
|
|
106 |
qed
|
|
107 |
|
|
108 |
theorem (in group)
|
|
109 |
inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"
|
|
110 |
proof (rule inv_equality)
|
|
111 |
show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"
|
|
112 |
proof -
|
|
113 |
have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc)
|
|
114 |
also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)
|
|
115 |
also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)
|
|
116 |
also have "\<dots> = \<one>" by (simp only: left_inv)
|
|
117 |
finally show ?thesis .
|
|
118 |
qed
|
|
119 |
qed
|
|
120 |
|
12099
|
121 |
text {*
|
|
122 |
\medskip Results are automatically propagated through the hierarchy
|
|
123 |
of locales. Below we establish a trivial fact of commutative
|
|
124 |
groups, while referring both to theorems of @{text group} and the
|
|
125 |
characteristic assumption of @{text abelian_group}.
|
|
126 |
*}
|
|
127 |
|
12075
|
128 |
theorem (in abelian_group)
|
|
129 |
inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
|
|
130 |
proof -
|
|
131 |
have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)
|
|
132 |
also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
|
|
133 |
finally show ?thesis .
|
|
134 |
qed
|
|
135 |
|
12099
|
136 |
text {*
|
|
137 |
\medskip Some further facts of general group theory follow.
|
|
138 |
*}
|
|
139 |
|
12075
|
140 |
theorem (in group)
|
|
141 |
inv_inv: "(x\<inv>)\<inv> = x"
|
|
142 |
proof (rule inv_equality)
|
|
143 |
show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)
|
|
144 |
qed
|
|
145 |
|
|
146 |
theorem (in group)
|
|
147 |
(assumes eq: "x\<inv> = y\<inv>")
|
|
148 |
inv_inject: "x = y"
|
|
149 |
proof -
|
|
150 |
have "x = x \<cdot> \<one>" by (simp only: right_one)
|
|
151 |
also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
|
|
152 |
also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)
|
|
153 |
also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)
|
|
154 |
also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)
|
|
155 |
also have "\<dots> = y" by (simp only: left_one)
|
|
156 |
finally show ?thesis .
|
|
157 |
qed
|
|
158 |
|
12099
|
159 |
text {*
|
|
160 |
\bigskip We see that this representation of structures as local
|
|
161 |
contexts is rather light-weight and convenient to use for abstract
|
|
162 |
reasoning. Here the ``components'' (the group operations) have been
|
|
163 |
exhibited directly as context parameters; logically this corresponds
|
|
164 |
to a curried predicate definition. Occasionally, this
|
|
165 |
``externalized'' version of the informal idea of classes of tuple
|
|
166 |
structures may cause some inconveniences, especially in
|
|
167 |
meta-theoretical studies (involving functors from groups to groups,
|
|
168 |
for example).
|
12091
|
169 |
|
12099
|
170 |
Another drawback of the naive approach above is that concrete syntax
|
|
171 |
will get lost on any kind of operation on the locale itself (such as
|
|
172 |
renaming, copying, or instantiation). Whenever the particular
|
|
173 |
terminology of local parameters is affected the associated syntax
|
|
174 |
would have to be changed as well, which is hard to achieve formally.
|
|
175 |
*}
|
|
176 |
|
|
177 |
|
|
178 |
subsection {* Referencing explicit structures implicitly *}
|
12091
|
179 |
|
12099
|
180 |
text {*
|
|
181 |
The issue of multiple parameters raised above may be easily
|
|
182 |
addressed by stating properties over a record of group operations,
|
|
183 |
instead of the individual constituents.
|
|
184 |
*}
|
|
185 |
|
|
186 |
record 'a group =
|
12091
|
187 |
prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
|
12099
|
188 |
inv :: "'a \<Rightarrow> 'a"
|
|
189 |
one :: 'a
|
|
190 |
|
|
191 |
text {*
|
|
192 |
Now concrete syntax essentially needs refer to record selections;
|
|
193 |
this is possible by giving defined operations with private syntax
|
|
194 |
within the locale (e.g.\ see appropriate examples by Kamm\"uller).
|
|
195 |
|
|
196 |
In the subsequent formulation of group structures we go one step
|
|
197 |
further by using \emph{implicit} references to the underlying
|
|
198 |
abstract entity. To this end we define global syntax, which is
|
|
199 |
translated to refer to the ``current'' structure at hand, denoted by
|
|
200 |
the dummy item ``@{text \<struct>}'' according to the builtin syntax
|
|
201 |
mechanism for locales.
|
|
202 |
*}
|
12091
|
203 |
|
|
204 |
syntax
|
12099
|
205 |
"_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)
|
|
206 |
"_inv" :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)
|
|
207 |
"_one" :: 'a ("\<one>")
|
12091
|
208 |
translations
|
12099
|
209 |
"x \<cdot> y" \<rightleftharpoons> "prod \<struct> x y"
|
|
210 |
"x\<inv>" \<rightleftharpoons> "inv \<struct> x"
|
|
211 |
"\<one>" \<rightleftharpoons> "one \<struct>"
|
|
212 |
|
|
213 |
text {*
|
|
214 |
The following locale definition introduces a single parameter, which
|
|
215 |
is declared as ``\isakeyword{structure}''.
|
|
216 |
*}
|
|
217 |
|
|
218 |
locale group_struct =
|
|
219 |
fixes G :: "'a group" (structure)
|
|
220 |
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
|
|
221 |
and left_inv: "x\<inv> \<cdot> x = \<one>"
|
|
222 |
and left_one: "\<one> \<cdot> x = x"
|
|
223 |
|
|
224 |
text {*
|
|
225 |
In its context the dummy ``@{text \<struct>}'' refers to this very
|
|
226 |
parameter, independently of the present naming. We may now proceed
|
|
227 |
to prove results within @{text group_struct} just as before for
|
|
228 |
@{text group}. Proper treatment of ``@{text \<struct>}'' is hidden in
|
|
229 |
concrete syntax, so the proof text is exactly the same as for @{text
|
|
230 |
group} given before.
|
|
231 |
*}
|
|
232 |
|
|
233 |
theorem (in group_struct)
|
|
234 |
right_inv: "x \<cdot> x\<inv> = \<one>"
|
|
235 |
proof -
|
|
236 |
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)
|
|
237 |
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)
|
|
238 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)
|
|
239 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)
|
|
240 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)
|
|
241 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)
|
|
242 |
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)
|
|
243 |
also have "\<dots> = \<one>" by (simp only: left_inv)
|
|
244 |
finally show ?thesis .
|
|
245 |
qed
|
|
246 |
|
|
247 |
theorem (in group_struct)
|
|
248 |
right_one: "x \<cdot> \<one> = x"
|
|
249 |
proof -
|
|
250 |
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)
|
|
251 |
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)
|
|
252 |
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)
|
|
253 |
also have "\<dots> = x" by (simp only: left_one)
|
|
254 |
finally show ?thesis .
|
|
255 |
qed
|
|
256 |
|
|
257 |
text {*
|
|
258 |
\medskip Several implicit structures may be active at the same time
|
|
259 |
(say up to 3 in practice). The concrete syntax facility for locales
|
|
260 |
actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
|
|
261 |
"\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as
|
|
262 |
@{text "\<struct>\<^sub>1"}). So we are able to provide concrete syntax to
|
|
263 |
cover the 2nd and 3rd group structure as well.
|
|
264 |
*}
|
|
265 |
|
|
266 |
syntax
|
|
267 |
"_prod'" :: "'a \<Rightarrow> index \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ \<cdot>_/ _)" [70, 1000, 71] 70)
|
|
268 |
"_inv'" :: "'a \<Rightarrow> index \<Rightarrow> 'a" ("(_\<inv>_)" [1000] 999)
|
|
269 |
"_one'" :: "index \<Rightarrow> 'a" ("\<one>_")
|
|
270 |
translations
|
|
271 |
"x \<cdot>\<^sub>2 y" \<rightleftharpoons> "prod \<struct>\<^sub>2 x y"
|
|
272 |
"x \<cdot>\<^sub>3 y" \<rightleftharpoons> "prod \<struct>\<^sub>3 x y"
|
|
273 |
"x\<inv>\<^sub>2" \<rightleftharpoons> "inv \<struct>\<^sub>2 x"
|
|
274 |
"x\<inv>\<^sub>3" \<rightleftharpoons> "inv \<struct>\<^sub>3 x"
|
|
275 |
"\<one>\<^sub>2" \<rightleftharpoons> "one \<struct>\<^sub>2"
|
|
276 |
"\<one>\<^sub>3" \<rightleftharpoons> "one \<struct>\<^sub>3"
|
|
277 |
|
|
278 |
text {*
|
|
279 |
\medskip The following synthetic example demonstrates how to refer
|
|
280 |
to several structures of type @{text group} succinctly; one might
|
|
281 |
also think of working with renamed versions of the @{text
|
|
282 |
group_struct} locale above.
|
|
283 |
*}
|
12091
|
284 |
|
|
285 |
lemma
|
12099
|
286 |
(fixes G :: "'a group" (structure)
|
|
287 |
and H :: "'a group" (structure))
|
|
288 |
True
|
|
289 |
proof
|
|
290 |
have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..
|
|
291 |
have "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" ..
|
|
292 |
have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
|
|
293 |
qed
|
12091
|
294 |
|
12099
|
295 |
text {*
|
|
296 |
\medskip As a minor drawback of this advanced technique we require
|
|
297 |
slightly more work to setup abstract and concrete syntax properly
|
|
298 |
(but only once in the beginning). The resulting casual mode of
|
|
299 |
writing @{text "x \<cdot> y"} for @{text "prod G x y"} etc.\ mimics common
|
|
300 |
practice of informal mathematics quite nicely, while using a simple
|
|
301 |
and robust formal representation.
|
|
302 |
*}
|
12091
|
303 |
|
12099
|
304 |
end
|