# HG changeset patch
# User nipkow
# Date 1262369743 -3600
# Node ID dce32a1e05fe28a3c6deaddae9e33d27ab26a292
# Parent  e33ee7369ecba2d445ca9661c92cb2451f347b9c
added lemmas

diff -r e33ee7369ecb -r dce32a1e05fe src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Jan 01 17:21:44 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Jan 01 19:15:43 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 *}
 
diff -r e33ee7369ecb -r dce32a1e05fe src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Jan 01 17:21:44 2010 +0100
+++ b/src/HOL/GCD.thy	Fri Jan 01 19:15:43 2010 +0100
@@ -1689,11 +1689,10 @@
   "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_dvd_mult_nat dvd.eq_iff gcd_lcm_lattice_nat.inf_sup_absorb
-     gcd_semilattice_nat.inf_le2 lcm_proj2_iff_nat nat_mult_1 prod_gcd_lcm_nat)
-apply (metis coprime_dvd_mult_nat gcd_proj1_if_dvd_nat
-       gcd_semilattice_nat.inf_commute lcm_dvd1_nat nat_mult_1
-       nat_mult_commute prod_gcd_lcm_nat)
+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: *}
diff -r e33ee7369ecb -r dce32a1e05fe src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Fri Jan 01 17:21:44 2010 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Jan 01 19:15:43 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]