author  ballarin 
Mon, 16 Oct 2006 10:27:54 +0200  
changeset 21041  60e418260b4d 
parent 20318  0e0ea63fe768 
child 22063  717425609192 
permissions  rwrr 
13813  1 
(* 
2 
Title: HOL/Algebra/Group.thy 

3 
Id: $Id$ 

4 
Author: Clemens Ballarin, started 4 February 2003 

5 

6 
Based on work by Florian Kammueller, L C Paulson and Markus Wenzel. 

7 
*) 

8 

16417  9 
theory Group imports FuncSet Lattice begin 
13813  10 

14761  11 

14963  12 
section {* Monoids and Groups *} 
13936  13 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

14 
subsection {* Definitions *} 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

15 

13813  16 
text {* 
14963  17 
Definitions follow \cite{Jacobson:1985}. 
13813  18 
*} 
19 

14963  20 
record 'a monoid = "'a partial_object" + 
21 
mult :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70) 

22 
one :: 'a ("\<one>\<index>") 

13817  23 

14651  24 
constdefs (structure G) 
14852  25 
m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80) 
14651  26 
"inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)" 
13936  27 

14651  28 
Units :: "_ => 'a set" 
14852  29 
{*The set of invertible elements*} 
14963  30 
"Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}" 
13936  31 

32 
consts 

33 
pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75) 

34 

19699  35 
defs (overloaded) 
14693  36 
nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n" 
13936  37 
int_pow_def: "pow G a z == 
14693  38 
let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) 
39 
in if neg z then inv\<^bsub>G\<^esub> (p (nat (z))) else p (nat z)" 

13813  40 

19783  41 
locale monoid = 
42 
fixes G (structure) 

13813  43 
assumes m_closed [intro, simp]: 
14963  44 
"\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> carrier G" 
45 
and m_assoc: 

46 
"\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> 

47 
\<Longrightarrow> (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 

48 
and one_closed [intro, simp]: "\<one> \<in> carrier G" 

49 
and l_one [simp]: "x \<in> carrier G \<Longrightarrow> \<one> \<otimes> x = x" 

50 
and r_one [simp]: "x \<in> carrier G \<Longrightarrow> x \<otimes> \<one> = x" 

13817  51 

13936  52 
lemma monoidI: 
19783  53 
fixes G (structure) 
13936  54 
assumes m_closed: 
14693  55 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y \<in> carrier G" 
56 
and one_closed: "\<one> \<in> carrier G" 

13936  57 
and m_assoc: 
58 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

14693  59 
(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 
60 
and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" 

61 
and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x" 

13936  62 
shows "monoid G" 
14963  63 
by (fast intro!: monoid.intro intro: prems) 
13936  64 

65 
lemma (in monoid) Units_closed [dest]: 

66 
"x \<in> Units G ==> x \<in> carrier G" 

67 
by (unfold Units_def) fast 

68 

69 
lemma (in monoid) inv_unique: 

14693  70 
assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>" 
71 
and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" 

13936  72 
shows "y = y'" 
73 
proof  

74 
from G eq have "y = y \<otimes> (x \<otimes> y')" by simp 

75 
also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc) 

76 
also from G eq have "... = y'" by simp 

77 
finally show ?thesis . 

78 
qed 

79 

13940  80 
lemma (in monoid) Units_one_closed [intro, simp]: 
81 
"\<one> \<in> Units G" 

82 
by (unfold Units_def) auto 

83 

13936  84 
lemma (in monoid) Units_inv_closed [intro, simp]: 
85 
"x \<in> Units G ==> inv x \<in> carrier G" 

13943  86 
apply (unfold Units_def m_inv_def, auto) 
13936  87 
apply (rule theI2, fast) 
13943  88 
apply (fast intro: inv_unique, fast) 
13936  89 
done 
90 

19981  91 
lemma (in monoid) Units_l_inv_ex: 
92 
"x \<in> Units G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" 

93 
by (unfold Units_def) auto 

94 

95 
lemma (in monoid) Units_r_inv_ex: 

96 
"x \<in> Units G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>" 

97 
by (unfold Units_def) auto 

98 

13936  99 
lemma (in monoid) Units_l_inv: 
100 
"x \<in> Units G ==> inv x \<otimes> x = \<one>" 

13943  101 
apply (unfold Units_def m_inv_def, auto) 
13936  102 
apply (rule theI2, fast) 
13943  103 
apply (fast intro: inv_unique, fast) 
13936  104 
done 
105 

106 
lemma (in monoid) Units_r_inv: 

107 
"x \<in> Units G ==> x \<otimes> inv x = \<one>" 

13943  108 
apply (unfold Units_def m_inv_def, auto) 
13936  109 
apply (rule theI2, fast) 
13943  110 
apply (fast intro: inv_unique, fast) 
13936  111 
done 
112 

113 
lemma (in monoid) Units_inv_Units [intro, simp]: 

114 
"x \<in> Units G ==> inv x \<in> Units G" 

115 
proof  

116 
assume x: "x \<in> Units G" 

117 
show "inv x \<in> Units G" 

118 
by (auto simp add: Units_def 

119 
intro: Units_l_inv Units_r_inv x Units_closed [OF x]) 

120 
qed 

121 

122 
lemma (in monoid) Units_l_cancel [simp]: 

123 
"[ x \<in> Units G; y \<in> carrier G; z \<in> carrier G ] ==> 

124 
(x \<otimes> y = x \<otimes> z) = (y = z)" 

125 
proof 

126 
assume eq: "x \<otimes> y = x \<otimes> z" 

14693  127 
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" 
13936  128 
then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" 
129 
by (simp add: m_assoc Units_closed) 

130 
with G show "y = z" by (simp add: Units_l_inv) 

131 
next 

132 
assume eq: "y = z" 

14693  133 
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" 
13936  134 
then show "x \<otimes> y = x \<otimes> z" by simp 
135 
qed 

136 

137 
lemma (in monoid) Units_inv_inv [simp]: 

138 
"x \<in> Units G ==> inv (inv x) = x" 

139 
proof  

140 
assume x: "x \<in> Units G" 

141 
then have "inv x \<otimes> inv (inv x) = inv x \<otimes> x" 

142 
by (simp add: Units_l_inv Units_r_inv) 

143 
with x show ?thesis by (simp add: Units_closed) 

144 
qed 

145 

146 
lemma (in monoid) inv_inj_on_Units: 

147 
"inj_on (m_inv G) (Units G)" 

148 
proof (rule inj_onI) 

149 
fix x y 

14693  150 
assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y" 
13936  151 
then have "inv (inv x) = inv (inv y)" by simp 
152 
with G show "x = y" by simp 

153 
qed 

154 

13940  155 
lemma (in monoid) Units_inv_comm: 
156 
assumes inv: "x \<otimes> y = \<one>" 

14693  157 
and G: "x \<in> Units G" "y \<in> Units G" 
13940  158 
shows "y \<otimes> x = \<one>" 
159 
proof  

160 
from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed) 

