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