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