src/HOL/Algebra/Divisibility.thy

   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "\<exists>x\<in>carrier G. x = somegcd G a b"
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_closed[simplified], fact+)
-  done
+    by (metis carr(1) carr(2) gcd_closed)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_l:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides a"
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_left[simplified], fact+)
-  done
+    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_r:
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides b"
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_right[simplified], fact+)
-  done
+    by (metis carr gcd_isgcd isgcd_def)
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides:
   assumes sub: "z divides x"  "z divides y"
     and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   shows "z divides (somegcd G x y)"
 proof -
   interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
-    apply (simp add: somegcd_meet L)
-    apply (rule meet_le[simplified], fact+)
-  done
+    by (metis gcd_isgcd isgcd_def assms)
 qed
 
 lemma (in gcd_condition_monoid) gcd_cong_l:
   assumes xx': "x \<sim> x'"
     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"

       using setparts afs'
       by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+)
 
     from aa2carr carr aa1fs aa2fs
       have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
-      apply (intro wfactors_mult_single)
-          apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
-         apply (fast intro: nth_mem[OF len])
-        apply fast
-       apply fast
-      apply assumption
-    done
+        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])?)+

       have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
       by (simp add: drop_Suc_conv_tl)
     with carr
       have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
       by simp
-
     with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
       have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
-      apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'"  "as'"])
-            apply fast+
-          apply (simp, fast)
-    done
+        by (metis as' ee_wfactorsD m_closed)
     then
     have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
-      apply (simp add: m_assoc[symmetric])
-      apply (simp add: m_comm)
-    done
+      by (metis aa1carr aa2carr asicarr m_lcomm)
     from carr asiah
     have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
-      apply (intro mult_cong_l)
-      apply (fast intro: associated_sym, simp+)
-    done
+      by (metis associated_sym m_closed mult_cong_l)
     also note t1
     finally
       have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
 
     with carr aa1carr aa2carr a'carr nth_mem[OF len]

   have "\<exists>as. set as \<subseteq> carrier G \<and> wfactors G as a" by (intro wfactors_exist, simp)
   from this obtain as
       where ascarr[simp]: "set as \<subseteq> carrier G"
       and afs: "wfactors G as a"
       by (auto simp del: carr)
-
   have "ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> length as = length as'"
     by (metis afs ascarr assms ee_length wfactors_unique)
   thus "EX c. ALL as'. set as' \<subseteq> carrier G \<and> wfactors G as' a \<longrightarrow> c = length as'" ..
 qed
 

       by auto
   have ac: "ac = factorcount G a"
     apply (simp add: factorcount_def)
     apply (rule theI2)
       apply (rule alen)
-     apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
-    apply (elim allE[of _ "as"], rule allE[OF alen, of "as"], simp add: ascarr afs)
+     apply (metis afs alen ascarr)+
   done
 
   from ascarr afs have "ac = length as" by (iprover intro: alen[rule_format])
   with ac show ?thesis by simp
 qed