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 {*

12105

12 
Locales provide a mechanism for encapsulating local contexts. The


13 
original version due to Florian Kamm\"uller \cite{Kammetal:1999}


14 
refers directly to the raw metalogic of Isabelle. The present


15 
version for Isabelle/Isar


16 
\cite{Wenzel:1999,Wenzel:2001:isarref,Wenzel:2001:Thesis} builds on


17 
top of the rich infrastructure of proof contexts instead; this also


18 
covers essential extralogical concepts like term abbreviations or


19 
local theorem attributes (e.g.\ declarations of simplification


20 
rules).


21 


22 
Subsequently, we demonstrate basic use of locales to model


23 
mathematical structures (by the inevitable group theory example).

12099

24 
*}


25 


26 
text_raw {*


27 
\newcommand{\isasyminv}{\isasyminverse}


28 
\newcommand{\isasymIN}{\isatext{\isakeyword{in}}}

12091

29 
*}


30 


31 


32 
subsection {* Local contexts as mathematical structures *}


33 

12099

34 
text {*


35 
The following definitions of @{text group} and @{text abelian_group}

12105

36 
merely encapsulate local parameters (with private syntax) and

12099

37 
assumptions; local definitions may be given as well, but are not


38 
shown here.

12075

39 
*}


40 


41 
locale group =


42 
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)


43 
and inv :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)


44 
and one :: 'a ("\<one>")


45 
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"


46 
and left_inv: "x\<inv> \<cdot> x = \<one>"


47 
and left_one: "\<one> \<cdot> x = x"


48 


49 
locale abelian_group = group +


50 
assumes commute: "x \<cdot> y = y \<cdot> x"


51 

12099

52 
text {*


53 
\medskip We may now prove theorems within a local context, just by


54 
including a directive ``@{text "(\<IN> name)"}'' in the goal


55 
specification. The final result will be stored within the named


56 
locale; a second copy is exported to the enclosing theory context.


57 
*}


58 

12075

59 
theorem (in group)


60 
right_inv: "x \<cdot> x\<inv> = \<one>"


61 
proof 


62 
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)


63 
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)


64 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)


65 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)


66 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)


67 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)


68 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)


69 
also have "\<dots> = \<one>" by (simp only: left_inv)


70 
finally show ?thesis .


71 
qed


72 


73 
theorem (in group)


74 
right_one: "x \<cdot> \<one> = x"


75 
proof 


76 
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)


77 
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)


78 
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)


79 
also have "\<dots> = x" by (simp only: left_one)


80 
finally show ?thesis .


81 
qed


82 

12099

83 
text {*

12105

84 
\medskip Apart from the named context we may also refer to further


85 
context elements (parameters, assumptions, etc.) in a casual manner;


86 
these are discharged when the proof is finished.

12099

87 
*}


88 

12075

89 
theorem (in group)


90 
(assumes eq: "e \<cdot> x = x")


91 
one_equality: "\<one> = e"


92 
proof 


93 
have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)


94 
also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)


95 
also have "\<dots> = e \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)


96 
also have "\<dots> = e \<cdot> \<one>" by (simp only: right_inv)


97 
also have "\<dots> = e" by (simp only: right_one)


98 
finally show ?thesis .


99 
qed


100 


101 
theorem (in group)


102 
(assumes eq: "x' \<cdot> x = \<one>")


103 
inv_equality: "x\<inv> = x'"


104 
proof 


105 
have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)


106 
also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)


107 
also have "\<dots> = x' \<cdot> (x \<cdot> x\<inv>)" by (simp only: assoc)


108 
also have "\<dots> = x' \<cdot> \<one>" by (simp only: right_inv)


109 
also have "\<dots> = x'" by (simp only: right_one)


110 
finally show ?thesis .


111 
qed


112 


113 
theorem (in group)


114 
inv_prod: "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>"


115 
proof (rule inv_equality)


116 
show "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = \<one>"


117 
proof 


118 
have "(y\<inv> \<cdot> x\<inv>) \<cdot> (x \<cdot> y) = (y\<inv> \<cdot> (x\<inv> \<cdot> x)) \<cdot> y" by (simp only: assoc)


119 
also have "\<dots> = (y\<inv> \<cdot> \<one>) \<cdot> y" by (simp only: left_inv)


120 
also have "\<dots> = y\<inv> \<cdot> y" by (simp only: right_one)


121 
also have "\<dots> = \<one>" by (simp only: left_inv)


122 
finally show ?thesis .


123 
qed