161 
with G show ?thesis by (simp del: r_one add: m_assoc Units_closed) 

162 
qed 

163 

13936  164 
text {* Power *} 
165 

166 
lemma (in monoid) nat_pow_closed [intro, simp]: 

167 
"x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G" 

168 
by (induct n) (simp_all add: nat_pow_def) 

169 

170 
lemma (in monoid) nat_pow_0 [simp]: 

171 
"x (^) (0::nat) = \<one>" 

172 
by (simp add: nat_pow_def) 

173 

174 
lemma (in monoid) nat_pow_Suc [simp]: 

175 
"x (^) (Suc n) = x (^) n \<otimes> x" 

176 
by (simp add: nat_pow_def) 

177 

178 
lemma (in monoid) nat_pow_one [simp]: 

179 
"\<one> (^) (n::nat) = \<one>" 

180 
by (induct n) simp_all 

181 

182 
lemma (in monoid) nat_pow_mult: 

183 
"x \<in> carrier G ==> x (^) (n::nat) \<otimes> x (^) m = x (^) (n + m)" 

184 
by (induct m) (simp_all add: m_assoc [THEN sym]) 

185 

186 
lemma (in monoid) nat_pow_pow: 

187 
"x \<in> carrier G ==> (x (^) n) (^) m = x (^) (n * m::nat)" 

188 
by (induct m) (simp, simp add: nat_pow_mult add_commute) 

189 

190 
text {* 

191 
A group is a monoid all of whose elements are invertible. 

192 
*} 

193 

194 
locale group = monoid + 

195 
assumes Units: "carrier G <= Units G" 

196 

14761  197 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

198 
lemma (in group) is_group: "group G" . 
14761  199 

13936  200 
theorem groupI: 
19783  201 
fixes G (structure) 
13936  202 
assumes m_closed [simp]: 
14693  203 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y \<in> carrier G" 
204 
and one_closed [simp]: "\<one> \<in> carrier G" 

13936  205 
and m_assoc: 
206 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

