src/HOL/Finite_Set.thy
changeset 17149 e2b19c92ef51
parent 17085 5b57f995a179
child 17189 b15f8e094874
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Aug 26 08:42:52 2005 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Aug 26 10:01:06 2005 +0200
     1.3 @@ -1144,6 +1144,7 @@
     1.4  done
     1.5  
     1.6  (* FIXME: this is distributitivty, name as such! *)
     1.7 +(* suggested name: setsum_right_distrib (CB) *)
     1.8  
     1.9  lemma setsum_mult: 
    1.10    fixes f :: "'a => ('b::semiring_0_cancel)"
    1.11 @@ -1160,6 +1161,34 @@
    1.12    case False thus ?thesis by (simp add: setsum_def)
    1.13  qed
    1.14  
    1.15 +lemma setsum_left_distrib:
    1.16 +  "setsum f A * (r::'a::semiring_0_cancel) = (\<Sum>n\<in>A. f n * r)"
    1.17 +proof (cases "finite A")
    1.18 +  case True
    1.19 +  then show ?thesis
    1.20 +  proof induct
    1.21 +    case empty thus ?case by simp
    1.22 +  next
    1.23 +    case (insert x A) thus ?case by (simp add: left_distrib)
    1.24 +  qed
    1.25 +next
    1.26 +  case False thus ?thesis by (simp add: setsum_def)
    1.27 +qed
    1.28 +
    1.29 +lemma setsum_divide_distrib:
    1.30 +  "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)"
    1.31 +proof (cases "finite A")
    1.32 +  case True
    1.33 +  then show ?thesis
    1.34 +  proof induct
    1.35 +    case empty thus ?case by simp
    1.36 +  next
    1.37 +    case (insert x A) thus ?case by (simp add: add_divide_distrib)
    1.38 +  qed
    1.39 +next
    1.40 +  case False thus ?thesis by (simp add: setsum_def)
    1.41 +qed
    1.42 +
    1.43  lemma setsum_abs[iff]: 
    1.44    fixes f :: "'a => ('b::lordered_ab_group_abs)"
    1.45    shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
    1.46 @@ -1213,6 +1242,33 @@
    1.47  qed
    1.48  
    1.49  
    1.50 +text {* Commuting outer and inner summation *}
    1.51 +
    1.52 +lemma swap_inj_on:
    1.53 +  "inj_on (%(i, j). (j, i)) (A \<times> B)"
    1.54 +  by (unfold inj_on_def) fast
    1.55 +
    1.56 +lemma swap_product:
    1.57 +  "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A"
    1.58 +  by (simp add: split_def image_def) blast
    1.59 +
    1.60 +lemma setsum_commute:
    1.61 +  "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
    1.62 +proof (simp add: setsum_cartesian_product)
    1.63 +  have "(\<Sum>z\<in>A \<times> B. f (fst z) (snd z)) =
    1.64 +    (\<Sum>z\<in>(%(i, j). (j, i)) ` (A \<times> B). f (snd z) (fst z))"
    1.65 +    (is "?s = _")
    1.66 +    apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on)
    1.67 +    apply (simp add: split_def)
    1.68 +    done
    1.69 +  also have "... = (\<Sum>z\<in>B \<times> A. f (snd z) (fst z))"
    1.70 +    (is "_ = ?t")
    1.71 +    apply (simp add: swap_product)
    1.72 +    done
    1.73 +  finally show "?s = ?t" .
    1.74 +qed
    1.75 +
    1.76 +
    1.77  subsection {* Generalized product over a set *}
    1.78  
    1.79  constdefs