src/HOL/Computational_Algebra/Factorial_Ring.thy
 changeset 67051 e7e54a0b9197 parent 66938 c78ff0aeba4c child 68606 96a49db47c97
```     1.1 --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -13,12 +13,6 @@
1.4
1.5  subsection \<open>Irreducible and prime elements\<close>
1.6
1.7 -(* TODO: Move ? *)
1.8 -lemma (in semiring_gcd) prod_coprime' [rule_format]:
1.9 -    "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1"
1.10 -  using prod_coprime[of A f a] by (simp add: gcd.commute)
1.11 -
1.12 -
1.13  context comm_semiring_1
1.14  begin
1.15
1.16 @@ -583,7 +577,7 @@
1.17  end
1.18
1.19
1.20 -subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
1.21 +subsection \<open>In a semiring with GCD, each irreducible element is a prime element\<close>
1.22
1.23  context semiring_gcd
1.24  begin
1.25 @@ -620,23 +614,26 @@
1.26    using assms by (simp add: prime_elem_imp_coprime)
1.27
1.28  lemma prime_elem_imp_power_coprime:
1.29 -  "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.30 -  by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
1.31 +  "prime_elem p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.32 +  by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps)
1.33
1.34  lemma prime_imp_power_coprime:
1.35 -  "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.36 -  by (simp add: prime_elem_imp_power_coprime)
1.37 +  "prime p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
1.38 +  by (rule prime_elem_imp_power_coprime) simp_all
1.39
1.40  lemma prime_elem_divprod_pow:
1.41    assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
1.42    shows   "p^n dvd a \<or> p^n dvd b"
1.43    using assms
1.44  proof -
1.45 -  from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
1.46 -    by (auto simp: coprime prime_elem_def)
1.47 -  with p have "coprime (p^n) a \<or> coprime (p^n) b"
1.48 -    by (auto intro: prime_elem_imp_coprime coprime_exp_left)
1.49 -  with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
1.50 +  from p have "\<not> is_unit p"
1.51 +    by simp
1.52 +  with ab p have "\<not> p dvd a \<or> \<not> p dvd b"
1.53 +    using not_coprimeI by blast
1.54 +  with p have "coprime (p ^ n) a \<or> coprime (p ^ n) b"
1.55 +    by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps)
1.56 +  with pab show ?thesis
1.57 +    by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff)
1.58  qed
1.59
1.60  lemma primes_coprime:
1.61 @@ -1524,6 +1521,27 @@
1.62      with assms[of P] assms[of Q] PQ show "P = Q" by simp
1.63  qed
1.64
1.65 +lemma divides_primepow:
1.66 +  assumes "prime p" and "a dvd p ^ n"
1.67 +  obtains m where "m \<le> n" and "normalize a = p ^ m"
1.68 +proof -
1.69 +  from assms have "a \<noteq> 0"
1.70 +    by auto
1.71 +  with assms
1.72 +  have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))"
1.73 +    by (simp add: prod_mset_prime_factorization)
1.74 +  then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)"
1.75 +    by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff)
1.76 +  with assms have "prime_factorization a \<subseteq># replicate_mset n p"
1.77 +    by (simp add: prime_factorization_prime_power)
1.78 +  then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p"
1.79 +    by (rule msubseteq_replicate_msetE)
1.80 +  then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)"
1.81 +    by simp
1.82 +  with \<open>a \<noteq> 0\<close> have "normalize a = p ^ m"
1.83 +    by (simp add: prod_mset_prime_factorization)
1.84 +  with \<open>m \<le> n\<close> show thesis ..
1.85 +qed
1.86
1.87
1.88  subsection \<open>GCD and LCM computation with unique factorizations\<close>
```