removed dangerous simp rule: prime computations can be excessively long
authorhaftmann
Wed Dec 21 21:26:25 2016 +0100 (2016-12-21)
changeset 646317705926ee595
parent 64630 96015aecfeba
child 64632 9df24b8b6c0a
removed dangerous simp rule: prime computations can be excessively long
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Gauss.thy
     1.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Tue Dec 20 15:39:13 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Wed Dec 21 21:26:25 2016 +0100
     1.3 @@ -451,7 +451,7 @@
     1.4  lemma prime_dvd_multD: "prime p \<Longrightarrow> p dvd a * b \<Longrightarrow> p dvd a \<or> p dvd b"
     1.5    by (intro prime_elem_dvd_multD) simp_all
     1.6  
     1.7 -lemma prime_dvd_mult_iff [simp]: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
     1.8 +lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
     1.9    by (auto dest: prime_dvd_multD)
    1.10  
    1.11  lemma prime_dvd_power: 
    1.12 @@ -1640,7 +1640,6 @@
    1.13         (insert nz False, auto simp: Gcd_factorial_eq_0_iff)
    1.14  qed (simp_all add: Gcd_factorial_def)
    1.15  
    1.16 -
    1.17  lemma normalize_Lcm_factorial:
    1.18    "normalize (Lcm_factorial A) = Lcm_factorial A"
    1.19  proof (cases "subset_mset.bdd_above (prime_factorization ` A)")
     2.1 --- a/src/HOL/Number_Theory/Gauss.thy	Tue Dec 20 15:39:13 2016 +0100
     2.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Wed Dec 21 21:26:25 2016 +0100
     2.3 @@ -12,12 +12,12 @@
     2.4  lemma cong_prime_prod_zero_nat: 
     2.5    fixes a::nat
     2.6    shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
     2.7 -  by (auto simp add: cong_altdef_nat)
     2.8 +  by (auto simp add: cong_altdef_nat prime_dvd_mult_iff)
     2.9  
    2.10  lemma cong_prime_prod_zero_int: 
    2.11    fixes a::int
    2.12    shows "\<lbrakk>[a * b = 0] (mod p); prime p\<rbrakk> \<Longrightarrow> [a = 0] (mod p) | [b = 0] (mod p)"
    2.13 -  by (auto simp add: cong_altdef_int)
    2.14 +  by (auto simp add: cong_altdef_int prime_dvd_mult_iff)
    2.15  
    2.16  
    2.17  locale GAUSS =