more modernisaton and de-applying
authorpaulson <lp15@cam.ac.uk>
Sun Jun 24 11:41:32 2018 +0100 (14 months ago)
changeset 68488dfbd80c3d180
parent 68485 28f9e9b80c49
child 68489 56034bd1b5f6
more modernisaton and de-applying
src/HOL/Algebra/Complete_Lattice.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Sylow.thy
     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.85        by (simp add: Cons_nth_drop_Suc)
    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.178 -  apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd zero_less_m)
   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.194 +      by (simp add: index_lem multiplicity_dvd order_G power_add)
   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