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 

12091

7 
header {* Basic use of locales *}

12075

8 


9 
theory Locales = Main:


10 

12091

11 
text {*


12 
The inevitable group theory examples formulated with locales.


13 
*}


14 


15 


16 
subsection {* Local contexts as mathematical structures *}


17 

12075

18 
text_raw {*


19 
\newcommand{\isasyminv}{\isasyminverse}


20 
\newcommand{\isasymone}{\isamath{1}}


21 
*}


22 


23 
locale group =


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


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


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


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


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


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


30 


31 
locale abelian_group = group +


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


33 


34 
theorem (in group)


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


36 
proof 


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


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


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


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


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


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


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


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


45 
finally show ?thesis .


46 
qed


47 


48 
theorem (in group)


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


50 
proof 


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


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


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


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


55 
finally show ?thesis .


56 
qed


57 


58 
theorem (in group)


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


60 
one_equality: "\<one> = e"


61 
proof 


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


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


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


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


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


67 
finally show ?thesis .


68 
qed


69 


70 
theorem (in group)


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


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


73 
proof 


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


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


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


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


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


79 
finally show ?thesis .


80 
qed


81 


82 
theorem (in group)


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


84 
proof (rule inv_equality)


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


86 
proof 


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


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


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


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


91 
finally show ?thesis .


92 
qed


93 
qed


94 


95 
theorem (in abelian_group)


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


97 
proof 


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


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


100 
finally show ?thesis .


101 
qed


102 


103 
theorem (in group)


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


105 
proof (rule inv_equality)


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


107 
qed


108 


109 
theorem (in group)


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


111 
inv_inject: "x = y"


112 
proof 


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


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


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


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


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


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


119 
finally show ?thesis .


120 
qed


121 

12091

122 


123 
subsection {* Referencing structures implicitly *}


124 


125 
record 'a semigroup =


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


127 


128 
syntax


129 
"_prod1" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)


130 
"_prod2" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>2" 70)


131 
"_prod3" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>\<^sub>3" 70)


132 
translations


133 
"x \<odot> y" \<rightleftharpoons> "(\<struct>prod) x y"


134 
"x \<odot>\<^sub>2 y" \<rightleftharpoons> "(\<struct>\<struct>prod) x y"


135 
"x \<odot>\<^sub>3 y" \<rightleftharpoons> "(\<struct>\<struct>\<struct>prod) x y"


136 


137 
lemma


138 
(fixes S :: "'a semigroup" (structure)


139 
and T :: "'a semigroup" (structure)


140 
and U :: "'a semigroup" (structure))


141 
"prod S a b = a \<odot> b" ..


142 


143 
lemma


144 
(fixes S :: "'a semigroup" (structure)


145 
and T :: "'a semigroup" (structure)


146 
and U :: "'a semigroup" (structure))


147 
"prod T a b = a \<odot>\<^sub>2 b" ..


148 


149 
lemma


150 
(fixes S :: "'a semigroup" (structure)


151 
and T :: "'a semigroup" (structure)


152 
and U :: "'a semigroup" (structure))


153 
"prod U a b = a \<odot>\<^sub>3 b" ..


154 


155 
end 