14693  207 
(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 
208 
and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" 

14963  209 
and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" 
13936  210 
shows "group G" 
211 
proof  

212 
have l_cancel [simp]: 

213 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

14693  214 
(x \<otimes> y = x \<otimes> z) = (y = z)" 
13936  215 
proof 
216 
fix x y z 

14693  217 
assume eq: "x \<otimes> y = x \<otimes> z" 
218 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 

13936  219 
with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" 
14693  220 
and l_inv: "x_inv \<otimes> x = \<one>" by fast 
221 
from G eq xG have "(x_inv \<otimes> x) \<otimes> y = (x_inv \<otimes> x) \<otimes> z" 

13936  222 
by (simp add: m_assoc) 
223 
with G show "y = z" by (simp add: l_inv) 

224 
next 

225 
fix x y z 

226 
assume eq: "y = z" 

14693  227 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 
228 
then show "x \<otimes> y = x \<otimes> z" by simp 

13936  229 
qed 
230 
have r_one: 

14693  231 
"!!x. x \<in> carrier G ==> x \<otimes> \<one> = x" 
13936  232 
proof  
233 
fix x 

234 
assume x: "x \<in> carrier G" 

235 
with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" 

14693  236 
and l_inv: "x_inv \<otimes> x = \<one>" by fast 
237 
from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x" 

13936  238 
by (simp add: m_assoc [symmetric] l_inv) 
14693  239 
with x xG show "x \<otimes> \<one> = x" by simp 
13936  240 
qed 
241 
have inv_ex: 

14963  242 
"!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>" 
13936  243 
proof  
244 
fix x 

245 
assume x: "x \<in> carrier G" 

246 
with l_inv_ex obtain y where y: "y \<in> carrier G" 

14693  247 
and l_inv: "y \<otimes> x = \<one>" by fast 
248 
from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>" 

13936  249 
by (simp add: m_assoc [symmetric] l_inv r_one) 
14693  250 
with x y have r_inv: "x \<otimes> y = \<one>" 
13936  251 
by simp 
14963  252 
from x y show "\<exists>y \<in> carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>" 
13936  253 
by (fast intro: l_inv r_inv) 
254 
qed 

255 
then have carrier_subset_Units: "carrier G <= Units G" 

256 
by (unfold Units_def) fast 

257 
show ?thesis 

14963  258 
by (fast intro!: group.intro monoid.intro group_axioms.intro 
13936  259 
carrier_subset_Units intro: prems r_one) 
260 
qed 

261 

262 
lemma (in monoid) monoid_groupI: 

263 
assumes l_inv_ex: 

14963  264 
"!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" 
13936  265 
shows "group G" 
266 
by (rule groupI) (auto intro: m_assoc l_inv_ex) 

267 

268 
lemma (in group) Units_eq [simp]: 

269 
"Units G = carrier G" 

270 
proof 

271 
show "Units G <= carrier G" by fast 

272 
next 

273 
show "carrier G <= Units G" by (rule Units) 

274 
qed 

275 

276 
lemma (in group) inv_closed [intro, simp]: 

277 
"x \<in> carrier G ==> inv x \<in> carrier G" 

278 
using Units_inv_closed by simp 

279 

19981  280 
lemma (in group) l_inv_ex [simp]: 
281 
"x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" 

282 
using Units_l_inv_ex by simp 

283 

284 
lemma (in group) r_inv_ex [simp]: 

285 
"x \<in> carrier G ==> \<exists>y \<in> carrier G. x \<otimes> y = \<one>" 

286 
using Units_r_inv_ex by simp 

287 

14963  288 
lemma (in group) l_inv [simp]: 
13936  289 
"x \<in> carrier G ==> inv x \<otimes> x = \<one>" 
290 
using Units_l_inv by simp 

13813  291 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

292 

13813  293 
subsection {* Cancellation Laws and Basic Properties *} 
294 

295 
lemma (in group) l_cancel [simp]: 

296 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

297 
(x \<otimes> y = x \<otimes> z) = (y = z)" 

13936  298 
using Units_l_inv by simp 
13940  299 

14963  300 
lemma (in group) r_inv [simp]: 
13813  301 
"x \<in> carrier G ==> x \<otimes> inv x = \<one>" 
302 
proof  

303 
assume x: "x \<in> carrier G" 

304 
then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>" 

305 
by (simp add: m_assoc [symmetric] l_inv) 

306 
with x show ?thesis by (simp del: r_one) 

307 
qed 

308 

309 
lemma (in group) r_cancel [simp]: 

310 
"[ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

311 
(y \<otimes> x = z \<otimes> x) = (y = z)" 

312 
proof 

313 
assume eq: "y \<otimes> x = z \<otimes> x" 

14693  314 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 
13813  315 
then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)" 
14963  316 
by (simp add: m_assoc [symmetric] del: r_inv) 
317 
with G show "y = z" by simp 

