added lemmas
authornipkow
Fri Jan 01 19:15:43 2010 +0100 (2010-01-01)
changeset 34223dce32a1e05fe
parent 34222 e33ee7369ecb
child 34224 143e3dabec2b
child 34225 21c5405deb6b
added lemmas
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Old_Number_Theory/Primes.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 01 17:21:44 2010 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 01 19:15:43 2010 +0100
     1.3 @@ -1737,6 +1737,13 @@
     1.4    shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)"
     1.5    by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute)
     1.6  
     1.7 +lemma setsum_mult_setsum_if_inj:
     1.8 +fixes f :: "'a => ('b::semiring_0)"
     1.9 +shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==>
    1.10 +  setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}"
    1.11 +by(auto simp: setsum_product setsum_cartesian_product
    1.12 +        intro!:  setsum_reindex_cong[symmetric])
    1.13 +
    1.14  
    1.15  subsection {* Generalized product over a set *}
    1.16  
     2.1 --- a/src/HOL/GCD.thy	Fri Jan 01 17:21:44 2010 +0100
     2.2 +++ b/src/HOL/GCD.thy	Fri Jan 01 19:15:43 2010 +0100
     2.3 @@ -1689,11 +1689,10 @@
     2.4    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
     2.5     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
     2.6  apply(auto simp add:inj_on_def)
     2.7 -apply (metis coprime_dvd_mult_nat dvd.eq_iff gcd_lcm_lattice_nat.inf_sup_absorb
     2.8 -     gcd_semilattice_nat.inf_le2 lcm_proj2_iff_nat nat_mult_1 prod_gcd_lcm_nat)
     2.9 -apply (metis coprime_dvd_mult_nat gcd_proj1_if_dvd_nat
    2.10 -       gcd_semilattice_nat.inf_commute lcm_dvd1_nat nat_mult_1
    2.11 -       nat_mult_commute prod_gcd_lcm_nat)
    2.12 +apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    2.13 +             dvd.neq_le_trans dvd_triv_left)
    2.14 +apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
    2.15 +             dvd.neq_le_trans dvd_triv_right mult_commute)
    2.16  done
    2.17  
    2.18  text{* Nitpick: *}
     3.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Fri Jan 01 17:21:44 2010 +0100
     3.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Jan 01 19:15:43 2010 +0100
     3.3 @@ -820,6 +820,14 @@
     3.4  lemma coprime_divisors: "d dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
     3.5    by (auto simp add: dvd_def coprime)
     3.6  
     3.7 +lemma mult_inj_if_coprime_nat:
     3.8 +  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
     3.9 +   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
    3.10 +apply(auto simp add:inj_on_def)
    3.11 +apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult)
    3.12 +apply(metis coprime_commute coprime_divprod dvd.neq_le_trans dvd_triv_right)
    3.13 +done
    3.14 +
    3.15  declare power_Suc0[simp del]
    3.16  declare even_dvd[simp del]
    3.17