810 apply simp |
821 apply simp |
811 apply (simp add:AC) |
822 apply (simp add:AC) |
812 done |
823 done |
813 |
824 |
814 |
825 |
|
826 subsection {* Generalized summation over a set *} |
|
827 |
|
828 constdefs |
|
829 setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" |
|
830 "setsum f A == if finite A then fold (op +) f 0 A else 0" |
|
831 |
|
832 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is |
|
833 written @{text"\<Sum>x\<in>A. e"}. *} |
|
834 |
|
835 syntax |
|
836 "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) |
|
837 syntax (xsymbols) |
|
838 "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
839 syntax (HTML output) |
|
840 "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
841 |
|
842 translations -- {* Beware of argument permutation! *} |
|
843 "SUM i:A. b" == "setsum (%i. b) A" |
|
844 "\<Sum>i\<in>A. b" == "setsum (%i. b) A" |
|
845 |
|
846 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter |
|
847 @{text"\<Sum>x|P. e"}. *} |
|
848 |
|
849 syntax |
|
850 "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10) |
|
851 syntax (xsymbols) |
|
852 "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
853 syntax (HTML output) |
|
854 "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
855 |
|
856 translations |
|
857 "SUM x|P. t" => "setsum (%x. t) {x. P}" |
|
858 "\<Sum>x|P. t" => "setsum (%x. t) {x. P}" |
|
859 |
|
860 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *} |
|
861 |
|
862 syntax |
|
863 "_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\<Sum>_" [1000] 999) |
|
864 |
|
865 parse_translation {* |
|
866 let |
|
867 fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A |
|
868 in [("_Setsum", Setsum_tr)] end; |
|
869 *} |
|
870 |
|
871 print_translation {* |
|
872 let |
|
873 fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A |
|
874 | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = |
|
875 if x<>y then raise Match |
|
876 else let val x' = Syntax.mark_bound x |
|
877 val t' = subst_bound(x',t) |
|
878 val P' = subst_bound(x',P) |
|
879 in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end |
|
880 in |
|
881 [("setsum", setsum_tr')] |
|
882 end |
|
883 *} |
|
884 |
|
885 lemma setsum_empty [simp]: "setsum f {} = 0" |
|
886 by (simp add: setsum_def) |
|
887 |
|
888 lemma setsum_insert [simp]: |
|
889 "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" |
|
890 by (simp add: setsum_def ACf.fold_insert [OF ACf_add]) |
|
891 |
|
892 lemma setsum_reindex: |
|
893 "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B" |
|
894 by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD) |
|
895 |
|
896 lemma setsum_reindex_id: |
|
897 "inj_on f B ==> setsum f B = setsum id (f ` B)" |
|
898 by (auto simp add: setsum_reindex) |
|
899 |
|
900 lemma setsum_cong: |
|
901 "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" |
|
902 by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add]) |
|
903 |
|
904 lemma setsum_reindex_cong: |
|
905 "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] |
|
906 ==> setsum h B = setsum g A" |
|
907 by (simp add: setsum_reindex cong: setsum_cong) |
|
908 |
|
909 lemma setsum_0: "setsum (%i. 0) A = 0" |
|
910 apply (clarsimp simp: setsum_def) |
|
911 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add]) |
|
912 done |
|
913 |
|
914 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0" |
|
915 apply (subgoal_tac "setsum f F = setsum (%x. 0) F") |
|
916 apply (erule ssubst, rule setsum_0) |
|
917 apply (rule setsum_cong, auto) |
|
918 done |
|
919 |
|
920 lemma setsum_Un_Int: "finite A ==> finite B ==> |
|
921 setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" |
|
922 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
|
923 by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric]) |
|
924 |
|
925 lemma setsum_Un_disjoint: "finite A ==> finite B |
|
926 ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" |
|
927 by (subst setsum_Un_Int [symmetric], auto) |
|
928 |
|
929 (* FIXME get rid of finite I. If infinite, rhs is directly 0, and UNION I A |
|
930 is also infinite and hence also 0 *) |
|
931 lemma setsum_UN_disjoint: |
|
932 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
933 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
934 setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))" |
|
935 by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong) |
|
936 |
|
937 |
|
938 (* FIXME get rid of finite C. If infinite, rhs is directly 0, and Union C |
|
939 is also infinite and hence also 0 *) |
|
940 lemma setsum_Union_disjoint: |
|
941 "finite C ==> (ALL A:C. finite A) ==> |
|
942 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==> |
|
943 setsum f (Union C) = setsum (setsum f) C" |
|
944 apply (frule setsum_UN_disjoint [of C id f]) |
|
945 apply (unfold Union_def id_def, assumption+) |
|
946 done |
|
947 |
|
948 (* FIXME get rid of finite A. If infinite, lhs is directly 0, and SIGMA A B |
|
949 is either infinite or empty, and in both cases the rhs is also 0 *) |
|
950 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
951 (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = |
|
952 (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))" |
|
953 by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong) |
|
954 |
|
955 lemma setsum_cartesian_product: "finite A ==> finite B ==> |
|
956 (\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = |
|
957 (\<Sum>z\<in>A <*> B. f (fst z) (snd z))" |
|
958 by (erule setsum_Sigma, auto) |
|
959 |
|
960 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" |
|
961 by(simp add:setsum_def ACe.fold_distrib[OF ACe_add]) |
|
962 |
|
963 |
|
964 subsubsection {* Properties in more restricted classes of structures *} |
|
965 |
|
966 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" |
|
967 apply (case_tac "finite A") |
|
968 prefer 2 apply (simp add: setsum_def) |
|
969 apply (erule rev_mp) |
|
970 apply (erule finite_induct, auto) |
|
971 done |
|
972 |
|
973 lemma setsum_eq_0_iff [simp]: |
|
974 "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" |
|
975 by (induct set: Finites) auto |
|
976 |
|
977 lemma setsum_Un_nat: "finite A ==> finite B ==> |
|
978 (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" |
|
979 -- {* For the natural numbers, we have subtraction. *} |
|
980 by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) |
|
981 |
|
982 lemma setsum_Un: "finite A ==> finite B ==> |
|
983 (setsum f (A Un B) :: 'a :: ab_group_add) = |
|
984 setsum f A + setsum f B - setsum f (A Int B)" |
|
985 by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) |
|
986 |
|
987 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = |
|
988 (if a:A then setsum f A - f a else setsum f A)" |
|
989 apply (case_tac "finite A") |
|
990 prefer 2 apply (simp add: setsum_def) |
|
991 apply (erule finite_induct) |
|
992 apply (auto simp add: insert_Diff_if) |
|
993 apply (drule_tac a = a in mk_disjoint_insert, auto) |
|
994 done |
|
995 |
|
996 lemma setsum_diff1: "finite A \<Longrightarrow> |
|
997 (setsum f (A - {a}) :: ('a::ab_group_add)) = |
|
998 (if a:A then setsum f A - f a else setsum f A)" |
|
999 by (erule finite_induct) (auto simp add: insert_Diff_if) |
|
1000 |
|
1001 (* By Jeremy Siek: *) |
|
1002 |
|
1003 lemma setsum_diff_nat: |
|
1004 assumes finB: "finite B" |
|
1005 shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" |
|
1006 using finB |
|
1007 proof (induct) |
|
1008 show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp |
|
1009 next |
|
1010 fix F x assume finF: "finite F" and xnotinF: "x \<notin> F" |
|
1011 and xFinA: "insert x F \<subseteq> A" |
|
1012 and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F" |
|
1013 from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp |
|
1014 from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" |
|
1015 by (simp add: setsum_diff1_nat) |
|
1016 from xFinA have "F \<subseteq> A" by simp |
|
1017 with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp |
|
1018 with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" |
|
1019 by simp |
|
1020 from xnotinF have "A - insert x F = (A - F) - {x}" by auto |
|
1021 with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x" |
|
1022 by simp |
|
1023 from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp |
|
1024 with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" |
|
1025 by simp |
|
1026 thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp |
|
1027 qed |
|
1028 |
|
1029 lemma setsum_diff: |
|
1030 assumes le: "finite A" "B \<subseteq> A" |
|
1031 shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))" |
|
1032 proof - |
|
1033 from le have finiteB: "finite B" using finite_subset by auto |
|
1034 show ?thesis using finiteB le |
|
1035 proof (induct) |
|
1036 case empty |
|
1037 thus ?case by auto |
|
1038 next |
|
1039 case (insert x F) |
|
1040 thus ?case using le finiteB |
|
1041 by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) |
|
1042 qed |
|
1043 qed |
|
1044 |
|
1045 lemma setsum_mono: |
|
1046 assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))" |
|
1047 shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" |
|
1048 proof (cases "finite K") |
|
1049 case True |
|
1050 thus ?thesis using le |
|
1051 proof (induct) |
|
1052 case empty |
|
1053 thus ?case by simp |
|
1054 next |
|
1055 case insert |
|
1056 thus ?case using add_mono |
|
1057 by force |
|
1058 qed |
|
1059 next |
|
1060 case False |
|
1061 thus ?thesis |
|
1062 by (simp add: setsum_def) |
|
1063 qed |
|
1064 |
|
1065 lemma setsum_mono2_nat: |
|
1066 assumes fin: "finite B" and sub: "A \<subseteq> B" |
|
1067 shows "setsum f A \<le> (setsum f B :: nat)" |
|
1068 proof - |
|
1069 have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith |
|
1070 also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin] |
|
1071 by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) |
|
1072 also have "A \<union> (B-A) = B" using sub by blast |
|
1073 finally show ?thesis . |
|
1074 qed |
|
1075 |
|
1076 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A = |
|
1077 - setsum f A" |
|
1078 by (induct set: Finites, auto) |
|
1079 |
|
1080 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A = |
|
1081 setsum f A - setsum g A" |
|
1082 by (simp add: diff_minus setsum_addf setsum_negf) |
|
1083 |
|
1084 lemma setsum_nonneg: "[| finite A; |
|
1085 \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==> |
|
1086 0 \<le> setsum f A"; |
|
1087 apply (induct set: Finites, auto) |
|
1088 apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp) |
|
1089 apply (blast intro: add_mono) |
|
1090 done |
|
1091 |
|
1092 lemma setsum_nonpos: "[| finite A; |
|
1093 \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==> |
|
1094 setsum f A \<le> 0"; |
|
1095 apply (induct set: Finites, auto) |
|
1096 apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp) |
|
1097 apply (blast intro: add_mono) |
|
1098 done |
|
1099 |
|
1100 lemma setsum_mult: |
|
1101 fixes f :: "'a => ('b::semiring_0_cancel)" |
|
1102 shows "r * setsum f A = setsum (%n. r * f n) A" |
|
1103 proof (cases "finite A") |
|
1104 case True |
|
1105 thus ?thesis |
|
1106 proof (induct) |
|
1107 case empty thus ?case by simp |
|
1108 next |
|
1109 case (insert x A) thus ?case by (simp add: right_distrib) |
|
1110 qed |
|
1111 next |
|
1112 case False thus ?thesis by (simp add: setsum_def) |
|
1113 qed |
|
1114 |
|
1115 lemma setsum_abs: |
|
1116 fixes f :: "'a => ('b::lordered_ab_group_abs)" |
|
1117 assumes fin: "finite A" |
|
1118 shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" |
|
1119 using fin |
|
1120 proof (induct) |
|
1121 case empty thus ?case by simp |
|
1122 next |
|
1123 case (insert x A) |
|
1124 thus ?case by (auto intro: abs_triangle_ineq order_trans) |
|
1125 qed |
|
1126 |
|
1127 lemma setsum_abs_ge_zero: |
|
1128 fixes f :: "'a => ('b::lordered_ab_group_abs)" |
|
1129 assumes fin: "finite A" |
|
1130 shows "0 \<le> setsum (%i. abs(f i)) A" |
|
1131 using fin |
|
1132 proof (induct) |
|
1133 case empty thus ?case by simp |
|
1134 next |
|
1135 case (insert x A) thus ?case by (auto intro: order_trans) |
|
1136 qed |
|
1137 |
|
1138 |
|
1139 subsection {* Generalized product over a set *} |
|
1140 |
|
1141 constdefs |
|
1142 setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult" |
|
1143 "setprod f A == if finite A then fold (op *) f 1 A else 1" |
|
1144 |
|
1145 syntax |
|
1146 "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_:_. _)" [0, 51, 10] 10) |
|
1147 |
|
1148 syntax (xsymbols) |
|
1149 "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1150 syntax (HTML output) |
|
1151 "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1152 translations |
|
1153 "\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *} |
|
1154 |
|
1155 syntax |
|
1156 "_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\<Prod>_" [1000] 999) |
|
1157 |
|
1158 parse_translation {* |
|
1159 let |
|
1160 fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A |
|
1161 in [("_Setprod", Setprod_tr)] end; |
|
1162 *} |
|
1163 print_translation {* |
|
1164 let fun setprod_tr' [Abs(x,Tx,t), A] = |
|
1165 if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match |
|
1166 in |
|
1167 [("setprod", setprod_tr')] |
|
1168 end |
|
1169 *} |
|
1170 |
|
1171 |
|
1172 lemma setprod_empty [simp]: "setprod f {} = 1" |
|
1173 by (auto simp add: setprod_def) |
|
1174 |
|
1175 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==> |
|
1176 setprod f (insert a A) = f a * setprod f A" |
|
1177 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult]) |
|
1178 |
|
1179 lemma setprod_reindex: |
|
1180 "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B" |
|
1181 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD) |
|
1182 |
|
1183 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)" |
|
1184 by (auto simp add: setprod_reindex) |
|
1185 |
|
1186 lemma setprod_cong: |
|
1187 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" |
|
1188 by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult]) |
|
1189 |
|
1190 lemma setprod_reindex_cong: "inj_on f A ==> |
|
1191 B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" |
|
1192 by (frule setprod_reindex, simp) |
|
1193 |
|
1194 |
|
1195 lemma setprod_1: "setprod (%i. 1) A = 1" |
|
1196 apply (case_tac "finite A") |
|
1197 apply (erule finite_induct, auto simp add: mult_ac) |
|
1198 apply (simp add: setprod_def) |
|
1199 done |
|
1200 |
|
1201 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1" |
|
1202 apply (subgoal_tac "setprod f F = setprod (%x. 1) F") |
|
1203 apply (erule ssubst, rule setprod_1) |
|
1204 apply (rule setprod_cong, auto) |
|
1205 done |
|
1206 |
|
1207 lemma setprod_Un_Int: "finite A ==> finite B |
|
1208 ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" |
|
1209 by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric]) |
|
1210 |
|
1211 lemma setprod_Un_disjoint: "finite A ==> finite B |
|
1212 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" |
|
1213 by (subst setprod_Un_Int [symmetric], auto) |
|
1214 |
|
1215 lemma setprod_UN_disjoint: |
|
1216 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
1217 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1218 setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" |
|
1219 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong) |
|
1220 |
|
1221 lemma setprod_Union_disjoint: |
|
1222 "finite C ==> (ALL A:C. finite A) ==> |
|
1223 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==> |
|
1224 setprod f (Union C) = setprod (setprod f) C" |
|
1225 apply (frule setprod_UN_disjoint [of C id f]) |
|
1226 apply (unfold Union_def id_def, assumption+) |
|
1227 done |
|
1228 |
|
1229 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
1230 (\<Prod>x:A. (\<Prod>y: B x. f x y)) = |
|
1231 (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))" |
|
1232 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong) |
|
1233 |
|
1234 lemma setprod_cartesian_product: "finite A ==> finite B ==> |
|
1235 (\<Prod>x:A. (\<Prod>y: B. f x y)) = |
|
1236 (\<Prod>z:(A <*> B). f (fst z) (snd z))" |
|
1237 by (erule setprod_Sigma, auto) |
|
1238 |
|
1239 lemma setprod_timesf: |
|
1240 "setprod (%x. f x * g x) A = (setprod f A * setprod g A)" |
|
1241 by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult]) |
|
1242 |
|
1243 |
|
1244 subsubsection {* Properties in more restricted classes of structures *} |
|
1245 |
|
1246 lemma setprod_eq_1_iff [simp]: |
|
1247 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
|
1248 by (induct set: Finites) auto |
|
1249 |
|
1250 lemma setprod_zero: |
|
1251 "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" |
|
1252 apply (induct set: Finites, force, clarsimp) |
|
1253 apply (erule disjE, auto) |
|
1254 done |
|
1255 |
|
1256 lemma setprod_nonneg [rule_format]: |
|
1257 "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A" |
|
1258 apply (case_tac "finite A") |
|
1259 apply (induct set: Finites, force, clarsimp) |
|
1260 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) |
|
1261 apply (rule mult_mono, assumption+) |
|
1262 apply (auto simp add: setprod_def) |
|
1263 done |
|
1264 |
|
1265 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) |
|
1266 --> 0 < setprod f A" |
|
1267 apply (case_tac "finite A") |
|
1268 apply (induct set: Finites, force, clarsimp) |
|
1269 apply (subgoal_tac "0 * 0 < f x * setprod f F", force) |
|
1270 apply (rule mult_strict_mono, assumption+) |
|
1271 apply (auto simp add: setprod_def) |
|
1272 done |
|
1273 |
|
1274 lemma setprod_nonzero [rule_format]: |
|
1275 "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> |
|
1276 finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0" |
|
1277 apply (erule finite_induct, auto) |
|
1278 done |
|
1279 |
|
1280 lemma setprod_zero_eq: |
|
1281 "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> |
|
1282 finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)" |
|
1283 apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast) |
|
1284 done |
|
1285 |
|
1286 lemma setprod_nonzero_field: |
|
1287 "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0" |
|
1288 apply (rule setprod_nonzero, auto) |
|
1289 done |
|
1290 |
|
1291 lemma setprod_zero_eq_field: |
|
1292 "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)" |
|
1293 apply (rule setprod_zero_eq, auto) |
|
1294 done |
|
1295 |
|
1296 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==> |
|
1297 (setprod f (A Un B) :: 'a ::{field}) |
|
1298 = setprod f A * setprod f B / setprod f (A Int B)" |
|
1299 apply (subst setprod_Un_Int [symmetric], auto) |
|
1300 apply (subgoal_tac "finite (A Int B)") |
|
1301 apply (frule setprod_nonzero_field [of "A Int B" f], assumption) |
|
1302 apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self) |
|
1303 done |
|
1304 |
|
1305 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> |
|
1306 (setprod f (A - {a}) :: 'a :: {field}) = |
|
1307 (if a:A then setprod f A / f a else setprod f A)" |
|
1308 apply (erule finite_induct) |
|
1309 apply (auto simp add: insert_Diff_if) |
|
1310 apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a") |
|
1311 apply (erule ssubst) |
|
1312 apply (subst times_divide_eq_right [THEN sym]) |
|
1313 apply (auto simp add: mult_ac times_divide_eq_right divide_self) |
|
1314 done |
|
1315 |
|
1316 lemma setprod_inversef: "finite A ==> |
|
1317 ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> |
|
1318 setprod (inverse \<circ> f) A = inverse (setprod f A)" |
|
1319 apply (erule finite_induct) |
|
1320 apply (simp, simp) |
|
1321 done |
|
1322 |
|
1323 lemma setprod_dividef: |
|
1324 "[|finite A; |
|
1325 \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|] |
|
1326 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
|
1327 apply (subgoal_tac |
|
1328 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
|
1329 apply (erule ssubst) |
|
1330 apply (subst divide_inverse) |
|
1331 apply (subst setprod_timesf) |
|
1332 apply (subst setprod_inversef, assumption+, rule refl) |
|
1333 apply (rule setprod_cong, rule refl) |
|
1334 apply (subst divide_inverse, auto) |
|
1335 done |
|
1336 |
815 subsection {* Finite cardinality *} |
1337 subsection {* Finite cardinality *} |
816 |
1338 |
817 text {* |
1339 text {* This definition, although traditional, is ugly to work with: |
818 This definition, although traditional, is ugly to work with: @{text |
1340 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}. |
819 "card A == LEAST n. EX f. A = {f i | i. i < n}"}. Therefore we have |
1341 But now that we have @{text setsum} things are easy: |
820 switched to an inductive one: |
|
821 *} |
1342 *} |
822 |
|
823 consts cardR :: "('a set \<times> nat) set" |
|
824 |
|
825 inductive cardR |
|
826 intros |
|
827 EmptyI: "({}, 0) : cardR" |
|
828 InsertI: "(A, n) : cardR ==> a \<notin> A ==> (insert a A, Suc n) : cardR" |
|
829 |
1343 |
830 constdefs |
1344 constdefs |
831 card :: "'a set => nat" |
1345 card :: "'a set => nat" |
832 "card A == THE n. (A, n) : cardR" |
1346 "card A == setsum (%x. 1::nat) A" |
833 |
|
834 inductive_cases cardR_emptyE: "({}, n) : cardR" |
|
835 inductive_cases cardR_insertE: "(insert a A,n) : cardR" |
|
836 |
|
837 lemma cardR_SucD: "(A, n) : cardR ==> a : A --> (EX m. n = Suc m)" |
|
838 by (induct set: cardR) simp_all |
|
839 |
|
840 lemma cardR_determ_aux1: |
|
841 "(A, m): cardR ==> (!!n a. m = Suc n ==> a:A ==> (A - {a}, n) : cardR)" |
|
842 apply (induct set: cardR, auto) |
|
843 apply (simp add: insert_Diff_if, auto) |
|
844 apply (drule cardR_SucD) |
|
845 apply (blast intro!: cardR.intros) |
|
846 done |
|
847 |
|
848 lemma cardR_determ_aux2: "(insert a A, Suc m) : cardR ==> a \<notin> A ==> (A, m) : cardR" |
|
849 by (drule cardR_determ_aux1) auto |
|
850 |
|
851 lemma cardR_determ: "(A, m): cardR ==> (!!n. (A, n) : cardR ==> n = m)" |
|
852 apply (induct set: cardR) |
|
853 apply (safe elim!: cardR_emptyE cardR_insertE) |
|
854 apply (rename_tac B b m) |
|
855 apply (case_tac "a = b") |
|
856 apply (subgoal_tac "A = B") |
|
857 prefer 2 apply (blast elim: equalityE, blast) |
|
858 apply (subgoal_tac "EX C. A = insert b C & B = insert a C") |
|
859 prefer 2 |
|
860 apply (rule_tac x = "A Int B" in exI) |
|
861 apply (blast elim: equalityE) |
|
862 apply (frule_tac A = B in cardR_SucD) |
|
863 apply (blast intro!: cardR.intros dest!: cardR_determ_aux2) |
|
864 done |
|
865 |
|
866 lemma cardR_imp_finite: "(A, n) : cardR ==> finite A" |
|
867 by (induct set: cardR) simp_all |
|
868 |
|
869 lemma finite_imp_cardR: "finite A ==> EX n. (A, n) : cardR" |
|
870 by (induct set: Finites) (auto intro!: cardR.intros) |
|
871 |
|
872 lemma card_equality: "(A,n) : cardR ==> card A = n" |
|
873 by (unfold card_def) (blast intro: cardR_determ) |
|
874 |
1347 |
875 lemma card_empty [simp]: "card {} = 0" |
1348 lemma card_empty [simp]: "card {} = 0" |
876 by (unfold card_def) (blast intro!: cardR.intros elim!: cardR_emptyE) |
1349 by (simp add: card_def) |
|
1350 |
|
1351 lemma card_eq_setsum: "card A = setsum (%x. 1) A" |
|
1352 by (simp add: card_def) |
877 |
1353 |
878 lemma card_insert_disjoint [simp]: |
1354 lemma card_insert_disjoint [simp]: |
879 "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" |
1355 "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" |
880 proof - |
1356 by(simp add: card_def ACf.fold_insert[OF ACf_add]) |
881 assume x: "x \<notin> A" |
1357 |
882 hence aux: "!!n. ((insert x A, n) : cardR) = (EX m. (A, m) : cardR & n = Suc m)" |
1358 lemma card_insert_if: |
883 apply (auto intro!: cardR.intros) |
1359 "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" |
884 apply (rule_tac A1 = A in finite_imp_cardR [THEN exE]) |
1360 by (simp add: insert_absorb) |
885 apply (force dest: cardR_imp_finite) |
|
886 apply (blast intro!: cardR.intros intro: cardR_determ) |
|
887 done |
|
888 assume "finite A" |
|
889 thus ?thesis |
|
890 apply (simp add: card_def aux) |
|
891 apply (rule the_equality) |
|
892 apply (auto intro: finite_imp_cardR |
|
893 cong: conj_cong simp: card_def [symmetric] card_equality) |
|
894 done |
|
895 qed |
|
896 |
1361 |
897 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" |
1362 lemma card_0_eq [simp]: "finite A ==> (card A = 0) = (A = {})" |
898 apply auto |
1363 apply auto |
899 apply (drule_tac a = x in mk_disjoint_insert, clarify) |
1364 apply (drule_tac a = x in mk_disjoint_insert, clarify) |
900 apply (rotate_tac -1, auto) |
1365 apply (auto) |
901 done |
1366 done |
902 |
|
903 lemma card_insert_if: |
|
904 "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" |
|
905 by (simp add: insert_absorb) |
|
906 |
1367 |
907 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A" |
1368 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A" |
908 apply(rule_tac t = A in insert_Diff [THEN subst], assumption) |
1369 apply(rule_tac t = A in insert_Diff [THEN subst], assumption) |
909 apply(simp del:insert_Diff_single) |
1370 apply(simp del:insert_Diff_single) |
910 done |
1371 done |
1445 assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:max_def) |
1954 assume "S \<noteq> {}" thus ?thesis using insert by (auto simp add:max_def) |
1446 qed |
1955 qed |
1447 qed |
1956 qed |
1448 |
1957 |
1449 |
1958 |
1450 subsection {* Generalized summation over a set *} |
|
1451 |
|
1452 constdefs |
|
1453 setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" |
|
1454 "setsum f A == if finite A then fold (op +) f 0 A else 0" |
|
1455 |
|
1456 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is |
|
1457 written @{text"\<Sum>x\<in>A. e"}. *} |
|
1458 |
|
1459 syntax |
|
1460 "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) |
|
1461 syntax (xsymbols) |
|
1462 "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
1463 syntax (HTML output) |
|
1464 "_setsum" :: "idt => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
1465 |
|
1466 translations -- {* Beware of argument permutation! *} |
|
1467 "SUM i:A. b" == "setsum (%i. b) A" |
|
1468 "\<Sum>i\<in>A. b" == "setsum (%i. b) A" |
|
1469 |
|
1470 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter |
|
1471 @{text"\<Sum>x|P. e"}. *} |
|
1472 |
|
1473 syntax |
|
1474 "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10) |
|
1475 syntax (xsymbols) |
|
1476 "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
1477 syntax (HTML output) |
|
1478 "_qsetsum" :: "idt \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
1479 |
|
1480 translations |
|
1481 "SUM x|P. t" => "setsum (%x. t) {x. P}" |
|
1482 "\<Sum>x|P. t" => "setsum (%x. t) {x. P}" |
|
1483 |
|
1484 text{* Finally we abbreviate @{term"\<Sum>x\<in>A. x"} by @{text"\<Sum>A"}. *} |
|
1485 |
|
1486 syntax |
|
1487 "_Setsum" :: "'a set => 'a::comm_monoid_mult" ("\<Sum>_" [1000] 999) |
|
1488 |
|
1489 parse_translation {* |
|
1490 let |
|
1491 fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A |
|
1492 in [("_Setsum", Setsum_tr)] end; |
|
1493 *} |
|
1494 |
|
1495 print_translation {* |
|
1496 let |
|
1497 fun setsum_tr' [Abs(_,_,Bound 0), A] = Syntax.const "_Setsum" $ A |
|
1498 | setsum_tr' [Abs(x,Tx,t), Const ("Collect",_) $ Abs(y,Ty,P)] = |
|
1499 if x<>y then raise Match |
|
1500 else let val x' = Syntax.mark_bound x |
|
1501 val t' = subst_bound(x',t) |
|
1502 val P' = subst_bound(x',P) |
|
1503 in Syntax.const "_qsetsum" $ Syntax.mark_bound x $ P' $ t' end |
|
1504 in |
|
1505 [("setsum", setsum_tr')] |
|
1506 end |
1959 end |
1507 *} |
|
1508 |
|
1509 text{* Instantiation of locales: *} |
|
1510 |
|
1511 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
1512 by(fastsimp intro: ACf.intro add_assoc add_commute) |
|
1513 |
|
1514 lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)" |
|
1515 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add) |
|
1516 |
|
1517 lemma setsum_empty [simp]: "setsum f {} = 0" |
|
1518 by (simp add: setsum_def) |
|
1519 |
|
1520 lemma setsum_insert [simp]: |
|
1521 "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" |
|
1522 by (simp add: setsum_def ACf.fold_insert [OF ACf_add]) |
|
1523 |
|
1524 lemma setsum_reindex: |
|
1525 "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B" |
|
1526 by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD) |
|
1527 |
|
1528 lemma setsum_reindex_id: |
|
1529 "inj_on f B ==> setsum f B = setsum id (f ` B)" |
|
1530 by (auto simp add: setsum_reindex) |
|
1531 |
|
1532 lemma setsum_cong: |
|
1533 "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" |
|
1534 by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add]) |
|
1535 |
|
1536 lemma setsum_reindex_cong: |
|
1537 "[|inj_on f A; B = f ` A; !!a. g a = h (f a)|] |
|
1538 ==> setsum h B = setsum g A" |
|
1539 by (simp add: setsum_reindex cong: setsum_cong) |
|
1540 |
|
1541 lemma setsum_0: "setsum (%i. 0) A = 0" |
|
1542 apply (clarsimp simp: setsum_def) |
|
1543 apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add]) |
|
1544 done |
|
1545 |
|
1546 lemma setsum_0': "ALL a:F. f a = 0 ==> setsum f F = 0" |
|
1547 apply (subgoal_tac "setsum f F = setsum (%x. 0) F") |
|
1548 apply (erule ssubst, rule setsum_0) |
|
1549 apply (rule setsum_cong, auto) |
|
1550 done |
|
1551 |
|
1552 lemma card_eq_setsum: "finite A ==> card A = setsum (%x. 1) A" |
|
1553 -- {* Could allow many @{text "card"} proofs to be simplified. *} |
|
1554 by (induct set: Finites) auto |
|
1555 |
|
1556 lemma setsum_Un_Int: "finite A ==> finite B ==> |
|
1557 setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" |
|
1558 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
|
1559 by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric]) |
|
1560 |
|
1561 lemma setsum_Un_disjoint: "finite A ==> finite B |
|
1562 ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" |
|
1563 by (subst setsum_Un_Int [symmetric], auto) |
|
1564 |
|
1565 lemma setsum_UN_disjoint: |
|
1566 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
1567 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1568 setsum f (UNION I A) = setsum (%i. setsum f (A i)) I" |
|
1569 by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong) |
|
1570 |
|
1571 |
|
1572 lemma setsum_Union_disjoint: |
|
1573 "finite C ==> (ALL A:C. finite A) ==> |
|
1574 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==> |
|
1575 setsum f (Union C) = setsum (setsum f) C" |
|
1576 apply (frule setsum_UN_disjoint [of C id f]) |
|
1577 apply (unfold Union_def id_def, assumption+) |
|
1578 done |
|
1579 |
|
1580 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
1581 (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = |
|
1582 (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))" |
|
1583 by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong) |
|
1584 |
|
1585 lemma setsum_cartesian_product: "finite A ==> finite B ==> |
|
1586 (\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = |
|
1587 (\<Sum>z\<in>A <*> B. f (fst z) (snd z))" |
|
1588 by (erule setsum_Sigma, auto) |
|
1589 |
|
1590 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" |
|
1591 by(simp add:setsum_def ACe.fold_distrib[OF ACe_add]) |
|
1592 |
|
1593 |
|
1594 subsubsection {* Properties in more restricted classes of structures *} |
|
1595 |
|
1596 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" |
|
1597 apply (case_tac "finite A") |
|
1598 prefer 2 apply (simp add: setsum_def) |
|
1599 apply (erule rev_mp) |
|
1600 apply (erule finite_induct, auto) |
|
1601 done |
|
1602 |
|
1603 lemma setsum_eq_0_iff [simp]: |
|
1604 "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" |
|
1605 by (induct set: Finites) auto |
|
1606 |
|
1607 lemma setsum_constant_nat: |
|
1608 "finite A ==> (\<Sum>x\<in>A. y) = (card A) * y" |
|
1609 -- {* Generalized to any @{text comm_semiring_1_cancel} in |
|
1610 @{text IntDef} as @{text setsum_constant}. *} |
|
1611 by (erule finite_induct, auto) |
|
1612 |
|
1613 lemma setsum_Un: "finite A ==> finite B ==> |
|
1614 (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" |
|
1615 -- {* For the natural numbers, we have subtraction. *} |
|
1616 by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) |
|
1617 |
|
1618 lemma setsum_Un_ring: "finite A ==> finite B ==> |
|
1619 (setsum f (A Un B) :: 'a :: ab_group_add) = |
|
1620 setsum f A + setsum f B - setsum f (A Int B)" |
|
1621 by (subst setsum_Un_Int [symmetric], auto simp add: ring_eq_simps) |
|
1622 |
|
1623 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = |
|
1624 (if a:A then setsum f A - f a else setsum f A)" |
|
1625 apply (case_tac "finite A") |
|
1626 prefer 2 apply (simp add: setsum_def) |
|
1627 apply (erule finite_induct) |
|
1628 apply (auto simp add: insert_Diff_if) |
|
1629 apply (drule_tac a = a in mk_disjoint_insert, auto) |
|
1630 done |
|
1631 |
|
1632 lemma setsum_diff1: "finite A \<Longrightarrow> |
|
1633 (setsum f (A - {a}) :: ('a::{pordered_ab_group_add})) = |
|
1634 (if a:A then setsum f A - f a else setsum f A)" |
|
1635 by (erule finite_induct) (auto simp add: insert_Diff_if) |
|
1636 |
|
1637 (* By Jeremy Siek: *) |
|
1638 |
|
1639 lemma setsum_diff_nat: |
|
1640 assumes finB: "finite B" |
|
1641 shows "B \<subseteq> A \<Longrightarrow> (setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" |
|
1642 using finB |
|
1643 proof (induct) |
|
1644 show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp |
|
1645 next |
|
1646 fix F x assume finF: "finite F" and xnotinF: "x \<notin> F" |
|
1647 and xFinA: "insert x F \<subseteq> A" |
|
1648 and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F" |
|
1649 from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp |
|
1650 from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" |
|
1651 by (simp add: setsum_diff1_nat) |
|
1652 from xFinA have "F \<subseteq> A" by simp |
|
1653 with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp |
|
1654 with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" |
|
1655 by simp |
|
1656 from xnotinF have "A - insert x F = (A - F) - {x}" by auto |
|
1657 with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x" |
|
1658 by simp |
|
1659 from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp |
|
1660 with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" |
|
1661 by simp |
|
1662 thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp |
|
1663 qed |
|
1664 |
|
1665 lemma setsum_diff: |
|
1666 assumes le: "finite A" "B \<subseteq> A" |
|
1667 shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::pordered_ab_group_add))" |
|
1668 proof - |
|
1669 from le have finiteB: "finite B" using finite_subset by auto |
|
1670 show ?thesis using finiteB le |
|
1671 proof (induct) |
|
1672 case empty |
|
1673 thus ?case by auto |
|
1674 next |
|
1675 case (insert x F) |
|
1676 thus ?case using le finiteB |
|
1677 by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) |
|
1678 qed |
|
1679 qed |
|
1680 |
|
1681 lemma setsum_mono: |
|
1682 assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, pordered_ab_semigroup_add}))" |
|
1683 shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" |
|
1684 proof (cases "finite K") |
|
1685 case True |
|
1686 thus ?thesis using le |
|
1687 proof (induct) |
|
1688 case empty |
|
1689 thus ?case by simp |
|
1690 next |
|
1691 case insert |
|
1692 thus ?case using add_mono |
|
1693 by force |
|
1694 qed |
|
1695 next |
|
1696 case False |
|
1697 thus ?thesis |
|
1698 by (simp add: setsum_def) |
|
1699 qed |
|
1700 |
|
1701 lemma setsum_negf: "finite A ==> setsum (%x. - (f x)::'a::ab_group_add) A = |
|
1702 - setsum f A" |
|
1703 by (induct set: Finites, auto) |
|
1704 |
|
1705 lemma setsum_subtractf: "finite A ==> setsum (%x. ((f x)::'a::ab_group_add) - g x) A = |
|
1706 setsum f A - setsum g A" |
|
1707 by (simp add: diff_minus setsum_addf setsum_negf) |
|
1708 |
|
1709 lemma setsum_nonneg: "[| finite A; |
|
1710 \<forall>x \<in> A. (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) \<le> f x |] ==> |
|
1711 0 \<le> setsum f A"; |
|
1712 apply (induct set: Finites, auto) |
|
1713 apply (subgoal_tac "0 + 0 \<le> f x + setsum f F", simp) |
|
1714 apply (blast intro: add_mono) |
|
1715 done |
|
1716 |
|
1717 lemma setsum_nonpos: "[| finite A; |
|
1718 \<forall>x \<in> A. f x \<le> (0::'a::{pordered_ab_semigroup_add, comm_monoid_add}) |] ==> |
|
1719 setsum f A \<le> 0"; |
|
1720 apply (induct set: Finites, auto) |
|
1721 apply (subgoal_tac "f x + setsum f F \<le> 0 + 0", simp) |
|
1722 apply (blast intro: add_mono) |
|
1723 done |
|
1724 |
|
1725 lemma setsum_mult: |
|
1726 fixes f :: "'a => ('b::semiring_0_cancel)" |
|
1727 shows "r * setsum f A = setsum (%n. r * f n) A" |
|
1728 proof (cases "finite A") |
|
1729 case True |
|
1730 thus ?thesis |
|
1731 proof (induct) |
|
1732 case empty thus ?case by simp |
|
1733 next |
|
1734 case (insert x A) thus ?case by (simp add: right_distrib) |
|
1735 qed |
|
1736 next |
|
1737 case False thus ?thesis by (simp add: setsum_def) |
|
1738 qed |
|
1739 |
|
1740 lemma setsum_abs: |
|
1741 fixes f :: "'a => ('b::lordered_ab_group_abs)" |
|
1742 assumes fin: "finite A" |
|
1743 shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" |
|
1744 using fin |
|
1745 proof (induct) |
|
1746 case empty thus ?case by simp |
|
1747 next |
|
1748 case (insert x A) |
|
1749 thus ?case by (auto intro: abs_triangle_ineq order_trans) |
|
1750 qed |
|
1751 |
|
1752 lemma setsum_abs_ge_zero: |
|
1753 fixes f :: "'a => ('b::lordered_ab_group_abs)" |
|
1754 assumes fin: "finite A" |
|
1755 shows "0 \<le> setsum (%i. abs(f i)) A" |
|
1756 using fin |
|
1757 proof (induct) |
|
1758 case empty thus ?case by simp |
|
1759 next |
|
1760 case (insert x A) thus ?case by (auto intro: order_trans) |
|
1761 qed |
|
1762 |
|
1763 subsubsection {* Cardinality of unions and Sigma sets *} |
|
1764 |
|
1765 lemma card_UN_disjoint: |
|
1766 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
1767 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1768 card (UNION I A) = setsum (%i. card (A i)) I" |
|
1769 apply (subst card_eq_setsum) |
|
1770 apply (subst finite_UN, assumption+) |
|
1771 apply (subgoal_tac |
|
1772 "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I") |
|
1773 apply (simp add: setsum_UN_disjoint) |
|
1774 apply (simp add: setsum_constant_nat cong: setsum_cong) |
|
1775 done |
|
1776 |
|
1777 lemma card_Union_disjoint: |
|
1778 "finite C ==> (ALL A:C. finite A) ==> |
|
1779 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==> |
|
1780 card (Union C) = setsum card C" |
|
1781 apply (frule card_UN_disjoint [of C id]) |
|
1782 apply (unfold Union_def id_def, assumption+) |
|
1783 done |
|
1784 |
|
1785 lemma SigmaI_insert: "y \<notin> A ==> |
|
1786 (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))" |
|
1787 by auto |
|
1788 |
|
1789 lemma card_cartesian_product_singleton: "finite A ==> |
|
1790 card({x} <*> A) = card(A)" |
|
1791 apply (subgoal_tac "inj_on (%y .(x,y)) A") |
|
1792 apply (frule card_image, assumption) |
|
1793 apply (subgoal_tac "(Pair x ` A) = {x} <*> A") |
|
1794 apply (auto simp add: inj_on_def) |
|
1795 done |
|
1796 |
|
1797 lemma card_SigmaI [rule_format,simp]: "finite A ==> |
|
1798 (ALL a:A. finite (B a)) --> |
|
1799 card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" |
|
1800 apply (erule finite_induct, auto) |
|
1801 apply (subst SigmaI_insert, assumption) |
|
1802 apply (subst card_Un_disjoint) |
|
1803 apply (auto intro: finite_SigmaI simp add: card_cartesian_product_singleton) |
|
1804 done |
|
1805 |
|
1806 lemma card_cartesian_product: |
|
1807 "[| finite A; finite B |] ==> card (A <*> B) = card(A) * card(B)" |
|
1808 by (simp add: setsum_constant_nat) |
|
1809 |
|
1810 |
|
1811 |
|
1812 subsection {* Generalized product over a set *} |
|
1813 |
|
1814 constdefs |
|
1815 setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult" |
|
1816 "setprod f A == if finite A then fold (op *) f 1 A else 1" |
|
1817 |
|
1818 syntax |
|
1819 "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_:_. _)" [0, 51, 10] 10) |
|
1820 |
|
1821 syntax (xsymbols) |
|
1822 "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1823 syntax (HTML output) |
|
1824 "_setprod" :: "idt => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1825 translations |
|
1826 "\<Prod>i:A. b" == "setprod (%i. b) A" -- {* Beware of argument permutation! *} |
|
1827 |
|
1828 syntax |
|
1829 "_Setprod" :: "'a set => 'a::comm_monoid_mult" ("\<Prod>_" [1000] 999) |
|
1830 |
|
1831 parse_translation {* |
|
1832 let |
|
1833 fun Setprod_tr [A] = Syntax.const "setprod" $ Abs ("", dummyT, Bound 0) $ A |
|
1834 in [("_Setprod", Setprod_tr)] end; |
|
1835 *} |
|
1836 print_translation {* |
|
1837 let fun setprod_tr' [Abs(x,Tx,t), A] = |
|
1838 if t = Bound 0 then Syntax.const "_Setprod" $ A else raise Match |
|
1839 in |
|
1840 [("setprod", setprod_tr')] |
|
1841 end |
|
1842 *} |
|
1843 |
|
1844 |
|
1845 text{* Instantiation of locales: *} |
|
1846 |
|
1847 lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)" |
|
1848 by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute) |
|
1849 |
|
1850 lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)" |
|
1851 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult) |
|
1852 |
|
1853 lemma setprod_empty [simp]: "setprod f {} = 1" |
|
1854 by (auto simp add: setprod_def) |
|
1855 |
|
1856 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==> |
|
1857 setprod f (insert a A) = f a * setprod f A" |
|
1858 by (simp add: setprod_def ACf.fold_insert [OF ACf_mult]) |
|
1859 |
|
1860 lemma setprod_reindex: |
|
1861 "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B" |
|
1862 by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD) |
|
1863 |
|
1864 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)" |
|
1865 by (auto simp add: setprod_reindex) |
|
1866 |
|
1867 lemma setprod_cong: |
|
1868 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" |
|
1869 by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult]) |
|
1870 |
|
1871 lemma setprod_reindex_cong: "inj_on f A ==> |
|
1872 B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" |
|
1873 by (frule setprod_reindex, simp) |
|
1874 |
|
1875 |
|
1876 lemma setprod_1: "setprod (%i. 1) A = 1" |
|
1877 apply (case_tac "finite A") |
|
1878 apply (erule finite_induct, auto simp add: mult_ac) |
|
1879 apply (simp add: setprod_def) |
|
1880 done |
|
1881 |
|
1882 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1" |
|
1883 apply (subgoal_tac "setprod f F = setprod (%x. 1) F") |
|
1884 apply (erule ssubst, rule setprod_1) |
|
1885 apply (rule setprod_cong, auto) |
|
1886 done |
|
1887 |
|
1888 lemma setprod_Un_Int: "finite A ==> finite B |
|
1889 ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" |
|
1890 by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric]) |
|
1891 |
|
1892 lemma setprod_Un_disjoint: "finite A ==> finite B |
|
1893 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" |
|
1894 by (subst setprod_Un_Int [symmetric], auto) |
|
1895 |
|
1896 lemma setprod_UN_disjoint: |
|
1897 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
1898 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1899 setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" |
|
1900 by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong) |
|
1901 |
|
1902 lemma setprod_Union_disjoint: |
|
1903 "finite C ==> (ALL A:C. finite A) ==> |
|
1904 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) ==> |
|
1905 setprod f (Union C) = setprod (setprod f) C" |
|
1906 apply (frule setprod_UN_disjoint [of C id f]) |
|
1907 apply (unfold Union_def id_def, assumption+) |
|
1908 done |
|
1909 |
|
1910 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
1911 (\<Prod>x:A. (\<Prod>y: B x. f x y)) = |
|
1912 (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))" |
|
1913 by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong) |
|
1914 |
|
1915 lemma setprod_cartesian_product: "finite A ==> finite B ==> |
|
1916 (\<Prod>x:A. (\<Prod>y: B. f x y)) = |
|
1917 (\<Prod>z:(A <*> B). f (fst z) (snd z))" |
|
1918 by (erule setprod_Sigma, auto) |
|
1919 |
|
1920 lemma setprod_timesf: |
|
1921 "setprod (%x. f x * g x) A = (setprod f A * setprod g A)" |
|
1922 by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult]) |
|
1923 |
|
1924 |
|
1925 subsubsection {* Properties in more restricted classes of structures *} |
|
1926 |
|
1927 lemma setprod_eq_1_iff [simp]: |
|
1928 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
|
1929 by (induct set: Finites) auto |
|
1930 |
|
1931 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)" |
|
1932 apply (erule finite_induct) |
|
1933 apply (auto simp add: power_Suc) |
|
1934 done |
|
1935 |
|
1936 lemma setprod_zero: |
|
1937 "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1_cancel) ==> setprod f A = 0" |
|
1938 apply (induct set: Finites, force, clarsimp) |
|
1939 apply (erule disjE, auto) |
|
1940 done |
|
1941 |
|
1942 lemma setprod_nonneg [rule_format]: |
|
1943 "(ALL x: A. (0::'a::ordered_idom) \<le> f x) --> 0 \<le> setprod f A" |
|
1944 apply (case_tac "finite A") |
|
1945 apply (induct set: Finites, force, clarsimp) |
|
1946 apply (subgoal_tac "0 * 0 \<le> f x * setprod f F", force) |
|
1947 apply (rule mult_mono, assumption+) |
|
1948 apply (auto simp add: setprod_def) |
|
1949 done |
|
1950 |
|
1951 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::ordered_idom) < f x) |
|
1952 --> 0 < setprod f A" |
|
1953 apply (case_tac "finite A") |
|
1954 apply (induct set: Finites, force, clarsimp) |
|
1955 apply (subgoal_tac "0 * 0 < f x * setprod f F", force) |
|
1956 apply (rule mult_strict_mono, assumption+) |
|
1957 apply (auto simp add: setprod_def) |
|
1958 done |
|
1959 |
|
1960 lemma setprod_nonzero [rule_format]: |
|
1961 "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> |
|
1962 finite A ==> (ALL x: A. f x \<noteq> (0::'a)) --> setprod f A \<noteq> 0" |
|
1963 apply (erule finite_induct, auto) |
|
1964 done |
|
1965 |
|
1966 lemma setprod_zero_eq: |
|
1967 "(ALL x y. (x::'a::comm_semiring_1_cancel) * y = 0 --> x = 0 | y = 0) ==> |
|
1968 finite A ==> (setprod f A = (0::'a)) = (EX x: A. f x = 0)" |
|
1969 apply (insert setprod_zero [of A f] setprod_nonzero [of A f], blast) |
|
1970 done |
|
1971 |
|
1972 lemma setprod_nonzero_field: |
|
1973 "finite A ==> (ALL x: A. f x \<noteq> (0::'a::field)) ==> setprod f A \<noteq> 0" |
|
1974 apply (rule setprod_nonzero, auto) |
|
1975 done |
|
1976 |
|
1977 lemma setprod_zero_eq_field: |
|
1978 "finite A ==> (setprod f A = (0::'a::field)) = (EX x: A. f x = 0)" |
|
1979 apply (rule setprod_zero_eq, auto) |
|
1980 done |
|
1981 |
|
1982 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==> |
|
1983 (setprod f (A Un B) :: 'a ::{field}) |
|
1984 = setprod f A * setprod f B / setprod f (A Int B)" |
|
1985 apply (subst setprod_Un_Int [symmetric], auto) |
|
1986 apply (subgoal_tac "finite (A Int B)") |
|
1987 apply (frule setprod_nonzero_field [of "A Int B" f], assumption) |
|
1988 apply (subst times_divide_eq_right [THEN sym], auto simp add: divide_self) |
|
1989 done |
|
1990 |
|
1991 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> |
|
1992 (setprod f (A - {a}) :: 'a :: {field}) = |
|
1993 (if a:A then setprod f A / f a else setprod f A)" |
|
1994 apply (erule finite_induct) |
|
1995 apply (auto simp add: insert_Diff_if) |
|
1996 apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a") |
|
1997 apply (erule ssubst) |
|
1998 apply (subst times_divide_eq_right [THEN sym]) |
|
1999 apply (auto simp add: mult_ac times_divide_eq_right divide_self) |
|
2000 done |
|
2001 |
|
2002 lemma setprod_inversef: "finite A ==> |
|
2003 ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> |
|
2004 setprod (inverse \<circ> f) A = inverse (setprod f A)" |
|
2005 apply (erule finite_induct) |
|
2006 apply (simp, simp) |
|
2007 done |
|
2008 |
|
2009 lemma setprod_dividef: |
|
2010 "[|finite A; |
|
2011 \<forall>x \<in> A. g x \<noteq> (0::'a::{field,division_by_zero})|] |
|
2012 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
|
2013 apply (subgoal_tac |
|
2014 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
|
2015 apply (erule ssubst) |
|
2016 apply (subst divide_inverse) |
|
2017 apply (subst setprod_timesf) |
|
2018 apply (subst setprod_inversef, assumption+, rule refl) |
|
2019 apply (rule setprod_cong, rule refl) |
|
2020 apply (subst divide_inverse, auto) |
|
2021 done |
|
2022 |
|
2023 end |
|