more lemmas
authorhaftmann
Fri Sep 16 12:30:55 2016 +0200 (2016-09-16)
changeset 63904b8482e12a2a8
parent 63903 8c9dc05fc055
child 63905 1c3dcb5fe6cb
more lemmas
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Primes.thy
     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.6  
     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)
    1.15  
     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.6  
     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.56  
    2.57  (* TODO Legacy names *)
    2.58  lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]