author paulson Sun Jun 24 11:41:32 2018 +0100 (14 months ago) changeset 68488 dfbd80c3d180 parent 68485 28f9e9b80c49 child 68489 56034bd1b5f6
more modernisaton and de-applying
 src/HOL/Algebra/Complete_Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/Divisibility.thy file | annotate | diff | revisions src/HOL/Algebra/Sylow.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/Complete_Lattice.thy	Fri Jun 22 21:55:20 2018 +0200
1.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy	Sun Jun 24 11:41:32 2018 +0100
1.3 @@ -43,11 +43,8 @@
1.4  proof -
1.5    interpret dual: weak_lattice "inv_gorder L"
1.6      by (metis dual_weak_lattice)
1.7 -
1.8    show ?thesis
1.9 -    apply (unfold_locales)
1.10 -    apply (simp_all add:inf_exists sup_exists)
1.11 -  done
1.12 +    by (unfold_locales) (simp_all add:inf_exists sup_exists)
1.13  qed
1.14
1.15  lemma (in weak_complete_lattice) supI:
1.16 @@ -125,32 +122,21 @@
1.17    have B_L: "?B \<subseteq> carrier L" by simp
1.18    from inf_exists [OF B_L B_non_empty]
1.19    obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
1.20 +  then have bcarr: "b \<in> carrier L"
1.21 +    by auto
1.22    have "least L b (Upper L A)"
1.23 -apply (rule least_UpperI)
1.24 -   apply (rule greatest_le [where A = "Lower L ?B"])
1.25 -    apply (rule b_inf_B)
1.26 -   apply (rule Lower_memI)
1.27 -    apply (erule Upper_memD [THEN conjunct1])
1.28 -     apply assumption
1.29 -    apply (rule L)
1.30 -   apply (fast intro: L [THEN subsetD])
1.31 -  apply (erule greatest_Lower_below [OF b_inf_B])
1.32 -  apply simp
1.33 - apply (rule L)
1.34 -apply (rule greatest_closed [OF b_inf_B])
1.35 -done
1.36 +  proof (rule least_UpperI)
1.37 +    show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
1.38 +      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)
1.39 +    show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
1.40 +      by (meson B_L b_inf_B greatest_Lower_below)
1.41 +  qed (use bcarr L in auto)
1.42    then show "\<exists>s. least L s (Upper L A)" ..
1.43  next
1.44    fix A
1.45    assume L: "A \<subseteq> carrier L"
1.46    show "\<exists>i. greatest L i (Lower L A)"
1.47 -  proof (cases "A = {}")
1.48 -    case True then show ?thesis
1.49 -      by (simp add: top_exists)
1.50 -  next
1.51 -    case False with L show ?thesis
1.52 -      by (rule inf_exists)
1.53 -  qed
1.54 +    by (metis L Lower_empty inf_exists top_exists)
1.55  qed
1.56
1.57
1.58 @@ -205,12 +191,8 @@
1.59  proof -
1.60    obtain i where "greatest L i (Lower L A)"
1.61      by (metis assms inf_exists)
1.62 -
1.63    thus ?thesis
1.64 -    apply (simp add: inf_def)
1.65 -    apply (rule someI2[of _ "i"])
1.66 -    apply (auto)
1.67 -  done
1.68 +    by (metis inf_def someI_ex)
1.69  qed
1.70
1.71  lemma inf_lower:
1.72 @@ -231,17 +213,20 @@
1.73    by (metis bottom_weak_eq inf_closed inf_lower subset_refl)
1.74
1.75  lemma weak_inf_insert [simp]:
1.76 -  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
1.77 -  apply (rule weak_le_antisym)
1.78 -  apply (force intro: meet_le inf_greatest inf_lower inf_closed)
1.79 -  apply (rule inf_greatest)
1.80 -  apply (force)
1.81 -  apply (force intro: inf_closed)
1.82 -  apply (auto)
1.83 -  apply (metis inf_closed meet_left)
1.84 -  apply (force intro: le_trans inf_closed meet_right meet_left inf_lower)
1.85 -done
1.86 -
1.87 +  assumes "a \<in> carrier L" "A \<subseteq> carrier L"
1.88 +  shows "\<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
1.89 +proof (rule weak_le_antisym)
1.90 +  show "\<Sqinter>insert a A \<sqsubseteq> a \<sqinter> \<Sqinter>A"
1.91 +    by (simp add: assms inf_lower local.inf_greatest meet_le)
1.92 +  show aA: "a \<sqinter> \<Sqinter>A \<in> carrier L"
1.93 +    using assms by simp
1.94 +  show "a \<sqinter> \<Sqinter>A \<sqsubseteq> \<Sqinter>insert a A"
1.95 +    apply (rule inf_greatest)
1.96 +    using assms apply (simp_all add: aA)
1.97 +    by (meson aA inf_closed inf_lower local.le_trans meet_left meet_right subsetCE)
1.98 +  show "\<Sqinter>insert a A \<in> carrier L"
1.99 +    using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
1.100 +qed
1.101
1.102  subsection \<open>Supremum Laws\<close>
1.103
1.104 @@ -268,17 +253,20 @@
1.105    by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)
1.106
1.107  lemma weak_sup_insert [simp]:
1.108 -  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Squnion>insert a A .= a \<squnion> \<Squnion>A"
1.109 -  apply (rule weak_le_antisym)
1.110 -  apply (rule sup_least)
1.111 -  apply (auto)
1.112 -  apply (metis join_left sup_closed)
1.113 -  apply (rule le_trans) defer
1.114 -  apply (rule join_right)
1.115 -  apply (auto)
1.116 -  apply (rule join_le)
1.117 -  apply (auto intro: sup_upper sup_least sup_closed)
1.118 -done
1.119 +  assumes "a \<in> carrier L" "A \<subseteq> carrier L"
1.120 +  shows "\<Squnion>insert a A .= a \<squnion> \<Squnion>A"
1.121 +proof (rule weak_le_antisym)
1.122 +  show aA: "a \<squnion> \<Squnion>A \<in> carrier L"
1.123 +    using assms by simp
1.124 +  show "\<Squnion>insert a A \<sqsubseteq> a \<squnion> \<Squnion>A"
1.125 +    apply (rule sup_least)
1.126 +    using assms apply (simp_all add: aA)
1.127 +    by (meson aA join_left join_right local.le_trans subsetCE sup_closed sup_upper)
1.128 +  show "a \<squnion> \<Squnion>A \<sqsubseteq> \<Squnion>insert a A"
1.129 +    by (simp add: assms join_le local.sup_least sup_upper)
1.130 +  show "\<Squnion>insert a A \<in> carrier L"
1.131 +    using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
1.132 +qed
1.133
1.134  end
1.135
1.136 @@ -303,30 +291,26 @@
1.137  proof -
1.138    from assms(2) have AL: "A \<subseteq> carrier L"
1.139      by (auto simp add: fps_def)
1.140 -
1.141    show ?thesis
1.142    proof (rule sup_cong, simp_all add: AL)
1.143      from assms(1) AL show "f ` A \<subseteq> carrier L"
1.144 -      by (auto)
1.145 +      by auto
1.146 +    then have *: "\<And>b. \<lbrakk>A \<subseteq> {x \<in> carrier L. f x .= x}; b \<in> A\<rbrakk> \<Longrightarrow> \<exists>a\<in>f ` A. b .= a"
1.147 +      by (meson AL assms(2) image_eqI local.sym subsetCE use_fps)
1.148      from assms(2) show "f ` A {.=} A"
1.149 -      apply (auto simp add: fps_def)
1.150 -      apply (rule set_eqI2)
1.151 -      apply blast
1.152 -      apply (rename_tac b)
1.153 -      apply (rule_tac x="f b" in bexI)
1.154 -      apply (metis (mono_tags, lifting) Ball_Collect assms(1) Pi_iff local.sym)
1.155 -      apply (auto)
1.156 -    done
1.157 +      by (auto simp add: fps_def intro: set_eqI2 [OF _ *])
1.158    qed
1.159  qed
1.160
1.161  lemma (in weak_complete_lattice) fps_idem:
1.162 -  "\<lbrakk> f \<in> carrier L \<rightarrow> carrier L; Idem f \<rbrakk> \<Longrightarrow> fps L f {.=} f ` carrier L"
1.163 -  apply (rule set_eqI2)
1.164 -  apply (auto simp add: idempotent_def fps_def)
1.165 -  apply (metis Pi_iff local.sym)
1.166 -  apply force
1.167 -done
1.168 +  assumes "f \<in> carrier L \<rightarrow> carrier L" "Idem f"
1.169 +  shows "fps L f {.=} f ` carrier L"
1.170 +proof (rule set_eqI2)
1.171 +  show "\<And>a. a \<in> fps L f \<Longrightarrow> \<exists>b\<in>f ` carrier L. a .= b"
1.172 +    using assms by (force simp add: fps_def intro: local.sym)
1.173 +  show "\<And>b. b \<in> f ` carrier L \<Longrightarrow> \<exists>a\<in>fps L f. b .= a"
1.174 +    using assms by (force simp add: idempotent_def fps_def)
1.175 +qed
1.176
1.177  context weak_complete_lattice
1.178  begin
1.179 @@ -392,20 +376,19 @@
1.180  lemma LFP_lemma2:
1.181    assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
1.182    shows "f (LFP f) \<sqsubseteq> LFP f"
1.183 -  using assms
1.184 -  apply (auto simp add:Pi_def)
1.185 -  apply (rule LFP_greatest)
1.186 -  apply (metis LFP_closed)
1.187 -  apply (metis LFP_closed LFP_lowerbound le_trans use_iso1)
1.188 -done
1.189 +proof (rule LFP_greatest)
1.190 +  have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
1.191 +    using assms by (auto simp add: Pi_def)
1.192 +  with assms show "f (LFP f) \<in> carrier L"
1.193 +    by blast
1.194 +  show "\<And>u. \<lbrakk>u \<in> carrier L; f u \<sqsubseteq> u\<rbrakk> \<Longrightarrow> f (LFP f) \<sqsubseteq> u"
1.195 +    by (meson LFP_closed LFP_lowerbound assms(1) f local.le_trans use_iso1)
1.196 +qed
1.197
1.198  lemma LFP_lemma3:
1.199    assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
1.200    shows "LFP f \<sqsubseteq> f (LFP f)"
1.201 -  using assms
1.202 -  apply (auto simp add:Pi_def)
1.203 -  apply (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
1.204 -done
1.205 +  using assms by (simp add: Pi_def) (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
1.206
1.207  lemma LFP_weak_unfold:
1.208    "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f .= f (LFP f)"
1.209 @@ -477,12 +460,14 @@
1.210  lemma GFP_lemma2:
1.211    assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
1.212    shows "GFP f \<sqsubseteq> f (GFP f)"
1.213 -  using assms
1.214 -  apply (auto simp add:Pi_def)
1.215 -  apply (rule GFP_least)
1.216 -  apply (metis GFP_closed)
1.217 -  apply (metis GFP_closed GFP_upperbound le_trans use_iso2)
1.218 -done
1.219 +proof (rule GFP_least)
1.220 +  have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
1.221 +    using assms by (auto simp add: Pi_def)
1.222 +  with assms show "f (GFP f) \<in> carrier L"
1.223 +    by blast
1.224 +  show "\<And>u. \<lbrakk>u \<in> carrier L; u \<sqsubseteq> f u\<rbrakk> \<Longrightarrow> u \<sqsubseteq> f (GFP f)"
1.225 +    by (meson GFP_closed GFP_upperbound le_trans assms(1) f local.le_trans use_iso1)
1.226 +qed
1.227
1.228  lemma GFP_lemma3:
1.229    assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
1.230 @@ -599,20 +584,15 @@
1.231    have B_L: "?B \<subseteq> carrier L" by simp
1.232    from inf_exists [OF B_L B_non_empty]
1.233    obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
1.234 +  then have bcarr: "b \<in> carrier L"
1.235 +    by blast
1.236    have "least L b (Upper L A)"
1.237 -apply (rule least_UpperI)
1.238 -   apply (rule greatest_le [where A = "Lower L ?B"])
1.239 -    apply (rule b_inf_B)
1.240 -   apply (rule Lower_memI)
1.241 -    apply (erule Upper_memD [THEN conjunct1])
1.242 -     apply assumption
1.243 -    apply (rule L)
1.244 -   apply (fast intro: L [THEN subsetD])
1.245 -  apply (erule greatest_Lower_below [OF b_inf_B])
1.246 -  apply simp
1.247 - apply (rule L)
1.248 -apply (rule greatest_closed [OF b_inf_B])
1.249 -done
1.250 +  proof (rule least_UpperI)
1.251 +    show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
1.252 +      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)
1.253 +    show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
1.254 +      by (auto elim: greatest_Lower_below [OF b_inf_B])
1.255 +  qed (use L bcarr in auto)
1.256    then show "\<exists>s. least L s (Upper L A)" ..
1.257  next
1.258    fix A
1.259 @@ -666,23 +646,11 @@
1.260  context weak_complete_lattice
1.261  begin
1.262
1.263 -  lemma at_least_at_most_Sup:
1.264 -    "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"
1.265 -    apply (rule weak_le_antisym)
1.266 -    apply (rule sup_least)
1.267 -    apply (auto simp add: at_least_at_most_closed)
1.268 -    apply (rule sup_upper)
1.269 -    apply (auto simp add: at_least_at_most_closed)
1.270 -  done
1.271 +  lemma at_least_at_most_Sup: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Squnion> \<lbrace>a..b\<rbrace> .= b"
1.272 +    by (rule weak_le_antisym [OF sup_least sup_upper]) (auto simp add: at_least_at_most_closed)
1.273
1.274 -  lemma at_least_at_most_Inf:
1.275 -    "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"
1.276 -    apply (rule weak_le_antisym)
1.277 -    apply (rule inf_lower)
1.278 -    apply (auto simp add: at_least_at_most_closed)
1.279 -    apply (rule inf_greatest)
1.280 -    apply (auto simp add: at_least_at_most_closed)
1.281 -  done
1.282 +  lemma at_least_at_most_Inf: "\<lbrakk> a \<in> carrier L; b \<in> carrier L; a \<sqsubseteq> b \<rbrakk> \<Longrightarrow> \<Sqinter> \<lbrace>a..b\<rbrace> .= a"
1.283 +    by (rule weak_le_antisym [OF inf_lower inf_greatest]) (auto simp add: at_least_at_most_closed)
1.284
1.285  end
1.286
1.287 @@ -695,7 +663,7 @@
1.288    interpret weak_partial_order "L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>"
1.289    proof -
1.290      have "\<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<subseteq> carrier L"
1.291 -      by (auto, simp add: at_least_at_most_def)
1.292 +      by (auto simp add: at_least_at_most_def)
1.293      thus "weak_partial_order (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
1.294        by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
1.295    qed
```
```     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Fri Jun 22 21:55:20 2018 +0200
2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Jun 24 11:41:32 2018 +0100
2.3 @@ -2382,10 +2382,8 @@
2.4    interpret weak_lower_semilattice "division_rel G"
2.5      by simp
2.6    show ?thesis
2.7 -    apply (subst (2 3) somegcd_meet, (simp add: carr)+)
2.8 -    apply (simp add: somegcd_meet carr)
2.9 -    apply (rule weak_meet_assoc[simplified], fact+)
2.10 -    done
2.11 +    unfolding associated_def
2.12 +    by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
2.13  qed
2.14
2.15  lemma (in gcd_condition_monoid) gcd_mult:
2.16 @@ -2645,10 +2643,7 @@
2.17        by blast
2.18      have a'fs: "wfactors G as a'"
2.19        apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
2.20 -      apply (simp add: a)
2.21 -      apply (insert ascarr a'carr)
2.22 -      apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
2.23 -      done
2.24 +      by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed)
2.25      from afs have ahirr: "irreducible G ah"
2.26        by (elim wfactorsE) simp
2.27      with ascarr have ahprime: "prime G ah"
2.28 @@ -2674,31 +2669,18 @@
2.29      from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
2.30        by blast
2.31      with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
2.32 -      apply -
2.33 -      apply (elim irreducible_prodE[of "ah" "x"], assumption+)
2.34 -       apply (rule associatedI2[of x], assumption+)
2.35 -      apply (rule irreducibleE[OF ahirr], simp)
2.36 -      done
2.37 -
2.38 +      by (metis ahprime associatedI2 irreducible_prodE primeE)
2.39      note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
2.40      note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
2.41      note carr = carr partscarr
2.42
2.43      have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
2.44 -      apply (intro wfactors_prod_exists)
2.45 -      using setparts afs'
2.46 -       apply (fast elim: wfactorsE)
2.47 -      apply simp
2.48 -      done
2.49 +      by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
2.50      then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
2.51        by auto
2.52
2.53      have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
2.54 -      apply (intro wfactors_prod_exists)
2.55 -      using setparts afs'
2.56 -       apply (fast elim: wfactorsE)
2.57 -      apply simp
2.58 -      done
2.59 +      by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
2.60      then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
2.61        and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
2.62        by auto
2.63 @@ -2709,21 +2691,12 @@
2.64      have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
2.65        by (intro wfactors_mult, simp+)
2.66      then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
2.67 -      apply (intro wfactors_mult_single)
2.68 -      using setparts afs'
2.69 -          apply (fast intro: nth_mem[OF len] elim: wfactorsE)
2.70 -         apply simp_all
2.71 -      done
2.72 -
2.73 +      using irrasi wfactors_mult_single by auto
2.74      from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
2.75        by (metis irrasi wfactors_mult_single)
2.76      with len carr aa1carr aa2carr aa1fs
2.77      have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
2.78 -      apply (intro wfactors_mult)
2.79 -           apply fast
2.80 -          apply (simp, (fast intro: nth_mem[OF len])?)+
2.81 -      done
2.82 -
2.83 +      using wfactors_mult by auto
2.84      from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
2.86      with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
2.87 @@ -2763,14 +2736,8 @@
2.88      note ee1
2.89      also note ee2
2.90      also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
2.91 -      (take i as' @ as' ! i # drop (Suc i) as')"
2.92 -      apply (intro essentially_equalI)
2.93 -       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
2.94 -          take i as' @ as' ! i # drop (Suc i) as'")
2.95 -        apply simp
2.96 -       apply (rule perm_append_Cons)
2.97 -      apply simp
2.98 -      done
2.99 +                                   (take i as' @ as' ! i # drop (Suc i) as')"
2.100 +      by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
2.101      finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
2.102        by simp
2.103      then show "essentially_equal G (ah # as) as'"
2.104 @@ -2813,21 +2780,17 @@
2.105
2.106  lemma (in factorial_monoid) factorcount_unique:
2.107    assumes afs: "wfactors G as a"
2.108 -    and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"
2.109 +    and acarr[simp]: "a \<in> carrier G" and ascarr: "set as \<subseteq> carrier G"
2.110    shows "factorcount G a = length as"
2.111  proof -
2.112    have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
2.113      by (rule factorcount_exists) simp
2.114    then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
2.115      by auto
2.116 -  have ac: "ac = factorcount G a"
2.117 -    apply (simp add: factorcount_def)
2.118 -    apply (rule theI2)
2.119 -      apply (rule alen)
2.120 -     apply (metis afs alen ascarr)+
2.121 -    done
2.122 +  then have ac: "ac = factorcount G a"
2.123 +    unfolding factorcount_def using ascarr by (blast intro: theI2 afs)
2.124    from ascarr afs have "ac = length as"
2.125 -    by (iprover intro: alen[rule_format])
2.126 +    by (simp add: alen)
2.127    with ac show ?thesis
2.128      by simp
2.129  qed
2.130 @@ -2872,11 +2835,8 @@
2.131      and bcarr: "b \<in> carrier G"
2.132      and asc: "a \<sim> b"
2.133    shows "factorcount G a = factorcount G b"
2.134 -  apply (rule associatedE[OF asc])
2.135 -  apply (drule divides_fcount[OF _ acarr bcarr])
2.136 -  apply (drule divides_fcount[OF _ bcarr acarr])
2.137 -  apply simp
2.138 -  done
2.139 +  using assms
2.140 +  by (auto simp: associated_def factorial_monoid.divides_fcount factorial_monoid_axioms le_antisym)
2.141
2.142  lemma (in factorial_monoid) properfactor_fcount:
2.143    assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
```
```     3.1 --- a/src/HOL/Algebra/Sylow.thy	Fri Jun 22 21:55:20 2018 +0200
3.2 +++ b/src/HOL/Algebra/Sylow.thy	Sun Jun 24 11:41:32 2018 +0100
3.3 @@ -161,23 +161,17 @@
3.4    by (simp add: H_def coset_mult_assoc [symmetric])
3.5
3.6  lemma H_not_empty: "H \<noteq> {}"
3.7 -  apply (simp add: H_def)
3.8 -  apply (rule exI [of _ \<one>])
3.9 -  apply simp
3.10 -  done
3.11 +  by (force simp add: H_def intro: exI [of _ \<one>])
3.12
3.13  lemma H_is_subgroup: "subgroup H G"
3.14 -  apply (rule subgroupI)
3.15 -     apply (rule subsetI)
3.16 -     apply (erule H_into_carrier_G)
3.17 -    apply (rule H_not_empty)
3.18 -   apply (simp add: H_def)
3.19 -   apply clarify
3.20 -   apply (erule_tac P = "\<lambda>z. lhs z = M1" for lhs in subst)
3.21 -   apply (simp add: coset_mult_assoc )
3.22 -  apply (blast intro: H_m_closed)
3.23 -  done
3.24 -
3.25 +proof (rule subgroupI)
3.26 +  show "H \<subseteq> carrier G"
3.27 +    using H_into_carrier_G by blast
3.28 +  show "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
3.29 +    by (metis H_I H_into_carrier_G H_m_closed M1_subset_G Units_eq Units_inv_closed Units_inv_inv coset_mult_inv1 in_H_imp_eq)
3.30 +  show "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
3.31 +    by (blast intro: H_m_closed)
3.32 +qed (use H_not_empty in auto)
3.33
3.34  lemma rcosetGM1g_subset_G: "\<lbrakk>g \<in> carrier G; x \<in> M1 #> g\<rbrakk> \<Longrightarrow> x \<in> carrier G"
3.35    by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
3.36 @@ -191,13 +185,19 @@
3.37  lemma M1_cardeq_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> card (M1 #> g) = card M1"
3.38    by (metis M1_subset_G card_rcosets_equal rcosetsI)
3.39
3.40 -lemma M1_RelM_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> (M1, M1 #> g) \<in> RelM"
3.41 -  apply (simp add: RelM_def calM_def card_M1)
3.42 -  apply (rule conjI)
3.43 -   apply (blast intro: rcosetGM1g_subset_G)
3.44 -  apply (simp add: card_M1 M1_cardeq_rcosetGM1g)
3.45 -  apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
3.46 -  done
3.47 +lemma M1_RelM_rcosetGM1g:
3.48 +  assumes "g \<in> carrier G"
3.49 +  shows "(M1, M1 #> g) \<in> RelM"
3.50 +proof -
3.51 +  have "M1 #> g \<subseteq> carrier G"
3.52 +    by (simp add: assms r_coset_subset_G)
3.53 +  moreover have "card (M1 #> g) = p ^ a"
3.54 +    using assms by (simp add: card_M1 M1_cardeq_rcosetGM1g)
3.55 +  moreover have "\<exists>h\<in>carrier G. M1 = M1 #> g #> h"
3.56 +    by (metis assms M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
3.57 +  ultimately show ?thesis
3.58 +    by (simp add: RelM_def calM_def card_M1)
3.59 +qed
3.60
3.61  end
3.62
3.63 @@ -226,20 +226,26 @@
3.64    by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset)
3.65
3.66  lemma inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
3.67 -  apply (rule bexI)
3.68 -   apply (rule_tac [2] M_funcset_rcosets_H)
3.69 -  apply (rule inj_onI, simp)
3.70 -  apply (rule trans [OF _ M_elem_map_eq])
3.71 -   prefer 2 apply assumption
3.72 -  apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
3.73 -  apply (rule coset_mult_inv1)
3.74 -     apply (erule_tac [2] M_elem_map_carrier)+
3.75 -   apply (rule_tac [2] M1_subset_G)
3.76 -  apply (rule coset_join1 [THEN in_H_imp_eq])
3.77 -    apply (rule_tac [3] H_is_subgroup)
3.78 -   prefer 2 apply (blast intro: M_elem_map_carrier)
3.79 -  apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
3.80 -  done
3.81 +proof
3.82 +  let ?inv = "\<lambda>x. SOME g. g \<in> carrier G \<and> M1 #> g = x"
3.83 +  show "inj_on (\<lambda>x\<in>M. H #> ?inv x) M"
3.84 +  proof (rule inj_onI, simp)
3.85 +    fix x y
3.86 +    assume eq: "H #> ?inv x = H #> ?inv y" and xy: "x \<in> M" "y \<in> M"
3.87 +    have "x = M1 #> ?inv x"
3.88 +      by (simp add: M_elem_map_eq \<open>x \<in> M\<close>)
3.89 +    also have "... = M1 #> ?inv y"
3.90 +    proof (rule coset_mult_inv1 [OF in_H_imp_eq [OF coset_join1]])
3.91 +      show "H #> ?inv x \<otimes> inv (?inv y) = H"
3.92 +        by (simp add: H_into_carrier_G M_elem_map_carrier xy coset_mult_inv2 eq subsetI)
3.93 +    qed (simp_all add: H_is_subgroup M_elem_map_carrier xy)
3.94 +    also have "... = y"
3.95 +      using M_elem_map_eq \<open>y \<in> M\<close> by simp
3.96 +    finally show "x=y" .
3.97 +  qed
3.98 +  show "(\<lambda>x\<in>M. H #> ?inv x) \<in> M \<rightarrow> rcosets H"
3.99 +    by (rule M_funcset_rcosets_H)
3.100 +qed
3.101
3.102  end
3.103
3.104 @@ -258,28 +264,34 @@
3.105
3.106  lemma rcosets_H_funcset_M:
3.107    "(\<lambda>C \<in> rcosets H. M1 #> (SOME g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
3.108 -  apply (simp add: RCOSETS_def)
3.109 -  apply (fast intro: someI2
3.110 -      intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
3.111 -  done
3.112 +  using in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g]
3.113 +  by (simp add: M1_in_M H_elem_map_carrier RCOSETS_def)
3.114
3.115 -text \<open>Close to a duplicate of \<open>inj_M_GmodH\<close>.\<close>
3.116  lemma inj_GmodH_M: "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
3.117 -  apply (rule bexI)
3.118 -   apply (rule_tac [2] rcosets_H_funcset_M)
3.119 -  apply (rule inj_onI)
3.120 -  apply (simp)
3.121 -  apply (rule trans [OF _ H_elem_map_eq])
3.122 -   prefer 2 apply assumption
3.123 -  apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
3.124 -  apply (rule coset_mult_inv1)
3.125 -     apply (erule_tac [2] H_elem_map_carrier)+
3.126 -   apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
3.127 -  apply (rule coset_join2)
3.128 -    apply (blast intro: H_elem_map_carrier)
3.129 -   apply (rule H_is_subgroup)
3.130 -  apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier)
3.131 -  done
3.132 +proof
3.133 +  let ?inv = "\<lambda>x. SOME g. g \<in> carrier G \<and> H #> g = x"
3.134 +  show "inj_on (\<lambda>C\<in>rcosets H. M1 #> ?inv C) (rcosets H)"
3.135 +  proof (rule inj_onI, simp)
3.136 +    fix x y
3.137 +    assume eq: "M1 #> ?inv x = M1 #> ?inv y" and xy: "x \<in> rcosets H" "y \<in> rcosets H"
3.138 +    have "x = H #> ?inv x"
3.139 +      by (simp add: H_elem_map_eq \<open>x \<in> rcosets H\<close>)
3.140 +    also have "... = H #> ?inv y"
3.141 +    proof (rule coset_mult_inv1 [OF coset_join2])
3.142 +      show "?inv x \<otimes> inv (?inv y) \<in> carrier G"
3.143 +        by (simp add: H_elem_map_carrier \<open>x \<in> rcosets H\<close> \<open>y \<in> rcosets H\<close>)
3.144 +      then show "(?inv x) \<otimes> inv (?inv y) \<in> H"
3.145 +        by (simp add: H_I H_elem_map_carrier xy coset_mult_inv2 eq)
3.146 +      show "H \<subseteq> carrier G"
3.147 +        by (simp add: H_is_subgroup subgroup.subset)
3.148 +    qed (simp_all add: H_is_subgroup H_elem_map_carrier xy)
3.149 +    also have "... = y"
3.150 +      by (simp add: H_elem_map_eq \<open>y \<in> rcosets H\<close>)
3.151 +    finally show "x=y" .
3.152 +  qed
3.153 +  show "(\<lambda>C\<in>rcosets H. M1 #> ?inv C) \<in> rcosets H \<rightarrow> M"
3.154 +    using rcosets_H_funcset_M by blast
3.155 +qed
3.156
3.157  lemma calM_subset_PowG: "calM \<subseteq> Pow (carrier G)"
3.158    by (auto simp: calM_def)
3.159 @@ -289,41 +301,42 @@
3.160    by (metis M_subset_calM finite_calM rev_finite_subset)
3.161
3.162  lemma cardMeqIndexH: "card M = card (rcosets H)"
3.163 -  apply (insert inj_M_GmodH inj_GmodH_M)
3.164 -  apply (blast intro: card_bij finite_M H_is_subgroup
3.165 -      rcosets_subset_PowG [THEN finite_subset]
3.166 -      finite_Pow_iff [THEN iffD2])
3.167 -  done
3.168 +  using inj_M_GmodH inj_GmodH_M
3.169 +  by (blast intro: card_bij finite_M H_is_subgroup rcosets_subset_PowG [THEN finite_subset])
3.170
3.171  lemma index_lem: "card M * card H = order G"
3.172    by (simp add: cardMeqIndexH lagrange H_is_subgroup)
3.173
3.174 -lemma lemma_leq1: "p^a \<le> card H"
3.175 -  apply (rule dvd_imp_le)
3.176 -   apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
3.177 -   prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
3.179 -  done
3.180 -
3.181 -lemma lemma_leq2: "card H \<le> p^a"
3.182 -  apply (subst card_M1 [symmetric])
3.183 -  apply (cut_tac M1_inj_H)
3.184 -  apply (blast intro!: M1_subset_G intro: card_inj H_into_carrier_G finite_subset [OF _ finite_G])
3.185 -  done
3.186 -
3.187  lemma card_H_eq: "card H = p^a"
3.188 -  by (blast intro: le_antisym lemma_leq1 lemma_leq2)
3.189 +proof (rule antisym)
3.190 +  show "p^a \<le> card H"
3.191 +  proof (rule dvd_imp_le)
3.192 +    show "p ^ a dvd card H"
3.193 +      apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
3.195 +    show "0 < card H"
3.196 +      by (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
3.197 +  qed
3.198 +next
3.199 +  show "card H \<le> p^a"
3.200 +    using M1_inj_H card_M1 card_inj finite_M1 by fastforce
3.201 +qed
3.202
3.203  end
3.204
3.205  lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G \<and> card H = p^a"
3.206 -  using lemma_A1
3.207 -  apply clarify
3.208 -  apply (frule existsM1inM, clarify)
3.209 -  apply (subgoal_tac "sylow_central G p a m M1 M")
3.210 -   apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
3.211 -  apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
3.212 -  done
3.213 +proof -
3.214 +  obtain M where M: "M \<in> calM // RelM" "\<not> (p ^ Suc (multiplicity p m) dvd card M)"
3.215 +    using lemma_A1 by blast
3.216 +  then obtain M1 where "M1 \<in> M"
3.217 +    by (metis existsM1inM)
3.218 +  define H where "H \<equiv> {g. g \<in> carrier G \<and> M1 #> g = M1}"
3.219 +  with M \<open>M1 \<in> M\<close>
3.220 +  interpret sylow_central G p a m calM RelM H M1 M
3.221 +    by unfold_locales (auto simp add: H_def calM_def RelM_def)
3.222 +  show ?thesis
3.223 +    using H_is_subgroup card_H_eq by blast
3.224 +qed
3.225
3.226  text \<open>Needed because the locale's automatic definition refers to
3.227    @{term "semigroup G"} and @{term "group_axioms G"} rather than
```