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 
metalogic, 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 adhoc 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 lightweight 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 
metatheoretical 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
