# HG changeset patch
# User paulson
# Date 1529836901 -3600
# Node ID 56034bd1b5f6a5825bb4ffd7872b7e9a3694b3e5
# Parent  3d710aa238463eedd826aec928f9d67f23ee0f63# Parent  dfbd80c3d18026fd8f79b7ec854a4f9ef453cbf4
merged

diff -r 3d710aa23846 -r 56034bd1b5f6 src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Sat Jun 23 17:05:59 2018 +0200
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Sun Jun 24 11:41:41 2018 +0100
@@ -43,11 +43,8 @@
 proof -
   interpret dual: weak_lattice "inv_gorder L"
     by (metis dual_weak_lattice)
-
   show ?thesis
-    apply (unfold_locales)
-    apply (simp_all add:inf_exists sup_exists)
-  done
+    by (unfold_locales) (simp_all add:inf_exists sup_exists)
 qed
 
 lemma (in weak_complete_lattice) supI:
@@ -125,32 +122,21 @@
   have B_L: "?B \<subseteq> carrier L" by simp
   from inf_exists [OF B_L B_non_empty]
   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
+  then have bcarr: "b \<in> carrier L"
+    by auto
   have "least L b (Upper L A)"
-apply (rule least_UpperI)
-   apply (rule greatest_le [where A = "Lower L ?B"])
-    apply (rule b_inf_B)
-   apply (rule Lower_memI)
-    apply (erule Upper_memD [THEN conjunct1])
-     apply assumption
-    apply (rule L)
-   apply (fast intro: L [THEN subsetD])
-  apply (erule greatest_Lower_below [OF b_inf_B])
-  apply simp
- apply (rule L)
-apply (rule greatest_closed [OF b_inf_B])
-done
+  proof (rule least_UpperI)
+    show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
+      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_mp)
+    show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
+      by (meson B_L b_inf_B greatest_Lower_below)
+  qed (use bcarr L in auto)
   then show "\<exists>s. least L s (Upper L A)" ..
 next
   fix A
   assume L: "A \<subseteq> carrier L"
   show "\<exists>i. greatest L i (Lower L A)"
-  proof (cases "A = {}")
-    case True then show ?thesis
-      by (simp add: top_exists)
-  next
-    case False with L show ?thesis
-      by (rule inf_exists)
-  qed
+    by (metis L Lower_empty inf_exists top_exists)
 qed
 
 
@@ -205,12 +191,8 @@
 proof -
   obtain i where "greatest L i (Lower L A)"
     by (metis assms inf_exists)
-
   thus ?thesis
-    apply (simp add: inf_def)
-    apply (rule someI2[of _ "i"])
-    apply (auto)
-  done
+    by (metis inf_def someI_ex)
 qed
 
 lemma inf_lower:
@@ -231,17 +213,20 @@
   by (metis bottom_weak_eq inf_closed inf_lower subset_refl)
 
 lemma weak_inf_insert [simp]: 
-  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
-  apply (rule weak_le_antisym)
-  apply (force intro: meet_le inf_greatest inf_lower inf_closed)
-  apply (rule inf_greatest)
-  apply (force)
-  apply (force intro: inf_closed)
-  apply (auto)
-  apply (metis inf_closed meet_left)
-  apply (force intro: le_trans inf_closed meet_right meet_left inf_lower)
-done
-
+  assumes "a \<in> carrier L" "A \<subseteq> carrier L"
+  shows "\<Sqinter>insert a A .= a \<sqinter> \<Sqinter>A"
+proof (rule weak_le_antisym)
+  show "\<Sqinter>insert a A \<sqsubseteq> a \<sqinter> \<Sqinter>A"
+    by (simp add: assms inf_lower local.inf_greatest meet_le)
+  show aA: "a \<sqinter> \<Sqinter>A \<in> carrier L"
+    using assms by simp
+  show "a \<sqinter> \<Sqinter>A \<sqsubseteq> \<Sqinter>insert a A"
+    apply (rule inf_greatest)
+    using assms apply (simp_all add: aA)
+    by (meson aA inf_closed inf_lower local.le_trans meet_left meet_right subsetCE)
+  show "\<Sqinter>insert a A \<in> carrier L"
+    using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
+qed
 
 subsection \<open>Supremum Laws\<close>
 