13813  318 
next 
319 
assume eq: "y = z" 

14693  320 
and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 
13813  321 
then show "y \<otimes> x = z \<otimes> x" by simp 
322 
qed 

323 

13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

324 
lemma (in group) inv_one [simp]: 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

325 
"inv \<one> = \<one>" 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

326 
proof  
14963  327 
have "inv \<one> = \<one> \<otimes> (inv \<one>)" by (simp del: r_inv) 
328 
moreover have "... = \<one>" by simp 

13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

329 
finally show ?thesis . 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

330 
qed 
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

331 

13813  332 
lemma (in group) inv_inv [simp]: 
333 
"x \<in> carrier G ==> inv (inv x) = x" 

13936  334 
using Units_inv_inv by simp 
335 

336 
lemma (in group) inv_inj: 

337 
"inj_on (m_inv G) (carrier G)" 

338 
using inv_inj_on_Units by simp 

13813  339 

13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

340 
lemma (in group) inv_mult_group: 
13813  341 
"[ x \<in> carrier G; y \<in> carrier G ] ==> inv (x \<otimes> y) = inv y \<otimes> inv x" 
342 
proof  

14693  343 
assume G: "x \<in> carrier G" "y \<in> carrier G" 
13813  344 
then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)" 
14963  345 
by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric]) 
346 
with G show ?thesis by (simp del: l_inv) 

13813  347 
qed 
348 

13940  349 
lemma (in group) inv_comm: 
350 
"[ x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G ] ==> y \<otimes> x = \<one>" 

14693  351 
by (rule Units_inv_comm) auto 
13940  352 

13944  353 
lemma (in group) inv_equality: 
13943  354 
"[y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G] ==> inv x = y" 
355 
apply (simp add: m_inv_def) 

356 
apply (rule the_equality) 

14693  357 
apply (simp add: inv_comm [of y x]) 
358 
apply (rule r_cancel [THEN iffD1], auto) 

13943  359 
done 
360 

13936  361 
text {* Power *} 
362 

363 
lemma (in group) int_pow_def2: 

364 
"a (^) (z::int) = (if neg z then inv (a (^) (nat (z))) else a (^) (nat z))" 

365 
by (simp add: int_pow_def nat_pow_def Let_def) 

366 

367 
lemma (in group) int_pow_0 [simp]: 

368 
"x (^) (0::int) = \<one>" 

369 
by (simp add: int_pow_def2) 

370 

371 
lemma (in group) int_pow_one [simp]: 

372 
"\<one> (^) (z::int) = \<one>" 

373 
by (simp add: int_pow_def2) 

374 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

375 

14963  376 
subsection {* Subgroups *} 
13813  377 

19783  378 
locale subgroup = 
379 
fixes H and G (structure) 

14963  380 
assumes subset: "H \<subseteq> carrier G" 
381 
and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H" 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

382 
and one_closed [simp]: "\<one> \<in> H" 
14963  383 
and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H" 
13813  384 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

385 
lemma (in subgroup) is_subgroup: 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

386 
"subgroup H G" . 
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

387 

13813  388 
declare (in subgroup) group.intro [intro] 
13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

389 

14963  390 
lemma (in subgroup) mem_carrier [simp]: 
391 
"x \<in> H \<Longrightarrow> x \<in> carrier G" 

392 
using subset by blast 

13813  393 

14963  394 
lemma subgroup_imp_subset: 
395 
"subgroup H G \<Longrightarrow> H \<subseteq> carrier G" 

396 
by (rule subgroup.subset) 

397 

398 
lemma (in subgroup) subgroup_is_group [intro]: 

13813  399 
includes group G 
14963  400 
shows "group (G\<lparr>carrier := H\<rparr>)" 
401 
by (rule groupI) (auto intro: m_assoc l_inv mem_carrier) 

13813  402 

403 
text {* 

404 
Since @{term H} is nonempty, it contains some element @{term x}. Since 

405 
it is closed under inverse, it contains @{text "inv x"}. Since 

406 
it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}. 

407 
*} 

408 

409 
lemma (in group) one_in_subset: 

410 
"[ H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H ] 

411 
==> \<one> \<in> H" 

412 
by (force simp add: l_inv) 

