# HG changeset patch # User wenzelm # Date 1484661375 -3600 # Node ID 68f0465d956b25113b71b10c4ba1935ccd2fb561 # Parent f0e07600de476cd92bc4ee41f3bdec18f5afbb7b misc tuning and modernization; diff -r f0e07600de47 -r 68f0465d956b src/HOL/Algebra/Sylow.thy --- a/src/HOL/Algebra/Sylow.thy Tue Jan 17 13:59:10 2017 +0100 +++ b/src/HOL/Algebra/Sylow.thy Tue Jan 17 14:56:15 2017 +0100 @@ -3,100 +3,94 @@ *) theory Sylow -imports Coset Exponent + imports Coset Exponent begin -text \ - See also @{cite "Kammueller-Paulson:1999"}. -\ +text \See also @{cite "Kammueller-Paulson:1999"}.\ + +text \The combinatorial argument is in theory @{theory Exponent}.\ -text\The combinatorial argument is in theory Exponent\ - -lemma le_extend_mult: - fixes c::nat shows "\0 < c; a \ b\ \ a \ b * c" -by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero) +lemma le_extend_mult: "\0 < c; a \ b\ \ a \ b * c" + for c :: nat + by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero) locale sylow = group + fixes p and a and m and calM and RelM - assumes prime_p: "prime p" - and order_G: "order(G) = (p^a) * m" - and finite_G [iff]: "finite (carrier G)" - defines "calM == {s. s \ carrier(G) & card(s) = p^a}" - and "RelM == {(N1,N2). N1 \ calM & N2 \ calM & - (\g \ carrier(G). N1 = (N2 #> g) )}" + assumes prime_p: "prime p" + and order_G: "order G = (p^a) * m" + and finite_G[iff]: "finite (carrier G)" + defines "calM \ {s. s \ carrier G \ card s = p^a}" + and "RelM \ {(N1, N2). N1 \ calM \ N2 \ calM \ (\g \ carrier G. N1 = N2 #> g)}" begin lemma RelM_refl_on: "refl_on calM RelM" -apply (auto simp add: refl_on_def RelM_def calM_def) -apply (blast intro!: coset_mult_one [symmetric]) -done + by (auto simp: refl_on_def RelM_def calM_def) (blast intro!: coset_mult_one [symmetric]) lemma RelM_sym: "sym RelM" proof (unfold sym_def RelM_def, clarify) fix y g - assume "y \ calM" + assume "y \ calM" and g: "g \ carrier G" - hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def) - thus "\g'\carrier G. y = y #> g #> g'" by (blast intro: g) + then have "y = y #> g #> (inv g)" + by (simp add: coset_mult_assoc calM_def) + then show "\g'\carrier G. y = y #> g #> g'" + by (blast intro: g) qed lemma RelM_trans: "trans RelM" -by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc) + by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc) lemma RelM_equiv: "equiv calM RelM" -apply (unfold equiv_def) -apply (blast intro: RelM_refl_on RelM_sym RelM_trans) -done + unfolding equiv_def by (blast intro: RelM_refl_on RelM_sym RelM_trans) -lemma M_subset_calM_prep: "M' \ calM // RelM ==> M' \ calM" -apply (unfold RelM_def) -apply (blast elim!: quotientE) -done +lemma M_subset_calM_prep: "M' \ calM // RelM \ M' \ calM" + unfolding RelM_def by (blast elim!: quotientE) end -subsection\Main Part of the Proof\ +subsection \Main Part of the Proof\ locale sylow_central = sylow + fixes H and M1 and M - assumes M_in_quot: "M \ calM // RelM" - and not_dvd_M: "~(p ^ Suc(multiplicity p m) dvd card(M))" - and M1_in_M: "M1 \ M" - defines "H == {g. g\carrier G & M1 #> g = M1}" - + assumes M_in_quot: "M \ calM // RelM" + and not_dvd_M: "\ (p ^ Suc (multiplicity p m) dvd card M)" + and M1_in_M: "M1 \ M" + defines "H \ {g. g \ carrier G \ M1 #> g = M1}" begin lemma M_subset_calM: "M \ calM" by (rule M_in_quot [THEN M_subset_calM_prep]) -lemma card_M1: "card(M1) = p^a" +lemma card_M1: "card M1 = p^a" using M1_in_M M_subset_calM calM_def by blast - + lemma exists_x_in_M1: "\x. x \ M1" -using prime_p [THEN prime_gt_Suc_0_nat] card_M1 -by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI) + using prime_p [THEN prime_gt_Suc_0_nat] card_M1 + by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI) lemma M1_subset_G [simp]: "M1 \ carrier G" - using M1_in_M M_subset_calM calM_def mem_Collect_eq subsetCE by blast + using M1_in_M M_subset_calM calM_def mem_Collect_eq subsetCE by blast lemma M1_inj_H: "\f \ H\M1. inj_on f H" proof - from exists_x_in_M1 obtain m1 where m1M: "m1 \ M1".. - have m1G: "m1 \ carrier G" by (simp add: m1M M1_subset_G [THEN subsetD]) + have m1: "m1 \ carrier G" + by (simp add: m1M M1_subset_G [THEN subsetD]) show ?thesis proof show "inj_on (\z\H. m1 \ z) H" - by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G) + by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1) show "restrict (op \ m1) H \ H \ M1" proof (rule restrictI) - fix z assume zH: "z \ H" + fix z + assume zH: "z \ H" show "m1 \ z \ M1" proof - from zH have zG: "z \ carrier G" and M1zeq: "M1 #> z = M1" by (auto simp add: H_def) show ?thesis - by (rule subst [OF M1zeq], simp add: m1M zG rcosI) + by (rule subst [OF M1zeq]) (simp add: m1M zG rcosI) qed qed qed @@ -104,247 +98,235 @@ end -subsection\Discharging the Assumptions of \sylow_central\\ + +subsection \Discharging the Assumptions of \sylow_central\\ context sylow begin lemma EmptyNotInEquivSet: "{} \ calM // RelM" -by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self]) + by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self]) -lemma existsM1inM: "M \ calM // RelM ==> \M1. M1 \ M" +lemma existsM1inM: "M \ calM // RelM \ \M1. M1 \ M" using RelM_equiv equiv_Eps_in by blast -lemma zero_less_o_G: "0 < order(G)" +lemma zero_less_o_G: "0 < order G" by (simp add: order_def card_gt_0_iff carrier_not_empty) lemma zero_less_m: "m > 0" using zero_less_o_G by (simp add: order_G) -lemma card_calM: "card(calM) = (p^a) * m choose p^a" -by (simp add: calM_def n_subsets order_G [symmetric] order_def) +lemma card_calM: "card calM = (p^a) * m choose p^a" + by (simp add: calM_def n_subsets order_G [symmetric] order_def) lemma zero_less_card_calM: "card calM > 0" -by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m) + by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m) -lemma max_p_div_calM: - "~ (p ^ Suc(multiplicity p m) dvd card(calM))" +lemma max_p_div_calM: "\ (p ^ Suc (multiplicity p m) dvd card calM)" proof assume "p ^ Suc (multiplicity p m) dvd card calM" - with zero_less_card_calM prime_p + with zero_less_card_calM prime_p have "Suc (multiplicity p m) \ multiplicity p (card calM)" by (intro multiplicity_geI) auto - hence "multiplicity p m < multiplicity p (card calM)" by simp + then have "multiplicity p m < multiplicity p (card calM)" by simp also have "multiplicity p m = multiplicity p (card calM)" by (simp add: const_p_fac prime_p zero_less_m card_calM) finally show False by simp qed lemma finite_calM: "finite calM" - unfolding calM_def - by (rule_tac B = "Pow (carrier G) " in finite_subset) auto + unfolding calM_def by (rule finite_subset [where B = "Pow (carrier G)"]) auto -lemma lemma_A1: - "\M \ calM // RelM. ~ (p ^ Suc(multiplicity p m) dvd card(M))" +lemma lemma_A1: "\M \ calM // RelM. \ (p ^ Suc (multiplicity p m) dvd card M)" using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast end -subsubsection\Introduction and Destruct Rules for @{term H}\ + +subsubsection \Introduction and Destruct Rules for \H\\ -lemma (in sylow_central) H_I: "[|g \ carrier G; M1 #> g = M1|] ==> g \ H" -by (simp add: H_def) - -lemma (in sylow_central) H_into_carrier_G: "x \ H ==> x \ carrier G" -by (simp add: H_def) +lemma (in sylow_central) H_I: "\g \ carrier G; M1 #> g = M1\ \ g \ H" + by (simp add: H_def) -lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1" -by (simp add: H_def) +lemma (in sylow_central) H_into_carrier_G: "x \ H \ x \ carrier G" + by (simp add: H_def) -lemma (in sylow_central) H_m_closed: "[| x\H; y\H|] ==> x \ y \ H" -apply (unfold H_def) -apply (simp add: coset_mult_assoc [symmetric]) -done +lemma (in sylow_central) in_H_imp_eq: "g \ H \ M1 #> g = M1" + by (simp add: H_def) + +lemma (in sylow_central) H_m_closed: "\x \ H; y \ H\ \ x \ y \ H" + by (simp add: H_def coset_mult_assoc [symmetric]) lemma (in sylow_central) H_not_empty: "H \ {}" -apply (simp add: H_def) -apply (rule exI [of _ \], simp) -done + apply (simp add: H_def) + apply (rule exI [of _ \]) + apply simp + done lemma (in sylow_central) H_is_subgroup: "subgroup H G" -apply (rule subgroupI) -apply (rule subsetI) -apply (erule H_into_carrier_G) -apply (rule H_not_empty) -apply (simp add: H_def, clarify) -apply (erule_tac P = "%z. lhs(z) = M1" for lhs in subst) -apply (simp add: coset_mult_assoc ) -apply (blast intro: H_m_closed) -done + apply (rule subgroupI) + apply (rule subsetI) + apply (erule H_into_carrier_G) + apply (rule H_not_empty) + apply (simp add: H_def) + apply clarify + apply (erule_tac P = "\z. lhs z = M1" for lhs in subst) + apply (simp add: coset_mult_assoc ) + apply (blast intro: H_m_closed) + done lemma (in sylow_central) rcosetGM1g_subset_G: - "[| g \ carrier G; x \ M1 #> g |] ==> x \ carrier G" -by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD]) + "\g \ carrier G; x \ M1 #> g\ \ x \ carrier G" + by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD]) lemma (in sylow_central) finite_M1: "finite M1" -by (rule finite_subset [OF M1_subset_G finite_G]) + by (rule finite_subset [OF M1_subset_G finite_G]) -lemma (in sylow_central) finite_rcosetGM1g: "g\carrier G ==> finite (M1 #> g)" +lemma (in sylow_central) finite_rcosetGM1g: "g \ carrier G \ finite (M1 #> g)" using rcosetGM1g_subset_G finite_G M1_subset_G cosets_finite rcosetsI by blast -lemma (in sylow_central) M1_cardeq_rcosetGM1g: - "g \ carrier G ==> card(M1 #> g) = card(M1)" -by (simp (no_asm_simp) add: card_cosets_equal rcosetsI) +lemma (in sylow_central) M1_cardeq_rcosetGM1g: "g \ carrier G \ card (M1 #> g) = card M1" + by (simp add: card_cosets_equal rcosetsI) -lemma (in sylow_central) M1_RelM_rcosetGM1g: - "g \ carrier G ==> (M1, M1 #> g) \ RelM" -apply (simp add: RelM_def calM_def card_M1) -apply (rule conjI) - apply (blast intro: rcosetGM1g_subset_G) -apply (simp add: card_M1 M1_cardeq_rcosetGM1g) -apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex) -done +lemma (in sylow_central) M1_RelM_rcosetGM1g: "g \ carrier G \ (M1, M1 #> g) \ RelM" + apply (simp add: RelM_def calM_def card_M1) + apply (rule conjI) + apply (blast intro: rcosetGM1g_subset_G) + apply (simp add: card_M1 M1_cardeq_rcosetGM1g) + apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex) + done -subsection\Equal Cardinalities of @{term M} and the Set of Cosets\ +subsection \Equal Cardinalities of \M\ and the Set of Cosets\ -text\Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that +text \Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that their cardinalities are equal.\ -lemma ElemClassEquiv: - "[| equiv A r; C \ A // r |] ==> \x \ C. \y \ C. (x,y)\r" -by (unfold equiv_def quotient_def sym_def trans_def, blast) +lemma ElemClassEquiv: "\equiv A r; C \ A // r\ \ \x \ C. \y \ C. (x, y) \ r" + unfolding equiv_def quotient_def sym_def trans_def by blast -lemma (in sylow_central) M_elem_map: - "M2 \ M ==> \g. g \ carrier G & M1 #> g = M2" -apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]) -apply (simp add: RelM_def) -apply (blast dest!: bspec) -done +lemma (in sylow_central) M_elem_map: "M2 \ M \ \g. g \ carrier G \ M1 #> g = M2" + using M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]] + by (simp add: RelM_def) (blast dest!: bspec) lemmas (in sylow_central) M_elem_map_carrier = - M_elem_map [THEN someI_ex, THEN conjunct1] + M_elem_map [THEN someI_ex, THEN conjunct1] lemmas (in sylow_central) M_elem_map_eq = - M_elem_map [THEN someI_ex, THEN conjunct2] + M_elem_map [THEN someI_ex, THEN conjunct2] lemma (in sylow_central) M_funcset_rcosets_H: - "(%x:M. H #> (SOME g. g \ carrier G & M1 #> g = x)) \ M \ rcosets H" + "(\x\M. H #> (SOME g. g \ carrier G \ M1 #> g = x)) \ M \ rcosets H" by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset) lemma (in sylow_central) inj_M_GmodH: "\f \ M \ rcosets H. inj_on f M" -apply (rule bexI) -apply (rule_tac [2] M_funcset_rcosets_H) -apply (rule inj_onI, simp) -apply (rule trans [OF _ M_elem_map_eq]) -prefer 2 apply assumption -apply (rule M_elem_map_eq [symmetric, THEN trans], assumption) -apply (rule coset_mult_inv1) -apply (erule_tac [2] M_elem_map_carrier)+ -apply (rule_tac [2] M1_subset_G) -apply (rule coset_join1 [THEN in_H_imp_eq]) -apply (rule_tac [3] H_is_subgroup) -prefer 2 apply (blast intro: M_elem_map_carrier) -apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq) -done + apply (rule bexI) + apply (rule_tac [2] M_funcset_rcosets_H) + apply (rule inj_onI, simp) + apply (rule trans [OF _ M_elem_map_eq]) + prefer 2 apply assumption + apply (rule M_elem_map_eq [symmetric, THEN trans], assumption) + apply (rule coset_mult_inv1) + apply (erule_tac [2] M_elem_map_carrier)+ + apply (rule_tac [2] M1_subset_G) + apply (rule coset_join1 [THEN in_H_imp_eq]) + apply (rule_tac [3] H_is_subgroup) + prefer 2 apply (blast intro: M_elem_map_carrier) + apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq) + done subsubsection\The Opposite Injection\ -lemma (in sylow_central) H_elem_map: - "H1 \ rcosets H ==> \g. g \ carrier G & H #> g = H1" -by (auto simp add: RCOSETS_def) +lemma (in sylow_central) H_elem_map: "H1 \ rcosets H \ \g. g \ carrier G \ H #> g = H1" + by (auto simp: RCOSETS_def) lemmas (in sylow_central) H_elem_map_carrier = - H_elem_map [THEN someI_ex, THEN conjunct1] + H_elem_map [THEN someI_ex, THEN conjunct1] lemmas (in sylow_central) H_elem_map_eq = - H_elem_map [THEN someI_ex, THEN conjunct2] + H_elem_map [THEN someI_ex, THEN conjunct2] lemma (in sylow_central) rcosets_H_funcset_M: "(\C \ rcosets H. M1 #> (@g. g \ carrier G \ H #> g = C)) \ rcosets H \ M" -apply (simp add: RCOSETS_def) -apply (fast intro: someI2 - intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) -done + apply (simp add: RCOSETS_def) + apply (fast intro: someI2 + intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g]) + done -text\close to a duplicate of \inj_M_GmodH\\ -lemma (in sylow_central) inj_GmodH_M: - "\g \ rcosets H\M. inj_on g (rcosets H)" -apply (rule bexI) -apply (rule_tac [2] rcosets_H_funcset_M) -apply (rule inj_onI) -apply (simp) -apply (rule trans [OF _ H_elem_map_eq]) -prefer 2 apply assumption -apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) -apply (rule coset_mult_inv1) -apply (erule_tac [2] H_elem_map_carrier)+ -apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset]) -apply (rule coset_join2) -apply (blast intro: H_elem_map_carrier) -apply (rule H_is_subgroup) -apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier) -done +text \Close to a duplicate of \inj_M_GmodH\.\ +lemma (in sylow_central) inj_GmodH_M: "\g \ rcosets H\M. inj_on g (rcosets H)" + apply (rule bexI) + apply (rule_tac [2] rcosets_H_funcset_M) + apply (rule inj_onI) + apply (simp) + apply (rule trans [OF _ H_elem_map_eq]) + prefer 2 apply assumption + apply (rule H_elem_map_eq [symmetric, THEN trans], assumption) + apply (rule coset_mult_inv1) + apply (erule_tac [2] H_elem_map_carrier)+ + apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset]) + apply (rule coset_join2) + apply (blast intro: H_elem_map_carrier) + apply (rule H_is_subgroup) + apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier) + done -lemma (in sylow_central) calM_subset_PowG: "calM \ Pow(carrier G)" -by (auto simp add: calM_def) +lemma (in sylow_central) calM_subset_PowG: "calM \ Pow (carrier G)" + by (auto simp: calM_def) lemma (in sylow_central) finite_M: "finite M" -by (metis M_subset_calM finite_calM rev_finite_subset) + by (metis M_subset_calM finite_calM rev_finite_subset) -lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)" -apply (insert inj_M_GmodH inj_GmodH_M) -apply (blast intro: card_bij finite_M H_is_subgroup - rcosets_subset_PowG [THEN finite_subset] - finite_Pow_iff [THEN iffD2]) -done +lemma (in sylow_central) cardMeqIndexH: "card M = card (rcosets H)" + apply (insert inj_M_GmodH inj_GmodH_M) + apply (blast intro: card_bij finite_M H_is_subgroup + rcosets_subset_PowG [THEN finite_subset] + finite_Pow_iff [THEN iffD2]) + done -lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)" -by (simp add: cardMeqIndexH lagrange H_is_subgroup) +lemma (in sylow_central) index_lem: "card M * card H = order G" + by (simp add: cardMeqIndexH lagrange H_is_subgroup) -lemma (in sylow_central) lemma_leq1: "p^a \ card(H)" -apply (rule dvd_imp_le) - apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M]) - prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup) -apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd - zero_less_m) -done +lemma (in sylow_central) lemma_leq1: "p^a \ card H" + apply (rule dvd_imp_le) + apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M]) + prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup) + apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd zero_less_m) + done -lemma (in sylow_central) lemma_leq2: "card(H) \ p^a" -apply (subst card_M1 [symmetric]) -apply (cut_tac M1_inj_H) -apply (blast intro!: M1_subset_G intro: - card_inj H_into_carrier_G finite_subset [OF _ finite_G]) -done +lemma (in sylow_central) lemma_leq2: "card H \ p^a" + apply (subst card_M1 [symmetric]) + apply (cut_tac M1_inj_H) + apply (blast intro!: M1_subset_G intro: card_inj H_into_carrier_G finite_subset [OF _ finite_G]) + done -lemma (in sylow_central) card_H_eq: "card(H) = p^a" -by (blast intro: le_antisym lemma_leq1 lemma_leq2) +lemma (in sylow_central) card_H_eq: "card H = p^a" + by (blast intro: le_antisym lemma_leq1 lemma_leq2) -lemma (in sylow) sylow_thm: "\H. subgroup H G & card(H) = p^a" -apply (cut_tac lemma_A1, clarify) -apply (frule existsM1inM, clarify) -apply (subgoal_tac "sylow_central G p a m M1 M") - apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq) -apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def) -done +lemma (in sylow) sylow_thm: "\H. subgroup H G \ card H = p^a" + using lemma_A1 + apply clarify + apply (frule existsM1inM, clarify) + apply (subgoal_tac "sylow_central G p a m M1 M") + apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq) + apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def) + done -text\Needed because the locale's automatic definition refers to - @{term "semigroup G"} and @{term "group_axioms G"} rather than +text \Needed because the locale's automatic definition refers to + @{term "semigroup G"} and @{term "group_axioms G"} rather than simply to @{term "group G"}.\ -lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)" -by (simp add: sylow_def group_def) +lemma sylow_eq: "sylow G p a m \ group G \ sylow_axioms G p a m" + by (simp add: sylow_def group_def) subsection \Sylow's Theorem\ theorem sylow_thm: - "[| prime p; group(G); order(G) = (p^a) * m; finite (carrier G)|] - ==> \H. subgroup H G & card(H) = p^a" -apply (rule sylow.sylow_thm [of G p a m]) -apply (simp add: sylow_eq sylow_axioms_def) -done + "\prime p; group G; order G = (p^a) * m; finite (carrier G)\ + \ \H. subgroup H G \ card H = p^a" + by (rule sylow.sylow_thm [of G p a m]) (simp add: sylow_eq sylow_axioms_def) end