author haftmann Fri Sep 16 12:30:55 2016 +0200 (2016-09-16) changeset 63904 b8482e12a2a8 parent 63903 8c9dc05fc055 child 63905 1c3dcb5fe6cb
more lemmas
1.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Sep 16 21:40:47 2016 +0200
1.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Sep 16 12:30:55 2016 +0200
1.3 @@ -1299,6 +1299,12 @@
1.4  lemma prime_factors_prime [intro]: "p \<in> prime_factors x \<Longrightarrow> prime p"
1.5    by (auto simp: prime_factors_def dest: in_prime_factorization_imp_prime)
1.7 +lemma prime_prime_factors:
1.8 +  assumes "prime p"
1.9 +  shows "prime_factors p = {p}"
1.10 +  using assms by (simp add: prime_factors_def)
1.11 +    (drule prime_factorization_prime, simp)
1.12 +
1.13  lemma prime_factors_dvd [dest]: "p \<in> prime_factors x \<Longrightarrow> p dvd x"
1.14    by (auto simp: prime_factors_def dest: in_prime_factorization_imp_dvd)
2.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Sep 16 21:40:47 2016 +0200
2.2 +++ b/src/HOL/Number_Theory/Primes.thy	Fri Sep 16 12:30:55 2016 +0200
2.3 @@ -597,22 +597,41 @@
2.4    finally show ?thesis .
2.5  qed
2.7 +lemma prime_factorization_prod_mset:
2.8 +  assumes "0 \<notin># A"
2.9 +  shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
2.10 +  using assms by (induct A) (auto simp add: prime_factorization_mult)
2.11 +
2.12 +lemma prime_factors_setprod:
2.13 +  assumes "finite A" and "0 \<notin> f ` A"
2.14 +  shows "prime_factors (setprod f A) = UNION A (prime_factors \<circ> f)"
2.15 +  using assms by (simp add: prime_factors_def setprod_unfold_prod_mset prime_factorization_prod_mset)
2.16 +
2.17 +lemma prime_factors_fact:
2.18 +  "prime_factors (fact n) = {p \<in> {2..n}. prime p}" (is "?M = ?N")
2.19 +proof (rule set_eqI)
2.20 +  fix p
2.21 +  { fix m :: nat
2.22 +    assume "p \<in> prime_factors m"
2.23 +    then have "prime p" and "p dvd m" by auto
2.24 +    moreover assume "m > 0"
2.25 +    ultimately have "2 \<le> p" and "p \<le> m"
2.26 +      by (auto intro: prime_ge_2_nat dest: dvd_imp_le)
2.27 +    moreover assume "m \<le> n"
2.28 +    ultimately have "2 \<le> p" and "p \<le> n"
2.29 +      by (auto intro: order_trans)
2.30 +  } note * = this
2.31 +  show "p \<in> ?M \<longleftrightarrow> p \<in> ?N"
2.32 +    by (auto simp add: fact_setprod prime_factors_setprod Suc_le_eq dest!: prime_prime_factors intro: *)
2.33 +qed
2.34 +
2.35  lemma prime_dvd_fact_iff:
2.36    assumes "prime p"
2.37 -  shows   "p dvd fact n \<longleftrightarrow> p \<le> n"
2.38 -proof (induction n)
2.39 -  case 0
2.40 -  with assms show ?case by auto
2.41 -next
2.42 -  case (Suc n)
2.43 -  have "p dvd fact (Suc n) \<longleftrightarrow> p dvd (Suc n) * fact n" by simp
2.44 -  also from assms have "\<dots> \<longleftrightarrow> p dvd Suc n \<or> p dvd fact n"
2.45 -    by (rule prime_dvd_mult_iff)
2.46 -  also note Suc.IH
2.47 -  also have "p dvd Suc n \<or> p \<le> n \<longleftrightarrow> p \<le> Suc n"
2.48 -    by (auto dest: dvd_imp_le simp: le_Suc_eq)
2.49 -  finally show ?case .
2.50 -qed
2.51 +  shows "p dvd fact n \<longleftrightarrow> p \<le> n"
2.52 +  using assms
2.53 +  by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
2.54 +    prime_factorization_prime prime_factors_def [symmetric]
2.55 +    prime_factors_fact prime_ge_2_nat)
2.57  (* TODO Legacy names *)
2.58  lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]