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
```