Re: [isabelle] [Isabelle2016-1-RC4] Simplification of numerals very slow when Primes is imported



Last round of refinementâ

I am still at a loss to explain why this obviously somehow evil simp
rule did not result in such a mess in earlier releases and hence I am
uncertain whether we should really attempt to resolved this now.

Cheers,
	Florian

Am 09.12.2016 um 08:08 schrieb Florian Haftmann:
> Next round of refinementâ
> 
> Am 08.12.2016 um 17:59 schrieb Florian Haftmann:
>> Hi all,
>>
>> after a short chat with Manuel I was able to pin down the offending simp
>> rule.
>>
>> But I have to check first whether this causes any breakdown in the distro.
>>
>> Cheers,
>> 	Florian
>>
>> Am 08.12.2016 um 16:59 schrieb Stefan Berghofer:
>>> Dear all,
>>>
>>> while updating some of my theories to Isabelle2016-1, I noticed that
>>> simplification of some goals
>>> involving numerals is extremely slow when the "Primes" theory is
>>> imported. In the attachment, you
>>> can find a small theory containing two applications of "simp". When the
>>> Primes theory is loaded,
>>> the first application takes about a minute to complete, whereas the
>>> second one returns almost
>>> immediately. When importing Main instead of Primes, both invocations of
>>> simp are equally fast.
>>> I did not observe this behaviour with Isabelle2016. Does anyone have an
>>> idea what is going wrong?
>>> Perhaps the simpset got messed up during the recent update of the number
>>> theory library?
>>>
>>> Greetings,
>>> Stefan
>>
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
# HG changeset patch
# Parent  3e20defb1e3cb9d3a774394c67e62741fa96f8b3
removed dangerous simp rule: prime computations can be excessively long

diff -r 3e20defb1e3c src/HOL/Number_Theory/Factorial_Ring.thy
--- a/src/HOL/Number_Theory/Factorial_Ring.thy	Thu Dec 08 15:11:20 2016 +0100
+++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Dec 09 08:07:24 2016 +0100
@@ -451,7 +451,7 @@
 lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
   by (intro prime_elem_dvd_multD) simp_all
 
-lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
+lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   by (auto dest: prime_dvd_multD)
 
 lemma prime_dvd_power: 
@@ -1640,7 +1640,6 @@
        (insert nz False, auto simp: Gcd_factorial_eq_0_iff)
 qed (simp_all add: Gcd_factorial_def)
 
-
 lemma normalize_Lcm_factorial:
   "normalize (Lcm_factorial A) = Lcm_factorial A"
 proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
diff -r 3e20defb1e3c src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Thu Dec 08 15:11:20 2016 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy	Fri Dec 09 08:07:24 2016 +0100
@@ -12,12 +12,12 @@
 lemma cong_prime_prod_zero_nat: 
   fixes a::nat
   shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
-  by (auto simp add: cong_altdef_nat)
+  by (auto simp add: cong_altdef_nat prime_dvd_mult_iff)
 
 lemma cong_prime_prod_zero_int: 
   fixes a::int
   shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
-  by (auto simp add: cong_altdef_int)
+  by (auto simp add: cong_altdef_int prime_dvd_mult_iff)
 
 
 locale GAUSS =
# 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

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.