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