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



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 =

Attachment: signature.asc
Description: OpenPGP digital signature



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