@@ -268,17 +253,20 @@
   by (metis Lower_closed Lower_empty sup_closed sup_upper top_closed top_higher weak_le_antisym)
 
 lemma weak_sup_insert [simp]: 
-  "\<lbrakk> a \<in> carrier L; A \<subseteq> carrier L \<rbrakk> \<Longrightarrow> \<Squnion>insert a A .= a \<squnion> \<Squnion>A"
-  apply (rule weak_le_antisym)
-  apply (rule sup_least)
-  apply (auto)
-  apply (metis join_left sup_closed)
-  apply (rule le_trans) defer
-  apply (rule join_right)
-  apply (auto)
-  apply (rule join_le)
-  apply (auto intro: sup_upper sup_least sup_closed)
-done
+  assumes "a \<in> carrier L" "A \<subseteq> carrier L"
+  shows "\<Squnion>insert a A .= a \<squnion> \<Squnion>A"
+proof (rule weak_le_antisym)
+  show aA: "a \<squnion> \<Squnion>A \<in> carrier L"
+    using assms by simp
+  show "\<Squnion>insert a A \<sqsubseteq> a \<squnion> \<Squnion>A"
+    apply (rule sup_least)
+    using assms apply (simp_all add: aA)
+    by (meson aA join_left join_right local.le_trans subsetCE sup_closed sup_upper)
+  show "a \<squnion> \<Squnion>A \<sqsubseteq> \<Squnion>insert a A"
+    by (simp add: assms join_le local.sup_least sup_upper)
+  show "\<Squnion>insert a A \<in> carrier L"
+    using assms by (force intro: le_trans inf_closed meet_right meet_left inf_lower)
+qed
 
 end
 
@@ -303,30 +291,26 @@
 proof -
   from assms(2) have AL: "A \<subseteq> carrier L"
     by (auto simp add: fps_def)
-  
   show ?thesis
   proof (rule sup_cong, simp_all add: AL)
     from assms(1) AL show "f ` A \<subseteq> carrier L"
-      by (auto)
+      by auto
+    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"
+      by (meson AL assms(2) image_eqI local.sym subsetCE use_fps)
     from assms(2) show "f ` A {.=} A"
-      apply (auto simp add: fps_def)
-      apply (rule set_eqI2)
-      apply blast
-      apply (rename_tac b)
-      apply (rule_tac x="f b" in bexI)
-      apply (metis (mono_tags, lifting) Ball_Collect assms(1) Pi_iff local.sym)
-      apply (auto)
-    done
+      by (auto simp add: fps_def intro: set_eqI2 [OF _ *])
   qed
 qed
 
 lemma (in weak_complete_lattice) fps_idem:
-  "\<lbrakk> f \<in> carrier L \<rightarrow> carrier L; Idem f \<rbrakk> \<Longrightarrow> fps L f {.=} f ` carrier L"
-  apply (rule set_eqI2)
-  apply (auto simp add: idempotent_def fps_def)
-  apply (metis Pi_iff local.sym)
-  apply force
-done
+  assumes "f \<in> carrier L \<rightarrow> carrier L" "Idem f"
+  shows "fps L f {.=} f ` carrier L"
+proof (rule set_eqI2)
+  show "\<And>a. a \<in> fps L f \<Longrightarrow> \<exists>b\<in>f ` carrier L. a .= b"
+    using assms by (force simp add: fps_def intro: local.sym)
+  show "\<And>b. b \<in> f ` carrier L \<Longrightarrow> \<exists>a\<in>fps L f. b .= a"
+    using assms by (force simp add: idempotent_def fps_def)
+qed
 
 context weak_complete_lattice
 begin
