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