124 
qed


125 

12099

126 
text {*

12105

127 
\medskip Established results are automatically propagated through


128 
the hierarchy of locales. Below we establish a trivial fact in


129 
commutative groups, while referring both to theorems of @{text


130 
group} and the additional assumption of @{text abelian_group}.

12099

131 
*}


132 

12075

133 
theorem (in abelian_group)


134 
inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"


135 
proof 


136 
have "(x \<cdot> y)\<inv> = y\<inv> \<cdot> x\<inv>" by (rule inv_prod)


137 
also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)


138 
finally show ?thesis .


139 
qed


140 

12099

141 
text {*

12105

142 
\medskip Some further properties of inversion in general group


143 
theory follow.

12099

144 
*}


145 

12075

146 
theorem (in group)


147 
inv_inv: "(x\<inv>)\<inv> = x"


148 
proof (rule inv_equality)


149 
show "x \<cdot> x\<inv> = \<one>" by (simp only: right_inv)


150 
qed


151 


152 
theorem (in group)


153 
(assumes eq: "x\<inv> = y\<inv>")


154 
inv_inject: "x = y"


155 
proof 


156 
have "x = x \<cdot> \<one>" by (simp only: right_one)


157 
also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)


158 
also have "\<dots> = x \<cdot> (x\<inv> \<cdot> y)" by (simp only: eq)


159 
also have "\<dots> = (x \<cdot> x\<inv>) \<cdot> y" by (simp only: assoc)


160 
also have "\<dots> = \<one> \<cdot> y" by (simp only: right_inv)


161 
also have "\<dots> = y" by (simp only: left_one)


162 
finally show ?thesis .


163 
qed


164 

12099

165 
text {*


166 
\bigskip We see that this representation of structures as local


167 
contexts is rather lightweight and convenient to use for abstract


168 
reasoning. Here the ``components'' (the group operations) have been


169 
exhibited directly as context parameters; logically this corresponds


170 
to a curried predicate definition. Occasionally, this


171 
``externalized'' version of the informal idea of classes of tuple


172 
structures may cause some inconveniences, especially in


173 
metatheoretical studies (involving functors from groups to groups,


174 
for example).

12091

175 

12099

176 
Another drawback of the naive approach above is that concrete syntax


177 
will get lost on any kind of operation on the locale itself (such as


178 
renaming, copying, or instantiation). Whenever the particular


179 
terminology of local parameters is affected the associated syntax


180 
would have to be changed as well, which is hard to achieve formally.


181 
*}


182 


183 

12105

184 
subsection {* Explicit structures referenced implicitly *}

12091

185 

12099

186 
text {*


187 
The issue of multiple parameters raised above may be easily


188 
addressed by stating properties over a record of group operations,

12105

189 
instead of the individual constituents. See


190 
\cite{NaraschewskiWenzel:1998,Nipkowetal:2001:HOL} on


191 
(extensible) record types in Isabelle/HOL.

12099

192 
*}


193 


194 
record 'a group =

12091

195 
prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

12099

196 
inv :: "'a \<Rightarrow> 'a"


197 
one :: 'a


198 


199 
text {*


200 
Now concrete syntax essentially needs refer to record selections;


201 
this is possible by giving defined operations with private syntax


202 
within the locale (e.g.\ see appropriate examples by Kamm\"uller).


203 


204 
In the subsequent formulation of group structures we go one step


205 
further by using \emph{implicit} references to the underlying


206 
abstract entity. To this end we define global syntax, which is


207 
translated to refer to the ``current'' structure at hand, denoted by

12105

208 
the dummy item ``@{text \<struct>}'' (according to the builtin syntax


209 
mechanism for locales).

12099

210 
*}

12091

211 


212 
syntax

12099

213 
"_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<cdot>" 70)


214 
"_inv" :: "'a \<Rightarrow> 'a" ("(_\<inv>)" [1000] 999)


215 
"_one" :: 'a ("\<one>")

12091

216 
translations

12099

217 
"x \<cdot> y" \<rightleftharpoons> "prod \<struct> x y"


218 
"x\<inv>" \<rightleftharpoons> "inv \<struct> x"


219 
"\<one>" \<rightleftharpoons> "one \<struct>"


220 


221 
text {*


222 
The following locale definition introduces a single parameter, which

12105

223 
is declared as a ``\isakeyword{structure}''. In its context the


224 
dummy ``@{text \<struct>}'' refers to this very parameter, independently of


225 
the present naming.

12099

226 
*}


227 


