--- 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 *}
--- 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: *}
--- 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]