413 

414 
text {* A characterization of subgroups: closed, nonempty subset. *} 

415 

416 
lemma (in group) subgroupI: 

417 
assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}" 

14963  418 
and inv: "!!a. a \<in> H \<Longrightarrow> inv a \<in> H" 
419 
and mult: "!!a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H" 

13813  420 
shows "subgroup H G" 
14963  421 
proof (simp add: subgroup_def prems) 
422 
show "\<one> \<in> H" by (rule one_in_subset) (auto simp only: prems) 

13813  423 
qed 
424 

13936  425 
declare monoid.one_closed [iff] group.inv_closed [simp] 
426 
monoid.l_one [simp] monoid.r_one [simp] group.inv_inv [simp] 

13813  427 

428 
lemma subgroup_nonempty: 

429 
"~ subgroup {} G" 

430 
by (blast dest: subgroup.one_closed) 

431 

432 
lemma (in subgroup) finite_imp_card_positive: 

433 
"finite (carrier G) ==> 0 < card H" 

434 
proof (rule classical) 

14963  435 
assume "finite (carrier G)" "~ 0 < card H" 
436 
then have "finite H" by (blast intro: finite_subset [OF subset]) 

437 
with prems have "subgroup {} G" by simp 

13813  438 
with subgroup_nonempty show ?thesis by contradiction 
439 
qed 

440 

13936  441 
(* 
442 
lemma (in monoid) Units_subgroup: 

443 
"subgroup (Units G) G" 

444 
*) 

445 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

446 

13813  447 
subsection {* Direct Products *} 
448 

14963  449 
constdefs 
450 
DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) 

451 
"G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H, 

452 
mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')), 

453 
one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>" 

13813  454 

14963  455 
lemma DirProd_monoid: 
456 
includes monoid G + monoid H 

457 
shows "monoid (G \<times>\<times> H)" 

458 
proof  

459 
from prems 

460 
show ?thesis by (unfold monoid_def DirProd_def, auto) 

461 
qed 

13813  462 

463 

14963  464 
text{*Does not use the previous result because it's easier just to use auto.*} 
465 
lemma DirProd_group: 

13813  466 
includes group G + group H 
14963  467 
shows "group (G \<times>\<times> H)" 
13936  468 
by (rule groupI) 
14963  469 
(auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv 
470 
simp add: DirProd_def) 

13813  471 

14963  472 
lemma carrier_DirProd [simp]: 
473 
"carrier (G \<times>\<times> H) = carrier G \<times> carrier H" 

474 
by (simp add: DirProd_def) 

13944  475 

14963  476 
lemma one_DirProd [simp]: 
477 
"\<one>\<^bsub>G \<times>\<times> H\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)" 

478 
by (simp add: DirProd_def) 

13944  479 

14963  480 
lemma mult_DirProd [simp]: 
481 
"(g, h) \<otimes>\<^bsub>(G \<times>\<times> H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')" 

482 
by (simp add: DirProd_def) 

13944  483 

14963  484 
lemma inv_DirProd [simp]: 
13944  485 
includes group G + group H 
486 
assumes g: "g \<in> carrier G" 

487 
and h: "h \<in> carrier H" 

14963  488 
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)" 
489 
apply (rule group.inv_equality [OF DirProd_group]) 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

490 
apply (simp_all add: prems group.l_inv) 
13944  491 
done 
492 

15696  493 
text{*This alternative proof of the previous result demonstrates interpret. 
15763
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15696
diff
changeset

494 
It uses @{text Prod.inv_equality} (available after @{text interpret}) 
b901a127ac73
Interpretation supports statically scoped attributes; documentation.
ballarin
parents:
15696
diff
changeset

495 
instead of @{text "group.inv_equality [OF DirProd_group]"}. *} 
14963  496 
lemma 
497 
includes group G + group H 

498 
assumes g: "g \<in> carrier G" 

499 
and h: "h \<in> carrier H" 

500 
shows "m_inv (G \<times>\<times> H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)" 

501 
proof  

15696  502 
interpret Prod: group ["G \<times>\<times> H"] 
503 
by (auto intro: DirProd_group group.intro group.axioms prems) 

14963  504 
show ?thesis by (simp add: Prod.inv_equality g h) 
505 
qed 

506 

507 

508 
subsection {* Homomorphisms and Isomorphisms *} 

13813  509 

14651  510 
constdefs (structure G and H) 
511 
hom :: "_ => _ => ('a => 'b) set" 

