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{\isasymone}{\isamath{1}}


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

12091

30 
*}


31 


32 


33 
subsection {* Local contexts as mathematical structures *}


34 

12099

35 
text {*


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

12105

37 
merely encapsulate local parameters (with private syntax) and

12099

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


39 
shown here.

12075

40 
*}


41 


42 
locale group =


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


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


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


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


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


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


49 


50 
locale abelian_group = group +


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


52 

12099

53 
text {*


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


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


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


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


58 
*}


59 

12075

60 
theorem (in group)


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


62 
proof 


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


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


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


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


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


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


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


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


71 
finally show ?thesis .


72 
qed


73 


74 
theorem (in group)


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


76 
proof 


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


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


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


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


81 
finally show ?thesis .


82 
qed


83 

12099

84 
text {*

12105

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


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


87 
these are discharged when the proof is finished.

12099

88 
*}


89 

12075

90 
theorem (in group)


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


92 
one_equality: "\<one> = e"


93 
proof 


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


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


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


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


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


99 
finally show ?thesis .


100 
qed


101 


102 
theorem (in group)


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


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


105 
proof 


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


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


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


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


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


111 
finally show ?thesis .


112 
qed


113 


114 
theorem (in group)


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


116 
proof (rule inv_equality)


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


118 
proof 


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


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


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


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


123 
finally show ?thesis .


124 
qed


125 
qed


126 

12099

127 
text {*

12105

128 
\medskip Established results are automatically propagated through


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


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


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

12099

132 
*}


133 

12075

134 
theorem (in abelian_group)


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


136 
proof 


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


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


139 
finally show ?thesis .


140 
qed


141 

12099

142 
text {*

12105

143 
\medskip Some further properties of inversion in general group


144 
theory follow.

12099

145 
*}


146 

12075

147 
theorem (in group)


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


149 
proof (rule inv_equality)


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


151 
qed


152 


153 
theorem (in group)


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


155 
inv_inject: "x = y"


156 
proof 


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


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


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


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


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


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


163 
finally show ?thesis .


164 
qed


165 

12099

166 
text {*


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


168 
contexts is rather lightweight and convenient to use for abstract


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


170 
exhibited directly as context parameters; logically this corresponds


171 
to a curried predicate definition. Occasionally, this


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


173 
structures may cause some inconveniences, especially in


174 
metatheoretical studies (involving functors from groups to groups,


175 
for example).

12091

176 

12099

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


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


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


180 
terminology of local parameters is affected the associated syntax


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


182 
*}


183 


184 

12105

185 
subsection {* Explicit structures referenced implicitly *}

12091

186 

12099

187 
text {*


188 
The issue of multiple parameters raised above may be easily


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

12105

190 
instead of the individual constituents. See


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


192 
(extensible) record types in Isabelle/HOL.

12099

193 
*}


194 


195 
record 'a group =

12091

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

12099

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


198 
one :: 'a


199 


200 
text {*


201 
Now concrete syntax essentially needs refer to record selections;


202 
this is possible by giving defined operations with private syntax


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


204 


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


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


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


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

12105

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


210 
mechanism for locales).

12099

211 
*}

12091

212 


213 
syntax

12099

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


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


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

12091

217 
translations

12099

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


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


220 
"\<one>" \<rightleftharpoons> "one \<struct>"


221 


222 
text {*


223 
The following locale definition introduces a single parameter, which

12105

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


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


226 
the present naming.

12099

227 
*}


228 


229 
locale group_struct =


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


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


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


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


234 


235 
text {*

12105

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


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


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


239 
before.

12099

240 
*}


241 


242 
theorem (in group_struct)


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


244 
proof 


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


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


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


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


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


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


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


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


253 
finally show ?thesis .


254 
qed


255 


256 
theorem (in group_struct)


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


258 
proof 


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


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


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


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


263 
finally show ?thesis .


264 
qed


265 


266 
text {*


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


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


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


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


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


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


273 
*}


274 


275 
syntax


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


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


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


279 
translations


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


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


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


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


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


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


286 


287 
text {*


288 
\medskip The following synthetic example demonstrates how to refer


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

12105

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

12099

291 
group_struct} locale above.


292 
*}

12091

293 


294 
lemma

12099

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


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


297 
True


298 
proof


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


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


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


302 
qed

12091

303 

12099

304 
text {*


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


306 
slightly more work to setup abstract and concrete syntax properly


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


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


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


310 
and robust formal representation.


311 
*}

12091

312 

12099

313 
end
