src/HOL/Computational_Algebra/Factorial_Ring.thy
 changeset 69785 9e326f6f8a24 parent 68606 96a49db47c97
```     1.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Feb 02 15:52:14 2019 +0100
1.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Feb 04 12:16:03 2019 +0100
1.3 @@ -1290,6 +1290,11 @@
1.4    with assms show "normalize x = normalize y" by (simp add: prod_mset_prime_factorization)
1.5  qed (rule prime_factorization_cong)
1.6
1.7 +lemma prime_factorization_eqI:
1.8 +  assumes "\<And>p. p \<in># P \<Longrightarrow> prime p" "prod_mset P = n"
1.9 +  shows   "prime_factorization n = P"
1.10 +  using prime_factorization_prod_mset_primes[of P] assms by simp
1.11 +
1.12  lemma prime_factorization_mult:
1.13    assumes "x \<noteq> 0" "y \<noteq> 0"
1.14    shows   "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
1.15 @@ -1543,6 +1548,40 @@
1.16    with \<open>m \<le> n\<close> show thesis ..
1.17  qed
1.18
1.19 +lemma divide_out_primepow_ex:
1.20 +  assumes "n \<noteq> 0" "\<exists>p\<in>prime_factors n. P p"
1.21 +  obtains p k n' where "P p" "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
1.22 +proof -
1.23 +  from assms obtain p where p: "P p" "prime p" "p dvd n"
1.24 +    by auto
1.25 +  define k where "k = multiplicity p n"
1.26 +  define n' where "n' = n div p ^ k"
1.27 +  have n': "n = p ^ k * n'" "\<not>p dvd n'"
1.28 +    using assms p multiplicity_decompose[of n p]
1.29 +    by (auto simp: n'_def k_def multiplicity_dvd)
1.30 +  from n' p have "k > 0" by (intro Nat.gr0I) auto
1.31 +  with n' p that[of p n' k] show ?thesis by auto
1.32 +qed
1.33 +
1.34 +lemma divide_out_primepow:
1.35 +  assumes "n \<noteq> 0" "\<not>is_unit n"
1.36 +  obtains p k n' where "prime p" "p dvd n" "\<not>p dvd n'" "k > 0" "n = p ^ k * n'"
1.37 +  using divide_out_primepow_ex[OF assms(1), of "\<lambda>_. True"] prime_divisor_exists[OF assms] assms
1.38 +        prime_factorsI by metis
1.39 +
1.40 +lemma Ex_other_prime_factor:
1.41 +  assumes "n \<noteq> 0" and "\<not>(\<exists>k. normalize n = p ^ k)" "prime p"
1.42 +  shows   "\<exists>q\<in>prime_factors n. q \<noteq> p"
1.43 +proof (rule ccontr)
1.44 +  assume *: "\<not>(\<exists>q\<in>prime_factors n. q \<noteq> p)"
1.45 +  have "normalize n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
1.46 +    using assms(1) by (intro prod_prime_factors [symmetric]) auto
1.47 +  also from * have "\<dots> = (\<Prod>p\<in>{p}. p ^ multiplicity p n)"
1.48 +    using assms(3) by (intro prod.mono_neutral_left) (auto simp: prime_factors_multiplicity)
1.49 +  finally have "normalize n = p ^ multiplicity p n" by auto
1.50 +  with assms show False by auto
1.51 +qed
1.52 +
1.53
1.54  subsection \<open>GCD and LCM computation with unique factorizations\<close>
1.55
```