13813  512 
"hom G H == 
513 
{h. h \<in> carrier G > carrier H & 

14693  514 
(\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}" 
13813  515 

516 
lemma hom_mult: 

14693  517 
"[ h \<in> hom G H; x \<in> carrier G; y \<in> carrier G ] 
518 
==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y" 

519 
by (simp add: hom_def) 

13813  520 

521 
lemma hom_closed: 

522 
"[ h \<in> hom G H; x \<in> carrier G ] ==> h x \<in> carrier H" 

523 
by (auto simp add: hom_def funcset_mem) 

524 

14761  525 
lemma (in group) hom_compose: 
526 
"[h \<in> hom G H; i \<in> hom H I] ==> compose (carrier G) i h \<in> hom G I" 

527 
apply (auto simp add: hom_def funcset_compose) 

528 
apply (simp add: compose_def funcset_mem) 

13943  529 
done 
530 

14803  531 
constdefs 
532 
iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) 

533 
"G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}" 

14761  534 

14803  535 
lemma iso_refl: "(%x. x) \<in> G \<cong> G" 
14761  536 
by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
537 

538 
lemma (in group) iso_sym: 

14803  539 
"h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G" 
14761  540 
apply (simp add: iso_def bij_betw_Inv) 
541 
apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G") 

542 
prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv]) 

543 
apply (simp add: hom_def bij_betw_def Inv_f_eq funcset_mem f_Inv_f) 

544 
done 

545 

546 
lemma (in group) iso_trans: 

14803  547 
"[h \<in> G \<cong> H; i \<in> H \<cong> I] ==> (compose (carrier G) i h) \<in> G \<cong> I" 
14761  548 
by (auto simp add: iso_def hom_compose bij_betw_compose) 
549 

14963  550 
lemma DirProd_commute_iso: 
551 
shows "(\<lambda>(x,y). (y,x)) \<in> (G \<times>\<times> H) \<cong> (H \<times>\<times> G)" 

14761  552 
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
553 

14963  554 
lemma DirProd_assoc_iso: 
555 
shows "(\<lambda>(x,y,z). (x,(y,z))) \<in> (G \<times>\<times> H \<times>\<times> I) \<cong> (G \<times>\<times> (H \<times>\<times> I))" 

14761  556 
by (auto simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def) 
557 

558 

14963  559 
text{*Basis for homomorphism proofs: we assume two groups @{term G} and 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14963
diff
changeset

560 
@{term H}, with a homomorphism @{term h} between them*} 
13813  561 
locale group_hom = group G + group H + var h + 
562 
assumes homh: "h \<in> hom G H" 

563 
notes hom_mult [simp] = hom_mult [OF homh] 

564 
and hom_closed [simp] = hom_closed [OF homh] 

565 

566 
lemma (in group_hom) one_closed [simp]: 

567 
"h \<one> \<in> carrier H" 

568 
by simp 

569 

570 
lemma (in group_hom) hom_one [simp]: 

14693  571 
"h \<one> = \<one>\<^bsub>H\<^esub>" 
13813  572 
proof  
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14963
diff
changeset

573 
have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^bsub>H\<^esub> h \<one>" 
13813  574 
by (simp add: hom_mult [symmetric] del: hom_mult) 
575 
then show ?thesis by (simp del: r_one) 

576 
qed 

577 

578 
lemma (in group_hom) inv_closed [simp]: 

579 
"x \<in> carrier G ==> h (inv x) \<in> carrier H" 

580 
by simp 

581 

582 
lemma (in group_hom) hom_inv [simp]: 

14693  583 
"x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)" 
13813  584 
proof  
585 
assume x: "x \<in> carrier G" 

14693  586 
then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>" 
14963  587 
by (simp add: hom_mult [symmetric] del: hom_mult) 
14693  588 
also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" 
14963  589 
by (simp add: hom_mult [symmetric] del: hom_mult) 
14693  590 
finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" . 
14963  591 
with x show ?thesis by (simp del: H.r_inv) 
13813  592 
qed 
593 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

594 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13944
diff
changeset

595 
subsection {* Commutative Structures *} 
13936  596 

597 
text {* 

598 
Naming convention: multiplicative structures that are commutative 

599 
are called \emph{commutative}, additive structures are called 

600 
\emph{Abelian}. 

601 
*} 

13813  602 

14963  603 
locale comm_monoid = monoid + 
604 
assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x" 

13813  605 

14963  606 
lemma (in comm_monoid) m_lcomm: 
607 
"\<lbrakk>x \<in> carrier G; y \<in> carrier G; z \<in> carrier G\<rbrakk> \<Longrightarrow> 

