author wenzelm Tue Jan 17 14:56:15 2017 +0100 (2017-01-17) changeset 64912 68f0465d956b parent 64911 f0e07600de47 child 64913 3a9eb793fa10
misc tuning and modernization;
```     1.1 --- a/src/HOL/Algebra/Sylow.thy	Tue Jan 17 13:59:10 2017 +0100
1.2 +++ b/src/HOL/Algebra/Sylow.thy	Tue Jan 17 14:56:15 2017 +0100
1.3 @@ -3,100 +3,94 @@
1.4  *)
1.5
1.6  theory Sylow
1.7 -imports Coset Exponent
1.8 +  imports Coset Exponent
1.9  begin
1.10
1.11 -text \<open>
1.13 -\<close>
1.15 +
1.16 +text \<open>The combinatorial argument is in theory @{theory Exponent}.\<close>
1.17
1.18 -text\<open>The combinatorial argument is in theory Exponent\<close>
1.19 -
1.20 -lemma le_extend_mult:
1.21 -  fixes c::nat shows "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
1.22 -by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero)
1.23 +lemma le_extend_mult: "\<lbrakk>0 < c; a \<le> b\<rbrakk> \<Longrightarrow> a \<le> b * c"
1.24 +  for c :: nat
1.25 +  by (metis divisors_zero dvd_triv_left leI less_le_trans nat_dvd_not_less zero_less_iff_neq_zero)
1.26
1.27  locale sylow = group +
1.28    fixes p and a and m and calM and RelM
1.29 -  assumes prime_p:   "prime p"
1.30 -      and order_G:   "order(G) = (p^a) * m"
1.31 -      and finite_G [iff]:  "finite (carrier G)"
1.32 -  defines "calM == {s. s \<subseteq> carrier(G) & card(s) = p^a}"
1.33 -      and "RelM == {(N1,N2). N1 \<in> calM & N2 \<in> calM &
1.34 -                             (\<exists>g \<in> carrier(G). N1 = (N2 #> g) )}"
1.35 +  assumes prime_p: "prime p"
1.36 +    and order_G: "order G = (p^a) * m"
1.37 +    and finite_G[iff]: "finite (carrier G)"
1.38 +  defines "calM \<equiv> {s. s \<subseteq> carrier G \<and> card s = p^a}"
1.39 +    and "RelM \<equiv> {(N1, N2). N1 \<in> calM \<and> N2 \<in> calM \<and> (\<exists>g \<in> carrier G. N1 = N2 #> g)}"
1.40  begin
1.41
1.42  lemma RelM_refl_on: "refl_on calM RelM"
1.43 -apply (auto simp add: refl_on_def RelM_def calM_def)
1.44 -apply (blast intro!: coset_mult_one [symmetric])
1.45 -done
1.46 +  by (auto simp: refl_on_def RelM_def calM_def) (blast intro!: coset_mult_one [symmetric])
1.47
1.48  lemma RelM_sym: "sym RelM"
1.49  proof (unfold sym_def RelM_def, clarify)
1.50    fix y g
1.51 -  assume   "y \<in> calM"
1.52 +  assume "y \<in> calM"
1.53      and g: "g \<in> carrier G"
1.54 -  hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def)
1.55 -  thus "\<exists>g'\<in>carrier G. y = y #> g #> g'" by (blast intro: g)
1.56 +  then have "y = y #> g #> (inv g)"
1.57 +    by (simp add: coset_mult_assoc calM_def)
1.58 +  then show "\<exists>g'\<in>carrier G. y = y #> g #> g'"
1.59 +    by (blast intro: g)
1.60  qed
1.61
1.62  lemma RelM_trans: "trans RelM"
1.63 -by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
1.64 +  by (auto simp add: trans_def RelM_def calM_def coset_mult_assoc)
1.65
1.66  lemma RelM_equiv: "equiv calM RelM"
1.67 -apply (unfold equiv_def)
1.68 -apply (blast intro: RelM_refl_on RelM_sym RelM_trans)
1.69 -done
1.70 +  unfolding equiv_def by (blast intro: RelM_refl_on RelM_sym RelM_trans)
1.71
1.72 -lemma M_subset_calM_prep: "M' \<in> calM // RelM  ==> M' \<subseteq> calM"
1.73 -apply (unfold RelM_def)
1.74 -apply (blast elim!: quotientE)
1.75 -done
1.76 +lemma M_subset_calM_prep: "M' \<in> calM // RelM  \<Longrightarrow> M' \<subseteq> calM"
1.77 +  unfolding RelM_def by (blast elim!: quotientE)
1.78
1.79  end
1.80
1.81 -subsection\<open>Main Part of the Proof\<close>
1.82 +subsection \<open>Main Part of the Proof\<close>
1.83
1.84  locale sylow_central = sylow +
1.85    fixes H and M1 and M
1.86 -  assumes M_in_quot:  "M \<in> calM // RelM"
1.87 -      and not_dvd_M:  "~(p ^ Suc(multiplicity p m) dvd card(M))"
1.88 -      and M1_in_M:    "M1 \<in> M"
1.89 -  defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
1.90 -
1.91 +  assumes M_in_quot: "M \<in> calM // RelM"
1.92 +    and not_dvd_M: "\<not> (p ^ Suc (multiplicity p m) dvd card M)"
1.93 +    and M1_in_M: "M1 \<in> M"
1.94 +  defines "H \<equiv> {g. g \<in> carrier G \<and> M1 #> g = M1}"
1.95  begin
1.96
1.97  lemma M_subset_calM: "M \<subseteq> calM"
1.98    by (rule M_in_quot [THEN M_subset_calM_prep])
1.99
1.100 -lemma card_M1: "card(M1) = p^a"
1.101 +lemma card_M1: "card M1 = p^a"
1.102    using M1_in_M M_subset_calM calM_def by blast
1.103 -
1.104 +
1.105  lemma exists_x_in_M1: "\<exists>x. x \<in> M1"
1.106 -using prime_p [THEN prime_gt_Suc_0_nat] card_M1
1.107 -by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI)
1.108 +  using prime_p [THEN prime_gt_Suc_0_nat] card_M1
1.109 +  by (metis Suc_lessD card_eq_0_iff empty_subsetI equalityI gr_implies_not0 nat_zero_less_power_iff subsetI)
1.110
1.111  lemma M1_subset_G [simp]: "M1 \<subseteq> carrier G"
1.112 -  using M1_in_M  M_subset_calM calM_def mem_Collect_eq subsetCE by blast
1.113 +  using M1_in_M M_subset_calM calM_def mem_Collect_eq subsetCE by blast
1.114
1.115  lemma M1_inj_H: "\<exists>f \<in> H\<rightarrow>M1. inj_on f H"
1.116  proof -
1.117    from exists_x_in_M1 obtain m1 where m1M: "m1 \<in> M1"..
1.118 -  have m1G: "m1 \<in> carrier G" by (simp add: m1M M1_subset_G [THEN subsetD])
1.119 +  have m1: "m1 \<in> carrier G"
1.120 +    by (simp add: m1M M1_subset_G [THEN subsetD])
1.121    show ?thesis
1.122    proof
1.123      show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
1.124 -      by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1G)
1.125 +      by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1)
1.126      show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
1.127      proof (rule restrictI)
1.128 -      fix z assume zH: "z \<in> H"
1.129 +      fix z
1.130 +      assume zH: "z \<in> H"
1.131        show "m1 \<otimes> z \<in> M1"
1.132        proof -
1.133          from zH
1.134          have zG: "z \<in> carrier G" and M1zeq: "M1 #> z = M1"
1.135            by (auto simp add: H_def)
1.136          show ?thesis
1.137 -          by (rule subst [OF M1zeq], simp add: m1M zG rcosI)
1.138 +          by (rule subst [OF M1zeq]) (simp add: m1M zG rcosI)
1.139        qed
1.140      qed
1.141    qed
1.142 @@ -104,247 +98,235 @@
1.143
1.144  end
1.145
1.146 -subsection\<open>Discharging the Assumptions of \<open>sylow_central\<close>\<close>
1.147 +
1.148 +subsection \<open>Discharging the Assumptions of \<open>sylow_central\<close>\<close>
1.149
1.150  context sylow
1.151  begin
1.152
1.153  lemma EmptyNotInEquivSet: "{} \<notin> calM // RelM"
1.154 -by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
1.155 +  by (blast elim!: quotientE dest: RelM_equiv [THEN equiv_class_self])
1.156
1.157 -lemma existsM1inM: "M \<in> calM // RelM ==> \<exists>M1. M1 \<in> M"
1.158 +lemma existsM1inM: "M \<in> calM // RelM \<Longrightarrow> \<exists>M1. M1 \<in> M"
1.159    using RelM_equiv equiv_Eps_in by blast
1.160
1.161 -lemma zero_less_o_G: "0 < order(G)"
1.162 +lemma zero_less_o_G: "0 < order G"
1.163    by (simp add: order_def card_gt_0_iff carrier_not_empty)
1.164
1.165  lemma zero_less_m: "m > 0"
1.166    using zero_less_o_G by (simp add: order_G)
1.167
1.168 -lemma card_calM: "card(calM) = (p^a) * m choose p^a"
1.169 -by (simp add: calM_def n_subsets order_G [symmetric] order_def)
1.170 +lemma card_calM: "card calM = (p^a) * m choose p^a"
1.171 +  by (simp add: calM_def n_subsets order_G [symmetric] order_def)
1.172
1.173  lemma zero_less_card_calM: "card calM > 0"
1.174 -by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
1.175 +  by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
1.176
1.177 -lemma max_p_div_calM:
1.178 -     "~ (p ^ Suc(multiplicity p m) dvd card(calM))"
1.179 +lemma max_p_div_calM: "\<not> (p ^ Suc (multiplicity p m) dvd card calM)"
1.180  proof
1.181    assume "p ^ Suc (multiplicity p m) dvd card calM"
1.182 -  with zero_less_card_calM prime_p
1.183 +  with zero_less_card_calM prime_p
1.184    have "Suc (multiplicity p m) \<le> multiplicity p (card calM)"
1.185      by (intro multiplicity_geI) auto
1.186 -  hence "multiplicity p m < multiplicity p (card calM)" by simp
1.187 +  then have "multiplicity p m < multiplicity p (card calM)" by simp
1.188    also have "multiplicity p m = multiplicity p (card calM)"
1.189      by (simp add: const_p_fac prime_p zero_less_m card_calM)
1.190    finally show False by simp
1.191  qed
1.192
1.193  lemma finite_calM: "finite calM"
1.194 -  unfolding calM_def
1.195 -  by (rule_tac B = "Pow (carrier G) " in finite_subset) auto
1.196 +  unfolding calM_def by (rule finite_subset [where B = "Pow (carrier G)"]) auto
1.197
1.198 -lemma lemma_A1:
1.199 -     "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(multiplicity p m) dvd card(M))"
1.200 +lemma lemma_A1: "\<exists>M \<in> calM // RelM. \<not> (p ^ Suc (multiplicity p m) dvd card M)"
1.201    using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast
1.202
1.203  end
1.204
1.205 -subsubsection\<open>Introduction and Destruct Rules for @{term H}\<close>
1.206 +
1.207 +subsubsection \<open>Introduction and Destruct Rules for \<open>H\<close>\<close>
1.208
1.209 -lemma (in sylow_central) H_I: "[|g \<in> carrier G; M1 #> g = M1|] ==> g \<in> H"
1.211 -
1.212 -lemma (in sylow_central) H_into_carrier_G: "x \<in> H ==> x \<in> carrier G"
1.214 +lemma (in sylow_central) H_I: "\<lbrakk>g \<in> carrier G; M1 #> g = M1\<rbrakk> \<Longrightarrow> g \<in> H"
1.215 +  by (simp add: H_def)
1.216
1.217 -lemma (in sylow_central) in_H_imp_eq: "g : H ==> M1 #> g = M1"
1.219 +lemma (in sylow_central) H_into_carrier_G: "x \<in> H \<Longrightarrow> x \<in> carrier G"
1.220 +  by (simp add: H_def)
1.221
1.222 -lemma (in sylow_central) H_m_closed: "[| x\<in>H; y\<in>H|] ==> x \<otimes> y \<in> H"
1.223 -apply (unfold H_def)
1.224 -apply (simp add: coset_mult_assoc [symmetric])
1.225 -done
1.226 +lemma (in sylow_central) in_H_imp_eq: "g \<in> H \<Longrightarrow> M1 #> g = M1"
1.227 +  by (simp add: H_def)
1.228 +
1.229 +lemma (in sylow_central) H_m_closed: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> H"
1.230 +  by (simp add: H_def coset_mult_assoc [symmetric])
1.231
1.232  lemma (in sylow_central) H_not_empty: "H \<noteq> {}"
1.234 -apply (rule exI [of _ \<one>], simp)
1.235 -done
1.236 +  apply (simp add: H_def)
1.237 +  apply (rule exI [of _ \<one>])
1.238 +  apply simp
1.239 +  done
1.240
1.241  lemma (in sylow_central) H_is_subgroup: "subgroup H G"
1.242 -apply (rule subgroupI)
1.243 -apply (rule subsetI)
1.244 -apply (erule H_into_carrier_G)
1.245 -apply (rule H_not_empty)
1.246 -apply (simp add: H_def, clarify)
1.247 -apply (erule_tac P = "%z. lhs(z) = M1" for lhs in subst)
1.248 -apply (simp add: coset_mult_assoc )
1.249 -apply (blast intro: H_m_closed)
1.250 -done
1.251 +  apply (rule subgroupI)
1.252 +     apply (rule subsetI)
1.253 +     apply (erule H_into_carrier_G)
1.254 +    apply (rule H_not_empty)
1.255 +   apply (simp add: H_def)
1.256 +   apply clarify
1.257 +   apply (erule_tac P = "\<lambda>z. lhs z = M1" for lhs in subst)
1.258 +   apply (simp add: coset_mult_assoc )
1.259 +  apply (blast intro: H_m_closed)
1.260 +  done
1.261
1.262
1.263  lemma (in sylow_central) rcosetGM1g_subset_G:
1.264 -     "[| g \<in> carrier G; x \<in> M1 #>  g |] ==> x \<in> carrier G"
1.265 -by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
1.266 +  "\<lbrakk>g \<in> carrier G; x \<in> M1 #> g\<rbrakk> \<Longrightarrow> x \<in> carrier G"
1.267 +  by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
1.268
1.269  lemma (in sylow_central) finite_M1: "finite M1"
1.270 -by (rule finite_subset [OF M1_subset_G finite_G])
1.271 +  by (rule finite_subset [OF M1_subset_G finite_G])
1.272
1.273 -lemma (in sylow_central) finite_rcosetGM1g: "g\<in>carrier G ==> finite (M1 #> g)"
1.274 +lemma (in sylow_central) finite_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> finite (M1 #> g)"
1.275    using rcosetGM1g_subset_G finite_G M1_subset_G cosets_finite rcosetsI by blast
1.276
1.277 -lemma (in sylow_central) M1_cardeq_rcosetGM1g:
1.278 -     "g \<in> carrier G ==> card(M1 #> g) = card(M1)"
1.279 -by (simp (no_asm_simp) add: card_cosets_equal rcosetsI)
1.280 +lemma (in sylow_central) M1_cardeq_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> card (M1 #> g) = card M1"
1.281 +  by (simp add: card_cosets_equal rcosetsI)
1.282
1.283 -lemma (in sylow_central) M1_RelM_rcosetGM1g:
1.284 -     "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
1.285 -apply (simp add: RelM_def calM_def card_M1)
1.286 -apply (rule conjI)
1.287 - apply (blast intro: rcosetGM1g_subset_G)
1.288 -apply (simp add: card_M1 M1_cardeq_rcosetGM1g)
1.289 -apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
1.290 -done
1.291 +lemma (in sylow_central) M1_RelM_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> (M1, M1 #> g) \<in> RelM"
1.292 +  apply (simp add: RelM_def calM_def card_M1)
1.293 +  apply (rule conjI)
1.294 +   apply (blast intro: rcosetGM1g_subset_G)
1.295 +  apply (simp add: card_M1 M1_cardeq_rcosetGM1g)
1.296 +  apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
1.297 +  done
1.298
1.299
1.300 -subsection\<open>Equal Cardinalities of @{term M} and the Set of Cosets\<close>
1.301 +subsection \<open>Equal Cardinalities of \<open>M\<close> and the Set of Cosets\<close>
1.302
1.303 -text\<open>Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
1.304 +text \<open>Injections between @{term M} and @{term "rcosets\<^bsub>G\<^esub> H"} show that
1.305   their cardinalities are equal.\<close>
1.306
1.307 -lemma ElemClassEquiv:
1.308 -     "[| equiv A r; C \<in> A // r |] ==> \<forall>x \<in> C. \<forall>y \<in> C. (x,y)\<in>r"
1.309 -by (unfold equiv_def quotient_def sym_def trans_def, blast)
1.310 +lemma ElemClassEquiv: "\<lbrakk>equiv A r; C \<in> A // r\<rbrakk> \<Longrightarrow> \<forall>x \<in> C. \<forall>y \<in> C. (x, y) \<in> r"
1.311 +  unfolding equiv_def quotient_def sym_def trans_def by blast
1.312
1.313 -lemma (in sylow_central) M_elem_map:
1.314 -     "M2 \<in> M ==> \<exists>g. g \<in> carrier G & M1 #> g = M2"
1.315 -apply (cut_tac M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]])
1.317 -apply (blast dest!: bspec)
1.318 -done
1.319 +lemma (in sylow_central) M_elem_map: "M2 \<in> M \<Longrightarrow> \<exists>g. g \<in> carrier G \<and> M1 #> g = M2"
1.320 +  using M1_in_M M_in_quot [THEN RelM_equiv [THEN ElemClassEquiv]]
1.321 +  by (simp add: RelM_def) (blast dest!: bspec)
1.322
1.323  lemmas (in sylow_central) M_elem_map_carrier =
1.324 -        M_elem_map [THEN someI_ex, THEN conjunct1]
1.325 +  M_elem_map [THEN someI_ex, THEN conjunct1]
1.326
1.327  lemmas (in sylow_central) M_elem_map_eq =
1.328 -        M_elem_map [THEN someI_ex, THEN conjunct2]
1.329 +  M_elem_map [THEN someI_ex, THEN conjunct2]
1.330
1.331  lemma (in sylow_central) M_funcset_rcosets_H:
1.332 -     "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
1.333 +  "(\<lambda>x\<in>M. H #> (SOME g. g \<in> carrier G \<and> M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
1.334    by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset)
1.335
1.336  lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
1.337 -apply (rule bexI)
1.338 -apply (rule_tac [2] M_funcset_rcosets_H)
1.339 -apply (rule inj_onI, simp)
1.340 -apply (rule trans [OF _ M_elem_map_eq])
1.341 -prefer 2 apply assumption
1.342 -apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
1.343 -apply (rule coset_mult_inv1)
1.344 -apply (erule_tac [2] M_elem_map_carrier)+
1.345 -apply (rule_tac [2] M1_subset_G)
1.346 -apply (rule coset_join1 [THEN in_H_imp_eq])
1.347 -apply (rule_tac [3] H_is_subgroup)
1.348 -prefer 2 apply (blast intro: M_elem_map_carrier)
1.349 -apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
1.350 -done
1.351 +  apply (rule bexI)
1.352 +   apply (rule_tac [2] M_funcset_rcosets_H)
1.353 +  apply (rule inj_onI, simp)
1.354 +  apply (rule trans [OF _ M_elem_map_eq])
1.355 +   prefer 2 apply assumption
1.356 +  apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
1.357 +  apply (rule coset_mult_inv1)
1.358 +     apply (erule_tac [2] M_elem_map_carrier)+
1.359 +   apply (rule_tac [2] M1_subset_G)
1.360 +  apply (rule coset_join1 [THEN in_H_imp_eq])
1.361 +    apply (rule_tac [3] H_is_subgroup)
1.362 +   prefer 2 apply (blast intro: M_elem_map_carrier)
1.363 +  apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
1.364 +  done
1.365
1.366
1.367  subsubsection\<open>The Opposite Injection\<close>
1.368
1.369 -lemma (in sylow_central) H_elem_map:
1.370 -     "H1 \<in> rcosets H ==> \<exists>g. g \<in> carrier G & H #> g = H1"
1.371 -by (auto simp add: RCOSETS_def)
1.372 +lemma (in sylow_central) H_elem_map: "H1 \<in> rcosets H \<Longrightarrow> \<exists>g. g \<in> carrier G \<and> H #> g = H1"
1.373 +  by (auto simp: RCOSETS_def)
1.374
1.375  lemmas (in sylow_central) H_elem_map_carrier =
1.376 -        H_elem_map [THEN someI_ex, THEN conjunct1]
1.377 +  H_elem_map [THEN someI_ex, THEN conjunct1]
1.378
1.379  lemmas (in sylow_central) H_elem_map_eq =
1.380 -        H_elem_map [THEN someI_ex, THEN conjunct2]
1.381 +  H_elem_map [THEN someI_ex, THEN conjunct2]
1.382
1.383  lemma (in sylow_central) rcosets_H_funcset_M:
1.384    "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
1.386 -apply (fast intro: someI2
1.387 -            intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
1.388 -done
1.389 +  apply (simp add: RCOSETS_def)
1.390 +  apply (fast intro: someI2
1.391 +      intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
1.392 +  done
1.393
1.394 -text\<open>close to a duplicate of \<open>inj_M_GmodH\<close>\<close>
1.395 -lemma (in sylow_central) inj_GmodH_M:
1.396 -     "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
1.397 -apply (rule bexI)
1.398 -apply (rule_tac [2] rcosets_H_funcset_M)
1.399 -apply (rule inj_onI)
1.400 -apply (simp)
1.401 -apply (rule trans [OF _ H_elem_map_eq])
1.402 -prefer 2 apply assumption
1.403 -apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
1.404 -apply (rule coset_mult_inv1)
1.405 -apply (erule_tac [2] H_elem_map_carrier)+
1.406 -apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
1.407 -apply (rule coset_join2)
1.408 -apply (blast intro: H_elem_map_carrier)
1.409 -apply (rule H_is_subgroup)
1.410 -apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier)
1.411 -done
1.412 +text \<open>Close to a duplicate of \<open>inj_M_GmodH\<close>.\<close>
1.413 +lemma (in sylow_central) inj_GmodH_M: "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
1.414 +  apply (rule bexI)
1.415 +   apply (rule_tac [2] rcosets_H_funcset_M)
1.416 +  apply (rule inj_onI)
1.417 +  apply (simp)
1.418 +  apply (rule trans [OF _ H_elem_map_eq])
1.419 +   prefer 2 apply assumption
1.420 +  apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
1.421 +  apply (rule coset_mult_inv1)
1.422 +     apply (erule_tac [2] H_elem_map_carrier)+
1.423 +   apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
1.424 +  apply (rule coset_join2)
1.425 +    apply (blast intro: H_elem_map_carrier)
1.426 +   apply (rule H_is_subgroup)
1.427 +  apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier)
1.428 +  done
1.429
1.430 -lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow(carrier G)"
1.431 -by (auto simp add: calM_def)
1.432 +lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow (carrier G)"
1.433 +  by (auto simp: calM_def)
1.434
1.435
1.436  lemma (in sylow_central) finite_M: "finite M"
1.437 -by (metis M_subset_calM finite_calM rev_finite_subset)
1.438 +  by (metis M_subset_calM finite_calM rev_finite_subset)
1.439
1.440 -lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)"
1.441 -apply (insert inj_M_GmodH inj_GmodH_M)
1.442 -apply (blast intro: card_bij finite_M H_is_subgroup
1.443 -             rcosets_subset_PowG [THEN finite_subset]
1.444 -             finite_Pow_iff [THEN iffD2])
1.445 -done
1.446 +lemma (in sylow_central) cardMeqIndexH: "card M = card (rcosets H)"
1.447 +  apply (insert inj_M_GmodH inj_GmodH_M)
1.448 +  apply (blast intro: card_bij finite_M H_is_subgroup
1.449 +      rcosets_subset_PowG [THEN finite_subset]
1.450 +      finite_Pow_iff [THEN iffD2])
1.451 +  done
1.452
1.453 -lemma (in sylow_central) index_lem: "card(M) * card(H) = order(G)"
1.454 -by (simp add: cardMeqIndexH lagrange H_is_subgroup)
1.455 +lemma (in sylow_central) index_lem: "card M * card H = order G"
1.456 +  by (simp add: cardMeqIndexH lagrange H_is_subgroup)
1.457
1.458 -lemma (in sylow_central) lemma_leq1: "p^a \<le> card(H)"
1.459 -apply (rule dvd_imp_le)
1.460 - apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
1.461 - prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
1.463 -                 zero_less_m)
1.464 -done
1.465 +lemma (in sylow_central) lemma_leq1: "p^a \<le> card H"
1.466 +  apply (rule dvd_imp_le)
1.467 +   apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
1.468 +   prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
1.470 +  done
1.471
1.472 -lemma (in sylow_central) lemma_leq2: "card(H) \<le> p^a"
1.473 -apply (subst card_M1 [symmetric])
1.474 -apply (cut_tac M1_inj_H)
1.475 -apply (blast intro!: M1_subset_G intro:
1.476 -             card_inj H_into_carrier_G finite_subset [OF _ finite_G])
1.477 -done
1.478 +lemma (in sylow_central) lemma_leq2: "card H \<le> p^a"
1.479 +  apply (subst card_M1 [symmetric])
1.480 +  apply (cut_tac M1_inj_H)
1.481 +  apply (blast intro!: M1_subset_G intro: card_inj H_into_carrier_G finite_subset [OF _ finite_G])
1.482 +  done
1.483
1.484 -lemma (in sylow_central) card_H_eq: "card(H) = p^a"
1.485 -by (blast intro: le_antisym lemma_leq1 lemma_leq2)
1.486 +lemma (in sylow_central) card_H_eq: "card H = p^a"
1.487 +  by (blast intro: le_antisym lemma_leq1 lemma_leq2)
1.488
1.489 -lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
1.490 -apply (cut_tac lemma_A1, clarify)
1.491 -apply (frule existsM1inM, clarify)
1.492 -apply (subgoal_tac "sylow_central G p a m M1 M")
1.493 - apply (blast dest:  sylow_central.H_is_subgroup sylow_central.card_H_eq)
1.494 -apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
1.495 -done
1.496 +lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G \<and> card H = p^a"
1.497 +  using lemma_A1
1.498 +  apply clarify
1.499 +  apply (frule existsM1inM, clarify)
1.500 +  apply (subgoal_tac "sylow_central G p a m M1 M")
1.501 +   apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
1.502 +  apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
1.503 +  done
1.504
1.505 -text\<open>Needed because the locale's automatic definition refers to
1.506 -   @{term "semigroup G"} and @{term "group_axioms G"} rather than
1.507 +text \<open>Needed because the locale's automatic definition refers to
1.508 +  @{term "semigroup G"} and @{term "group_axioms G"} rather than
1.509    simply to @{term "group G"}.\<close>
1.510 -lemma sylow_eq: "sylow G p a m = (group G & sylow_axioms G p a m)"
1.511 -by (simp add: sylow_def group_def)
1.512 +lemma sylow_eq: "sylow G p a m \<longleftrightarrow> group G \<and> sylow_axioms G p a m"
1.513 +  by (simp add: sylow_def group_def)
1.514
1.515
1.516  subsection \<open>Sylow's Theorem\<close>
1.517
1.518  theorem sylow_thm:
1.519 -     "[| prime p;  group(G);  order(G) = (p^a) * m; finite (carrier G)|]
1.520 -      ==> \<exists>H. subgroup H G & card(H) = p^a"
1.521 -apply (rule sylow.sylow_thm [of G p a m])
1.522 -apply (simp add: sylow_eq sylow_axioms_def)
1.523 -done
1.524 +  "\<lbrakk>prime p; group G; order G = (p^a) * m; finite (carrier G)\<rbrakk>
1.525 +    \<Longrightarrow> \<exists>H. subgroup H G \<and> card H = p^a"
1.526 +  by (rule sylow.sylow_thm [of G p a m]) (simp add: sylow_eq sylow_axioms_def)
1.527
1.528  end
```