src/HOL/Finite_Set.thy
changeset 15047 fa62de5862b9
parent 15042 fa7d27ef7e59
child 15074 277b3a4da341
equal deleted inserted replaced
15046:d6a4c3992e9d 15047:fa62de5862b9
   796 in
   796 in
   797 [("setsum", setsum_tr')]
   797 [("setsum", setsum_tr')]
   798 end
   798 end
   799 *}
   799 *}
   800 
   800 
   801 text{* As Jeremy Avigad notes: ultimately the analogous
   801 text{* As Jeremy Avigad notes, setprod needs the same treatment \dots *}
   802    thing should be done for setprod as well \dots *}
       
   803 
       
   804 
   802 
   805 lemma setsum_empty [simp]: "setsum f {} = 0"
   803 lemma setsum_empty [simp]: "setsum f {} = 0"
   806   by (simp add: setsum_def)
   804   by (simp add: setsum_def)
   807 
   805 
   808 lemma setsum_insert [simp]:
   806 lemma setsum_insert [simp]:
   809     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   807     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
   810   by (simp add: setsum_def
   808   by (simp add: setsum_def LC.fold_insert [OF LC.intro] add_left_commute)
   811     LC.fold_insert [OF LC.intro] add_left_commute)
       
   812 
   809 
   813 lemma setsum_reindex [rule_format]:
   810 lemma setsum_reindex [rule_format]:
   814      "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   811      "finite B ==> inj_on f B --> setsum h (f ` B) = setsum (h \<circ> f) B"
   815 apply (rule finite_induct, assumption, force)
   812 apply (rule finite_induct, assumption, force)
   816 apply (rule impI, auto)
   813 apply (rule impI, auto)
   936 
   933 
   937 lemma setsum_eq_0_iff [simp]:
   934 lemma setsum_eq_0_iff [simp]:
   938     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   935     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
   939   by (induct set: Finites) auto
   936   by (induct set: Finites) auto
   940 
   937 
   941 lemma setsum_constant_nat [simp]:
   938 lemma setsum_constant_nat:
   942     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
   939     "finite A ==> (\<Sum>x: A. y) = (card A) * y"
   943   -- {* Later generalized to any @{text comm_semiring_1_cancel}. *}
   940   -- {* Generalized to any @{text comm_semiring_1_cancel} in
       
   941         @{text IntDef} as @{text setsum_constant}. *}
   944   by (erule finite_induct, auto)
   942   by (erule finite_induct, auto)
   945 
   943 
   946 lemma setsum_Un: "finite A ==> finite B ==>
   944 lemma setsum_Un: "finite A ==> finite B ==>
   947     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   945     (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   948   -- {* For the natural numbers, we have subtraction. *}
   946   -- {* For the natural numbers, we have subtraction. *}
   976   apply (induct set: Finites, auto)
   974   apply (induct set: Finites, auto)
   977   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
   975   apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp)
   978   apply (blast intro: add_mono)
   976   apply (blast intro: add_mono)
   979   done
   977   done
   980 
   978 
       
   979 lemma setsum_mult: 
       
   980   fixes f :: "'a => ('b::semiring_0_cancel)"
       
   981   assumes fin: "finite A" 
       
   982   shows "r * setsum f A = setsum (%n. r * f n) A"
       
   983 using fin 
       
   984 proof (induct) 
       
   985   case empty thus ?case by simp
       
   986 next
       
   987   case (insert A x)
       
   988   thus ?case by (simp add: right_distrib) 
       
   989 qed
       
   990 
       
   991 lemma setsum_abs: 
       
   992   fixes f :: "'a => ('b::lordered_ab_group_abs)"
       
   993   assumes fin: "finite A" 
       
   994   shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
       
   995 using fin 
       
   996 proof (induct) 
       
   997   case empty thus ?case by simp
       
   998 next
       
   999   case (insert A x)
       
  1000   thus ?case by (auto intro: abs_triangle_ineq order_trans)
       
  1001 qed
       
  1002 
       
  1003 lemma setsum_abs_ge_zero: 
       
  1004   fixes f :: "'a => ('b::lordered_ab_group_abs)"
       
  1005   assumes fin: "finite A" 
       
  1006   shows "0 \<le> setsum (%i. abs(f i)) A"
       
  1007 using fin 
       
  1008 proof (induct) 
       
  1009   case empty thus ?case by simp
       
  1010 next
       
  1011   case (insert A x) thus ?case by (auto intro: order_trans)
       
  1012 qed
       
  1013 
   981 subsubsection {* Cardinality of unions and Sigma sets *}
  1014 subsubsection {* Cardinality of unions and Sigma sets *}
   982 
  1015 
   983 lemma card_UN_disjoint:
  1016 lemma card_UN_disjoint:
   984     "finite I ==> (ALL i:I. finite (A i)) ==>
  1017     "finite I ==> (ALL i:I. finite (A i)) ==>
   985         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
  1018         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   986       card (UNION I A) = setsum (%i. card (A i)) I"
  1019       card (UNION I A) = setsum (%i. card (A i)) I"
   987   apply (subst card_eq_setsum)
  1020   apply (subst card_eq_setsum)
   988   apply (subst finite_UN, assumption+)
  1021   apply (subst finite_UN, assumption+)
   989   apply (subgoal_tac "setsum (%i. card (A i)) I =
  1022   apply (subgoal_tac
   990       setsum (%i. (setsum (%x. 1) (A i))) I")
  1023            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
   991   apply (erule ssubst)
  1024   apply (simp add: setsum_UN_disjoint) 
   992   apply (erule setsum_UN_disjoint, assumption+)
  1025   apply (simp add: setsum_constant_nat cong: setsum_cong) 
   993   apply (rule setsum_cong)
       
   994   apply simp+
       
   995   done
  1026   done
   996 
  1027 
   997 lemma card_Union_disjoint:
  1028 lemma card_Union_disjoint:
   998   "finite C ==> (ALL A:C. finite A) ==>
  1029   "finite C ==> (ALL A:C. finite A) ==>
   999         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1030         (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==>
  1021   apply (subst SigmaI_insert, assumption)
  1052   apply (subst SigmaI_insert, assumption)
  1022   apply (subst card_Un_disjoint)
  1053   apply (subst card_Un_disjoint)
  1023   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
  1054   apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton)
  1024   done
  1055   done
  1025 
  1056 
  1026 lemma card_cartesian_product: "[| finite A; finite B |] ==>
  1057 lemma card_cartesian_product:
  1027   card (A <*> B) = card(A) * card(B)"
  1058      "[| finite A; finite B |] ==> card (A <*> B) = card(A) * card(B)"
  1028   by simp
  1059   by (simp add: setsum_constant_nat)
       
  1060 
  1029 
  1061 
  1030 
  1062 
  1031 subsection {* Generalized product over a set *}
  1063 subsection {* Generalized product over a set *}
  1032 
  1064 
  1033 constdefs
  1065 constdefs