13813  608 
x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)" 
609 
proof  

14693  610 
assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 
13813  611 
from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc) 
612 
also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm) 

613 
also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc) 

614 
finally show ?thesis . 

615 
qed 

616 

14963  617 
lemmas (in comm_monoid) m_ac = m_assoc m_comm m_lcomm 
13813  618 

13936  619 
lemma comm_monoidI: 
19783  620 
fixes G (structure) 
13936  621 
assumes m_closed: 
14693  622 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y \<in> carrier G" 
623 
and one_closed: "\<one> \<in> carrier G" 

13936  624 
and m_assoc: 
625 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

14693  626 
(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 
627 
and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" 

13936  628 
and m_comm: 
14693  629 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y = y \<otimes> x" 
13936  630 
shows "comm_monoid G" 
631 
using l_one 

14963  632 
by (auto intro!: comm_monoid.intro comm_monoid_axioms.intro monoid.intro 
633 
intro: prems simp: m_closed one_closed m_comm) 

13817  634 

13936  635 
lemma (in monoid) monoid_comm_monoidI: 
636 
assumes m_comm: 

14693  637 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y = y \<otimes> x" 
13936  638 
shows "comm_monoid G" 
639 
by (rule comm_monoidI) (auto intro: m_assoc m_comm) 

14963  640 

14693  641 
(*lemma (in comm_monoid) r_one [simp]: 
13817  642 
"x \<in> carrier G ==> x \<otimes> \<one> = x" 
643 
proof  

644 
assume G: "x \<in> carrier G" 

645 
then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm) 

646 
also from G have "... = x" by simp 

647 
finally show ?thesis . 

14693  648 
qed*) 
14963  649 

13936  650 
lemma (in comm_monoid) nat_pow_distr: 
651 
"[ x \<in> carrier G; y \<in> carrier G ] ==> 

