src/HOL/Number_Theory/Primes.thy
changeset 63905 1c3dcb5fe6cb
parent 63904 b8482e12a2a8
child 64272 f76b6dda2e56
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Sep 16 12:30:55 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Sep 16 12:30:55 2016 +0200
     1.3 @@ -458,18 +458,17 @@
     1.4  
     1.5  lemma prime_factors_gt_0_nat:
     1.6    "p \<in> prime_factors x \<Longrightarrow> p > (0::nat)"
     1.7 -  by (simp add: prime_factors_prime prime_gt_0_nat)
     1.8 +  by (simp add: in_prime_factors_imp_prime prime_gt_0_nat)
     1.9  
    1.10  lemma prime_factors_gt_0_int:
    1.11    "p \<in> prime_factors x \<Longrightarrow> p > (0::int)"
    1.12 -  by (simp add: prime_factors_prime prime_gt_0_int)
    1.13 +  by (simp add: in_prime_factors_imp_prime prime_gt_0_int)
    1.14  
    1.15 -lemma prime_factors_ge_0_int [elim]:
    1.16 +lemma prime_factors_ge_0_int [elim]: (* FIXME !? *)
    1.17    fixes n :: int
    1.18    shows "p \<in> prime_factors n \<Longrightarrow> p \<ge> 0"
    1.19 -  unfolding prime_factors_def 
    1.20 -  by (auto split: if_splits simp: prime_def dest!: in_prime_factorization_imp_prime)
    1.21 -
    1.22 +  by (drule prime_factors_gt_0_int) simp
    1.23 +  
    1.24  lemma prod_mset_prime_factorization_int:
    1.25    fixes n :: int
    1.26    assumes "n > 0"
    1.27 @@ -605,7 +604,7 @@
    1.28  lemma prime_factors_setprod:
    1.29    assumes "finite A" and "0 \<notin> f ` A"
    1.30    shows "prime_factors (setprod f A) = UNION A (prime_factors \<circ> f)"
    1.31 -  using assms by (simp add: prime_factors_def setprod_unfold_prod_mset prime_factorization_prod_mset)
    1.32 +  using assms by (simp add: setprod_unfold_prod_mset prime_factorization_prod_mset)
    1.33  
    1.34  lemma prime_factors_fact:
    1.35    "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
    1.36 @@ -630,8 +629,7 @@
    1.37    shows "p dvd fact n \<longleftrightarrow> p \<le> n"
    1.38    using assms
    1.39    by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
    1.40 -    prime_factorization_prime prime_factors_def [symmetric]
    1.41 -    prime_factors_fact prime_ge_2_nat)
    1.42 +    prime_factorization_prime prime_factors_fact prime_ge_2_nat)
    1.43  
    1.44  (* TODO Legacy names *)
    1.45  lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]