author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12574  ff84d5f14085 
child 12955  f4d60f358cb6 
permissions  rwrr 
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{Kammetal:1999} 
12507  22 
refers directly to the raw metalogic of Isabelle. Semantically, a 
23 
locale is just a (curried) predicate of the pure metalogic 

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:isarref,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 extralogical 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 ``antiquotations'' or generalized deBruijn 

44 
indexes demonstrated in \cite[\S1314]{Wenzel:2001:Isarexamples}). 

12105  45 

12507  46 
Implicit structures work particular well together with extensible 
47 
records in HOL \cite{NaraschewskiWenzel:1998} (the 

48 
``objectoriented'' 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 
simplytyped records we are able to give succinct specifications, 

53 
without caring about signature morphisms ourselves. Further 

54 
eyecandy 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:isarref}) 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 

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) 
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 lightweight 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 
metatheoretical 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 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset

338 
lemma 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset

339 
uses group G + group H 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12574
diff
changeset

340 
shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and 
12574  341 
"x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and 
342 
"x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+ 

343 

344 
text {* 

345 
Note that the trivial statements above need to be given as a 

346 
simultaneous goal in order to have typeinference make the implicit 

347 
typing of structures @{text G} and @{text H} agree. 

348 
*} 

12091  349 

12099  350 
end 