src/HOL/GCD.thy
changeset 63924 f91766530e13
parent 63915 bab633745c7f
child 64240 eabf80376aab
     1.1 --- a/src/HOL/GCD.thy	Tue Sep 20 14:51:58 2016 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sun Sep 18 17:57:55 2016 +0200
     1.3 @@ -939,6 +939,25 @@
     1.4  lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
     1.5    using lcm_proj1_iff [of n m] by (simp add: ac_simps)
     1.6  
     1.7 +lemma dvd_productE:
     1.8 +  assumes "p dvd (a * b)"
     1.9 +  obtains x y where "p = x * y" "x dvd a" "y dvd b"
    1.10 +proof (cases "a = 0")
    1.11 +  case True
    1.12 +  thus ?thesis by (intro that[of p 1]) simp_all
    1.13 +next
    1.14 +  case False
    1.15 +  define x y where "x = gcd a p" and "y = p div x"
    1.16 +  have "p = x * y" by (simp add: x_def y_def)
    1.17 +  moreover have "x dvd a" by (simp add: x_def)
    1.18 +  moreover from assms have "p dvd gcd (b * a) (b * p)"
    1.19 +    by (intro gcd_greatest) (simp_all add: mult.commute)
    1.20 +  hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
    1.21 +  with False have "y dvd b" 
    1.22 +    by (simp add: x_def y_def div_dvd_iff_mult assms)
    1.23 +  ultimately show ?thesis by (rule that)
    1.24 +qed
    1.25 +
    1.26  end
    1.27  
    1.28  class ring_gcd = comm_ring_1 + semiring_gcd