src/HOL/Algebra/Sylow.thy
 author wenzelm Sat Oct 10 16:26:23 2015 +0200 (2015-10-10) changeset 61382 efac889fccbc parent 59807 22bc39064290 child 62410 2fc7a8d9c529 permissions -rw-r--r--
isabelle update_cartouches;
 wenzelm@14706 ` 1` ```(* Title: HOL/Algebra/Sylow.thy ``` paulson@13870 ` 2` ``` Author: Florian Kammueller, with new proofs by L C Paulson ``` paulson@13870 ` 3` ```*) ``` paulson@13870 ` 4` wenzelm@35849 ` 5` ```theory Sylow ``` wenzelm@35849 ` 6` ```imports Coset Exponent ``` wenzelm@35849 ` 7` ```begin ``` paulson@13870 ` 8` wenzelm@61382 ` 9` ```text \ ``` wenzelm@58622 ` 10` ``` See also @{cite "Kammueller-Paulson:1999"}. ``` wenzelm@61382 ` 11` ```\ ``` wenzelm@14706 ` 12` wenzelm@61382 ` 13` ```text\The combinatorial argument is in theory Exponent\ ``` paulson@13870 ` 14` paulson@14747 ` 15` ```locale sylow = group + ``` paulson@13870 ` 16` ``` fixes p and a and m and calM and RelM ``` nipkow@16663 ` 17` ``` assumes prime_p: "prime p" ``` paulson@13870 ` 18` ``` and order_G: "order(G) = (p^a) * m" ``` paulson@13870 ` 19` ``` and finite_G [iff]: "finite (carrier G)" ``` paulson@14747 ` 20` ``` defines "calM == {s. s \ carrier(G) & card(s) = p^a}" ``` paulson@13870 ` 21` ``` and "RelM == {(N1,N2). N1 \ calM & N2 \ calM & ``` wenzelm@14666 ` 22` ``` (\g \ carrier(G). N1 = (N2 #> g) )}" ``` paulson@13870 ` 23` nipkow@30198 ` 24` ```lemma (in sylow) RelM_refl_on: "refl_on calM RelM" ``` nipkow@30198 ` 25` ```apply (auto simp add: refl_on_def RelM_def calM_def) ``` wenzelm@14666 ` 26` ```apply (blast intro!: coset_mult_one [symmetric]) ``` paulson@13870 ` 27` ```done ``` paulson@13870 ` 28` paulson@13870 ` 29` ```lemma (in sylow) RelM_sym: "sym RelM" ``` paulson@13870 ` 30` ```proof (unfold sym_def RelM_def, clarify) ``` paulson@13870 ` 31` ``` fix y g ``` paulson@13870 ` 32` ``` assume "y \ calM" ``` paulson@13870 ` 33` ``` and g: "g \ carrier G" ``` paulson@13870 ` 34` ``` hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def) ``` wenzelm@41541 ` 35` ``` thus "\g'\carrier G. y = y #> g #> g'" by (blast intro: g) ``` paulson@13870 ` 36` ```qed ``` paulson@13870 ` 37` paulson@13870 ` 38` ```lemma (in sylow) RelM_trans: "trans RelM" ``` wenzelm@14666 ` 39` ```by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc) ``` paulson@13870 ` 40` paulson@13870 ` 41` ```lemma (in sylow) RelM_equiv: "equiv calM RelM" ``` paulson@13870 ` 42` ```apply (unfold equiv_def) ``` nipkow@30198 ` 43` ```apply (blast intro: RelM_refl_on RelM_sym RelM_trans) ``` paulson@13870 ` 44` ```done ``` paulson@13870 ` 45` paulson@14747 ` 46` ```lemma (in sylow) M_subset_calM_prep: "M' \ calM // RelM ==> M' \ calM" ``` paulson@13870 ` 47` ```apply (unfold RelM_def) ``` paulson@13870 ` 48` ```apply (blast elim!: quotientE) ``` paulson@13870 ` 49` ```done ``` paulson@13870 ` 50` ballarin@20318 ` 51` wenzelm@61382 ` 52` ```subsection\Main Part of the Proof\ ``` paulson@13870 ` 53` paulson@13870 ` 54` ```locale sylow_central = sylow + ``` paulson@13870 ` 55` ``` fixes H and M1 and M ``` paulson@13870 ` 56` ``` assumes M_in_quot: "M \ calM // RelM" ``` paulson@13870 ` 57` ``` and not_dvd_M: "~(p ^ Suc(exponent p m) dvd card(M))" ``` paulson@13870 ` 58` ``` and M1_in_M: "M1 \ M" ``` paulson@13870 ` 59` ``` defines "H == {g. g\carrier G & M1 #> g = M1}" ``` paulson@13870 ` 60` paulson@14747 ` 61` ```lemma (in sylow_central) M_subset_calM: "M \ calM" ``` paulson@13870 ` 62` ```by (rule M_in_quot [THEN M_subset_calM_prep]) ``` paulson@13870 ` 63` paulson@13870 ` 64` ```lemma (in sylow_central) card_M1: "card(M1) = p^a" ``` paulson@13870 ` 65` ```apply (cut_tac M_subset_calM M1_in_M) ``` paulson@13870 ` 66` ```apply (simp add: calM_def, blast) ``` paulson@13870 ` 67` ```done ``` paulson@13870 ` 68` paulson@13870 ` 69` ```lemma card_nonempty: "0 < card(S) ==> S \ {}" ``` paulson@13870 ` 70` ```by force ``` paulson@13870 ` 71` wenzelm@14666 ` 72` ```lemma (in sylow_central) exists_x_in_M1: "\x. x\M1" ``` wenzelm@14666 ` 73` ```apply (subgoal_tac "0 < card M1") ``` wenzelm@14666 ` 74` ``` apply (blast dest: card_nonempty) ``` lp15@55157 ` 75` ```apply (cut_tac prime_p [THEN prime_gt_Suc_0_nat]) ``` paulson@13870 ` 76` ```apply (simp (no_asm_simp) add: card_M1) ``` paulson@13870 ` 77` ```done ``` paulson@13870 ` 78` paulson@14747 ` 79` ```lemma (in sylow_central) M1_subset_G [simp]: "M1 \ carrier G" ``` paulson@13870 ` 80` ```apply (rule subsetD [THEN PowD]) ``` paulson@13870 ` 81` ```apply (rule_tac [2] M1_in_M) ``` paulson@13870 ` 82` ```apply (rule M_subset_calM [THEN subset_trans]) ``` paulson@13870 ` 83` ```apply (auto simp add: calM_def) ``` paulson@13870 ` 84` ```done ``` paulson@13870 ` 85` paulson@13870 ` 86` ```lemma (in sylow_central) M1_inj_H: "\f \ H\M1. inj_on f H" ``` paulson@13870 ` 87` ``` proof - ``` paulson@13870 ` 88` ``` from exists_x_in_M1 obtain m1 where m1M: "m1 \ M1".. ``` paulson@13870 ` 89` ``` have m1G: "m1 \ carrier G" by (simp add: m1M M1_subset_G [THEN subsetD]) ``` paulson@13870 ` 90` ``` show ?thesis ``` paulson@13870 ` 91` ``` proof ``` paulson@13870 ` 92` ``` show "inj_on (\z\H. m1 \ z) H" ``` wenzelm@14666 ` 93` ``` by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G) ``` paulson@13870 ` 94` ``` show "restrict (op \ m1) H \ H \ M1" ``` paulson@13870 ` 95` ``` proof (rule restrictI) ``` wenzelm@14666 ` 96` ``` fix z assume zH: "z \ H" ``` wenzelm@14666 ` 97` ``` show "m1 \ z \ M1" ``` wenzelm@14666 ` 98` ``` proof - ``` wenzelm@14666 ` 99` ``` from zH ``` wenzelm@14666 ` 100` ``` have zG: "z \ carrier G" and M1zeq: "M1 #> z = M1" ``` wenzelm@14666 ` 101` ``` by (auto simp add: H_def) ``` wenzelm@14666 ` 102` ``` show ?thesis ``` wenzelm@14666 ` 103` ``` by (rule subst [OF M1zeq], simp add: m1M zG rcosI) ``` wenzelm@14666 ` 104` ``` qed ``` paulson@13870 ` 105` ``` qed ``` paulson@13870 ` 106` ``` qed ``` paulson@13870 ` 107` ``` qed ``` paulson@13870 ` 108` paulson@13870 ` 109` wenzelm@61382 ` 110` ```subsection\Discharging the Assumptions of @{text sylow_central}\ ``` paulson@13870 ` 111` paulson@13870 ` 112` ```lemma (in sylow) EmptyNotInEquivSet: "{} \ calM // RelM" ``` paulson@13870 ` 113` ```by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self]) ``` paulson@13870 ` 114` paulson@13870 ` 115` ```lemma (in sylow) existsM1inM: "M \ calM // RelM ==> \M1. M1 \ M" ``` wenzelm@14666 ` 116` ```apply (subgoal_tac "M \ {}") ``` wenzelm@14666 ` 117` ``` apply blast ``` paulson@13870 ` 118` ```apply (cut_tac EmptyNotInEquivSet, blast) ``` paulson@13870 ` 119` ```done ``` paulson@13870 ` 120` paulson@13870 ` 121` ```lemma (in sylow) zero_less_o_G: "0 < order(G)" ``` paulson@13870 ` 122` ```apply (unfold order_def) ``` wenzelm@41541 ` 123` ```apply (blast intro: zero_less_card_empty) ``` paulson@13870 ` 124` ```done ``` paulson@13870 ` 125` nipkow@25162 ` 126` ```lemma (in sylow) zero_less_m: "m > 0" ``` paulson@13870 ` 127` ```apply (cut_tac zero_less_o_G) ``` paulson@13870 ` 128` ```apply (simp add: order_G) ``` paulson@13870 ` 129` ```done ``` paulson@13870 ` 130` paulson@13870 ` 131` ```lemma (in sylow) card_calM: "card(calM) = (p^a) * m choose p^a" ``` paulson@13870 ` 132` ```by (simp add: calM_def n_subsets order_G [symmetric] order_def) ``` paulson@13870 ` 133` nipkow@25162 ` 134` ```lemma (in sylow) zero_less_card_calM: "card calM > 0" ``` paulson@13870 ` 135` ```by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m) ``` paulson@13870 ` 136` paulson@13870 ` 137` ```lemma (in sylow) max_p_div_calM: ``` paulson@13870 ` 138` ``` "~ (p ^ Suc(exponent p m) dvd card(calM))" ``` paulson@13870 ` 139` ```apply (subgoal_tac "exponent p m = exponent p (card calM) ") ``` paulson@13870 ` 140` ``` apply (cut_tac zero_less_card_calM prime_p) ``` paulson@13870 ` 141` ``` apply (force dest: power_Suc_exponent_Not_dvd) ``` paulson@13870 ` 142` ```apply (simp add: card_calM zero_less_m [THEN const_p_fac]) ``` paulson@13870 ` 143` ```done ``` paulson@13870 ` 144` paulson@13870 ` 145` ```lemma (in sylow) finite_calM: "finite calM" ``` paulson@13870 ` 146` ```apply (unfold calM_def) ``` paulson@13870 ` 147` ```apply (rule_tac B = "Pow (carrier G) " in finite_subset) ``` paulson@13870 ` 148` ```apply auto ``` paulson@13870 ` 149` ```done ``` paulson@13870 ` 150` paulson@13870 ` 151` ```lemma (in sylow) lemma_A1: ``` paulson@13870 ` 152` ``` "\M \ calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))" ``` paulson@13870 ` 153` ```apply (rule max_p_div_calM [THEN contrapos_np]) ``` paulson@13870 ` 154` ```apply (simp add: finite_calM equiv_imp_dvd_card [OF _ RelM_equiv]) ``` paulson@13870 ` 155` ```done ``` paulson@13870 ` 156` paulson@13870 ` 157` wenzelm@61382 ` 158` ```subsubsection\Introduction and Destruct Rules for @{term H}\ ``` paulson@13870 ` 159` paulson@13870 ` 160` ```lemma (in sylow_central) H_I: "[|g \ carrier G; M1 #> g = M1|] ==> g \ H" ``` paulson@13870 ` 161` ```by (simp add: H_def) ``` paulson@13870 ` 162` paulson@13870 ` 163` ```lemma (in sylow_central) H_into_carrier_G: "x \ H ==> x \ carrier G" ``` paulson@13870 ` 164` ```by (simp add: H_def) ``` paulson@13870 ` 165` paulson@13870 ` 166` ```lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1" ``` paulson@13870 ` 167` ```by (simp add: H_def) ``` paulson@13870 ` 168` paulson@13870 ` 169` ```lemma (in sylow_central) H_m_closed: "[| x\H; y\H|] ==> x \ y \ H" ``` paulson@13870 ` 170` ```apply (unfold H_def) ``` wenzelm@41541 ` 171` ```apply (simp add: coset_mult_assoc [symmetric]) ``` paulson@13870 ` 172` ```done ``` paulson@13870 ` 173` paulson@13870 ` 174` ```lemma (in sylow_central) H_not_empty: "H \ {}" ``` paulson@13870 ` 175` ```apply (simp add: H_def) ``` paulson@13870 ` 176` ```apply (rule exI [of _ \], simp) ``` paulson@13870 ` 177` ```done ``` paulson@13870 ` 178` paulson@13870 ` 179` ```lemma (in sylow_central) H_is_subgroup: "subgroup H G" ``` paulson@13870 ` 180` ```apply (rule subgroupI) ``` paulson@13870 ` 181` ```apply (rule subsetI) ``` paulson@13870 ` 182` ```apply (erule H_into_carrier_G) ``` paulson@13870 ` 183` ```apply (rule H_not_empty) ``` paulson@13870 ` 184` ```apply (simp add: H_def, clarify) ``` wenzelm@59807 ` 185` ```apply (erule_tac P = "%z. lhs(z) = M1" for lhs in subst) ``` paulson@13870 ` 186` ```apply (simp add: coset_mult_assoc ) ``` paulson@13870 ` 187` ```apply (blast intro: H_m_closed) ``` paulson@13870 ` 188` ```done ``` paulson@13870 ` 189` paulson@13870 ` 190` paulson@13870 ` 191` ```lemma (in sylow_central) rcosetGM1g_subset_G: ``` paulson@13870 ` 192` ``` "[| g \ carrier G; x \ M1 #> g |] ==> x \ carrier G" ``` paulson@13870 ` 193` ```by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD]) ``` paulson@13870 ` 194` paulson@13870 ` 195` ```lemma (in sylow_central) finite_M1: "finite M1" ``` paulson@13870 ` 196` ```by (rule finite_subset [OF M1_subset_G finite_G]) ``` paulson@13870 ` 197` paulson@13870 ` 198` ```lemma (in sylow_central) finite_rcosetGM1g: "g\carrier G ==> finite (M1 #> g)" ``` paulson@13870 ` 199` ```apply (rule finite_subset) ``` paulson@13870 ` 200` ```apply (rule subsetI) ``` paulson@13870 ` 201` ```apply (erule rcosetGM1g_subset_G, assumption) ``` paulson@13870 ` 202` ```apply (rule finite_G) ``` paulson@13870 ` 203` ```done ``` paulson@13870 ` 204` paulson@13870 ` 205` ```lemma (in sylow_central) M1_cardeq_rcosetGM1g: ``` paulson@13870 ` 206` ``` "g \ carrier G ==> card(M1 #> g) = card(M1)" ``` wenzelm@41541 ` 207` ```by (simp (no_asm_simp) add: card_cosets_equal rcosetsI) ``` paulson@13870 ` 208` paulson@13870 ` 209` ```lemma (in sylow_central) M1_RelM_rcosetGM1g: ``` paulson@13870 ` 210` ``` "g \ carrier G ==> (M1, M1 #> g) \ RelM" ``` lp15@55157 ` 211` ```apply (simp add: RelM_def calM_def card_M1) ``` paulson@13870 ` 212` ```apply (rule conjI) ``` paulson@13870 ` 213` ``` apply (blast intro: rcosetGM1g_subset_G) ``` lp15@55157 ` 214` ```apply (simp add: card_M1 M1_cardeq_rcosetGM1g) ``` lp15@55157 ` 215` ```apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex) ``` paulson@13870 ` 216` ```done ``` paulson@13870 ` 217` paulson@13870 ` 218` wenzelm@61382 ` 219` ```subsection\Equal Cardinalities of @{term M} and the Set of Cosets\ ``` paulson@13870 ` 220` wenzelm@61382 ` 221` ```text\Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that ``` wenzelm@61382 ` 222` ``` their cardinalities are equal.\ ``` paulson@13870 ` 223` wenzelm@14666 ` 224` ```lemma ElemClassEquiv: ``` paulson@14963 ` 225` ``` "[| equiv A r; C \ A // r |] ==> \x \ C. \y \ C. (x,y)\r" ``` paulson@14963 ` 226` ```by (unfold equiv_def quotient_def sym_def trans_def, blast) ``` paulson@13870 ` 227` paulson@13870 ` 228` ```lemma (in sylow_central) M_elem_map: ``` paulson@13870 ` 229` ``` "M2 \ M ==> \g. g \ carrier G & M1 #> g = M2" ``` paulson@13870 ` 230` ```apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]) ``` paulson@13870 ` 231` ```apply (simp add: RelM_def) ``` paulson@13870 ` 232` ```apply (blast dest!: bspec) ``` paulson@13870 ` 233` ```done ``` paulson@13870 ` 234` wenzelm@14666 ` 235` ```lemmas (in sylow_central) M_elem_map_carrier = ``` wenzelm@14666 ` 236` ``` M_elem_map [THEN someI_ex, THEN conjunct1] ``` paulson@13870 ` 237` paulson@13870 ` 238` ```lemmas (in sylow_central) M_elem_map_eq = ``` wenzelm@14666 ` 239` ``` M_elem_map [THEN someI_ex, THEN conjunct2] ``` paulson@13870 ` 240` paulson@14963 ` 241` ```lemma (in sylow_central) M_funcset_rcosets_H: ``` paulson@14963 ` 242` ``` "(%x:M. H #> (SOME g. g \ carrier G & M1 #> g = x)) \ M \ rcosets H" ``` lp15@55157 ` 243` ``` by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset) ``` paulson@13870 ` 244` paulson@14963 ` 245` ```lemma (in sylow_central) inj_M_GmodH: "\f \ M\rcosets H. inj_on f M" ``` paulson@13870 ` 246` ```apply (rule bexI) ``` paulson@14963 ` 247` ```apply (rule_tac [2] M_funcset_rcosets_H) ``` paulson@13870 ` 248` ```apply (rule inj_onI, simp) ``` paulson@13870 ` 249` ```apply (rule trans [OF _ M_elem_map_eq]) ``` paulson@13870 ` 250` ```prefer 2 apply assumption ``` paulson@13870 ` 251` ```apply (rule M_elem_map_eq [symmetric, THEN trans], assumption) ``` paulson@13870 ` 252` ```apply (rule coset_mult_inv1) ``` paulson@13870 ` 253` ```apply (erule_tac [2] M_elem_map_carrier)+ ``` paulson@13870 ` 254` ```apply (rule_tac [2] M1_subset_G) ``` paulson@13870 ` 255` ```apply (rule coset_join1 [THEN in_H_imp_eq]) ``` paulson@13870 ` 256` ```apply (rule_tac [3] H_is_subgroup) ``` wenzelm@41541 ` 257` ```prefer 2 apply (blast intro: M_elem_map_carrier) ``` berghofe@26806 ` 258` ```apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq) ``` paulson@13870 ` 259` ```done ``` paulson@13870 ` 260` paulson@13870 ` 261` wenzelm@61382 ` 262` ```subsubsection\The Opposite Injection\ ``` paulson@13870 ` 263` paulson@13870 ` 264` ```lemma (in sylow_central) H_elem_map: ``` paulson@14963 ` 265` ``` "H1 \ rcosets H ==> \g. g \ carrier G & H #> g = H1" ``` paulson@14963 ` 266` ```by (auto simp add: RCOSETS_def) ``` paulson@13870 ` 267` wenzelm@14666 ` 268` ```lemmas (in sylow_central) H_elem_map_carrier = ``` wenzelm@14666 ` 269` ``` H_elem_map [THEN someI_ex, THEN conjunct1] ``` paulson@13870 ` 270` paulson@13870 ` 271` ```lemmas (in sylow_central) H_elem_map_eq = ``` wenzelm@14666 ` 272` ``` H_elem_map [THEN someI_ex, THEN conjunct2] ``` paulson@13870 ` 273` paulson@14963 ` 274` ```lemma (in sylow_central) rcosets_H_funcset_M: ``` paulson@14963 ` 275` ``` "(\C \ rcosets H. M1 #> (@g. g \ carrier G \ H #> g = C)) \ rcosets H \ M" ``` paulson@14963 ` 276` ```apply (simp add: RCOSETS_def) ``` paulson@13870 ` 277` ```apply (fast intro: someI2 ``` lp15@55157 ` 278` ``` intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) ``` paulson@13870 ` 279` ```done ``` paulson@13870 ` 280` wenzelm@61382 ` 281` ```text\close to a duplicate of @{text inj_M_GmodH}\ ``` paulson@13870 ` 282` ```lemma (in sylow_central) inj_GmodH_M: ``` paulson@14963 ` 283` ``` "\g \ rcosets H\M. inj_on g (rcosets H)" ``` paulson@13870 ` 284` ```apply (rule bexI) ``` paulson@14963 ` 285` ```apply (rule_tac [2] rcosets_H_funcset_M) ``` paulson@13870 ` 286` ```apply (rule inj_onI) ``` paulson@13870 ` 287` ```apply (simp) ``` paulson@13870 ` 288` ```apply (rule trans [OF _ H_elem_map_eq]) ``` paulson@13870 ` 289` ```prefer 2 apply assumption ``` paulson@13870 ` 290` ```apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) ``` paulson@13870 ` 291` ```apply (rule coset_mult_inv1) ``` paulson@13870 ` 292` ```apply (erule_tac [2] H_elem_map_carrier)+ ``` paulson@13870 ` 293` ```apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset]) ``` paulson@13870 ` 294` ```apply (rule coset_join2) ``` wenzelm@41541 ` 295` ```apply (blast intro: H_elem_map_carrier) ``` wenzelm@14666 ` 296` ```apply (rule H_is_subgroup) ``` wenzelm@41541 ` 297` ```apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier) ``` paulson@13870 ` 298` ```done ``` paulson@13870 ` 299` paulson@14747 ` 300` ```lemma (in sylow_central) calM_subset_PowG: "calM \ Pow(carrier G)" ``` paulson@13870 ` 301` ```by (auto simp add: calM_def) ``` paulson@13870 ` 302` paulson@13870 ` 303` paulson@13870 ` 304` ```lemma (in sylow_central) finite_M: "finite M" ``` lp15@55157 ` 305` ```by (metis M_subset_calM finite_calM rev_finite_subset) ``` paulson@13870 ` 306` paulson@14963 ` 307` ```lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)" ``` wenzelm@14666 ` 308` ```apply (insert inj_M_GmodH inj_GmodH_M) ``` wenzelm@14666 ` 309` ```apply (blast intro: card_bij finite_M H_is_subgroup ``` paulson@14963 ` 310` ``` rcosets_subset_PowG [THEN finite_subset] ``` paulson@13870 ` 311` ``` finite_Pow_iff [THEN iffD2]) ``` paulson@13870 ` 312` ```done ``` paulson@13870 ` 313` paulson@13870 ` 314` ```lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)" ``` paulson@13870 ` 315` ```by (simp add: cardMeqIndexH lagrange H_is_subgroup) ``` paulson@13870 ` 316` paulson@14747 ` 317` ```lemma (in sylow_central) lemma_leq1: "p^a \ card(H)" ``` paulson@13870 ` 318` ```apply (rule dvd_imp_le) ``` paulson@13870 ` 319` ``` apply (rule div_combine [OF prime_p not_dvd_M]) ``` paulson@13870 ` 320` ``` prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup) ``` paulson@13870 ` 321` ```apply (simp add: index_lem order_G power_add mult_dvd_mono power_exponent_dvd ``` paulson@13870 ` 322` ``` zero_less_m) ``` paulson@13870 ` 323` ```done ``` paulson@13870 ` 324` paulson@14747 ` 325` ```lemma (in sylow_central) lemma_leq2: "card(H) \ p^a" ``` paulson@13870 ` 326` ```apply (subst card_M1 [symmetric]) ``` paulson@13870 ` 327` ```apply (cut_tac M1_inj_H) ``` wenzelm@14666 ` 328` ```apply (blast intro!: M1_subset_G intro: ``` paulson@13870 ` 329` ``` card_inj H_into_carrier_G finite_subset [OF _ finite_G]) ``` paulson@13870 ` 330` ```done ``` paulson@13870 ` 331` paulson@13870 ` 332` ```lemma (in sylow_central) card_H_eq: "card(H) = p^a" ``` nipkow@33657 ` 333` ```by (blast intro: le_antisym lemma_leq1 lemma_leq2) ``` paulson@13870 ` 334` paulson@13870 ` 335` ```lemma (in sylow) sylow_thm: "\H. subgroup H G & card(H) = p^a" ``` wenzelm@14666 ` 336` ```apply (cut_tac lemma_A1, clarify) ``` wenzelm@14666 ` 337` ```apply (frule existsM1inM, clarify) ``` paulson@13870 ` 338` ```apply (subgoal_tac "sylow_central G p a m M1 M") ``` paulson@13870 ` 339` ``` apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq) ``` wenzelm@41541 ` 340` ```apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def) ``` paulson@13870 ` 341` ```done ``` paulson@13870 ` 342` wenzelm@61382 ` 343` ```text\Needed because the locale's automatic definition refers to ``` wenzelm@14666 ` 344` ``` @{term "semigroup G"} and @{term "group_axioms G"} rather than ``` wenzelm@61382 ` 345` ``` simply to @{term "group G"}.\ ``` paulson@13870 ` 346` ```lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)" ``` paulson@13870 ` 347` ```by (simp add: sylow_def group_def) ``` paulson@13870 ` 348` ballarin@20318 ` 349` wenzelm@61382 ` 350` ```subsection \Sylow's Theorem\ ``` ballarin@20318 ` 351` paulson@13870 ` 352` ```theorem sylow_thm: ``` nipkow@16663 ` 353` ``` "[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|] ``` paulson@13870 ` 354` ``` ==> \H. subgroup H G & card(H) = p^a" ``` paulson@13870 ` 355` ```apply (rule sylow.sylow_thm [of G p a m]) ``` wenzelm@14666 ` 356` ```apply (simp add: sylow_eq sylow_axioms_def) ``` paulson@13870 ` 357` ```done ``` paulson@13870 ` 358` paulson@13870 ` 359` ```end ```