# HG changeset patch
# Parent  0a9050b518eed667807fbec5c4a2f09e9031fd63
remove potentially dangerous simp rule prime_dvd_mult_iff

diff -r 0a9050b518ee thys/Algebraic_Numbers/Algebraic_Numbers.thy
--- a/thys/Algebraic_Numbers/Algebraic_Numbers.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/Algebraic_Numbers/Algebraic_Numbers.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -287,7 +287,8 @@
     assume "?gcd \<noteq> 0" 
     from prime_divisor_exists[OF this no_unit] obtain f
       where fg: "f dvd ?gcd" and f: "prime f" by auto
-    from f have prime: "\<And>s t. f dvd s * t \<Longrightarrow> f dvd s \<or> f dvd t" by auto
+    from f have prime: "\<And>s t. f dvd s * t \<Longrightarrow> f dvd s \<or> f dvd t"
+      by (rule prime_dvd_multD)
     have "?gcd dvd p" "?gcd dvd q" by auto
     with fg have "f dvd p" "f dvd q" by auto
     from no_prime_divisor[OF this prime] have "is_unit f" by auto
diff -r 0a9050b518ee thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy
--- a/thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -1074,7 +1074,8 @@
   qed
   moreover have "(fact n::nat) = fact k * fact (n-k) * (n choose k)"
     using binomial_fact_lemma kn by auto
-  ultimately show ?thesis using prime_n by auto
+  ultimately show ?thesis using prime_n
+    by (auto simp add: prime_dvd_mult_iff)
 qed
 
 
diff -r 0a9050b518ee thys/Coinductive/Examples/Hamming_Stream.thy
--- a/thys/Coinductive/Examples/Hamming_Stream.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/Coinductive/Examples/Hamming_Stream.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -238,7 +238,7 @@
 unfolding prime_nat_iff by simp
 
 lemma smooth_times [simp]: "smooth (x * y) \<longleftrightarrow> smooth x \<and> smooth y"
-by(auto simp add: smooth_def)
+by(auto simp add: smooth_def prime_dvd_mult_iff)
 
 lemma smooth2 [simp]: "smooth 2"
 by(auto simp add: smooth_def dest: prime_nat_dvdD[of 2, simplified])
diff -r 0a9050b518ee thys/Fermat3_4/Fermat3.thy
--- a/thys/Fermat3_4/Fermat3.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/Fermat3_4/Fermat3.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -172,7 +172,7 @@
       proof (rule ccontr)
         assume "\<not> \<not> 3 dvd ?g" hence "3 dvd 2*p" by simp
         hence "(3::int) dvd 2 \<or> 3 dvd p"
-          using prime_dvd_multD[of 3] by fastforce
+          using prime_dvd_multD[of 3] by (fastforce simp add: prime_dvd_mult_iff)
         with p3 show False by arith
       qed
       have pq_relprime: "gcd p q=1"
@@ -403,7 +403,7 @@
           moreover have "(3::int) \<noteq> 0" by simp
           ultimately have "h dvd 2*r" by (rule zdvd_mult_cancel)
           with h have "h dvd 2 \<or> h dvd r" 
-            by (auto simp: prime_int_nat_transfer dest: prime_dvd_multD)
+            by (auto simp: prime_int_nat_transfer prime_dvd_mult_iff dest: prime_dvd_multD)
           moreover have "\<not> h dvd 2" 
           proof (rule ccontr, simp)
             assume "h dvd 2" 
diff -r 0a9050b518ee thys/Fermat3_4/Quad_Form.thy
--- a/thys/Fermat3_4/Quad_Form.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/Fermat3_4/Quad_Form.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -147,7 +147,7 @@
       finally show ?thesis by simp
     qed
     with ass have "?P dvd (b*p + a*q) \<or> ?P dvd (b*p - a*q)"
-      by (simp add: nat_abs_mult_distrib prime_int_iff)
+      by (simp add: nat_abs_mult_distrib prime_int_iff prime_dvd_mult_iff)
     moreover
     { assume "?P dvd b*p + a*q"
       hence "?P dvd b*p + 1*a*q \<and> \<bar>1\<bar> = (1::int)" by simp }