228 
locale group_struct =


229 
fixes G :: "'a group" (structure)


230 
assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"


231 
and left_inv: "x\<inv> \<cdot> x = \<one>"


232 
and left_one: "\<one> \<cdot> x = x"


233 


234 
text {*

12105

235 
We may now proceed to prove results within @{text group_struct} just


236 
as before for @{text group}. Proper treatment of ``@{text \<struct>}'' is


237 
hidden in concrete syntax, so the proof text is exactly the same as


238 
before.

12099

239 
*}


240 


241 
theorem (in group_struct)


242 
right_inv: "x \<cdot> x\<inv> = \<one>"


243 
proof 


244 
have "x \<cdot> x\<inv> = \<one> \<cdot> (x \<cdot> x\<inv>)" by (simp only: left_one)


245 
also have "\<dots> = \<one> \<cdot> x \<cdot> x\<inv>" by (simp only: assoc)


246 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv> \<cdot> x \<cdot> x\<inv>" by (simp only: left_inv)


247 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (x\<inv> \<cdot> x) \<cdot> x\<inv>" by (simp only: assoc)


248 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> \<one> \<cdot> x\<inv>" by (simp only: left_inv)


249 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> (\<one> \<cdot> x\<inv>)" by (simp only: assoc)


250 
also have "\<dots> = (x\<inv>)\<inv> \<cdot> x\<inv>" by (simp only: left_one)


251 
also have "\<dots> = \<one>" by (simp only: left_inv)


252 
finally show ?thesis .


253 
qed


254 


255 
theorem (in group_struct)


256 
right_one: "x \<cdot> \<one> = x"


257 
proof 


258 
have "x \<cdot> \<one> = x \<cdot> (x\<inv> \<cdot> x)" by (simp only: left_inv)


259 
also have "\<dots> = x \<cdot> x\<inv> \<cdot> x" by (simp only: assoc)


260 
also have "\<dots> = \<one> \<cdot> x" by (simp only: right_inv)


261 
also have "\<dots> = x" by (simp only: left_one)


262 
finally show ?thesis .


263 
qed


264 


265 
text {*


266 
\medskip Several implicit structures may be active at the same time


267 
(say up to 3 in practice). The concrete syntax facility for locales


268 
actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text


269 
"\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as


270 
@{text "\<struct>\<^sub>1"}). So we are able to provide concrete syntax to


271 
cover the 2nd and 3rd group structure as well.


272 
*}


273 


274 
syntax


275 
"_prod'" :: "'a \<Rightarrow> index \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ \<cdot>_/ _)" [70, 1000, 71] 70)


276 
"_inv'" :: "'a \<Rightarrow> index \<Rightarrow> 'a" ("(_\<inv>_)" [1000] 999)


277 
"_one'" :: "index \<Rightarrow> 'a" ("\<one>_")


278 
translations


279 
"x \<cdot>\<^sub>2 y" \<rightleftharpoons> "prod \<struct>\<^sub>2 x y"


280 
"x \<cdot>\<^sub>3 y" \<rightleftharpoons> "prod \<struct>\<^sub>3 x y"


281 
"x\<inv>\<^sub>2" \<rightleftharpoons> "inv \<struct>\<^sub>2 x"


282 
"x\<inv>\<^sub>3" \<rightleftharpoons> "inv \<struct>\<^sub>3 x"


283 
"\<one>\<^sub>2" \<rightleftharpoons> "one \<struct>\<^sub>2"


284 
"\<one>\<^sub>3" \<rightleftharpoons> "one \<struct>\<^sub>3"


285 


286 
text {*


287 
\medskip The following synthetic example demonstrates how to refer


288 
to several structures of type @{text group} succinctly; one might

12105

289 
also think of working with several renamed versions of the @{text

12099

290 
group_struct} locale above.


291 
*}

12091

292 


293 
lemma

12099

294 
(fixes G :: "'a group" (structure)


295 
and H :: "'a group" (structure))


296 
True


297 
proof


298 
have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..


299 
have "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" ..


300 
have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..


301 
qed

12091

302 

12099

303 
text {*


304 
\medskip As a minor drawback of this advanced technique we require


305 
slightly more work to setup abstract and concrete syntax properly


306 
(but only once in the beginning). The resulting casual mode of


307 
writing @{text "x \<cdot> y"} for @{text "prod G x y"} etc.\ mimics common


308 
practice of informal mathematics quite nicely, while using a simple


309 
and robust formal representation.


310 
*}

12091

311 

12099

312 
end
