# HG changeset patch
# User haftmann
# Date 1527153986 0
# Node ID 2bc921b2159b1e79a2891757f30c5ab561b3a16e
# Parent  5ff0ccc7488458a8594bab289d812559c5763b71
treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd

diff -r 5ff0ccc74884 -r 2bc921b2159b src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu May 24 22:28:26 2018 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Thu May 24 09:26:26 2018 +0000
@@ -999,7 +999,7 @@
           using real_of_int_div[OF gpdd] th2 gp0 by simp
         finally have "?lhs = Inum bs t / real_of_int n" by simp
         then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
-      ultimately have ?thesis by blast }
+      ultimately have ?thesis by auto }
     ultimately have ?thesis by blast }
   ultimately show ?thesis by blast
 qed
@@ -1031,7 +1031,7 @@
         have "n div ?g' >0" by simp
         hence ?thesis using assms g1 g'1
           by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
-      ultimately have ?thesis by blast }
+      ultimately have ?thesis by auto }
     ultimately have ?thesis by blast }
   ultimately show ?thesis by blast
 qed
@@ -1171,7 +1171,7 @@
         using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]]
           th2[symmetric] by simp
       finally have ?thesis by simp  }
-    ultimately have ?thesis by blast
+    ultimately have ?thesis by auto
   }
   ultimately show ?thesis by blast
 qed
@@ -3397,7 +3397,7 @@
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))"
-    using int_cases[rule_format] by blast
+    by (auto split: if_splits)
   also have "\<dots> =
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un
    (UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n>0} (\<lambda>(p,n,s). set(map(?f(p,n,s)) [0..n]))) Un
@@ -3411,12 +3411,14 @@
   also have "\<dots> =
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
-    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast
+    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
+    by blast
   finally
   have FS: "?SS (Floor a) =
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
-    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))"    by blast
+    (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s).  {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
+    by blast
   show ?case
   proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, -)
     fix p n s
@@ -3552,7 +3554,7 @@
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))"
-    using int_cases[rule_format] by blast
+    by (auto split: if_splits)
   also have "\<dots> =
     ((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un
     (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [0..n]))) Un
diff -r 5ff0ccc74884 -r 2bc921b2159b src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu May 24 22:28:26 2018 +0200
+++ b/src/HOL/GCD.thy	Thu May 24 09:26:26 2018 +0000
@@ -1287,7 +1287,7 @@
     by (simp add: t_def)
 qed
 
-lemma gcd_eq_1_imp_coprime:
+lemma gcd_eq_1_imp_coprime [dest!]:
   "coprime a b" if "gcd a b = 1"
 proof (rule coprimeI)
   fix c