misc tuning and modernization;
authorwenzelm
Tue Jan 17 14:56:15 2017 +0100 (2017-01-17)
changeset 6491268f0465d956b
parent 64911 f0e07600de47
child 64913 3a9eb793fa10
misc tuning and modernization;
src/HOL/Algebra/Sylow.thy
     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.12 -  See also @{cite "Kammueller-Paulson:1999"}.
    1.13 -\<close>
    1.14 +text \<open>See also @{cite "Kammueller-Paulson:1999"}.\<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.210 -by (simp add: H_def)
   1.211 -
   1.212 -lemma (in sylow_central) H_into_carrier_G: "x \<in> H ==> x \<in> carrier G"
   1.213 -by (simp add: H_def)
   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.218 -by (simp add: H_def)
   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.233 -apply (simp add: H_def)
   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.316 -apply (simp add: RelM_def)
   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.385 -apply (simp add: RCOSETS_def)
   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.462 -apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd
   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.469 +  apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd zero_less_m)
   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