merged

--- a/src/HOL/Finite_Set.thy	Sat Jan 02 20:08:04 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Jan 02 20:10:21 2010 +0100
@@ -1737,6 +1737,13 @@
   shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
   by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
 
+lemma setsum_mult_setsum_if_inj:
+fixes f :: "'a => ('b::semiring_0)"
+shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
+  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
+by(auto simp: setsum_product setsum_cartesian_product
+        intro!:  setsum_reindex_cong[symmetric])
+
 
 subsection {* Generalized product over a set *}
 

--- a/src/HOL/GCD.thy	Sat Jan 02 20:08:04 2010 +0100
+++ b/src/HOL/GCD.thy	Sat Jan 02 20:10:21 2010 +0100
@@ -878,7 +878,6 @@
   ultimately show ?thesis by blast
 qed
 
-(* FIXME move to Divides(?) *)
 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   by (auto intro: pow_divides_pow_nat dvd_power_same)
 
@@ -1685,6 +1684,19 @@
   show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
 qed
 
+
+lemma mult_inj_if_coprime_nat:
+  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
+   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
+apply(auto simp add:inj_on_def)
+apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
+             dvd.neq_le_trans dvd_triv_left)
+apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
+             dvd.neq_le_trans dvd_triv_right mult_commute)
+done
+
+text{* Nitpick: *}
+
 lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
 apply (rule eq_reflection)
 apply (induct x y rule: nat_gcd.induct)

--- a/src/HOL/Old_Number_Theory/Primes.thy	Sat Jan 02 20:08:04 2010 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Sat Jan 02 20:10:21 2010 +0100
@@ -820,6 +820,14 @@
 lemma coprime_divisors: "d dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
   by (auto simp add: dvd_def coprime)
 
+lemma mult_inj_if_coprime_nat:
+  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
+   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
+apply(auto simp add:inj_on_def)
+apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult)
+apply(metis coprime_commute coprime_divprod dvd.neq_le_trans dvd_triv_right)
+done
+
 declare power_Suc0[simp del]
 declare even_dvd[simp del]