652 
(x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n" 

653 
by (induct n) (simp, simp add: m_ac) 

654 

655 
locale comm_group = comm_monoid + group 

656 

657 
lemma (in group) group_comm_groupI: 

658 
assumes m_comm: "!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> 

14693  659 
x \<otimes> y = y \<otimes> x" 
13936  660 
shows "comm_group G" 
19984
29bb4659f80a
Method intro_locales replaced by intro_locales and unfold_locales.
ballarin
parents:
19981
diff
changeset

661 
by unfold_locales (simp_all add: m_comm) 
13817  662 

13936  663 
lemma comm_groupI: 
19783  664 
fixes G (structure) 
13936  665 
assumes m_closed: 
14693  666 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y \<in> carrier G" 
667 
and one_closed: "\<one> \<in> carrier G" 

13936  668 
and m_assoc: 
669 
"!!x y z. [ x \<in> carrier G; y \<in> carrier G; z \<in> carrier G ] ==> 

14693  670 
(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" 
13936  671 
and m_comm: 
14693  672 
"!!x y. [ x \<in> carrier G; y \<in> carrier G ] ==> x \<otimes> y = y \<otimes> x" 
673 
and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" 

14963  674 
and l_inv_ex: "!!x. x \<in> carrier G ==> \<exists>y \<in> carrier G. y \<otimes> x = \<one>" 
13936  675 
shows "comm_group G" 
676 
by (fast intro: group.group_comm_groupI groupI prems) 

677 

678 
lemma (in comm_group) inv_mult: 

13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

679 
"[ x \<in> carrier G; y \<in> carrier G ] ==> inv (x \<otimes> y) = inv x \<otimes> inv y" 
13936  680 
by (simp add: m_ac inv_mult_group) 
13854
91c9ab25fece
First distributed version of Group and Ring theory.
ballarin
parents:
13835
diff
changeset

681 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

682 

0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
19984
diff
changeset

683 
subsection {* The Lattice of Subgroups of a Group *} 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

684 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

685 
text_raw {* \label{sec:subgrouplattice} *} 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

686 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

687 
theorem (in group) subgroups_partial_order: 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

688 
"partial_order {H. subgroup H G} (op \<subseteq>)" 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

689 
by (rule partial_order.intro) simp_all 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

690 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

691 
lemma (in group) subgroup_self: 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

692 
"subgroup (carrier G) G" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

693 
by (rule subgroupI) auto 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

694 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

695 
lemma (in group) subgroup_imp_group: 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

696 
"subgroup H G ==> group (G( carrier := H ))" 
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19783
diff
changeset

697 
by (rule subgroup.subgroup_is_group) 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

698 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

699 
lemma (in group) is_monoid [intro, simp]: 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

700 
"monoid G" 
14963  701 
by (auto intro: monoid.intro m_assoc) 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

702 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

703 
lemma (in group) subgroup_inv_equality: 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

704 
"[ subgroup H G; x \<in> H ] ==> m_inv (G ( carrier := H )) x = inv x" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

705 
apply (rule_tac inv_equality [THEN sym]) 
14761  706 
apply (rule group.l_inv [OF subgroup_imp_group, simplified], assumption+) 
707 
apply (rule subsetD [OF subgroup.subset], assumption+) 

708 
apply (rule subsetD [OF subgroup.subset], assumption) 

709 
apply (rule_tac group.inv_closed [OF subgroup_imp_group, simplified], assumption+) 

14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

710 
done 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

711 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

712 
theorem (in group) subgroups_Inter: 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

713 
assumes subgr: "(!!H. H \<in> A ==> subgroup H G)" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

714 
and not_empty: "A ~= {}" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

715 
shows "subgroup (\<Inter>A) G" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

716 
proof (rule subgroupI) 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

717 
from subgr [THEN subgroup.subset] and not_empty 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

718 
show "\<Inter>A \<subseteq> carrier G" by blast 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

719 
next 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

720 
from subgr [THEN subgroup.one_closed] 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

721 
show "\<Inter>A ~= {}" by blast 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

722 
next 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

723 
fix x assume "x \<in> \<Inter>A" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

724 
with subgr [THEN subgroup.m_inv_closed] 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

725 
show "inv x \<in> \<Inter>A" by blast 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

726 
next 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

727 
fix x y assume "x \<in> \<Inter>A" "y \<in> \<Inter>A" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

728 
with subgr [THEN subgroup.m_closed] 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

729 
show "x \<otimes> y \<in> \<Inter>A" by blast 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

730 
qed 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

731 

0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

732 
theorem (in group) subgroups_complete_lattice: 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

733 
"complete_lattice {H. subgroup H G} (op \<subseteq>)" 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

734 
(is "complete_lattice ?car ?le") 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

735 
proof (rule partial_order.complete_lattice_criterion1) 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

736 
show "partial_order ?car ?le" by (rule subgroups_partial_order) 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

737 
next 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

738 
have "order_syntax.greatest ?car ?le (carrier G) ?car" 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

739 
by (unfold order_syntax.greatest_def) 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

740 
(simp add: subgroup.subset subgroup_self) 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

741 
then show "\<exists>G. order_syntax.greatest ?car ?le G ?car" .. 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

742 
next 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

743 
fix A 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

744 
assume L: "A \<subseteq> ?car" and non_empty: "A ~= {}" 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

745 
then have Int_subgroup: "subgroup (\<Inter>A) G" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

746 
by (fastsimp intro: subgroups_Inter) 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

747 
have "order_syntax.greatest ?car ?le (\<Inter>A) (order_syntax.Lower ?car ?le A)" 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

748 
(is "order_syntax.greatest _ _ ?Int _") 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

749 
proof (rule order_syntax.greatest_LowerI) 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

750 
fix H 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

751 
assume H: "H \<in> A" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

752 
with L have subgroupH: "subgroup H G" by auto 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

753 
from subgroupH have groupH: "group (G ( carrier := H ))" (is "group ?H") 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

754 
by (rule subgroup_imp_group) 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

755 
from groupH have monoidH: "monoid ?H" 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

756 
by (rule group.is_monoid) 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

757 
from H have Int_subset: "?Int \<subseteq> H" by fastsimp 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

758 
then show "?le ?Int H" by simp 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

759 
next 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

760 
fix H 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

761 
assume H: "H \<in> order_syntax.Lower ?car ?le A" 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

762 
with L Int_subgroup show "?le H ?Int" 
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

763 
by (fastsimp simp: order_syntax.Lower_def intro: Inter_greatest) 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

764 
next 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

765 
show "A \<subseteq> ?car" by (rule L) 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

766 
next 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

767 
show "?Int \<in> ?car" by simp (rule Int_subgroup) 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

768 
qed 
21041
60e418260b4d
Order and lattice structures no longer based on records.
ballarin
parents:
20318
diff
changeset

769 
then show "\<exists>I. order_syntax.greatest ?car ?le I (order_syntax.Lower ?car ?le A)" .. 
14751
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

770 
qed 
0d7850e27fed
Change of theory hierarchy: Group is now based in Lattice.
ballarin
parents:
14706
diff
changeset

771 

13813  772 
end 