src/HOL/Finite_Set.thy
 changeset 15539 333a88244569 parent 15535 a0cf3a19ee36 child 15542 ee6cd48cf840
```     1.1 --- a/src/HOL/Finite_Set.thy	Sat Feb 19 18:44:34 2005 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Mon Feb 21 15:04:10 2005 +0100
1.3 @@ -1064,17 +1064,6 @@
1.4      by (simp add: setsum_def)
1.5  qed
1.6
1.7 -lemma setsum_mono2_nat:
1.8 -  assumes fin: "finite B" and sub: "A \<subseteq> B"
1.9 -shows "setsum f A \<le> (setsum f B :: nat)"
1.10 -proof -
1.11 -  have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
1.12 -  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
1.13 -    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
1.14 -  also have "A \<union> (B-A) = B" using sub by blast
1.15 -  finally show ?thesis .
1.16 -qed
1.17 -
1.18  lemma setsum_negf:
1.19   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
1.20  proof (cases "finite A")
1.21 @@ -1118,6 +1107,30 @@
1.22    case False thus ?thesis by (simp add: setsum_def)
1.23  qed
1.24
1.25 +lemma setsum_mono2:
1.26 +fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
1.27 +assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
1.28 +shows "setsum f A \<le> setsum f B"
1.29 +proof -
1.30 +  have "setsum f A \<le> setsum f A + setsum f (B-A)"
1.31 +    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
1.32 +  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
1.33 +    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
1.34 +  also have "A \<union> (B-A) = B" using sub by blast
1.35 +  finally show ?thesis .
1.36 +qed
1.37 +(*
1.38 +lemma setsum_mono2_nat:
1.39 +  assumes fin: "finite B" and sub: "A \<subseteq> B"
1.40 +shows "setsum f A \<le> (setsum f B :: nat)"
1.41 +proof -
1.42 +  have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
1.43 +  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
1.44 +    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
1.45 +  also have "A \<union> (B-A) = B" using sub by blast
1.46 +  finally show ?thesis .
1.47 +qed
1.48 +*)
1.49  lemma setsum_mult:
1.50    fixes f :: "'a => ('b::semiring_0_cancel)"
1.51    shows "r * setsum f A = setsum (%n. r * f n) A"
1.52 @@ -1164,6 +1177,26 @@
1.53    case False thus ?thesis by (simp add: setsum_def)
1.54  qed
1.55
1.56 +lemma abs_setsum_abs[simp]:
1.57 +  fixes f :: "'a => ('b::lordered_ab_group_abs)"
1.58 +  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
1.59 +proof (cases "finite A")
1.60 +  case True
1.61 +  thus ?thesis
1.62 +  proof (induct)
1.63 +    case empty thus ?case by simp
1.64 +  next
1.65 +    case (insert a A)
1.66 +    hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
1.67 +    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
1.68 +    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
1.69 +    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
1.70 +    finally show ?case .
1.71 +  qed
1.72 +next
1.73 +  case False thus ?thesis by (simp add: setsum_def)
1.74 +qed
1.75 +
1.76
1.77  subsection {* Generalized product over a set *}
1.78
1.79 @@ -1430,7 +1463,7 @@
1.80    by (simp add: card_insert_if)
1.81
1.82  lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
1.83 -by (simp add: card_def setsum_mono2_nat)
1.84 +by (simp add: card_def setsum_mono2)
1.85
1.86  lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
1.87    apply (induct set: Finites, simp, clarify)
1.88 @@ -1497,13 +1530,13 @@
1.89  done
1.90
1.91
1.92 -lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
1.93 -  -- {* Generalized to any @{text comm_semiring_1_cancel} in
1.94 -        @{text IntDef} as @{text setsum_constant}. *}
1.95 -apply (cases "finite A")
1.96 -apply (erule finite_induct, auto)
1.97 +lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
1.98 +apply (cases "finite A")
1.99 +apply (erule finite_induct)
1.100 +apply (auto simp add: ring_distrib add_ac)
1.101  done
1.102
1.103 +
1.104  lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
1.105    apply (erule finite_induct)
1.106    apply (auto simp add: power_Suc)
1.107 @@ -1512,15 +1545,18 @@
1.108
1.109  subsubsection {* Cardinality of unions *}
1.110
1.111 +lemma of_nat_id[simp]: "(of_nat n :: nat) = n"
1.112 +by(induct n, auto)
1.113 +
1.114  lemma card_UN_disjoint:
1.115      "finite I ==> (ALL i:I. finite (A i)) ==>
1.116          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.117        card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
1.118 -  apply (simp add: card_def)
1.119 +  apply (simp add: card_def del: setsum_constant)
1.120    apply (subgoal_tac
1.121             "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
1.122 -  apply (simp add: setsum_UN_disjoint)
1.123 -  apply (simp add: setsum_constant_nat cong: setsum_cong)
1.124 +  apply (simp add: setsum_UN_disjoint del: setsum_constant)
1.125 +  apply (simp cong: setsum_cong)
1.126    done
1.127
1.128  lemma card_Union_disjoint:
1.129 @@ -1546,7 +1582,7 @@
1.130    done
1.131
1.132  lemma card_image: "inj_on f A ==> card (f ` A) = card A"
1.133 -by(simp add:card_def setsum_reindex o_def)
1.134 +by(simp add:card_def setsum_reindex o_def del:setsum_constant)
1.135
1.136  lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
1.137    by (simp add: card_seteq card_image)
1.138 @@ -1587,18 +1623,17 @@
1.139  lemma card_SigmaI [simp]:
1.140    "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
1.141    \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
1.142 -by(simp add:card_def setsum_Sigma)
1.143 +by(simp add:card_def setsum_Sigma del:setsum_constant)
1.144
1.145  lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
1.146  apply (cases "finite A")
1.147  apply (cases "finite B")
1.148 -  apply (simp add: setsum_constant_nat)
1.149  apply (auto simp add: card_eq_0_iff
1.150 -            dest: finite_cartesian_productD1 finite_cartesian_productD2)
1.151 +            dest: finite_cartesian_productD1 finite_cartesian_productD2)
1.152  done
1.153
1.154  lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
1.155 -by (simp add: card_cartesian_product)
1.156 +by (simp add: card_cartesian_product)
1.157
1.158
1.159
```