src/HOL/Algebra/Divisibility.thy

   fixes G (structure)
   assumes d: "a divides b"
     and elim: "\<And>c. \<lbrakk>b = a \<otimes> c; c \<in> carrier G\<rbrakk> \<Longrightarrow> P"
   shows "P"
 proof -
-  from dividesD[OF d]
-  obtain c where "c \<in> carrier G" and "b = a \<otimes> c" by auto
+  from dividesD[OF d] obtain c where "c \<in> carrier G" and "b = a \<otimes> c" by auto
   then show P by (elim elim)
 qed
 
 lemma (in monoid) divides_refl[simp, intro!]:
   assumes carr: "a \<in> carrier G"

   shows "\<exists>u\<in>Units G. a = b \<otimes> u"
   using assoc
   unfolding associated_def
 proof clarify
   assume "b divides a"
-  then have "\<exists>u\<in>carrier G. a = b \<otimes> u" by (rule dividesD)
   then obtain u where ucarr: "u \<in> carrier G" and a: "a = b \<otimes> u"
-    by auto
+    by (rule dividesE)
 
   assume "a divides b"
-  then have "\<exists>u'\<in>carrier G. b = a \<otimes> u'" by (rule dividesD)
   then obtain u' where u'carr: "u' \<in> carrier G" and b: "b = a \<otimes> u'"
-    by auto
+    by (rule dividesE)
   note carr = carr ucarr u'carr
 
   from carr have "a \<otimes> \<one> = a" by simp
   also have "\<dots> = b \<otimes> u" by (simp add: a)
   also have "\<dots> = a \<otimes> u' \<otimes> u" by (simp add: b)

 lemma properfactorI2:
   fixes G (structure)
   assumes advdb: "a divides b"
     and neq: "\<not>(a \<sim> b)"
   shows "properfactor G a b"
-  apply (rule properfactorI, rule advdb)
-proof (rule ccontr, simp)
+proof (rule properfactorI, rule advdb, rule notI)
   assume "b divides a"
   with advdb have "a \<sim> b" by (rule associatedI)
   with neq show "False" by fast
 qed
 

     and isunit[rule_format]: "\<forall>ba. ba \<in> carrier G \<and> properfactor G ba (a \<otimes> b) \<longrightarrow> ba \<in> Units G"
   show P
   proof (cases "a \<in> Units G")
     case aunit: True
     have "irreducible G b"
-      apply (rule irreducibleI)
-    proof (rule ccontr, simp)
+    proof (rule irreducibleI, rule notI)
       assume "b \<in> Units G"
       with aunit have "(a \<otimes> b) \<in> Units G" by fast
       with abnunit show "False" ..
     next
       fix c

     with carr have "properfactor G b (b \<otimes> a)" by (fast intro: properfactorI3)
     then have bf: "properfactor G b (a \<otimes> b)" by (subst m_comm[of a b], simp+)
     then have bunit: "b \<in> Units G" by (intro isunit, simp)
 
     have "irreducible G a"
-      apply (rule irreducibleI)
-    proof (rule ccontr, simp)
+    proof (rule irreducibleI, rule notI)
       assume "a \<in> Units G"
       with bunit have "(a \<otimes> b) \<in> Units G" by fast
       with abnunit show "False" ..
     next
       fix c

 lemma (in comm_monoid_cancel) unit_wfactors_empty:
   assumes aunit: "a \<in> Units G"
     and wf: "wfactors G fs a"
     and carr[simp]: "set fs \<subseteq> carrier G"
   shows "fs = []"
-proof (rule ccontr, cases fs, simp)
-  fix f fs'
-  assume fs: "fs = f # fs'"
-
+proof (cases fs)
+  case Nil
+  then show ?thesis .
+next
+  case fs: (Cons f fs')
   from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"
     by (simp_all add: fs)
 
   from fs wf have "irreducible G f" by (simp add: wfactors_def)
   then have fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)

   have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
   have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>"
     by (simp add: Units_closed[OF aunit] a[symmetric])
   finally have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp
   then have "f \<in> Units G" by (intro unit_factor[of f], simp+)
-  with fnunit show "False" by simp
+  with fnunit show ?thesis by contradiction
 qed
 
 
 text \<open>Comparing wfactors\<close>
 

       finally have "p divides a" by simp
       then show ?thesis ..
     next
       case bnunit: False
       have cnunit: "c \<notin> Units G"
-      proof (rule ccontr, simp)
+      proof
         assume cunit: "c \<in> Units G"
         from bnunit have "properfactor G a (a \<otimes> b)"
           by (intro properfactorI3[of _ _ b], simp+)
         also note abpc
         also from cunit have "p \<otimes> c \<sim> p"

            apply (fast intro: unit_divides)
           apply (fast intro: unit_divides)
          apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
          apply (rule r, rule, assumption)
          apply (rule properfactorI, assumption)
-    proof (rule ccontr, simp)
+    proof
       fix y
       assume ycarr: "y \<in> carrier G"
       assume "p divides y"
       also assume "y divides a"
       finally have "p divides a"

            apply (fast intro: unit_divides)
           apply (fast intro: unit_divides)
          apply (clarsimp simp add: Unit_eq_dividesone[symmetric])
          apply (rule r, rule, assumption)
          apply (rule properfactorI, assumption)
-    proof (rule ccontr, simp)
+    proof
       fix y
       assume ycarr: "y \<in> carrier G"
       assume "p divides y"
       also assume "y divides b"
       finally have "p divides b" by (simp add: pcarr ycarr bcarr)

   then have fcb: "factorcount G b = length as + length cs"
     by simp
 
   assume nbdvda: "\<not> b divides a"
   have "c \<notin> Units G"
-  proof (rule ccontr, simp)
+  proof
     assume cunit:"c \<in> Units G"
     have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c"
       by (simp add: b)
     also from ccarr acarr cunit have "\<dots> = a \<otimes> (c \<otimes> inv c)"
       by (fast intro: m_assoc)