40 |
40 |
41 consts |
41 consts |
42 pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75) |
42 pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75) |
43 |
43 |
44 defs (overloaded) |
44 defs (overloaded) |
45 nat_pow_def: "pow G a n == nat_rec (one G) (%u b. mult G b a) n" |
45 nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n" |
46 int_pow_def: "pow G a z == |
46 int_pow_def: "pow G a z == |
47 let p = nat_rec (one G) (%u b. mult G b a) |
47 let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) |
48 in if neg z then m_inv G (p (nat (-z))) else p (nat z)" |
48 in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)" |
49 |
49 |
50 locale magma = struct G + |
50 locale magma = struct G + |
51 assumes m_closed [intro, simp]: |
51 assumes m_closed [intro, simp]: |
52 "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
52 "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
53 |
53 |
60 assumes one_closed [intro, simp]: "\<one> \<in> carrier G" |
60 assumes one_closed [intro, simp]: "\<one> \<in> carrier G" |
61 and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x" |
61 and l_one [simp]: "x \<in> carrier G ==> \<one> \<otimes> x = x" |
62 and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x" |
62 and r_one [simp]: "x \<in> carrier G ==> x \<otimes> \<one> = x" |
63 |
63 |
64 lemma monoidI: |
64 lemma monoidI: |
|
65 includes struct G |
65 assumes m_closed: |
66 assumes m_closed: |
66 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G" |
67 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
67 and one_closed: "one G \<in> carrier G" |
68 and one_closed: "\<one> \<in> carrier G" |
68 and m_assoc: |
69 and m_assoc: |
69 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
70 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
70 mult G (mult G x y) z = mult G x (mult G y z)" |
71 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
71 and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x" |
72 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" |
72 and r_one: "!!x. x \<in> carrier G ==> mult G x (one G) = x" |
73 and r_one: "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x" |
73 shows "monoid G" |
74 shows "monoid G" |
74 by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro |
75 by (fast intro!: monoid.intro magma.intro semigroup_axioms.intro |
75 semigroup.intro monoid_axioms.intro |
76 semigroup.intro monoid_axioms.intro |
76 intro: prems) |
77 intro: prems) |
77 |
78 |
78 lemma (in monoid) Units_closed [dest]: |
79 lemma (in monoid) Units_closed [dest]: |
79 "x \<in> Units G ==> x \<in> carrier G" |
80 "x \<in> Units G ==> x \<in> carrier G" |
80 by (unfold Units_def) fast |
81 by (unfold Units_def) fast |
81 |
82 |
82 lemma (in monoid) inv_unique: |
83 lemma (in monoid) inv_unique: |
83 assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>" |
84 assumes eq: "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>" |
84 and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" |
85 and G: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" |
85 shows "y = y'" |
86 shows "y = y'" |
86 proof - |
87 proof - |
87 from G eq have "y = y \<otimes> (x \<otimes> y')" by simp |
88 from G eq have "y = y \<otimes> (x \<otimes> y')" by simp |
88 also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc) |
89 also from G have "... = (y \<otimes> x) \<otimes> y'" by (simp add: m_assoc) |
89 also from G eq have "... = y'" by simp |
90 also from G eq have "... = y'" by simp |
127 lemma (in monoid) Units_l_cancel [simp]: |
128 lemma (in monoid) Units_l_cancel [simp]: |
128 "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==> |
129 "[| x \<in> Units G; y \<in> carrier G; z \<in> carrier G |] ==> |
129 (x \<otimes> y = x \<otimes> z) = (y = z)" |
130 (x \<otimes> y = x \<otimes> z) = (y = z)" |
130 proof |
131 proof |
131 assume eq: "x \<otimes> y = x \<otimes> z" |
132 assume eq: "x \<otimes> y = x \<otimes> z" |
132 and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" |
133 and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" |
133 then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" |
134 then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z" |
134 by (simp add: m_assoc Units_closed) |
135 by (simp add: m_assoc Units_closed) |
135 with G show "y = z" by (simp add: Units_l_inv) |
136 with G show "y = z" by (simp add: Units_l_inv) |
136 next |
137 next |
137 assume eq: "y = z" |
138 assume eq: "y = z" |
138 and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" |
139 and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G" |
139 then show "x \<otimes> y = x \<otimes> z" by simp |
140 then show "x \<otimes> y = x \<otimes> z" by simp |
140 qed |
141 qed |
141 |
142 |
142 lemma (in monoid) Units_inv_inv [simp]: |
143 lemma (in monoid) Units_inv_inv [simp]: |
143 "x \<in> Units G ==> inv (inv x) = x" |
144 "x \<in> Units G ==> inv (inv x) = x" |
150 |
151 |
151 lemma (in monoid) inv_inj_on_Units: |
152 lemma (in monoid) inv_inj_on_Units: |
152 "inj_on (m_inv G) (Units G)" |
153 "inj_on (m_inv G) (Units G)" |
153 proof (rule inj_onI) |
154 proof (rule inj_onI) |
154 fix x y |
155 fix x y |
155 assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y" |
156 assume G: "x \<in> Units G" "y \<in> Units G" and eq: "inv x = inv y" |
156 then have "inv (inv x) = inv (inv y)" by simp |
157 then have "inv (inv x) = inv (inv y)" by simp |
157 with G show "x = y" by simp |
158 with G show "x = y" by simp |
158 qed |
159 qed |
159 |
160 |
160 lemma (in monoid) Units_inv_comm: |
161 lemma (in monoid) Units_inv_comm: |
161 assumes inv: "x \<otimes> y = \<one>" |
162 assumes inv: "x \<otimes> y = \<one>" |
162 and G: "x \<in> Units G" "y \<in> Units G" |
163 and G: "x \<in> Units G" "y \<in> Units G" |
163 shows "y \<otimes> x = \<one>" |
164 shows "y \<otimes> x = \<one>" |
164 proof - |
165 proof - |
165 from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed) |
166 from G have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by (auto simp add: inv Units_closed) |
166 with G show ?thesis by (simp del: r_one add: m_assoc Units_closed) |
167 with G show ?thesis by (simp del: r_one add: m_assoc Units_closed) |
167 qed |
168 qed |
198 |
199 |
199 locale group = monoid + |
200 locale group = monoid + |
200 assumes Units: "carrier G <= Units G" |
201 assumes Units: "carrier G <= Units G" |
201 |
202 |
202 theorem groupI: |
203 theorem groupI: |
|
204 includes struct G |
203 assumes m_closed [simp]: |
205 assumes m_closed [simp]: |
204 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G" |
206 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
205 and one_closed [simp]: "one G \<in> carrier G" |
207 and one_closed [simp]: "\<one> \<in> carrier G" |
206 and m_assoc: |
208 and m_assoc: |
207 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
209 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
208 mult G (mult G x y) z = mult G x (mult G y z)" |
210 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
209 and l_one [simp]: "!!x. x \<in> carrier G ==> mult G (one G) x = x" |
211 and l_one [simp]: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" |
210 and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G" |
212 and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>" |
211 shows "group G" |
213 shows "group G" |
212 proof - |
214 proof - |
213 have l_cancel [simp]: |
215 have l_cancel [simp]: |
214 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
216 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
215 (mult G x y = mult G x z) = (y = z)" |
217 (x \<otimes> y = x \<otimes> z) = (y = z)" |
216 proof |
218 proof |
217 fix x y z |
219 fix x y z |
218 assume eq: "mult G x y = mult G x z" |
220 assume eq: "x \<otimes> y = x \<otimes> z" |
219 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
221 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
220 with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" |
222 with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" |
221 and l_inv: "mult G x_inv x = one G" by fast |
223 and l_inv: "x_inv \<otimes> x = \<one>" by fast |
222 from G eq xG have "mult G (mult G x_inv x) y = mult G (mult G x_inv x) z" |
224 from G eq xG have "(x_inv \<otimes> x) \<otimes> y = (x_inv \<otimes> x) \<otimes> z" |
223 by (simp add: m_assoc) |
225 by (simp add: m_assoc) |
224 with G show "y = z" by (simp add: l_inv) |
226 with G show "y = z" by (simp add: l_inv) |
225 next |
227 next |
226 fix x y z |
228 fix x y z |
227 assume eq: "y = z" |
229 assume eq: "y = z" |
228 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
230 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
229 then show "mult G x y = mult G x z" by simp |
231 then show "x \<otimes> y = x \<otimes> z" by simp |
230 qed |
232 qed |
231 have r_one: |
233 have r_one: |
232 "!!x. x \<in> carrier G ==> mult G x (one G) = x" |
234 "!!x. x \<in> carrier G ==> x \<otimes> \<one> = x" |
233 proof - |
235 proof - |
234 fix x |
236 fix x |
235 assume x: "x \<in> carrier G" |
237 assume x: "x \<in> carrier G" |
236 with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" |
238 with l_inv_ex obtain x_inv where xG: "x_inv \<in> carrier G" |
237 and l_inv: "mult G x_inv x = one G" by fast |
239 and l_inv: "x_inv \<otimes> x = \<one>" by fast |
238 from x xG have "mult G x_inv (mult G x (one G)) = mult G x_inv x" |
240 from x xG have "x_inv \<otimes> (x \<otimes> \<one>) = x_inv \<otimes> x" |
239 by (simp add: m_assoc [symmetric] l_inv) |
241 by (simp add: m_assoc [symmetric] l_inv) |
240 with x xG show "mult G x (one G) = x" by simp |
242 with x xG show "x \<otimes> \<one> = x" by simp |
241 qed |
243 qed |
242 have inv_ex: |
244 have inv_ex: |
243 "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G & |
245 "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>" |
244 mult G x y = one G" |
|
245 proof - |
246 proof - |
246 fix x |
247 fix x |
247 assume x: "x \<in> carrier G" |
248 assume x: "x \<in> carrier G" |
248 with l_inv_ex obtain y where y: "y \<in> carrier G" |
249 with l_inv_ex obtain y where y: "y \<in> carrier G" |
249 and l_inv: "mult G y x = one G" by fast |
250 and l_inv: "y \<otimes> x = \<one>" by fast |
250 from x y have "mult G y (mult G x y) = mult G y (one G)" |
251 from x y have "y \<otimes> (x \<otimes> y) = y \<otimes> \<one>" |
251 by (simp add: m_assoc [symmetric] l_inv r_one) |
252 by (simp add: m_assoc [symmetric] l_inv r_one) |
252 with x y have r_inv: "mult G x y = one G" |
253 with x y have r_inv: "x \<otimes> y = \<one>" |
253 by simp |
254 by simp |
254 from x y show "EX y : carrier G. mult G y x = one G & |
255 from x y show "EX y : carrier G. y \<otimes> x = \<one> & x \<otimes> y = \<one>" |
255 mult G x y = one G" |
|
256 by (fast intro: l_inv r_inv) |
256 by (fast intro: l_inv r_inv) |
257 qed |
257 qed |
258 then have carrier_subset_Units: "carrier G <= Units G" |
258 then have carrier_subset_Units: "carrier G <= Units G" |
259 by (unfold Units_def) fast |
259 by (unfold Units_def) fast |
260 show ?thesis |
260 show ?thesis |
304 lemma (in group) r_cancel [simp]: |
304 lemma (in group) r_cancel [simp]: |
305 "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
305 "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
306 (y \<otimes> x = z \<otimes> x) = (y = z)" |
306 (y \<otimes> x = z \<otimes> x) = (y = z)" |
307 proof |
307 proof |
308 assume eq: "y \<otimes> x = z \<otimes> x" |
308 assume eq: "y \<otimes> x = z \<otimes> x" |
309 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
309 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
310 then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)" |
310 then have "y \<otimes> (x \<otimes> inv x) = z \<otimes> (x \<otimes> inv x)" |
311 by (simp add: m_assoc [symmetric]) |
311 by (simp add: m_assoc [symmetric]) |
312 with G show "y = z" by (simp add: r_inv) |
312 with G show "y = z" by (simp add: r_inv) |
313 next |
313 next |
314 assume eq: "y = z" |
314 assume eq: "y = z" |
315 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
315 and G: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
316 then show "y \<otimes> x = z \<otimes> x" by simp |
316 then show "y \<otimes> x = z \<otimes> x" by simp |
317 qed |
317 qed |
318 |
318 |
319 lemma (in group) inv_one [simp]: |
319 lemma (in group) inv_one [simp]: |
320 "inv \<one> = \<one>" |
320 "inv \<one> = \<one>" |
333 using inv_inj_on_Units by simp |
333 using inv_inj_on_Units by simp |
334 |
334 |
335 lemma (in group) inv_mult_group: |
335 lemma (in group) inv_mult_group: |
336 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x" |
336 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x" |
337 proof - |
337 proof - |
338 assume G: "x \<in> carrier G" "y \<in> carrier G" |
338 assume G: "x \<in> carrier G" "y \<in> carrier G" |
339 then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)" |
339 then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)" |
340 by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv) |
340 by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric] l_inv) |
341 with G show ?thesis by simp |
341 with G show ?thesis by simp |
342 qed |
342 qed |
343 |
343 |
344 lemma (in group) inv_comm: |
344 lemma (in group) inv_comm: |
345 "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>" |
345 "[| x \<otimes> y = \<one>; x \<in> carrier G; y \<in> carrier G |] ==> y \<otimes> x = \<one>" |
346 by (rule Units_inv_comm) auto |
346 by (rule Units_inv_comm) auto |
347 |
347 |
348 lemma (in group) inv_equality: |
348 lemma (in group) inv_equality: |
349 "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y" |
349 "[|y \<otimes> x = \<one>; x \<in> carrier G; y \<in> carrier G|] ==> inv x = y" |
350 apply (simp add: m_inv_def) |
350 apply (simp add: m_inv_def) |
351 apply (rule the_equality) |
351 apply (rule the_equality) |
352 apply (simp add: inv_comm [of y x]) |
352 apply (simp add: inv_comm [of y x]) |
353 apply (rule r_cancel [THEN iffD1], auto) |
353 apply (rule r_cancel [THEN iffD1], auto) |
354 done |
354 done |
355 |
355 |
356 text {* Power *} |
356 text {* Power *} |
357 |
357 |
358 lemma (in group) int_pow_def2: |
358 lemma (in group) int_pow_def2: |
491 subsection {* Direct Products *} |
491 subsection {* Direct Products *} |
492 |
492 |
493 constdefs (structure G and H) |
493 constdefs (structure G and H) |
494 DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup" (infixr "\<times>\<^sub>s" 80) |
494 DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup" (infixr "\<times>\<^sub>s" 80) |
495 "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H, |
495 "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H, |
496 mult = (%(xg, xh) (yg, yh). (xg \<otimes> yg, xh \<otimes>\<^sub>2 yh)) |)" |
496 mult = (%(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')) |)" |
497 |
497 |
498 DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid" (infixr "\<times>\<^sub>g" 80) |
498 DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid" (infixr "\<times>\<^sub>g" 80) |
499 "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>, \<one>\<^sub>2) |)" |
499 "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>) |)" |
500 |
500 |
501 lemma DirProdSemigroup_magma: |
501 lemma DirProdSemigroup_magma: |
502 includes magma G + magma H |
502 includes magma G + magma H |
503 shows "magma (G \<times>\<^sub>s H)" |
503 shows "magma (G \<times>\<^sub>s H)" |
504 by (rule magma.intro) (auto simp add: DirProdSemigroup_def) |
504 by (rule magma.intro) (auto simp add: DirProdSemigroup_def) |
548 lemma carrier_DirProdGroup [simp]: |
548 lemma carrier_DirProdGroup [simp]: |
549 "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H" |
549 "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H" |
550 by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs) |
550 by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs) |
551 |
551 |
552 lemma one_DirProdGroup [simp]: |
552 lemma one_DirProdGroup [simp]: |
553 "one (G \<times>\<^sub>g H) = (one G, one H)" |
553 "\<one>\<^bsub>(G \<times>\<^sub>g H)\<^esub> = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)" |
554 by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs) |
554 by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs) |
555 |
555 |
556 lemma mult_DirProdGroup [simp]: |
556 lemma mult_DirProdGroup [simp]: |
557 "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')" |
557 "(g, h) \<otimes>\<^bsub>(G \<times>\<^sub>g H)\<^esub> (g', h') = (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')" |
558 by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs) |
558 by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs) |
559 |
559 |
560 lemma inv_DirProdGroup [simp]: |
560 lemma inv_DirProdGroup [simp]: |
561 includes group G + group H |
561 includes group G + group H |
562 assumes g: "g \<in> carrier G" |
562 assumes g: "g \<in> carrier G" |
563 and h: "h \<in> carrier H" |
563 and h: "h \<in> carrier H" |
564 shows "m_inv (G \<times>\<^sub>g H) (g, h) = (m_inv G g, m_inv H h)" |
564 shows "m_inv (G \<times>\<^sub>g H) (g, h) = (inv\<^bsub>G\<^esub> g, inv\<^bsub>H\<^esub> h)" |
565 apply (rule group.inv_equality [OF DirProdGroup_group]) |
565 apply (rule group.inv_equality [OF DirProdGroup_group]) |
566 apply (simp_all add: prems group_def group.l_inv) |
566 apply (simp_all add: prems group_def group.l_inv) |
567 done |
567 done |
568 |
568 |
569 subsection {* Homomorphisms *} |
569 subsection {* Homomorphisms *} |
570 |
570 |
571 constdefs (structure G and H) |
571 constdefs (structure G and H) |
572 hom :: "_ => _ => ('a => 'b) set" |
572 hom :: "_ => _ => ('a => 'b) set" |
573 "hom G H == |
573 "hom G H == |
574 {h. h \<in> carrier G -> carrier H & |
574 {h. h \<in> carrier G -> carrier H & |
575 (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^sub>2 h y)}" |
575 (\<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)}" |
576 |
576 |
577 lemma (in semigroup) hom: |
577 lemma (in semigroup) hom: |
578 includes semigroup G |
578 includes semigroup G |
579 shows "semigroup (| carrier = hom G G, mult = op o |)" |
579 shows "semigroup (| carrier = hom G G, mult = op o |)" |
580 proof (rule semigroup.intro) |
580 proof (rule semigroup.intro) |
584 show "semigroup_axioms (| carrier = hom G G, mult = op o |)" |
584 show "semigroup_axioms (| carrier = hom G G, mult = op o |)" |
585 by (rule semigroup_axioms.intro) (simp add: o_assoc) |
585 by (rule semigroup_axioms.intro) (simp add: o_assoc) |
586 qed |
586 qed |
587 |
587 |
588 lemma hom_mult: |
588 lemma hom_mult: |
589 "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |] |
589 "[| h \<in> hom G H; x \<in> carrier G; y \<in> carrier G |] |
590 ==> h (mult G x y) = mult H (h x) (h y)" |
590 ==> h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y" |
591 by (simp add: hom_def) |
591 by (simp add: hom_def) |
592 |
592 |
593 lemma hom_closed: |
593 lemma hom_closed: |
594 "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H" |
594 "[| h \<in> hom G H; x \<in> carrier G |] ==> h x \<in> carrier H" |
595 by (auto simp add: hom_def funcset_mem) |
595 by (auto simp add: hom_def funcset_mem) |
596 |
596 |
597 lemma compose_hom: |
597 lemma compose_hom: |
598 "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|] |
598 "[|group G; h \<in> hom G G; h' \<in> hom G G; h' \<in> carrier G -> carrier G|] |
599 ==> compose (carrier G) h h' \<in> hom G G" |
599 ==> compose (carrier G) h h' \<in> hom G G" |
600 apply (simp (no_asm_simp) add: hom_def) |
600 apply (simp (no_asm_simp) add: hom_def) |
601 apply (intro conjI) |
601 apply (intro conjI) |
602 apply (force simp add: funcset_compose hom_def) |
602 apply (force simp add: funcset_compose hom_def) |
603 apply (simp add: compose_def group.axioms hom_mult funcset_mem) |
603 apply (simp add: compose_def group.axioms hom_mult funcset_mem) |
604 done |
604 done |
605 |
605 |
606 locale group_hom = group G + group H + var h + |
606 locale group_hom = group G + group H + var h + |
607 assumes homh: "h \<in> hom G H" |
607 assumes homh: "h \<in> hom G H" |
608 notes hom_mult [simp] = hom_mult [OF homh] |
608 notes hom_mult [simp] = hom_mult [OF homh] |
611 lemma (in group_hom) one_closed [simp]: |
611 lemma (in group_hom) one_closed [simp]: |
612 "h \<one> \<in> carrier H" |
612 "h \<one> \<in> carrier H" |
613 by simp |
613 by simp |
614 |
614 |
615 lemma (in group_hom) hom_one [simp]: |
615 lemma (in group_hom) hom_one [simp]: |
616 "h \<one> = \<one>\<^sub>2" |
616 "h \<one> = \<one>\<^bsub>H\<^esub>" |
617 proof - |
617 proof - |
618 have "h \<one> \<otimes>\<^sub>2 \<one>\<^sub>2 = h \<one> \<otimes>\<^sub>2 h \<one>" |
618 have "h \<one> \<otimes>\<^bsub>H\<^esub> \<one>\<^bsub>H\<^esub> = h \<one> \<otimes>\<^sub>2 h \<one>" |
619 by (simp add: hom_mult [symmetric] del: hom_mult) |
619 by (simp add: hom_mult [symmetric] del: hom_mult) |
620 then show ?thesis by (simp del: r_one) |
620 then show ?thesis by (simp del: r_one) |
621 qed |
621 qed |
622 |
622 |
623 lemma (in group_hom) inv_closed [simp]: |
623 lemma (in group_hom) inv_closed [simp]: |
624 "x \<in> carrier G ==> h (inv x) \<in> carrier H" |
624 "x \<in> carrier G ==> h (inv x) \<in> carrier H" |
625 by simp |
625 by simp |
626 |
626 |
627 lemma (in group_hom) hom_inv [simp]: |
627 lemma (in group_hom) hom_inv [simp]: |
628 "x \<in> carrier G ==> h (inv x) = inv\<^sub>2 (h x)" |
628 "x \<in> carrier G ==> h (inv x) = inv\<^bsub>H\<^esub> (h x)" |
629 proof - |
629 proof - |
630 assume x: "x \<in> carrier G" |
630 assume x: "x \<in> carrier G" |
631 then have "h x \<otimes>\<^sub>2 h (inv x) = \<one>\<^sub>2" |
631 then have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = \<one>\<^bsub>H\<^esub>" |
632 by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult) |
632 by (simp add: hom_mult [symmetric] G.r_inv del: hom_mult) |
633 also from x have "... = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" |
633 also from x have "... = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" |
634 by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult) |
634 by (simp add: hom_mult [symmetric] H.r_inv del: hom_mult) |
635 finally have "h x \<otimes>\<^sub>2 h (inv x) = h x \<otimes>\<^sub>2 inv\<^sub>2 (h x)" . |
635 finally have "h x \<otimes>\<^bsub>H\<^esub> h (inv x) = h x \<otimes>\<^bsub>H\<^esub> inv\<^bsub>H\<^esub> (h x)" . |
636 with x show ?thesis by simp |
636 with x show ?thesis by simp |
637 qed |
637 qed |
638 |
638 |
639 subsection {* Commutative Structures *} |
639 subsection {* Commutative Structures *} |
640 |
640 |
651 |
651 |
652 lemma (in comm_semigroup) m_lcomm: |
652 lemma (in comm_semigroup) m_lcomm: |
653 "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
653 "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
654 x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)" |
654 x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)" |
655 proof - |
655 proof - |
656 assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
656 assume xyz: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
657 from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc) |
657 from xyz have "x \<otimes> (y \<otimes> z) = (x \<otimes> y) \<otimes> z" by (simp add: m_assoc) |
658 also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm) |
658 also from xyz have "... = (y \<otimes> x) \<otimes> z" by (simp add: m_comm) |
659 also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc) |
659 also from xyz have "... = y \<otimes> (x \<otimes> z)" by (simp add: m_assoc) |
660 finally show ?thesis . |
660 finally show ?thesis . |
661 qed |
661 qed |
663 lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm |
663 lemmas (in comm_semigroup) m_ac = m_assoc m_comm m_lcomm |
664 |
664 |
665 locale comm_monoid = comm_semigroup + monoid |
665 locale comm_monoid = comm_semigroup + monoid |
666 |
666 |
667 lemma comm_monoidI: |
667 lemma comm_monoidI: |
|
668 includes struct G |
668 assumes m_closed: |
669 assumes m_closed: |
669 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G" |
670 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
670 and one_closed: "one G \<in> carrier G" |
671 and one_closed: "\<one> \<in> carrier G" |
671 and m_assoc: |
672 and m_assoc: |
672 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
673 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
673 mult G (mult G x y) z = mult G x (mult G y z)" |
674 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
674 and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x" |
675 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" |
675 and m_comm: |
676 and m_comm: |
676 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x" |
677 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x" |
677 shows "comm_monoid G" |
678 shows "comm_monoid G" |
678 using l_one |
679 using l_one |
679 by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro |
680 by (auto intro!: comm_monoid.intro magma.intro semigroup_axioms.intro |
680 comm_semigroup_axioms.intro monoid_axioms.intro |
681 comm_semigroup_axioms.intro monoid_axioms.intro |
681 intro: prems simp: m_closed one_closed m_comm) |
682 intro: prems simp: m_closed one_closed m_comm) |
682 |
683 |
683 lemma (in monoid) monoid_comm_monoidI: |
684 lemma (in monoid) monoid_comm_monoidI: |
684 assumes m_comm: |
685 assumes m_comm: |
685 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x" |
686 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x" |
686 shows "comm_monoid G" |
687 shows "comm_monoid G" |
687 by (rule comm_monoidI) (auto intro: m_assoc m_comm) |
688 by (rule comm_monoidI) (auto intro: m_assoc m_comm) |
688 (* |
689 (*lemma (in comm_monoid) r_one [simp]: |
689 lemma (in comm_monoid) r_one [simp]: |
|
690 "x \<in> carrier G ==> x \<otimes> \<one> = x" |
690 "x \<in> carrier G ==> x \<otimes> \<one> = x" |
691 proof - |
691 proof - |
692 assume G: "x \<in> carrier G" |
692 assume G: "x \<in> carrier G" |
693 then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm) |
693 then have "x \<otimes> \<one> = \<one> \<otimes> x" by (simp add: m_comm) |
694 also from G have "... = x" by simp |
694 also from G have "... = x" by simp |
695 finally show ?thesis . |
695 finally show ?thesis . |
696 qed |
696 qed*) |
697 *) |
|
698 |
|
699 lemma (in comm_monoid) nat_pow_distr: |
697 lemma (in comm_monoid) nat_pow_distr: |
700 "[| x \<in> carrier G; y \<in> carrier G |] ==> |
698 "[| x \<in> carrier G; y \<in> carrier G |] ==> |
701 (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n" |
699 (x \<otimes> y) (^) (n::nat) = x (^) n \<otimes> y (^) n" |
702 by (induct n) (simp, simp add: m_ac) |
700 by (induct n) (simp, simp add: m_ac) |
703 |
701 |
704 locale comm_group = comm_monoid + group |
702 locale comm_group = comm_monoid + group |
705 |
703 |
706 lemma (in group) group_comm_groupI: |
704 lemma (in group) group_comm_groupI: |
707 assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> |
705 assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> |
708 mult G x y = mult G y x" |
706 x \<otimes> y = y \<otimes> x" |
709 shows "comm_group G" |
707 shows "comm_group G" |
710 by (fast intro: comm_group.intro comm_semigroup_axioms.intro |
708 by (fast intro: comm_group.intro comm_semigroup_axioms.intro |
711 group.axioms prems) |
709 group.axioms prems) |
712 |
710 |
713 lemma comm_groupI: |
711 lemma comm_groupI: |
|
712 includes struct G |
714 assumes m_closed: |
713 assumes m_closed: |
715 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y \<in> carrier G" |
714 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y \<in> carrier G" |
716 and one_closed: "one G \<in> carrier G" |
715 and one_closed: "\<one> \<in> carrier G" |
717 and m_assoc: |
716 and m_assoc: |
718 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
717 "!!x y z. [| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==> |
719 mult G (mult G x y) z = mult G x (mult G y z)" |
718 (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" |
720 and m_comm: |
719 and m_comm: |
721 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> mult G x y = mult G y x" |
720 "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==> x \<otimes> y = y \<otimes> x" |
722 and l_one: "!!x. x \<in> carrier G ==> mult G (one G) x = x" |
721 and l_one: "!!x. x \<in> carrier G ==> \<one> \<otimes> x = x" |
723 and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. mult G y x = one G" |
722 and l_inv_ex: "!!x. x \<in> carrier G ==> EX y : carrier G. y \<otimes> x = \<one>" |
724 shows "comm_group G" |
723 shows "comm_group G" |
725 by (fast intro: group.group_comm_groupI groupI prems) |
724 by (fast intro: group.group_comm_groupI groupI prems) |
726 |
725 |
727 lemma (in comm_group) inv_mult: |
726 lemma (in comm_group) inv_mult: |
728 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y" |
727 "[| x \<in> carrier G; y \<in> carrier G |] ==> inv (x \<otimes> y) = inv x \<otimes> inv y" |