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>