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]
```