# HG changeset patch
# User wenzelm
# Date 1473629423 -7200
# Node ID 23134a486dc676c50753f0e273e709c95266d209
# Parent  9c22a97b767445cc323e6e7a3b5d9000b9c344e2
tuned proofs;

diff -r 9c22a97b7674 -r 23134a486dc6 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Sep 11 18:12:16 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Sep 11 23:30:23 2016 +0200
@@ -187,8 +187,7 @@
     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
 
@@ -319,14 +318,12 @@
   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
@@ -559,8 +556,7 @@
   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
@@ -784,8 +780,7 @@
   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" ..
@@ -804,8 +799,7 @@
     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" ..
@@ -1184,10 +1178,11 @@
     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)
 
@@ -1203,7 +1198,7 @@
     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
 
 
@@ -2181,7 +2176,7 @@
     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+)
@@ -2840,7 +2835,7 @@
          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"
@@ -2860,7 +2855,7 @@
          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"
@@ -3311,7 +3306,7 @@
 
   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)