diff -r 0a9050b518ee thys/Polynomial_Factorization/Gauss_Lemma.thy
--- a/thys/Polynomial_Factorization/Gauss_Lemma.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/Polynomial_Factorization/Gauss_Lemma.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -294,7 +294,8 @@
       with `int n dvd coeff p r * coeff q s` pn r s
         have "n dvd (nat (abs ?r) * nat (abs ?s))"
           by (subst (asm) (1 2) prime_dvd_mult_eq_int) simp_all
-      with pn have "n dvd nat (abs ?r) \<or> n dvd nat (abs ?s)" by simp
+        with pn have "n dvd nat (abs ?r) \<or> n dvd nat (abs ?s)"
+          by (simp add: prime_dvd_mult_iff)
       also have "(n dvd nat (abs ?r)) = (?n dvd ?r)" using int_dvd_iff by blast
       also have "(n dvd nat (abs ?s)) = (?n dvd ?s)" using int_dvd_iff by blast
       finally have False using r s by auto
diff -r 0a9050b518ee thys/RSAPSS/Productdivides.thy
--- a/thys/RSAPSS/Productdivides.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/RSAPSS/Productdivides.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -16,14 +16,7 @@
 
 lemma productdivides: "\<lbrakk>x mod a = (0::nat); x mod b = 0; prime a; prime b; a \<noteq> b\<rbrakk> \<Longrightarrow> x mod (a*b) = 0"
   apply (simp add: mod_eq_0_iff [of x a])
-  apply (erule exE)
-  apply (simp)
-  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-  apply (drule prime_dvd_mult_nat [of b])
-  apply (erule disjE)
-  apply auto
-  apply (simp add: prime_nat_iff)
-  apply auto
+  apply (auto simp add: dvd_eq_mod_eq_0 [symmetric] prime_dvd_mult_iff dest: primes_dvd_imp_eq)
   done
 
 lemma specializedtoprimes1: 
diff -r 0a9050b518ee thys/SumSquares/FourSquares.thy
--- a/thys/SumSquares/FourSquares.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/SumSquares/FourSquares.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -117,7 +117,7 @@
       hence "p dvd x^2-y^2" using cong_altdef_int by blast
       hence "p dvd (x+y)*(x-y)" by (simp add: power2_eq_square algebra_simps)
       hence "p dvd x+y \<or> p dvd x-y" using p1 p0 
-        by (auto dest: prime_dvd_multD simp: prime_int_nat_transfer)
+        by (auto dest: prime_dvd_multD simp: prime_dvd_mult_iff prime_int_nat_transfer)
       moreover
       { assume "p dvd x+y"
         moreover from xn yn n have "x+y < p" by auto
@@ -154,7 +154,7 @@
       ultimately have "p dvd x^2-y^2" by simp
       hence "p dvd (x+y)*(x-y)" by (simp add: power2_eq_square algebra_simps)
       with p1 have "p dvd x+y \<or> p dvd x-y" using p1 p0 
-        by (auto dest: prime_dvd_multD simp: prime_int_nat_transfer)
+        by (auto dest: prime_dvd_multD simp: prime_dvd_mult_iff prime_int_nat_transfer)
       moreover
       { assume "p dvd x+y"
         moreover from xn yn n have "x+y < p" by auto
diff -r 0a9050b518ee thys/SumSquares/TwoSquares.thy
--- a/thys/SumSquares/TwoSquares.thy	Thu Dec 08 17:40:50 2016 +1100
+++ b/thys/SumSquares/TwoSquares.thy	Fri Dec 09 21:17:18 2016 +0100
@@ -107,7 +107,8 @@
       using assms(1) h3(3) coprime_common_divisor_nat[of a' b' ?p] not_prime_1 by linarith
   }
   hence "\<not> (?p dvd a'^2)" ..
-  hence h7: "\<not> (?p dvd a')" using assms(1) by (simp add: power2_eq_square)
+  hence h7: "\<not> (?p dvd a')" using assms(1)
+    by (simp add: power2_eq_square prime_dvd_mult_iff)
   hence "gcd ?p a' = 1" using assms(1) by (fastforce intro: prime_imp_coprime_nat)
   thm prime_imp_coprime_nat
   moreover have "a' \<noteq> 0" using h7 dvd_0_right[of ?p] by meson