author | ballarin |
Thu, 06 Nov 2003 14:18:05 +0100 | |
changeset 14254 | 342634f38451 |
parent 13943 | 83d842ccd4aa |
child 14530 | e94fd774ecf5 |
permissions | -rw-r--r-- |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/GroupTheory/Coset |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
3 |
Author: Florian Kammueller, with new proofs by L C Paulson |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
4 |
*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
5 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
6 |
header{*Theory of Cosets*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
7 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
8 |
theory Coset = Group + Exponent: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
9 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
10 |
declare (in group) l_inv [simp] r_inv [simp] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
11 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
12 |
constdefs |
13936 | 13 |
r_coset :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
14 |
"r_coset G H a == (% x. (mult G) x a) ` H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
15 |
|
13936 | 16 |
l_coset :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
17 |
"l_coset G a H == (% x. (mult G) a x) ` H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
18 |
|
13936 | 19 |
rcosets :: "[('a,'b) monoid_scheme,'a set] => ('a set)set" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
20 |
"rcosets G H == r_coset G H ` (carrier G)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
21 |
|
13936 | 22 |
set_mult :: "[('a,'b) monoid_scheme,'a set,'a set] => 'a set" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
23 |
"set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
24 |
|
13936 | 25 |
set_inv :: "[('a,'b) monoid_scheme,'a set] => 'a set" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
26 |
"set_inv G H == (m_inv G) ` H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
27 |
|
13936 | 28 |
normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "<|" 60) |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
29 |
"normal H G == subgroup H G & |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
30 |
(\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
31 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
32 |
syntax (xsymbols) |
13936 | 33 |
normal :: "['a set, ('a,'b) monoid_scheme] => bool" (infixl "\<lhd>" 60) |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
34 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
35 |
locale coset = group G + |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
36 |
fixes rcos :: "['a set, 'a] => 'a set" (infixl "#>" 60) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
37 |
and lcos :: "['a, 'a set] => 'a set" (infixl "<#" 60) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
38 |
and setmult :: "['a set, 'a set] => 'a set" (infixl "<#>" 60) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
39 |
defines rcos_def: "H #> x == r_coset G H x" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
40 |
and lcos_def: "x <# H == l_coset G x H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
41 |
and setmult_def: "H <#> K == set_mult G H K" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
42 |
|
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
43 |
text {* |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
44 |
Locale @{term coset} provides only syntax. |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
45 |
Logically, groups are cosets. |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
46 |
*} |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
47 |
lemma (in group) is_coset: |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
48 |
"coset G" |
14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13943
diff
changeset
|
49 |
by (rule coset.intro) |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
50 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
51 |
text{*Lemmas useful for Sylow's Theorem*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
52 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
53 |
lemma card_inj: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
54 |
"[|f \<in> A\<rightarrow>B; inj_on f A; finite A; finite B|] ==> card(A) <= card(B)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
55 |
apply (rule card_inj_on_le) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
56 |
apply (auto simp add: Pi_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
57 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
58 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
59 |
lemma card_bij: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
60 |
"[|f \<in> A\<rightarrow>B; inj_on f A; |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
61 |
g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
62 |
by (blast intro: card_inj order_antisym) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
63 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
64 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
65 |
subsection{*Lemmas Using Locale Constants*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
66 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
67 |
lemma (in coset) r_coset_eq: "H #> a = {b . \<exists>h\<in>H. h \<otimes> a = b}" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
68 |
by (auto simp add: rcos_def r_coset_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
69 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
70 |
lemma (in coset) l_coset_eq: "a <# H = {b . \<exists>h\<in>H. a \<otimes> h = b}" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
71 |
by (auto simp add: lcos_def l_coset_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
72 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
73 |
lemma (in coset) setrcos_eq: "rcosets G H = {C . \<exists>a\<in>carrier G. C = H #> a}" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
74 |
by (auto simp add: rcosets_def rcos_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
75 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
76 |
lemma (in coset) set_mult_eq: "H <#> K = {c . \<exists>h\<in>H. \<exists>k\<in>K. c = h \<otimes> k}" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
77 |
by (simp add: setmult_def set_mult_def image_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
78 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
79 |
lemma (in coset) coset_mult_assoc: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
80 |
"[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
81 |
==> (M #> g) #> h = M #> (g \<otimes> h)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
82 |
by (force simp add: r_coset_eq m_assoc) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
83 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
84 |
lemma (in coset) coset_mult_one [simp]: "M <= carrier G ==> M #> \<one> = M" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
85 |
by (force simp add: r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
86 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
87 |
lemma (in coset) coset_mult_inv1: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
88 |
"[| M #> (x \<otimes> (inv y)) = M; x \<in> carrier G ; y \<in> carrier G; |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
89 |
M <= carrier G |] ==> M #> x = M #> y" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
90 |
apply (erule subst [of concl: "%z. M #> x = z #> y"]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
91 |
apply (simp add: coset_mult_assoc m_assoc) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
92 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
93 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
94 |
lemma (in coset) coset_mult_inv2: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
95 |
"[| M #> x = M #> y; x \<in> carrier G; y \<in> carrier G; M <= carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
96 |
==> M #> (x \<otimes> (inv y)) = M " |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
97 |
apply (simp add: coset_mult_assoc [symmetric]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
98 |
apply (simp add: coset_mult_assoc) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
99 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
100 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
101 |
lemma (in coset) coset_join1: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
102 |
"[| H #> x = H; x \<in> carrier G; subgroup H G |] ==> x\<in>H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
103 |
apply (erule subst) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
104 |
apply (simp add: r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
105 |
apply (blast intro: l_one subgroup.one_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
106 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
107 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
108 |
text{*Locales don't currently work with @{text rule_tac}, so we |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
109 |
must prove this lemma separately.*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
110 |
lemma (in coset) solve_equation: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
111 |
"\<lbrakk>subgroup H G; x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> \<exists>h\<in>H. h \<otimes> x = y" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
112 |
apply (rule bexI [of _ "y \<otimes> (inv x)"]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
113 |
apply (auto simp add: subgroup.m_closed subgroup.m_inv_closed m_assoc |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
114 |
subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
115 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
116 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
117 |
lemma (in coset) coset_join2: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
118 |
"[| x \<in> carrier G; subgroup H G; x\<in>H |] ==> H #> x = H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
119 |
by (force simp add: subgroup.m_closed r_coset_eq solve_equation) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
120 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
121 |
lemma (in coset) r_coset_subset_G: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
122 |
"[| H <= carrier G; x \<in> carrier G |] ==> H #> x <= carrier G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
123 |
by (auto simp add: r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
124 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
125 |
lemma (in coset) rcosI: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
126 |
"[| h \<in> H; H <= carrier G; x \<in> carrier G|] ==> h \<otimes> x \<in> H #> x" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
127 |
by (auto simp add: r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
128 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
129 |
lemma (in coset) setrcosI: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
130 |
"[| H <= carrier G; x \<in> carrier G |] ==> H #> x \<in> rcosets G H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
131 |
by (auto simp add: setrcos_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
132 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
133 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
134 |
text{*Really needed?*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
135 |
lemma (in coset) transpose_inv: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
136 |
"[| x \<otimes> y = z; x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
137 |
==> (inv x) \<otimes> z = y" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
138 |
by (force simp add: m_assoc [symmetric]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
139 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
140 |
lemma (in coset) repr_independence: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
141 |
"[| y \<in> H #> x; x \<in> carrier G; subgroup H G |] ==> H #> x = H #> y" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
142 |
by (auto simp add: r_coset_eq m_assoc [symmetric] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
143 |
subgroup.subset [THEN subsetD] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
144 |
subgroup.m_closed solve_equation) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
145 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
146 |
lemma (in coset) rcos_self: "[| x \<in> carrier G; subgroup H G |] ==> x \<in> H #> x" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
147 |
apply (simp add: r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
148 |
apply (blast intro: l_one subgroup.subset [THEN subsetD] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
149 |
subgroup.one_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
150 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
151 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
152 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
153 |
subsection{*normal subgroups*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
154 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
155 |
(*???????????????? |
13936 | 156 |
text "Allows use of theorems proved in the locale coset" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
157 |
lemma subgroup_imp_coset: "subgroup H G ==> coset G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
158 |
apply (drule subgroup_imp_group) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
159 |
apply (simp add: group_def coset_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
160 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
161 |
*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
162 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
163 |
lemma normal_imp_subgroup: "H <| G ==> subgroup H G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
164 |
by (simp add: normal_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
165 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
166 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
167 |
(*???????????????? |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
168 |
lemmas normal_imp_group = normal_imp_subgroup [THEN subgroup_imp_group] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
169 |
lemmas normal_imp_coset = normal_imp_subgroup [THEN subgroup_imp_coset] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
170 |
*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
171 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
172 |
lemma (in coset) normal_iff: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
173 |
"(H <| G) = (subgroup H G & (\<forall>x \<in> carrier G. H #> x = x <# H))" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
174 |
by (simp add: lcos_def rcos_def normal_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
175 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
176 |
lemma (in coset) normal_imp_rcos_eq_lcos: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
177 |
"[| H <| G; x \<in> carrier G |] ==> H #> x = x <# H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
178 |
by (simp add: lcos_def rcos_def normal_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
179 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
180 |
lemma (in coset) normal_inv_op_closed1: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
181 |
"\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> (inv x) \<otimes> h \<otimes> x \<in> H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
182 |
apply (auto simp add: l_coset_eq r_coset_eq normal_iff) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
183 |
apply (drule bspec, assumption) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
184 |
apply (drule equalityD1 [THEN subsetD], blast, clarify) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
185 |
apply (simp add: m_assoc subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
186 |
apply (erule subst) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
187 |
apply (simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
188 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
189 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
190 |
lemma (in coset) normal_inv_op_closed2: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
191 |
"\<lbrakk>H \<lhd> G; x \<in> carrier G; h \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> h \<otimes> (inv x) \<in> H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
192 |
apply (drule normal_inv_op_closed1 [of H "(inv x)"]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
193 |
apply auto |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
194 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
195 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
196 |
lemma (in coset) lcos_m_assoc: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
197 |
"[| M <= carrier G; g \<in> carrier G; h \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
198 |
==> g <# (h <# M) = (g \<otimes> h) <# M" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
199 |
by (force simp add: l_coset_eq m_assoc) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
200 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
201 |
lemma (in coset) lcos_mult_one: "M <= carrier G ==> \<one> <# M = M" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
202 |
by (force simp add: l_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
203 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
204 |
lemma (in coset) l_coset_subset_G: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
205 |
"[| H <= carrier G; x \<in> carrier G |] ==> x <# H <= carrier G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
206 |
by (auto simp add: l_coset_eq subsetD) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
207 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
208 |
lemma (in coset) l_repr_independence: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
209 |
"[| y \<in> x <# H; x \<in> carrier G; subgroup H G |] ==> x <# H = y <# H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
210 |
apply (auto simp add: l_coset_eq m_assoc |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
211 |
subgroup.subset [THEN subsetD] subgroup.m_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
212 |
apply (rule_tac x = "mult G (m_inv G h) ha" in bexI) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
213 |
--{*FIXME: locales don't currently work with @{text rule_tac}, |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
214 |
want @{term "(inv h) \<otimes> ha"}*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
215 |
apply (auto simp add: m_assoc [symmetric] subgroup.subset [THEN subsetD] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
216 |
subgroup.m_inv_closed subgroup.m_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
217 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
218 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
219 |
lemma (in coset) setmult_subset_G: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
220 |
"[| H <= carrier G; K <= carrier G |] ==> H <#> K <= carrier G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
221 |
by (auto simp add: set_mult_eq subsetD) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
222 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
223 |
lemma (in coset) subgroup_mult_id: "subgroup H G ==> H <#> H = H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
224 |
apply (auto simp add: subgroup.m_closed set_mult_eq Sigma_def image_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
225 |
apply (rule_tac x = x in bexI) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
226 |
apply (rule bexI [of _ "\<one>"]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
227 |
apply (auto simp add: subgroup.m_closed subgroup.one_closed |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
228 |
r_one subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
229 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
230 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
231 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
232 |
(* set of inverses of an r_coset *) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
233 |
lemma (in coset) rcos_inv: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
234 |
assumes normalHG: "H <| G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
235 |
and xinG: "x \<in> carrier G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
236 |
shows "set_inv G (H #> x) = H #> (inv x)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
237 |
proof - |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
238 |
have H_subset: "H <= carrier G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
239 |
by (rule subgroup.subset [OF normal_imp_subgroup, OF normalHG]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
240 |
show ?thesis |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
241 |
proof (auto simp add: r_coset_eq image_def set_inv_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
242 |
fix h |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
243 |
assume "h \<in> H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
244 |
hence "((inv x) \<otimes> (inv h) \<otimes> x) \<otimes> inv x = inv (h \<otimes> x)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
245 |
by (simp add: xinG m_assoc inv_mult_group H_subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
246 |
thus "\<exists>j\<in>H. j \<otimes> inv x = inv (h \<otimes> x)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
247 |
using prems |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
248 |
by (blast intro: normal_inv_op_closed1 normal_imp_subgroup |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
249 |
subgroup.m_inv_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
250 |
next |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
251 |
fix h |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
252 |
assume "h \<in> H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
253 |
hence eq: "(x \<otimes> (inv h) \<otimes> (inv x)) \<otimes> x = x \<otimes> inv h" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
254 |
by (simp add: xinG m_assoc H_subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
255 |
hence "(\<exists>j\<in>H. j \<otimes> x = inv (h \<otimes> (inv x))) \<and> h \<otimes> inv x = inv (inv (h \<otimes> (inv x)))" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
256 |
using prems |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
257 |
by (simp add: m_assoc inv_mult_group H_subset [THEN subsetD], |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
258 |
blast intro: eq normal_inv_op_closed2 normal_imp_subgroup |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
259 |
subgroup.m_inv_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
260 |
thus "\<exists>y. (\<exists>h\<in>H. h \<otimes> x = y) \<and> h \<otimes> inv x = inv y" .. |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
261 |
qed |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
262 |
qed |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
263 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
264 |
(*The old proof is something like this, but the rule_tac calls make |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
265 |
illegal references to implicit structures. |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
266 |
lemma (in coset) rcos_inv: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
267 |
"[| H <| G; x \<in> carrier G |] ==> set_inv G (H #> x) = H #> (inv x)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
268 |
apply (frule normal_imp_subgroup) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
269 |
apply (auto simp add: r_coset_eq image_def set_inv_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
270 |
apply (rule_tac x = "(inv x) \<otimes> (inv h) \<otimes> x" in bexI) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
271 |
apply (simp add: m_assoc inv_mult_group subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
272 |
apply (simp add: subgroup.m_inv_closed, assumption+) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
273 |
apply (rule_tac x = "inv (h \<otimes> (inv x)) " in exI) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
274 |
apply (simp add: inv_mult_group subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
275 |
apply (rule_tac x = "x \<otimes> (inv h) \<otimes> (inv x)" in bexI) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
276 |
apply (simp add: m_assoc subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
277 |
apply (simp add: normal_inv_op_closed2 subgroup.m_inv_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
278 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
279 |
*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
280 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
281 |
lemma (in coset) rcos_inv2: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
282 |
"[| H <| G; K \<in> rcosets G H; x \<in> K |] ==> set_inv G K = H #> (inv x)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
283 |
apply (simp add: setrcos_eq, clarify) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
284 |
apply (subgoal_tac "x : carrier G") |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
285 |
prefer 2 |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
286 |
apply (blast dest: r_coset_subset_G subgroup.subset normal_imp_subgroup) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
287 |
apply (drule repr_independence) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
288 |
apply assumption |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
289 |
apply (erule normal_imp_subgroup) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
290 |
apply (simp add: rcos_inv) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
291 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
292 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
293 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
294 |
(* some rules for <#> with #> or <# *) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
295 |
lemma (in coset) setmult_rcos_assoc: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
296 |
"[| H <= carrier G; K <= carrier G; x \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
297 |
==> H <#> (K #> x) = (H <#> K) #> x" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
298 |
apply (auto simp add: rcos_def r_coset_def setmult_def set_mult_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
299 |
apply (force simp add: m_assoc)+ |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
300 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
301 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
302 |
lemma (in coset) rcos_assoc_lcos: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
303 |
"[| H <= carrier G; K <= carrier G; x \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
304 |
==> (H #> x) <#> K = H <#> (x <# K)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
305 |
apply (auto simp add: rcos_def r_coset_def lcos_def l_coset_def |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
306 |
setmult_def set_mult_def Sigma_def image_def) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
307 |
apply (force intro!: exI bexI simp add: m_assoc)+ |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
308 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
309 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
310 |
lemma (in coset) rcos_mult_step1: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
311 |
"[| H <| G; x \<in> carrier G; y \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
312 |
==> (H #> x) <#> (H #> y) = (H <#> (x <# H)) #> y" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
313 |
by (simp add: setmult_rcos_assoc normal_imp_subgroup [THEN subgroup.subset] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
314 |
r_coset_subset_G l_coset_subset_G rcos_assoc_lcos) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
315 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
316 |
lemma (in coset) rcos_mult_step2: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
317 |
"[| H <| G; x \<in> carrier G; y \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
318 |
==> (H <#> (x <# H)) #> y = (H <#> (H #> x)) #> y" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
319 |
by (simp add: normal_imp_rcos_eq_lcos) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
320 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
321 |
lemma (in coset) rcos_mult_step3: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
322 |
"[| H <| G; x \<in> carrier G; y \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
323 |
==> (H <#> (H #> x)) #> y = H #> (x \<otimes> y)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
324 |
by (simp add: setmult_rcos_assoc r_coset_subset_G coset_mult_assoc |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
325 |
setmult_subset_G subgroup_mult_id |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
326 |
subgroup.subset normal_imp_subgroup) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
327 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
328 |
lemma (in coset) rcos_sum: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
329 |
"[| H <| G; x \<in> carrier G; y \<in> carrier G |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
330 |
==> (H #> x) <#> (H #> y) = H #> (x \<otimes> y)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
331 |
by (simp add: rcos_mult_step1 rcos_mult_step2 rcos_mult_step3) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
332 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
333 |
(*generalizes subgroup_mult_id*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
334 |
lemma (in coset) setrcos_mult_eq: "[|H <| G; M \<in> rcosets G H|] ==> H <#> M = M" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
335 |
by (auto simp add: setrcos_eq normal_imp_subgroup subgroup.subset |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
336 |
setmult_rcos_assoc subgroup_mult_id) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
337 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
338 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
339 |
subsection{*Lemmas Leading to Lagrange's Theorem*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
340 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
341 |
lemma (in coset) setrcos_part_G: "subgroup H G ==> \<Union> rcosets G H = carrier G" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
342 |
apply (rule equalityI) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
343 |
apply (force simp add: subgroup.subset [THEN subsetD] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
344 |
setrcos_eq r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
345 |
apply (auto simp add: setrcos_eq subgroup.subset rcos_self) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
346 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
347 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
348 |
lemma (in coset) cosets_finite: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
349 |
"[| c \<in> rcosets G H; H <= carrier G; finite (carrier G) |] ==> finite c" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
350 |
apply (auto simp add: setrcos_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
351 |
apply (simp (no_asm_simp) add: r_coset_subset_G [THEN finite_subset]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
352 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
353 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
354 |
text{*The next two lemmas support the proof of @{text card_cosets_equal}, |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
355 |
since we can't use @{text rule_tac} with explicit terms for @{term f} and |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
356 |
@{term g}.*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
357 |
lemma (in coset) inj_on_f: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
358 |
"[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> inv a) (H #> a)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
359 |
apply (rule inj_onI) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
360 |
apply (subgoal_tac "x \<in> carrier G & y \<in> carrier G") |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
361 |
prefer 2 apply (blast intro: r_coset_subset_G [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
362 |
apply (simp add: subsetD) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
363 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
364 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
365 |
lemma (in coset) inj_on_g: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
366 |
"[|H \<subseteq> carrier G; a \<in> carrier G|] ==> inj_on (\<lambda>y. y \<otimes> a) H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
367 |
by (force simp add: inj_on_def subsetD) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
368 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
369 |
lemma (in coset) card_cosets_equal: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
370 |
"[| c \<in> rcosets G H; H <= carrier G; finite(carrier G) |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
371 |
==> card c = card H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
372 |
apply (auto simp add: setrcos_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
373 |
apply (rule card_bij_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
374 |
apply (rule inj_on_f, assumption+) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
375 |
apply (force simp add: m_assoc subsetD r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
376 |
apply (rule inj_on_g, assumption+) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
377 |
apply (force simp add: m_assoc subsetD r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
378 |
txt{*The sets @{term "H #> a"} and @{term "H"} are finite.*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
379 |
apply (simp add: r_coset_subset_G [THEN finite_subset]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
380 |
apply (blast intro: finite_subset) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
381 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
382 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
383 |
subsection{*Two distinct right cosets are disjoint*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
384 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
385 |
lemma (in coset) rcos_equation: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
386 |
"[|subgroup H G; a \<in> carrier G; b \<in> carrier G; ha \<otimes> a = h \<otimes> b; |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
387 |
h \<in> H; ha \<in> H; hb \<in> H|] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
388 |
==> \<exists>h\<in>H. h \<otimes> b = hb \<otimes> a" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
389 |
apply (rule bexI [of _"hb \<otimes> ((inv ha) \<otimes> h)"]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
390 |
apply (simp add: m_assoc transpose_inv subgroup.subset [THEN subsetD]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
391 |
apply (simp add: subgroup.m_closed subgroup.m_inv_closed) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
392 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
393 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
394 |
lemma (in coset) rcos_disjoint: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
395 |
"[|subgroup H G; a \<in> rcosets G H; b \<in> rcosets G H; a\<noteq>b|] ==> a \<inter> b = {}" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
396 |
apply (simp add: setrcos_eq r_coset_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
397 |
apply (blast intro: rcos_equation sym) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
398 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
399 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
400 |
lemma (in coset) setrcos_subset_PowG: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
401 |
"subgroup H G ==> rcosets G H <= Pow(carrier G)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
402 |
apply (simp add: setrcos_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
403 |
apply (blast dest: r_coset_subset_G subgroup.subset) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
404 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
405 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
406 |
subsection {*Factorization of a Group*} |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
407 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
408 |
constdefs |
13936 | 409 |
FactGroup :: "[('a,'b) monoid_scheme, 'a set] => ('a set) monoid" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
410 |
(infixl "Mod" 60) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
411 |
"FactGroup G H == |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
412 |
(| carrier = rcosets G H, |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
413 |
mult = (%X: rcosets G H. %Y: rcosets G H. set_mult G X Y), |
13936 | 414 |
one = H (*, |
415 |
m_inv = (%X: rcosets G H. set_inv G X) *) |)" |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
416 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
417 |
lemma (in coset) setmult_closed: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
418 |
"[| H <| G; K1 \<in> rcosets G H; K2 \<in> rcosets G H |] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
419 |
==> K1 <#> K2 \<in> rcosets G H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
420 |
by (auto simp add: normal_imp_subgroup [THEN subgroup.subset] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
421 |
rcos_sum setrcos_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
422 |
|
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
423 |
lemma (in group) setinv_closed: |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
424 |
"[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H" |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
425 |
by (auto simp add: normal_imp_subgroup |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
426 |
subgroup.subset coset.rcos_inv [OF is_coset] |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
427 |
coset.setrcos_eq [OF is_coset]) |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
428 |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
429 |
(* |
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
430 |
The old version is no longer valid: "group G" has to be an explicit premise. |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
431 |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
432 |
lemma setinv_closed: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
433 |
"[| H <| G; K \<in> rcosets G H |] ==> set_inv G K \<in> rcosets G H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
434 |
by (auto simp add: normal_imp_subgroup |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
435 |
subgroup.subset coset.rcos_inv coset.setrcos_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
436 |
*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
437 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
438 |
lemma (in coset) setrcos_assoc: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
439 |
"[|H <| G; M1 \<in> rcosets G H; M2 \<in> rcosets G H; M3 \<in> rcosets G H|] |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
440 |
==> M1 <#> M2 <#> M3 = M1 <#> (M2 <#> M3)" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
441 |
by (auto simp add: setrcos_eq rcos_sum normal_imp_subgroup |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
442 |
subgroup.subset m_assoc) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
443 |
|
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
444 |
lemma (in group) subgroup_in_rcosets: |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
445 |
"subgroup H G ==> H \<in> rcosets G H" |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
446 |
proof - |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
447 |
assume sub: "subgroup H G" |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
448 |
have "r_coset G H \<one> = H" |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
449 |
by (rule coset.coset_join2) |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
450 |
(auto intro: sub subgroup.one_closed is_coset) |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
451 |
then show ?thesis |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
452 |
by (auto simp add: coset.setrcos_eq [OF is_coset]) |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
453 |
qed |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
454 |
|
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
455 |
(* |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
456 |
lemma subgroup_in_rcosets: |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
457 |
"subgroup H G ==> H \<in> rcosets G H" |
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
458 |
apply (frule subgroup_imp_coset) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
459 |
apply (frule subgroup_imp_group) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
460 |
apply (simp add: coset.setrcos_eq) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
461 |
apply (blast del: equalityI |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
462 |
intro!: group.subgroup.one_closed group.one_closed |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
463 |
coset.coset_join2 [symmetric]) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
464 |
done |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
465 |
*) |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
466 |
|
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
467 |
lemma (in coset) setrcos_inv_mult_group_eq: |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
468 |
"[|H <| G; M \<in> rcosets G H|] ==> set_inv G M <#> M = H" |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
469 |
by (auto simp add: setrcos_eq rcos_inv rcos_sum normal_imp_subgroup |
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
470 |
subgroup.subset) |
13940 | 471 |
(* |
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
472 |
lemma (in group) factorgroup_is_magma: |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
473 |
"H <| G ==> magma (G Mod H)" |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
474 |
by rule (simp add: FactGroup_def coset.setmult_closed [OF is_coset]) |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
475 |
|
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
476 |
lemma (in group) factorgroup_semigroup_axioms: |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
477 |
"H <| G ==> semigroup_axioms (G Mod H)" |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
478 |
by rule (simp add: FactGroup_def coset.setrcos_assoc [OF is_coset] |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
479 |
coset.setmult_closed [OF is_coset]) |
13940 | 480 |
*) |
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
481 |
theorem (in group) factorgroup_is_group: |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
482 |
"H <| G ==> group (G Mod H)" |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
483 |
apply (insert is_coset) |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
484 |
apply (simp add: FactGroup_def) |
13936 | 485 |
apply (rule groupI) |
486 |
apply (simp add: coset.setmult_closed) |
|
487 |
apply (simp add: normal_imp_subgroup subgroup_in_rcosets) |
|
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
488 |
apply (simp add: restrictI coset.setmult_closed coset.setrcos_assoc) |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
489 |
apply (simp add: normal_imp_subgroup |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
490 |
subgroup_in_rcosets coset.setrcos_mult_eq) |
13936 | 491 |
apply (auto dest: coset.setrcos_inv_mult_group_eq simp add: setinv_closed) |
13889
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
492 |
done |
6676ac2527fa
Fixed Coset.thy (proved theorem factorgroup_is_group).
ballarin
parents:
13870
diff
changeset
|
493 |
|
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset
|
494 |
end |