@@ -392,20 +376,19 @@
 lemma LFP_lemma2: 
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   shows "f (LFP f) \<sqsubseteq> LFP f"
-  using assms
-  apply (auto simp add:Pi_def)
-  apply (rule LFP_greatest)
-  apply (metis LFP_closed)
-  apply (metis LFP_closed LFP_lowerbound le_trans use_iso1)
-done
+proof (rule LFP_greatest)
+  have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
+    using assms by (auto simp add: Pi_def)
+  with assms show "f (LFP f) \<in> carrier L"
+    by blast
+  show "\<And>u. \<lbrakk>u \<in> carrier L; f u \<sqsubseteq> u\<rbrakk> \<Longrightarrow> f (LFP f) \<sqsubseteq> u"
+    by (meson LFP_closed LFP_lowerbound assms(1) f local.le_trans use_iso1)
+qed
 
 lemma LFP_lemma3: 
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   shows "LFP f \<sqsubseteq> f (LFP f)"
-  using assms
-  apply (auto simp add:Pi_def)
-  apply (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
-done
+  using assms by (simp add: Pi_def) (metis LFP_closed LFP_lemma2 LFP_lowerbound assms(2) use_iso2)
 
 lemma LFP_weak_unfold: 
   "\<lbrakk> Mono f; f \<in> carrier L \<rightarrow> carrier L \<rbrakk> \<Longrightarrow> LFP f .= f (LFP f)"
@@ -477,12 +460,14 @@
 lemma GFP_lemma2:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
   shows "GFP f \<sqsubseteq> f (GFP f)"
-  using assms
-  apply (auto simp add:Pi_def)
-  apply (rule GFP_least)
-  apply (metis GFP_closed)
-  apply (metis GFP_closed GFP_upperbound le_trans use_iso2)
-done
+proof (rule GFP_least)
+  have f: "\<And>x. x \<in> carrier L \<Longrightarrow> f x \<in> carrier L"
+    using assms by (auto simp add: Pi_def)
+  with assms show "f (GFP f) \<in> carrier L"
+    by blast
+  show "\<And>u. \<lbrakk>u \<in> carrier L; u \<sqsubseteq> f u\<rbrakk> \<Longrightarrow> u \<sqsubseteq> f (GFP f)"
+    by (meson GFP_closed GFP_upperbound le_trans assms(1) f local.le_trans use_iso1)
+qed
 
 lemma GFP_lemma3:
   assumes "Mono f" "f \<in> carrier L \<rightarrow> carrier L"
@@ -599,20 +584,15 @@
   have B_L: "?B \<subseteq> carrier L" by simp
   from inf_exists [OF B_L B_non_empty]
   obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
+  then have bcarr: "b \<in> carrier L"
+    by blast
   have "least L b (Upper L A)"
-apply (rule least_UpperI)
-   apply (rule greatest_le [where A = "Lower L ?B"])
-    apply (rule b_inf_B)
-   apply (rule Lower_memI)
-    apply (erule Upper_memD [THEN conjunct1])
-     apply assumption
-    apply (rule L)
-   apply (fast intro: L [THEN subsetD])
-  apply (erule greatest_Lower_below [OF b_inf_B])
-  apply simp
- apply (rule L)
-apply (rule greatest_closed [OF b_inf_B])
-done
+  proof (rule least_UpperI)
+    show "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> b"
+      by (meson L Lower_memI Upper_memD b_inf_B greatest_le set_rev_mp)
+    show "\<And>y. y \<in> Upper L A \<Longrightarrow> b \<sqsubseteq> y"
+      by (auto elim: greatest_Lower_below [OF b_inf_B])
+  qed (use L bcarr in auto)
   then show "\<exists>s. least L s (Upper L A)" ..
 next
   fix A
@@ -666,23 +646,11 @@
 context weak_complete_lattice
 begin
 
-  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"
-    apply (rule weak_le_antisym)
-    apply (rule sup_least)
-    apply (auto simp add: at_least_at_most_closed)
-    apply (rule sup_upper)
-    apply (auto simp add: at_least_at_most_closed)
-  done
+  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"
+    by (rule weak_le_antisym [OF sup_least sup_upper]) (auto simp add: at_least_at_most_closed)
 
-  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"
-    apply (rule weak_le_antisym)
-    apply (rule inf_lower)
-    apply (auto simp add: at_least_at_most_closed)
-    apply (rule inf_greatest)
-    apply (auto simp add: at_least_at_most_closed)
-  done
+  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"
+    by (rule weak_le_antisym [OF inf_lower inf_greatest]) (auto simp add: at_least_at_most_closed)
 
 end
 
@@ -695,7 +663,7 @@
   interpret weak_partial_order "L \<lparr> carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<rparr>"
   proof -
     have "\<lbrace>a..b\<rbrace>\<^bsub>L\<^esub> \<subseteq> carrier L"
-      by (auto, simp add: at_least_at_most_def)
+      by (auto simp add: at_least_at_most_def)
     thus "weak_partial_order (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>)"
       by (simp add: L.weak_partial_order_axioms weak_partial_order_subset)
   qed
diff -r 3d710aa23846 -r 56034bd1b5f6 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sat Jun 23 17:05:59 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Jun 24 11:41:41 2018 +0100
@@ -2382,10 +2382,8 @@
   interpret weak_lower_semilattice "division_rel G"
     by simp
   show ?thesis
-    apply (subst (2 3) somegcd_meet, (simp add: carr)+)
-    apply (simp add: somegcd_meet carr)
-    apply (rule weak_meet_assoc[simplified], fact+)
-    done
+    unfolding associated_def
+    by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
 qed
 
 lemma (in gcd_condition_monoid) gcd_mult:
@@ -2645,10 +2643,7 @@
       by blast
     have a'fs: "wfactors G as a'"
       apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
-      apply (simp add: a)
-      apply (insert ascarr a'carr)
-      apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
-      done
+      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)
     from afs have ahirr: "irreducible G ah"
       by (elim wfactorsE) simp
     with ascarr have ahprime: "prime G ah"
@@ -2674,31 +2669,18 @@
     from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
       by blast
     with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
-      apply -
-      apply (elim irreducible_prodE[of "ah" "x"], assumption+)
-       apply (rule associatedI2[of x], assumption+)
-      apply (rule irreducibleE[OF ahirr], simp)
-      done
-
+      by (metis ahprime associatedI2 irreducible_prodE primeE)
     note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
     note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
     note carr = carr partscarr
 
     have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
-      apply (intro wfactors_prod_exists)
-      using setparts afs'
-       apply (fast elim: wfactorsE)
-      apply simp
-      done
+      by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
     then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
       by auto
 
     have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
-      apply (intro wfactors_prod_exists)
-      using setparts afs'
-       apply (fast elim: wfactorsE)
-      apply simp
-      done
+      by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
     then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
       and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
       by auto
@@ -2709,21 +2691,12 @@
     have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
       by (intro wfactors_mult, simp+)
     then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
-      apply (intro wfactors_mult_single)
-      using setparts afs'
-          apply (fast intro: nth_mem[OF len] elim: wfactorsE)
-         apply simp_all
-      done
-
+      using irrasi wfactors_mult_single by auto
     from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
       by (metis irrasi wfactors_mult_single)
     with len carr aa1carr aa2carr aa1fs
     have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
-      apply (intro wfactors_mult)
-           apply fast
-          apply (simp, (fast intro: nth_mem[OF len])?)+
-      done
-
+      using wfactors_mult by auto
     from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
       by (simp add: Cons_nth_drop_Suc)
     with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
@@ -2763,14 +2736,8 @@
     note ee1
     also note ee2
     also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
-      (take i as' @ as' ! i # drop (Suc i) as')"
-      apply (intro essentially_equalI)
-       apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
-          take i as' @ as' ! i # drop (Suc i) as'")
-        apply simp
-       apply (rule perm_append_Cons)
-      apply simp
-      done
+                                   (take i as' @ as' ! i # drop (Suc i) as')"
+      by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
     finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
       by simp
     then show "essentially_equal G (ah # as) as'"
@@ -2813,21 +2780,17 @@
 
 lemma (in factorial_monoid) factorcount_unique:
   assumes afs: "wfactors G as a"
-    and acarr[simp]: "a \<in> carrier G" and ascarr[simp]: "set as \<subseteq> carrier G"
+    and acarr[simp]: "a \<in> carrier G" and ascarr: "set as \<subseteq> carrier G"
   shows "factorcount G a = length as"
 proof -
   have "\<exists>ac. \<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
     by (rule factorcount_exists) simp
   then obtain ac where alen: "\<forall>as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> ac = length as"
     by auto
-  have ac: "ac = factorcount G a"
-    apply (simp add: factorcount_def)
-    apply (rule theI2)
-      apply (rule alen)
-     apply (metis afs alen ascarr)+
-    done
+  then have ac: "ac = factorcount G a"
+    unfolding factorcount_def using ascarr by (blast intro: theI2 afs)
   from ascarr afs have "ac = length as"
-    by (iprover intro: alen[rule_format])
+    by (simp add: alen)
   with ac show ?thesis
     by simp
 qed
@@ -2872,11 +2835,8 @@
     and bcarr: "b \<in> carrier G"
     and asc: "a \<sim> b"
   shows "factorcount G a = factorcount G b"
-  apply (rule associatedE[OF asc])
-  apply (drule divides_fcount[OF _ acarr bcarr])
-  apply (drule divides_fcount[OF _ bcarr acarr])
-  apply simp
-  done
+  using assms
+  by (auto simp: associated_def factorial_monoid.divides_fcount factorial_monoid_axioms le_antisym)
 
 lemma (in factorial_monoid) properfactor_fcount:
   assumes acarr: "a \<in> carrier G" and bcarr:"b \<in> carrier G"
diff -r 3d710aa23846 -r 56034bd1b5f6 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Sat Jun 23 17:05:59 2018 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Sun Jun 24 11:41:41 2018 +0100
@@ -161,23 +161,17 @@
   by (simp add: H_def coset_mult_assoc [symmetric])
 
 lemma H_not_empty: "H \<noteq> {}"
-  apply (simp add: H_def)
-  apply (rule exI [of _ \<one>])
-  apply simp
-  done
+  by (force simp add: H_def intro: exI [of _ \<one>])
 
 lemma H_is_subgroup: "subgroup H G"
-  apply (rule subgroupI)
-     apply (rule subsetI)
-     apply (erule H_into_carrier_G)
-    apply (rule H_not_empty)
-   apply (simp add: H_def)
-   apply clarify
-   apply (erule_tac P = "\<lambda>z. lhs z = M1" for lhs in subst)
-   apply (simp add: coset_mult_assoc )
-  apply (blast intro: H_m_closed)
-  done
-
+proof (rule subgroupI)
+  show "H \<subseteq> carrier G"
+    using H_into_carrier_G by blast
+  show "\<And>a. a \<in> H \<Longrightarrow> inv a \<in> H"
+    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)
+  show "\<And>a b. \<lbrakk>a \<in> H; b \<in> H\<rbrakk> \<Longrightarrow> a \<otimes> b \<in> H"
+    by (blast intro: H_m_closed)
+qed (use H_not_empty in auto)
 
 lemma rcosetGM1g_subset_G: "\<lbrakk>g \<in> carrier G; x \<in> M1 #> g\<rbrakk> \<Longrightarrow> x \<in> carrier G"
   by (blast intro: M1_subset_G [THEN r_coset_subset_G, THEN subsetD])
@@ -191,13 +185,19 @@
 lemma M1_cardeq_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> card (M1 #> g) = card M1"
   by (metis M1_subset_G card_rcosets_equal rcosetsI)
 
-lemma M1_RelM_rcosetGM1g: "g \<in> carrier G \<Longrightarrow> (M1, M1 #> g) \<in> RelM"
-  apply (simp add: RelM_def calM_def card_M1)
-  apply (rule conjI)
-   apply (blast intro: rcosetGM1g_subset_G)
-  apply (simp add: card_M1 M1_cardeq_rcosetGM1g)
-  apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
-  done
+lemma M1_RelM_rcosetGM1g: 
+  assumes "g \<in> carrier G"
+  shows "(M1, M1 #> g) \<in> RelM"
+proof -
+  have "M1 #> g \<subseteq> carrier G"
+    by (simp add: assms r_coset_subset_G)
+  moreover have "card (M1 #> g) = p ^ a"
+    using assms by (simp add: card_M1 M1_cardeq_rcosetGM1g)
+  moreover have "\<exists>h\<in>carrier G. M1 = M1 #> g #> h"
+    by (metis assms M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
+  ultimately show ?thesis
+    by (simp add: RelM_def calM_def card_M1)
+qed
 
 end
 
@@ -226,20 +226,26 @@
   by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup.subset)
 
 lemma inj_M_GmodH: "\<exists>f \<in> M \<rightarrow> rcosets H. inj_on f M"
-  apply (rule bexI)
-   apply (rule_tac [2] M_funcset_rcosets_H)
-  apply (rule inj_onI, simp)
-  apply (rule trans [OF _ M_elem_map_eq])
-   prefer 2 apply assumption
-  apply (rule M_elem_map_eq [symmetric, THEN trans], assumption)
-  apply (rule coset_mult_inv1)
-     apply (erule_tac [2] M_elem_map_carrier)+
-   apply (rule_tac [2] M1_subset_G)
-  apply (rule coset_join1 [THEN in_H_imp_eq])
-    apply (rule_tac [3] H_is_subgroup)
-   prefer 2 apply (blast intro: M_elem_map_carrier)
-  apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
-  done
+proof
+  let ?inv = "\<lambda>x. SOME g. g \<in> carrier G \<and> M1 #> g = x"
+  show "inj_on (\<lambda>x\<in>M. H #> ?inv x) M"
+  proof (rule inj_onI, simp)
+    fix x y
+    assume eq: "H #> ?inv x = H #> ?inv y" and xy: "x \<in> M" "y \<in> M"
+    have "x = M1 #> ?inv x"
+      by (simp add: M_elem_map_eq \<open>x \<in> M\<close>)
+    also have "... = M1 #> ?inv y"
+    proof (rule coset_mult_inv1 [OF in_H_imp_eq [OF coset_join1]])
+      show "H #> ?inv x \<otimes> inv (?inv y) = H"
+        by (simp add: H_into_carrier_G M_elem_map_carrier xy coset_mult_inv2 eq subsetI)
+    qed (simp_all add: H_is_subgroup M_elem_map_carrier xy)
+    also have "... = y"
+      using M_elem_map_eq \<open>y \<in> M\<close> by simp
+    finally show "x=y" .
+  qed
+  show "(\<lambda>x\<in>M. H #> ?inv x) \<in> M \<rightarrow> rcosets H"
+    by (rule M_funcset_rcosets_H)
+qed
 
 end
 
@@ -258,28 +264,34 @@
 
 lemma rcosets_H_funcset_M:
   "(\<lambda>C \<in> rcosets H. M1 #> (SOME g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
-  apply (simp add: RCOSETS_def)
-  apply (fast intro: someI2
-      intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
-  done
+  using in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g]
+  by (simp add: M1_in_M H_elem_map_carrier RCOSETS_def)
 
-text \<open>Close to a duplicate of \<open>inj_M_GmodH\<close>.\<close>
 lemma inj_GmodH_M: "\<exists>g \<in> rcosets H\<rightarrow>M. inj_on g (rcosets H)"
-  apply (rule bexI)
-   apply (rule_tac [2] rcosets_H_funcset_M)
-  apply (rule inj_onI)
-  apply (simp)
-  apply (rule trans [OF _ H_elem_map_eq])
-   prefer 2 apply assumption
-  apply (rule H_elem_map_eq [symmetric, THEN trans], assumption)
-  apply (rule coset_mult_inv1)
-     apply (erule_tac [2] H_elem_map_carrier)+
-   apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
-  apply (rule coset_join2)
-    apply (blast intro: H_elem_map_carrier)
-   apply (rule H_is_subgroup)
-  apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier)
-  done
+proof
+  let ?inv = "\<lambda>x. SOME g. g \<in> carrier G \<and> H #> g = x"
+  show "inj_on (\<lambda>C\<in>rcosets H. M1 #> ?inv C) (rcosets H)"
+  proof (rule inj_onI, simp)
+    fix x y
+    assume eq: "M1 #> ?inv x = M1 #> ?inv y" and xy: "x \<in> rcosets H" "y \<in> rcosets H"
+    have "x = H #> ?inv x"
+      by (simp add: H_elem_map_eq \<open>x \<in> rcosets H\<close>)
+    also have "... = H #> ?inv y"
+    proof (rule coset_mult_inv1 [OF coset_join2])
+      show "?inv x \<otimes> inv (?inv y) \<in> carrier G"
+        by (simp add: H_elem_map_carrier \<open>x \<in> rcosets H\<close> \<open>y \<in> rcosets H\<close>)
+      then show "(?inv x) \<otimes> inv (?inv y) \<in> H"
+        by (simp add: H_I H_elem_map_carrier xy coset_mult_inv2 eq)
+      show "H \<subseteq> carrier G"
+        by (simp add: H_is_subgroup subgroup.subset)
+    qed (simp_all add: H_is_subgroup H_elem_map_carrier xy)
+    also have "... = y"
+      by (simp add: H_elem_map_eq \<open>y \<in> rcosets H\<close>)
+    finally show "x=y" .
+  qed
+  show "(\<lambda>C\<in>rcosets H. M1 #> ?inv C) \<in> rcosets H \<rightarrow> M"
+    using rcosets_H_funcset_M by blast
+qed
 
 lemma calM_subset_PowG: "calM \<subseteq> Pow (carrier G)"
   by (auto simp: calM_def)
@@ -289,41 +301,42 @@
   by (metis M_subset_calM finite_calM rev_finite_subset)
 
 lemma cardMeqIndexH: "card M = card (rcosets H)"
-  apply (insert inj_M_GmodH inj_GmodH_M)
-  apply (blast intro: card_bij finite_M H_is_subgroup
-      rcosets_subset_PowG [THEN finite_subset]
-      finite_Pow_iff [THEN iffD2])
-  done
+  using inj_M_GmodH inj_GmodH_M
+  by (blast intro: card_bij finite_M H_is_subgroup rcosets_subset_PowG [THEN finite_subset])
 
 lemma index_lem: "card M * card H = order G"
   by (simp add: cardMeqIndexH lagrange H_is_subgroup)
 
-lemma lemma_leq1: "p^a \<le> card H"
-  apply (rule dvd_imp_le)
-   apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
-   prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
-  apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd zero_less_m)
-  done
-
-lemma lemma_leq2: "card H \<le> p^a"
-  apply (subst card_M1 [symmetric])
-  apply (cut_tac M1_inj_H)
-  apply (blast intro!: M1_subset_G intro: card_inj H_into_carrier_G finite_subset [OF _ finite_G])
-  done
-
 lemma card_H_eq: "card H = p^a"
-  by (blast intro: le_antisym lemma_leq1 lemma_leq2)
+proof (rule antisym)
+  show "p^a \<le> card H"
+  proof (rule dvd_imp_le)
+    show "p ^ a dvd card H"
+      apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
+      by (simp add: index_lem multiplicity_dvd order_G power_add)
+    show "0 < card H"
+      by (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
+  qed
+next
+  show "card H \<le> p^a"
+    using M1_inj_H card_M1 card_inj finite_M1 by fastforce
+qed
 
 end
 
 lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G \<and> card H = p^a"
-  using lemma_A1
-  apply clarify
-  apply (frule existsM1inM, clarify)
-  apply (subgoal_tac "sylow_central G p a m M1 M")
-   apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
-  apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
-  done
+proof -
+  obtain M where M: "M \<in> calM // RelM" "\<not> (p ^ Suc (multiplicity p m) dvd card M)"
+    using lemma_A1 by blast
+  then obtain M1 where "M1 \<in> M"
+    by (metis existsM1inM) 
+  define H where "H \<equiv> {g. g \<in> carrier G \<and> M1 #> g = M1}"
+  with M \<open>M1 \<in> M\<close>
+  interpret sylow_central G p a m calM RelM H M1 M
+    by unfold_locales (auto simp add: H_def calM_def RelM_def)
+  show ?thesis
+    using H_is_subgroup card_H_eq by blast
+qed
 
 text \<open>Needed because the locale's automatic definition refers to
   @{term "semigroup G"} and @{term "group_axioms G"} rather than