1051 apply blast |
1058 apply blast |
1052 done |
1059 done |
1053 |
1060 |
1054 end |
1061 end |
1055 |
1062 |
1056 subsection {* Generalized summation over a set *} |
|
1057 |
|
1058 interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add" |
|
1059 proof qed (auto intro: add_assoc add_commute) |
|
1060 |
|
1061 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add" |
|
1062 where "setsum f A == if finite A then fold_image (op +) f 0 A else 0" |
|
1063 |
|
1064 abbreviation |
|
1065 Setsum ("\<Sum>_" [1000] 999) where |
|
1066 "\<Sum>A == setsum (%x. x) A" |
|
1067 |
|
1068 text{* Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is |
|
1069 written @{text"\<Sum>x\<in>A. e"}. *} |
|
1070 |
|
1071 syntax |
|
1072 "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3SUM _:_. _)" [0, 51, 10] 10) |
|
1073 syntax (xsymbols) |
|
1074 "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
1075 syntax (HTML output) |
|
1076 "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add" ("(3\<Sum>_\<in>_. _)" [0, 51, 10] 10) |
|
1077 |
|
1078 translations -- {* Beware of argument permutation! *} |
|
1079 "SUM i:A. b" == "CONST setsum (%i. b) A" |
|
1080 "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A" |
|
1081 |
|
1082 text{* Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter |
|
1083 @{text"\<Sum>x|P. e"}. *} |
|
1084 |
|
1085 syntax |
|
1086 "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10) |
|
1087 syntax (xsymbols) |
|
1088 "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
1089 syntax (HTML output) |
|
1090 "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Sum>_ | (_)./ _)" [0,0,10] 10) |
|
1091 |
|
1092 translations |
|
1093 "SUM x|P. t" => "CONST setsum (%x. t) {x. P}" |
|
1094 "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}" |
|
1095 |
|
1096 print_translation {* |
|
1097 let |
|
1098 fun setsum_tr' [Abs (x, Tx, t), Const (@{const_syntax Collect}, _) $ Abs (y, Ty, P)] = |
|
1099 if x <> y then raise Match |
|
1100 else |
|
1101 let |
|
1102 val x' = Syntax.mark_bound x; |
|
1103 val t' = subst_bound (x', t); |
|
1104 val P' = subst_bound (x', P); |
|
1105 in Syntax.const @{syntax_const "_qsetsum"} $ Syntax.mark_bound x $ P' $ t' end |
|
1106 | setsum_tr' _ = raise Match; |
|
1107 in [(@{const_syntax setsum}, setsum_tr')] end |
|
1108 *} |
|
1109 |
|
1110 |
|
1111 lemma setsum_empty [simp]: "setsum f {} = 0" |
|
1112 by (simp add: setsum_def) |
|
1113 |
|
1114 lemma setsum_insert [simp]: |
|
1115 "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F" |
|
1116 by (simp add: setsum_def) |
|
1117 |
|
1118 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0" |
|
1119 by (simp add: setsum_def) |
|
1120 |
|
1121 lemma setsum_reindex: |
|
1122 "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B" |
|
1123 by(auto simp add: setsum_def comm_monoid_add.fold_image_reindex dest!:finite_imageD) |
|
1124 |
|
1125 lemma setsum_reindex_id: |
|
1126 "inj_on f B ==> setsum f B = setsum id (f ` B)" |
|
1127 by (auto simp add: setsum_reindex) |
|
1128 |
|
1129 lemma setsum_reindex_nonzero: |
|
1130 assumes fS: "finite S" |
|
1131 and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0" |
|
1132 shows "setsum h (f ` S) = setsum (h o f) S" |
|
1133 using nz |
|
1134 proof(induct rule: finite_induct[OF fS]) |
|
1135 case 1 thus ?case by simp |
|
1136 next |
|
1137 case (2 x F) |
|
1138 {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto |
|
1139 then obtain y where y: "y \<in> F" "f x = f y" by auto |
|
1140 from "2.hyps" y have xy: "x \<noteq> y" by auto |
|
1141 |
|
1142 from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp |
|
1143 have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto |
|
1144 also have "\<dots> = setsum (h o f) (insert x F)" |
|
1145 unfolding setsum_insert[OF `finite F` `x\<notin>F`] |
|
1146 using h0 |
|
1147 apply simp |
|
1148 apply (rule "2.hyps"(3)) |
|
1149 apply (rule_tac y="y" in "2.prems") |
|
1150 apply simp_all |
|
1151 done |
|
1152 finally have ?case .} |
|
1153 moreover |
|
1154 {assume fxF: "f x \<notin> f ` F" |
|
1155 have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" |
|
1156 using fxF "2.hyps" by simp |
|
1157 also have "\<dots> = setsum (h o f) (insert x F)" |
|
1158 unfolding setsum_insert[OF `finite F` `x\<notin>F`] |
|
1159 apply simp |
|
1160 apply (rule cong[OF refl[of "op + (h (f x))"]]) |
|
1161 apply (rule "2.hyps"(3)) |
|
1162 apply (rule_tac y="y" in "2.prems") |
|
1163 apply simp_all |
|
1164 done |
|
1165 finally have ?case .} |
|
1166 ultimately show ?case by blast |
|
1167 qed |
|
1168 |
|
1169 lemma setsum_cong: |
|
1170 "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B" |
|
1171 by(fastsimp simp: setsum_def intro: comm_monoid_add.fold_image_cong) |
|
1172 |
|
1173 lemma strong_setsum_cong[cong]: |
|
1174 "A = B ==> (!!x. x:B =simp=> f x = g x) |
|
1175 ==> setsum (%x. f x) A = setsum (%x. g x) B" |
|
1176 by(fastsimp simp: simp_implies_def setsum_def intro: comm_monoid_add.fold_image_cong) |
|
1177 |
|
1178 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A" |
|
1179 by (rule setsum_cong[OF refl], auto) |
|
1180 |
|
1181 lemma setsum_reindex_cong: |
|
1182 "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] |
|
1183 ==> setsum h B = setsum g A" |
|
1184 by (simp add: setsum_reindex cong: setsum_cong) |
|
1185 |
|
1186 |
|
1187 lemma setsum_0[simp]: "setsum (%i. 0) A = 0" |
|
1188 apply (clarsimp simp: setsum_def) |
|
1189 apply (erule finite_induct, auto) |
|
1190 done |
|
1191 |
|
1192 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0" |
|
1193 by(simp add:setsum_cong) |
|
1194 |
|
1195 lemma setsum_Un_Int: "finite A ==> finite B ==> |
|
1196 setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B" |
|
1197 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *} |
|
1198 by(simp add: setsum_def comm_monoid_add.fold_image_Un_Int [symmetric]) |
|
1199 |
|
1200 lemma setsum_Un_disjoint: "finite A ==> finite B |
|
1201 ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B" |
|
1202 by (subst setsum_Un_Int [symmetric], auto) |
|
1203 |
|
1204 lemma setsum_mono_zero_left: |
|
1205 assumes fT: "finite T" and ST: "S \<subseteq> T" |
|
1206 and z: "\<forall>i \<in> T - S. f i = 0" |
|
1207 shows "setsum f S = setsum f T" |
|
1208 proof- |
|
1209 have eq: "T = S \<union> (T - S)" using ST by blast |
|
1210 have d: "S \<inter> (T - S) = {}" using ST by blast |
|
1211 from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) |
|
1212 show ?thesis |
|
1213 by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) |
|
1214 qed |
|
1215 |
|
1216 lemma setsum_mono_zero_right: |
|
1217 "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. f i = 0 \<Longrightarrow> setsum f T = setsum f S" |
|
1218 by(blast intro!: setsum_mono_zero_left[symmetric]) |
|
1219 |
|
1220 lemma setsum_mono_zero_cong_left: |
|
1221 assumes fT: "finite T" and ST: "S \<subseteq> T" |
|
1222 and z: "\<forall>i \<in> T - S. g i = 0" |
|
1223 and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
|
1224 shows "setsum f S = setsum g T" |
|
1225 proof- |
|
1226 have eq: "T = S \<union> (T - S)" using ST by blast |
|
1227 have d: "S \<inter> (T - S) = {}" using ST by blast |
|
1228 from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) |
|
1229 show ?thesis |
|
1230 using fg by (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] setsum_0'[OF z]) |
|
1231 qed |
|
1232 |
|
1233 lemma setsum_mono_zero_cong_right: |
|
1234 assumes fT: "finite T" and ST: "S \<subseteq> T" |
|
1235 and z: "\<forall>i \<in> T - S. f i = 0" |
|
1236 and fg: "\<And>x. x \<in> S \<Longrightarrow> f x = g x" |
|
1237 shows "setsum f T = setsum g S" |
|
1238 using setsum_mono_zero_cong_left[OF fT ST z] fg[symmetric] by auto |
|
1239 |
|
1240 lemma setsum_delta: |
|
1241 assumes fS: "finite S" |
|
1242 shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)" |
|
1243 proof- |
|
1244 let ?f = "(\<lambda>k. if k=a then b k else 0)" |
|
1245 {assume a: "a \<notin> S" |
|
1246 hence "\<forall> k\<in> S. ?f k = 0" by simp |
|
1247 hence ?thesis using a by simp} |
|
1248 moreover |
|
1249 {assume a: "a \<in> S" |
|
1250 let ?A = "S - {a}" |
|
1251 let ?B = "{a}" |
|
1252 have eq: "S = ?A \<union> ?B" using a by blast |
|
1253 have dj: "?A \<inter> ?B = {}" by simp |
|
1254 from fS have fAB: "finite ?A" "finite ?B" by auto |
|
1255 have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" |
|
1256 using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] |
|
1257 by simp |
|
1258 then have ?thesis using a by simp} |
|
1259 ultimately show ?thesis by blast |
|
1260 qed |
|
1261 lemma setsum_delta': |
|
1262 assumes fS: "finite S" shows |
|
1263 "setsum (\<lambda>k. if a = k then b k else 0) S = |
|
1264 (if a\<in> S then b a else 0)" |
|
1265 using setsum_delta[OF fS, of a b, symmetric] |
|
1266 by (auto intro: setsum_cong) |
|
1267 |
|
1268 lemma setsum_restrict_set: |
|
1269 assumes fA: "finite A" |
|
1270 shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A" |
|
1271 proof- |
|
1272 from fA have fab: "finite (A \<inter> B)" by auto |
|
1273 have aba: "A \<inter> B \<subseteq> A" by blast |
|
1274 let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0" |
|
1275 from setsum_mono_zero_left[OF fA aba, of ?g] |
|
1276 show ?thesis by simp |
|
1277 qed |
|
1278 |
|
1279 lemma setsum_cases: |
|
1280 assumes fA: "finite A" |
|
1281 shows "setsum (\<lambda>x. if P x then f x else g x) A = |
|
1282 setsum f (A \<inter> {x. P x}) + setsum g (A \<inter> - {x. P x})" |
|
1283 proof- |
|
1284 have a: "A = A \<inter> {x. P x} \<union> A \<inter> -{x. P x}" |
|
1285 "(A \<inter> {x. P x}) \<inter> (A \<inter> -{x. P x}) = {}" |
|
1286 by blast+ |
|
1287 from fA |
|
1288 have f: "finite (A \<inter> {x. P x})" "finite (A \<inter> -{x. P x})" by auto |
|
1289 let ?g = "\<lambda>x. if P x then f x else g x" |
|
1290 from setsum_Un_disjoint[OF f a(2), of ?g] a(1) |
|
1291 show ?thesis by simp |
|
1292 qed |
|
1293 |
|
1294 |
|
1295 (*But we can't get rid of finite I. If infinite, although the rhs is 0, |
|
1296 the lhs need not be, since UNION I A could still be finite.*) |
|
1297 lemma setsum_UN_disjoint: |
|
1298 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
1299 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1300 setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))" |
|
1301 by(simp add: setsum_def comm_monoid_add.fold_image_UN_disjoint cong: setsum_cong) |
|
1302 |
|
1303 text{*No need to assume that @{term C} is finite. If infinite, the rhs is |
|
1304 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*} |
|
1305 lemma setsum_Union_disjoint: |
|
1306 "[| (ALL A:C. finite A); |
|
1307 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] |
|
1308 ==> setsum f (Union C) = setsum (setsum f) C" |
|
1309 apply (cases "finite C") |
|
1310 prefer 2 apply (force dest: finite_UnionD simp add: setsum_def) |
|
1311 apply (frule setsum_UN_disjoint [of C id f]) |
|
1312 apply (unfold Union_def id_def, assumption+) |
|
1313 done |
|
1314 |
|
1315 (*But we can't get rid of finite A. If infinite, although the lhs is 0, |
|
1316 the rhs need not be, since SIGMA A B could still be finite.*) |
|
1317 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
1318 (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)" |
|
1319 by(simp add:setsum_def comm_monoid_add.fold_image_Sigma split_def cong:setsum_cong) |
|
1320 |
|
1321 text{*Here we can eliminate the finiteness assumptions, by cases.*} |
|
1322 lemma setsum_cartesian_product: |
|
1323 "(\<Sum>x\<in>A. (\<Sum>y\<in>B. f x y)) = (\<Sum>(x,y) \<in> A <*> B. f x y)" |
|
1324 apply (cases "finite A") |
|
1325 apply (cases "finite B") |
|
1326 apply (simp add: setsum_Sigma) |
|
1327 apply (cases "A={}", simp) |
|
1328 apply (simp) |
|
1329 apply (auto simp add: setsum_def |
|
1330 dest: finite_cartesian_productD1 finite_cartesian_productD2) |
|
1331 done |
|
1332 |
|
1333 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)" |
|
1334 by(simp add:setsum_def comm_monoid_add.fold_image_distrib) |
|
1335 |
|
1336 |
|
1337 subsubsection {* Properties in more restricted classes of structures *} |
|
1338 |
|
1339 lemma setsum_SucD: "setsum f A = Suc n ==> EX a:A. 0 < f a" |
|
1340 apply (case_tac "finite A") |
|
1341 prefer 2 apply (simp add: setsum_def) |
|
1342 apply (erule rev_mp) |
|
1343 apply (erule finite_induct, auto) |
|
1344 done |
|
1345 |
|
1346 lemma setsum_eq_0_iff [simp]: |
|
1347 "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))" |
|
1348 by (induct set: finite) auto |
|
1349 |
|
1350 lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow> |
|
1351 (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))" |
|
1352 apply(erule finite_induct) |
|
1353 apply (auto simp add:add_is_1) |
|
1354 done |
|
1355 |
|
1356 lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]] |
|
1357 |
|
1358 lemma setsum_Un_nat: "finite A ==> finite B ==> |
|
1359 (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)" |
|
1360 -- {* For the natural numbers, we have subtraction. *} |
|
1361 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) |
|
1362 |
|
1363 lemma setsum_Un: "finite A ==> finite B ==> |
|
1364 (setsum f (A Un B) :: 'a :: ab_group_add) = |
|
1365 setsum f A + setsum f B - setsum f (A Int B)" |
|
1366 by (subst setsum_Un_Int [symmetric], auto simp add: algebra_simps) |
|
1367 |
|
1368 lemma (in comm_monoid_mult) fold_image_1: "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1" |
|
1369 apply (induct set: finite) |
|
1370 apply simp by auto |
|
1371 |
|
1372 lemma (in comm_monoid_mult) fold_image_Un_one: |
|
1373 assumes fS: "finite S" and fT: "finite T" |
|
1374 and I0: "\<forall>x \<in> S\<inter>T. f x = 1" |
|
1375 shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T" |
|
1376 proof- |
|
1377 have "fold_image op * f 1 (S \<inter> T) = 1" |
|
1378 apply (rule fold_image_1) |
|
1379 using fS fT I0 by auto |
|
1380 with fold_image_Un_Int[OF fS fT] show ?thesis by simp |
|
1381 qed |
|
1382 |
|
1383 lemma setsum_eq_general_reverses: |
|
1384 assumes fS: "finite S" and fT: "finite T" |
|
1385 and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y" |
|
1386 and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x" |
|
1387 shows "setsum f S = setsum g T" |
|
1388 apply (simp add: setsum_def fS fT) |
|
1389 apply (rule comm_monoid_add.fold_image_eq_general_inverses[OF fS]) |
|
1390 apply (erule kh) |
|
1391 apply (erule hk) |
|
1392 done |
|
1393 |
|
1394 |
|
1395 |
|
1396 lemma setsum_Un_zero: |
|
1397 assumes fS: "finite S" and fT: "finite T" |
|
1398 and I0: "\<forall>x \<in> S\<inter>T. f x = 0" |
|
1399 shows "setsum f (S \<union> T) = setsum f S + setsum f T" |
|
1400 using fS fT |
|
1401 apply (simp add: setsum_def) |
|
1402 apply (rule comm_monoid_add.fold_image_Un_one) |
|
1403 using I0 by auto |
|
1404 |
|
1405 |
|
1406 lemma setsum_UNION_zero: |
|
1407 assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T" |
|
1408 and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0" |
|
1409 shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S" |
|
1410 using fSS f0 |
|
1411 proof(induct rule: finite_induct[OF fS]) |
|
1412 case 1 thus ?case by simp |
|
1413 next |
|
1414 case (2 T F) |
|
1415 then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" |
|
1416 and H: "setsum f (\<Union> F) = setsum (setsum f) F" by auto |
|
1417 from fTF have fUF: "finite (\<Union>F)" by auto |
|
1418 from "2.prems" TF fTF |
|
1419 show ?case |
|
1420 by (auto simp add: H[symmetric] intro: setsum_Un_zero[OF fTF(1) fUF, of f]) |
|
1421 qed |
|
1422 |
|
1423 |
|
1424 lemma setsum_diff1_nat: "(setsum f (A - {a}) :: nat) = |
|
1425 (if a:A then setsum f A - f a else setsum f A)" |
|
1426 apply (case_tac "finite A") |
|
1427 prefer 2 apply (simp add: setsum_def) |
|
1428 apply (erule finite_induct) |
|
1429 apply (auto simp add: insert_Diff_if) |
|
1430 apply (drule_tac a = a in mk_disjoint_insert, auto) |
|
1431 done |
|
1432 |
|
1433 lemma setsum_diff1: "finite A \<Longrightarrow> |
|
1434 (setsum f (A - {a}) :: ('a::ab_group_add)) = |
|
1435 (if a:A then setsum f A - f a else setsum f A)" |
|
1436 by (erule finite_induct) (auto simp add: insert_Diff_if) |
|
1437 |
|
1438 lemma setsum_diff1'[rule_format]: |
|
1439 "finite A \<Longrightarrow> a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x)" |
|
1440 apply (erule finite_induct[where F=A and P="% A. (a \<in> A \<longrightarrow> (\<Sum> x \<in> A. f x) = f a + (\<Sum> x \<in> (A - {a}). f x))"]) |
|
1441 apply (auto simp add: insert_Diff_if add_ac) |
|
1442 done |
|
1443 |
|
1444 lemma setsum_diff1_ring: assumes "finite A" "a \<in> A" |
|
1445 shows "setsum f (A - {a}) = setsum f A - (f a::'a::ring)" |
|
1446 unfolding setsum_diff1'[OF assms] by auto |
|
1447 |
|
1448 (* By Jeremy Siek: *) |
|
1449 |
|
1450 lemma setsum_diff_nat: |
|
1451 assumes "finite B" and "B \<subseteq> A" |
|
1452 shows "(setsum f (A - B) :: nat) = (setsum f A) - (setsum f B)" |
|
1453 using assms |
|
1454 proof induct |
|
1455 show "setsum f (A - {}) = (setsum f A) - (setsum f {})" by simp |
|
1456 next |
|
1457 fix F x assume finF: "finite F" and xnotinF: "x \<notin> F" |
|
1458 and xFinA: "insert x F \<subseteq> A" |
|
1459 and IH: "F \<subseteq> A \<Longrightarrow> setsum f (A - F) = setsum f A - setsum f F" |
|
1460 from xnotinF xFinA have xinAF: "x \<in> (A - F)" by simp |
|
1461 from xinAF have A: "setsum f ((A - F) - {x}) = setsum f (A - F) - f x" |
|
1462 by (simp add: setsum_diff1_nat) |
|
1463 from xFinA have "F \<subseteq> A" by simp |
|
1464 with IH have "setsum f (A - F) = setsum f A - setsum f F" by simp |
|
1465 with A have B: "setsum f ((A - F) - {x}) = setsum f A - setsum f F - f x" |
|
1466 by simp |
|
1467 from xnotinF have "A - insert x F = (A - F) - {x}" by auto |
|
1468 with B have C: "setsum f (A - insert x F) = setsum f A - setsum f F - f x" |
|
1469 by simp |
|
1470 from finF xnotinF have "setsum f (insert x F) = setsum f F + f x" by simp |
|
1471 with C have "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" |
|
1472 by simp |
|
1473 thus "setsum f (A - insert x F) = setsum f A - setsum f (insert x F)" by simp |
|
1474 qed |
|
1475 |
|
1476 lemma setsum_diff: |
|
1477 assumes le: "finite A" "B \<subseteq> A" |
|
1478 shows "setsum f (A - B) = setsum f A - ((setsum f B)::('a::ab_group_add))" |
|
1479 proof - |
|
1480 from le have finiteB: "finite B" using finite_subset by auto |
|
1481 show ?thesis using finiteB le |
|
1482 proof induct |
|
1483 case empty |
|
1484 thus ?case by auto |
|
1485 next |
|
1486 case (insert x F) |
|
1487 thus ?case using le finiteB |
|
1488 by (simp add: Diff_insert[where a=x and B=F] setsum_diff1 insert_absorb) |
|
1489 qed |
|
1490 qed |
|
1491 |
|
1492 lemma setsum_mono: |
|
1493 assumes le: "\<And>i. i\<in>K \<Longrightarrow> f (i::'a) \<le> ((g i)::('b::{comm_monoid_add, ordered_ab_semigroup_add}))" |
|
1494 shows "(\<Sum>i\<in>K. f i) \<le> (\<Sum>i\<in>K. g i)" |
|
1495 proof (cases "finite K") |
|
1496 case True |
|
1497 thus ?thesis using le |
|
1498 proof induct |
|
1499 case empty |
|
1500 thus ?case by simp |
|
1501 next |
|
1502 case insert |
|
1503 thus ?case using add_mono by fastsimp |
|
1504 qed |
|
1505 next |
|
1506 case False |
|
1507 thus ?thesis |
|
1508 by (simp add: setsum_def) |
|
1509 qed |
|
1510 |
|
1511 lemma setsum_strict_mono: |
|
1512 fixes f :: "'a \<Rightarrow> 'b::{ordered_cancel_ab_semigroup_add,comm_monoid_add}" |
|
1513 assumes "finite A" "A \<noteq> {}" |
|
1514 and "!!x. x:A \<Longrightarrow> f x < g x" |
|
1515 shows "setsum f A < setsum g A" |
|
1516 using prems |
|
1517 proof (induct rule: finite_ne_induct) |
|
1518 case singleton thus ?case by simp |
|
1519 next |
|
1520 case insert thus ?case by (auto simp: add_strict_mono) |
|
1521 qed |
|
1522 |
|
1523 lemma setsum_negf: |
|
1524 "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" |
|
1525 proof (cases "finite A") |
|
1526 case True thus ?thesis by (induct set: finite) auto |
|
1527 next |
|
1528 case False thus ?thesis by (simp add: setsum_def) |
|
1529 qed |
|
1530 |
|
1531 lemma setsum_subtractf: |
|
1532 "setsum (%x. ((f x)::'a::ab_group_add) - g x) A = |
|
1533 setsum f A - setsum g A" |
|
1534 proof (cases "finite A") |
|
1535 case True thus ?thesis by (simp add: diff_minus setsum_addf setsum_negf) |
|
1536 next |
|
1537 case False thus ?thesis by (simp add: setsum_def) |
|
1538 qed |
|
1539 |
|
1540 lemma setsum_nonneg: |
|
1541 assumes nn: "\<forall>x\<in>A. (0::'a::{ordered_ab_semigroup_add,comm_monoid_add}) \<le> f x" |
|
1542 shows "0 \<le> setsum f A" |
|
1543 proof (cases "finite A") |
|
1544 case True thus ?thesis using nn |
|
1545 proof induct |
|
1546 case empty then show ?case by simp |
|
1547 next |
|
1548 case (insert x F) |
|
1549 then have "0 + 0 \<le> f x + setsum f F" by (blast intro: add_mono) |
|
1550 with insert show ?case by simp |
|
1551 qed |
|
1552 next |
|
1553 case False thus ?thesis by (simp add: setsum_def) |
|
1554 qed |
|
1555 |
|
1556 lemma setsum_nonpos: |
|
1557 assumes np: "\<forall>x\<in>A. f x \<le> (0::'a::{ordered_ab_semigroup_add,comm_monoid_add})" |
|
1558 shows "setsum f A \<le> 0" |
|
1559 proof (cases "finite A") |
|
1560 case True thus ?thesis using np |
|
1561 proof induct |
|
1562 case empty then show ?case by simp |
|
1563 next |
|
1564 case (insert x F) |
|
1565 then have "f x + setsum f F \<le> 0 + 0" by (blast intro: add_mono) |
|
1566 with insert show ?case by simp |
|
1567 qed |
|
1568 next |
|
1569 case False thus ?thesis by (simp add: setsum_def) |
|
1570 qed |
|
1571 |
|
1572 lemma setsum_mono2: |
|
1573 fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}" |
|
1574 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b" |
|
1575 shows "setsum f A \<le> setsum f B" |
|
1576 proof - |
|
1577 have "setsum f A \<le> setsum f A + setsum f (B-A)" |
|
1578 by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def) |
|
1579 also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin] |
|
1580 by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) |
|
1581 also have "A \<union> (B-A) = B" using sub by blast |
|
1582 finally show ?thesis . |
|
1583 qed |
|
1584 |
|
1585 lemma setsum_mono3: "finite B ==> A <= B ==> |
|
1586 ALL x: B - A. |
|
1587 0 <= ((f x)::'a::{comm_monoid_add,ordered_ab_semigroup_add}) ==> |
|
1588 setsum f A <= setsum f B" |
|
1589 apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)") |
|
1590 apply (erule ssubst) |
|
1591 apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)") |
|
1592 apply simp |
|
1593 apply (rule add_left_mono) |
|
1594 apply (erule setsum_nonneg) |
|
1595 apply (subst setsum_Un_disjoint [THEN sym]) |
|
1596 apply (erule finite_subset, assumption) |
|
1597 apply (rule finite_subset) |
|
1598 prefer 2 |
|
1599 apply assumption |
|
1600 apply (auto simp add: sup_absorb2) |
|
1601 done |
|
1602 |
|
1603 lemma setsum_right_distrib: |
|
1604 fixes f :: "'a => ('b::semiring_0)" |
|
1605 shows "r * setsum f A = setsum (%n. r * f n) A" |
|
1606 proof (cases "finite A") |
|
1607 case True |
|
1608 thus ?thesis |
|
1609 proof induct |
|
1610 case empty thus ?case by simp |
|
1611 next |
|
1612 case (insert x A) thus ?case by (simp add: right_distrib) |
|
1613 qed |
|
1614 next |
|
1615 case False thus ?thesis by (simp add: setsum_def) |
|
1616 qed |
|
1617 |
|
1618 lemma setsum_left_distrib: |
|
1619 "setsum f A * (r::'a::semiring_0) = (\<Sum>n\<in>A. f n * r)" |
|
1620 proof (cases "finite A") |
|
1621 case True |
|
1622 then show ?thesis |
|
1623 proof induct |
|
1624 case empty thus ?case by simp |
|
1625 next |
|
1626 case (insert x A) thus ?case by (simp add: left_distrib) |
|
1627 qed |
|
1628 next |
|
1629 case False thus ?thesis by (simp add: setsum_def) |
|
1630 qed |
|
1631 |
|
1632 lemma setsum_divide_distrib: |
|
1633 "setsum f A / (r::'a::field) = (\<Sum>n\<in>A. f n / r)" |
|
1634 proof (cases "finite A") |
|
1635 case True |
|
1636 then show ?thesis |
|
1637 proof induct |
|
1638 case empty thus ?case by simp |
|
1639 next |
|
1640 case (insert x A) thus ?case by (simp add: add_divide_distrib) |
|
1641 qed |
|
1642 next |
|
1643 case False thus ?thesis by (simp add: setsum_def) |
|
1644 qed |
|
1645 |
|
1646 lemma setsum_abs[iff]: |
|
1647 fixes f :: "'a => ('b::ordered_ab_group_add_abs)" |
|
1648 shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A" |
|
1649 proof (cases "finite A") |
|
1650 case True |
|
1651 thus ?thesis |
|
1652 proof induct |
|
1653 case empty thus ?case by simp |
|
1654 next |
|
1655 case (insert x A) |
|
1656 thus ?case by (auto intro: abs_triangle_ineq order_trans) |
|
1657 qed |
|
1658 next |
|
1659 case False thus ?thesis by (simp add: setsum_def) |
|
1660 qed |
|
1661 |
|
1662 lemma setsum_abs_ge_zero[iff]: |
|
1663 fixes f :: "'a => ('b::ordered_ab_group_add_abs)" |
|
1664 shows "0 \<le> setsum (%i. abs(f i)) A" |
|
1665 proof (cases "finite A") |
|
1666 case True |
|
1667 thus ?thesis |
|
1668 proof induct |
|
1669 case empty thus ?case by simp |
|
1670 next |
|
1671 case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg) |
|
1672 qed |
|
1673 next |
|
1674 case False thus ?thesis by (simp add: setsum_def) |
|
1675 qed |
|
1676 |
|
1677 lemma abs_setsum_abs[simp]: |
|
1678 fixes f :: "'a => ('b::ordered_ab_group_add_abs)" |
|
1679 shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))" |
|
1680 proof (cases "finite A") |
|
1681 case True |
|
1682 thus ?thesis |
|
1683 proof induct |
|
1684 case empty thus ?case by simp |
|
1685 next |
|
1686 case (insert a A) |
|
1687 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 |
|
1688 also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" using insert by simp |
|
1689 also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" |
|
1690 by (simp del: abs_of_nonneg) |
|
1691 also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp |
|
1692 finally show ?case . |
|
1693 qed |
|
1694 next |
|
1695 case False thus ?thesis by (simp add: setsum_def) |
|
1696 qed |
|
1697 |
|
1698 |
|
1699 lemma setsum_Plus: |
|
1700 fixes A :: "'a set" and B :: "'b set" |
|
1701 assumes fin: "finite A" "finite B" |
|
1702 shows "setsum f (A <+> B) = setsum (f \<circ> Inl) A + setsum (f \<circ> Inr) B" |
|
1703 proof - |
|
1704 have "A <+> B = Inl ` A \<union> Inr ` B" by auto |
|
1705 moreover from fin have "finite (Inl ` A :: ('a + 'b) set)" "finite (Inr ` B :: ('a + 'b) set)" |
|
1706 by(auto intro: finite_imageI) |
|
1707 moreover have "Inl ` A \<inter> Inr ` B = ({} :: ('a + 'b) set)" by auto |
|
1708 moreover have "inj_on (Inl :: 'a \<Rightarrow> 'a + 'b) A" "inj_on (Inr :: 'b \<Rightarrow> 'a + 'b) B" by(auto intro: inj_onI) |
|
1709 ultimately show ?thesis using fin by(simp add: setsum_Un_disjoint setsum_reindex) |
|
1710 qed |
|
1711 |
|
1712 |
|
1713 text {* Commuting outer and inner summation *} |
|
1714 |
|
1715 lemma swap_inj_on: |
|
1716 "inj_on (%(i, j). (j, i)) (A \<times> B)" |
|
1717 by (unfold inj_on_def) fast |
|
1718 |
|
1719 lemma swap_product: |
|
1720 "(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A" |
|
1721 by (simp add: split_def image_def) blast |
|
1722 |
|
1723 lemma setsum_commute: |
|
1724 "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)" |
|
1725 proof (simp add: setsum_cartesian_product) |
|
1726 have "(\<Sum>(x,y) \<in> A <*> B. f x y) = |
|
1727 (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)" |
|
1728 (is "?s = _") |
|
1729 apply (simp add: setsum_reindex [where f = "%(i, j). (j, i)"] swap_inj_on) |
|
1730 apply (simp add: split_def) |
|
1731 done |
|
1732 also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)" |
|
1733 (is "_ = ?t") |
|
1734 apply (simp add: swap_product) |
|
1735 done |
|
1736 finally show "?s = ?t" . |
|
1737 qed |
|
1738 |
|
1739 lemma setsum_product: |
|
1740 fixes f :: "'a => ('b::semiring_0)" |
|
1741 shows "setsum f A * setsum g B = (\<Sum>i\<in>A. \<Sum>j\<in>B. f i * g j)" |
|
1742 by (simp add: setsum_right_distrib setsum_left_distrib) (rule setsum_commute) |
|
1743 |
|
1744 lemma setsum_mult_setsum_if_inj: |
|
1745 fixes f :: "'a => ('b::semiring_0)" |
|
1746 shows "inj_on (%(a,b). f a * g b) (A \<times> B) ==> |
|
1747 setsum f A * setsum g B = setsum id {f a * g b|a b. a:A & b:B}" |
|
1748 by(auto simp: setsum_product setsum_cartesian_product |
|
1749 intro!: setsum_reindex_cong[symmetric]) |
|
1750 |
|
1751 |
|
1752 subsection {* Generalized product over a set *} |
|
1753 |
|
1754 definition setprod :: "('a => 'b) => 'a set => 'b::comm_monoid_mult" |
|
1755 where "setprod f A == if finite A then fold_image (op *) f 1 A else 1" |
|
1756 |
|
1757 abbreviation |
|
1758 Setprod ("\<Prod>_" [1000] 999) where |
|
1759 "\<Prod>A == setprod (%x. x) A" |
|
1760 |
|
1761 syntax |
|
1762 "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3PROD _:_. _)" [0, 51, 10] 10) |
|
1763 syntax (xsymbols) |
|
1764 "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1765 syntax (HTML output) |
|
1766 "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(3\<Prod>_\<in>_. _)" [0, 51, 10] 10) |
|
1767 |
|
1768 translations -- {* Beware of argument permutation! *} |
|
1769 "PROD i:A. b" == "CONST setprod (%i. b) A" |
|
1770 "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" |
|
1771 |
|
1772 text{* Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter |
|
1773 @{text"\<Prod>x|P. e"}. *} |
|
1774 |
|
1775 syntax |
|
1776 "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3PROD _ |/ _./ _)" [0,0,10] 10) |
|
1777 syntax (xsymbols) |
|
1778 "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10) |
|
1779 syntax (HTML output) |
|
1780 "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<Prod>_ | (_)./ _)" [0,0,10] 10) |
|
1781 |
|
1782 translations |
|
1783 "PROD x|P. t" => "CONST setprod (%x. t) {x. P}" |
|
1784 "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}" |
|
1785 |
|
1786 |
|
1787 lemma setprod_empty [simp]: "setprod f {} = 1" |
|
1788 by (auto simp add: setprod_def) |
|
1789 |
|
1790 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==> |
|
1791 setprod f (insert a A) = f a * setprod f A" |
|
1792 by (simp add: setprod_def) |
|
1793 |
|
1794 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1" |
|
1795 by (simp add: setprod_def) |
|
1796 |
|
1797 lemma setprod_reindex: |
|
1798 "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B" |
|
1799 by(auto simp: setprod_def fold_image_reindex dest!:finite_imageD) |
|
1800 |
|
1801 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)" |
|
1802 by (auto simp add: setprod_reindex) |
|
1803 |
|
1804 lemma setprod_cong: |
|
1805 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B" |
|
1806 by(fastsimp simp: setprod_def intro: fold_image_cong) |
|
1807 |
|
1808 lemma strong_setprod_cong[cong]: |
|
1809 "A = B ==> (!!x. x:B =simp=> f x = g x) ==> setprod f A = setprod g B" |
|
1810 by(fastsimp simp: simp_implies_def setprod_def intro: fold_image_cong) |
|
1811 |
|
1812 lemma setprod_reindex_cong: "inj_on f A ==> |
|
1813 B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A" |
|
1814 by (frule setprod_reindex, simp) |
|
1815 |
|
1816 lemma strong_setprod_reindex_cong: assumes i: "inj_on f A" |
|
1817 and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x" |
|
1818 shows "setprod h B = setprod g A" |
|
1819 proof- |
|
1820 have "setprod h B = setprod (h o f) A" |
|
1821 by (simp add: B setprod_reindex[OF i, of h]) |
|
1822 then show ?thesis apply simp |
|
1823 apply (rule setprod_cong) |
|
1824 apply simp |
|
1825 by (simp add: eq) |
|
1826 qed |
|
1827 |
|
1828 lemma setprod_Un_one: |
|
1829 assumes fS: "finite S" and fT: "finite T" |
|
1830 and I0: "\<forall>x \<in> S\<inter>T. f x = 1" |
|
1831 shows "setprod f (S \<union> T) = setprod f S * setprod f T" |
|
1832 using fS fT |
|
1833 apply (simp add: setprod_def) |
|
1834 apply (rule fold_image_Un_one) |
|
1835 using I0 by auto |
|
1836 |
|
1837 |
|
1838 lemma setprod_1: "setprod (%i. 1) A = 1" |
|
1839 apply (case_tac "finite A") |
|
1840 apply (erule finite_induct, auto simp add: mult_ac) |
|
1841 done |
|
1842 |
|
1843 lemma setprod_1': "ALL a:F. f a = 1 ==> setprod f F = 1" |
|
1844 apply (subgoal_tac "setprod f F = setprod (%x. 1) F") |
|
1845 apply (erule ssubst, rule setprod_1) |
|
1846 apply (rule setprod_cong, auto) |
|
1847 done |
|
1848 |
|
1849 lemma setprod_Un_Int: "finite A ==> finite B |
|
1850 ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B" |
|
1851 by(simp add: setprod_def fold_image_Un_Int[symmetric]) |
|
1852 |
|
1853 lemma setprod_Un_disjoint: "finite A ==> finite B |
|
1854 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B" |
|
1855 by (subst setprod_Un_Int [symmetric], auto) |
|
1856 |
|
1857 lemma setprod_mono_one_left: |
|
1858 assumes fT: "finite T" and ST: "S \<subseteq> T" |
|
1859 and z: "\<forall>i \<in> T - S. f i = 1" |
|
1860 shows "setprod f S = setprod f T" |
|
1861 proof- |
|
1862 have eq: "T = S \<union> (T - S)" using ST by blast |
|
1863 have d: "S \<inter> (T - S) = {}" using ST by blast |
|
1864 from fT ST have f: "finite S" "finite (T - S)" by (auto intro: finite_subset) |
|
1865 show ?thesis |
|
1866 by (simp add: setprod_Un_disjoint[OF f d, unfolded eq[symmetric]] setprod_1'[OF z]) |
|
1867 qed |
|
1868 |
|
1869 lemmas setprod_mono_one_right = setprod_mono_one_left [THEN sym] |
|
1870 |
|
1871 lemma setprod_delta: |
|
1872 assumes fS: "finite S" |
|
1873 shows "setprod (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)" |
|
1874 proof- |
|
1875 let ?f = "(\<lambda>k. if k=a then b k else 1)" |
|
1876 {assume a: "a \<notin> S" |
|
1877 hence "\<forall> k\<in> S. ?f k = 1" by simp |
|
1878 hence ?thesis using a by (simp add: setprod_1 cong add: setprod_cong) } |
|
1879 moreover |
|
1880 {assume a: "a \<in> S" |
|
1881 let ?A = "S - {a}" |
|
1882 let ?B = "{a}" |
|
1883 have eq: "S = ?A \<union> ?B" using a by blast |
|
1884 have dj: "?A \<inter> ?B = {}" by simp |
|
1885 from fS have fAB: "finite ?A" "finite ?B" by auto |
|
1886 have fA1: "setprod ?f ?A = 1" apply (rule setprod_1') by auto |
|
1887 have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" |
|
1888 using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] |
|
1889 by simp |
|
1890 then have ?thesis using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)} |
|
1891 ultimately show ?thesis by blast |
|
1892 qed |
|
1893 |
|
1894 lemma setprod_delta': |
|
1895 assumes fS: "finite S" shows |
|
1896 "setprod (\<lambda>k. if a = k then b k else 1) S = |
|
1897 (if a\<in> S then b a else 1)" |
|
1898 using setprod_delta[OF fS, of a b, symmetric] |
|
1899 by (auto intro: setprod_cong) |
|
1900 |
|
1901 |
|
1902 lemma setprod_UN_disjoint: |
|
1903 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
1904 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==> |
|
1905 setprod f (UNION I A) = setprod (%i. setprod f (A i)) I" |
|
1906 by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong) |
|
1907 |
|
1908 lemma setprod_Union_disjoint: |
|
1909 "[| (ALL A:C. finite A); |
|
1910 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |] |
|
1911 ==> setprod f (Union C) = setprod (setprod f) C" |
|
1912 apply (cases "finite C") |
|
1913 prefer 2 apply (force dest: finite_UnionD simp add: setprod_def) |
|
1914 apply (frule setprod_UN_disjoint [of C id f]) |
|
1915 apply (unfold Union_def id_def, assumption+) |
|
1916 done |
|
1917 |
|
1918 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==> |
|
1919 (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) = |
|
1920 (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)" |
|
1921 by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong) |
|
1922 |
|
1923 text{*Here we can eliminate the finiteness assumptions, by cases.*} |
|
1924 lemma setprod_cartesian_product: |
|
1925 "(\<Prod>x\<in>A. (\<Prod>y\<in> B. f x y)) = (\<Prod>(x,y)\<in>(A <*> B). f x y)" |
|
1926 apply (cases "finite A") |
|
1927 apply (cases "finite B") |
|
1928 apply (simp add: setprod_Sigma) |
|
1929 apply (cases "A={}", simp) |
|
1930 apply (simp add: setprod_1) |
|
1931 apply (auto simp add: setprod_def |
|
1932 dest: finite_cartesian_productD1 finite_cartesian_productD2) |
|
1933 done |
|
1934 |
|
1935 lemma setprod_timesf: |
|
1936 "setprod (%x. f x * g x) A = (setprod f A * setprod g A)" |
|
1937 by(simp add:setprod_def fold_image_distrib) |
|
1938 |
|
1939 |
|
1940 subsubsection {* Properties in more restricted classes of structures *} |
|
1941 |
|
1942 lemma setprod_eq_1_iff [simp]: |
|
1943 "finite F ==> (setprod f F = 1) = (ALL a:F. f a = (1::nat))" |
|
1944 by (induct set: finite) auto |
|
1945 |
|
1946 lemma setprod_zero: |
|
1947 "finite A ==> EX x: A. f x = (0::'a::comm_semiring_1) ==> setprod f A = 0" |
|
1948 apply (induct set: finite, force, clarsimp) |
|
1949 apply (erule disjE, auto) |
|
1950 done |
|
1951 |
|
1952 lemma setprod_nonneg [rule_format]: |
|
1953 "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A" |
|
1954 by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg) |
|
1955 |
|
1956 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x) |
|
1957 --> 0 < setprod f A" |
|
1958 by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos) |
|
1959 |
|
1960 lemma setprod_zero_iff[simp]: "finite A ==> |
|
1961 (setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors})) = |
|
1962 (EX x: A. f x = 0)" |
|
1963 by (erule finite_induct, auto simp:no_zero_divisors) |
|
1964 |
|
1965 lemma setprod_pos_nat: |
|
1966 "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0" |
|
1967 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric]) |
|
1968 |
|
1969 lemma setprod_pos_nat_iff[simp]: |
|
1970 "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))" |
|
1971 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric]) |
|
1972 |
|
1973 lemma setprod_Un: "finite A ==> finite B ==> (ALL x: A Int B. f x \<noteq> 0) ==> |
|
1974 (setprod f (A Un B) :: 'a ::{field}) |
|
1975 = setprod f A * setprod f B / setprod f (A Int B)" |
|
1976 by (subst setprod_Un_Int [symmetric], auto) |
|
1977 |
|
1978 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==> |
|
1979 (setprod f (A - {a}) :: 'a :: {field}) = |
|
1980 (if a:A then setprod f A / f a else setprod f A)" |
|
1981 by (erule finite_induct) (auto simp add: insert_Diff_if) |
|
1982 |
|
1983 lemma setprod_inversef: |
|
1984 fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}" |
|
1985 shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
|
1986 by (erule finite_induct) auto |
|
1987 |
|
1988 lemma setprod_dividef: |
|
1989 fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}" |
|
1990 shows "finite A |
|
1991 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
|
1992 apply (subgoal_tac |
|
1993 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
|
1994 apply (erule ssubst) |
|
1995 apply (subst divide_inverse) |
|
1996 apply (subst setprod_timesf) |
|
1997 apply (subst setprod_inversef, assumption+, rule refl) |
|
1998 apply (rule setprod_cong, rule refl) |
|
1999 apply (subst divide_inverse, auto) |
|
2000 done |
|
2001 |
|
2002 lemma setprod_dvd_setprod [rule_format]: |
|
2003 "(ALL x : A. f x dvd g x) \<longrightarrow> setprod f A dvd setprod g A" |
|
2004 apply (cases "finite A") |
|
2005 apply (induct set: finite) |
|
2006 apply (auto simp add: dvd_def) |
|
2007 apply (rule_tac x = "k * ka" in exI) |
|
2008 apply (simp add: algebra_simps) |
|
2009 done |
|
2010 |
|
2011 lemma setprod_dvd_setprod_subset: |
|
2012 "finite B \<Longrightarrow> A <= B \<Longrightarrow> setprod f A dvd setprod f B" |
|
2013 apply (subgoal_tac "setprod f B = setprod f A * setprod f (B - A)") |
|
2014 apply (unfold dvd_def, blast) |
|
2015 apply (subst setprod_Un_disjoint [symmetric]) |
|
2016 apply (auto elim: finite_subset intro: setprod_cong) |
|
2017 done |
|
2018 |
|
2019 lemma setprod_dvd_setprod_subset2: |
|
2020 "finite B \<Longrightarrow> A <= B \<Longrightarrow> ALL x : A. (f x::'a::comm_semiring_1) dvd g x \<Longrightarrow> |
|
2021 setprod f A dvd setprod g B" |
|
2022 apply (rule dvd_trans) |
|
2023 apply (rule setprod_dvd_setprod, erule (1) bspec) |
|
2024 apply (erule (1) setprod_dvd_setprod_subset) |
|
2025 done |
|
2026 |
|
2027 lemma dvd_setprod: "finite A \<Longrightarrow> i:A \<Longrightarrow> |
|
2028 (f i ::'a::comm_semiring_1) dvd setprod f A" |
|
2029 by (induct set: finite) (auto intro: dvd_mult) |
|
2030 |
|
2031 lemma dvd_setsum [rule_format]: "(ALL i : A. d dvd f i) \<longrightarrow> |
|
2032 (d::'a::comm_semiring_1) dvd (SUM x : A. f x)" |
|
2033 apply (cases "finite A") |
|
2034 apply (induct set: finite) |
|
2035 apply auto |
|
2036 done |
|
2037 |
|
2038 lemma setprod_mono: |
|
2039 fixes f :: "'a \<Rightarrow> 'b\<Colon>linordered_semidom" |
|
2040 assumes "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i" |
|
2041 shows "setprod f A \<le> setprod g A" |
|
2042 proof (cases "finite A") |
|
2043 case True |
|
2044 hence ?thesis "setprod f A \<ge> 0" using subset_refl[of A] |
|
2045 proof (induct A rule: finite_subset_induct) |
|
2046 case (insert a F) |
|
2047 thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)" |
|
2048 unfolding setprod_insert[OF insert(1,3)] |
|
2049 using assms[rule_format,OF insert(2)] insert |
|
2050 by (auto intro: mult_mono mult_nonneg_nonneg) |
|
2051 qed auto |
|
2052 thus ?thesis by simp |
|
2053 qed auto |
|
2054 |
|
2055 lemma abs_setprod: |
|
2056 fixes f :: "'a \<Rightarrow> 'b\<Colon>{linordered_field,abs}" |
|
2057 shows "abs (setprod f A) = setprod (\<lambda>x. abs (f x)) A" |
|
2058 proof (cases "finite A") |
|
2059 case True thus ?thesis |
|
2060 by induct (auto simp add: field_simps abs_mult) |
|
2061 qed auto |
|
2062 |
|
2063 |
|
2064 subsection {* Finite cardinality *} |
|
2065 |
|
2066 text {* This definition, although traditional, is ugly to work with: |
|
2067 @{text "card A == LEAST n. EX f. A = {f i | i. i < n}"}. |
|
2068 But now that we have @{text setsum} things are easy: |
|
2069 *} |
|
2070 |
|
2071 definition card :: "'a set \<Rightarrow> nat" where |
|
2072 "card A = setsum (\<lambda>x. 1) A" |
|
2073 |
|
2074 lemmas card_eq_setsum = card_def |
|
2075 |
|
2076 lemma card_empty [simp]: "card {} = 0" |
|
2077 by (simp add: card_def) |
|
2078 |
|
2079 lemma card_insert_disjoint [simp]: |
|
2080 "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)" |
|
2081 by (simp add: card_def) |
|
2082 |
|
2083 lemma card_insert_if: |
|
2084 "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))" |
|
2085 by (simp add: insert_absorb) |
|
2086 |
|
2087 lemma card_infinite [simp]: "~ finite A ==> card A = 0" |
|
2088 by (simp add: card_def) |
|
2089 |
|
2090 lemma card_ge_0_finite: |
|
2091 "card A > 0 \<Longrightarrow> finite A" |
|
2092 by (rule ccontr) simp |
|
2093 |
|
2094 lemma card_0_eq [simp,noatp]: "finite A ==> (card A = 0) = (A = {})" |
|
2095 apply auto |
|
2096 apply (drule_tac a = x in mk_disjoint_insert, clarify, auto) |
|
2097 done |
|
2098 |
|
2099 lemma finite_UNIV_card_ge_0: |
|
2100 "finite (UNIV :: 'a set) \<Longrightarrow> card (UNIV :: 'a set) > 0" |
|
2101 by (rule ccontr) simp |
|
2102 |
|
2103 lemma card_eq_0_iff: "(card A = 0) = (A = {} | ~ finite A)" |
|
2104 by auto |
|
2105 |
|
2106 lemma card_gt_0_iff: "(0 < card A) = (A \<noteq> {} & finite A)" |
|
2107 by (simp add: neq0_conv [symmetric] card_eq_0_iff) |
|
2108 |
|
2109 lemma card_Suc_Diff1: "finite A ==> x: A ==> Suc (card (A - {x})) = card A" |
|
2110 apply(rule_tac t = A in insert_Diff [THEN subst], assumption) |
|
2111 apply(simp del:insert_Diff_single) |
|
2112 done |
|
2113 |
|
2114 lemma card_Diff_singleton: |
|
2115 "finite A ==> x: A ==> card (A - {x}) = card A - 1" |
|
2116 by (simp add: card_Suc_Diff1 [symmetric]) |
|
2117 |
|
2118 lemma card_Diff_singleton_if: |
|
2119 "finite A ==> card (A-{x}) = (if x : A then card A - 1 else card A)" |
|
2120 by (simp add: card_Diff_singleton) |
|
2121 |
|
2122 lemma card_Diff_insert[simp]: |
|
2123 assumes "finite A" and "a:A" and "a ~: B" |
|
2124 shows "card(A - insert a B) = card(A - B) - 1" |
|
2125 proof - |
|
2126 have "A - insert a B = (A - B) - {a}" using assms by blast |
|
2127 then show ?thesis using assms by(simp add:card_Diff_singleton) |
|
2128 qed |
|
2129 |
|
2130 lemma card_insert: "finite A ==> card (insert x A) = Suc (card (A - {x}))" |
|
2131 by (simp add: card_insert_if card_Suc_Diff1 del:card_Diff_insert) |
|
2132 |
|
2133 lemma card_insert_le: "finite A ==> card A <= card (insert x A)" |
|
2134 by (simp add: card_insert_if) |
|
2135 |
|
2136 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B" |
|
2137 by (simp add: card_def setsum_mono2) |
|
2138 |
|
2139 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" |
|
2140 apply (induct set: finite, simp, clarify) |
|
2141 apply (subgoal_tac "finite A & A - {x} <= F") |
|
2142 prefer 2 apply (blast intro: finite_subset, atomize) |
|
2143 apply (drule_tac x = "A - {x}" in spec) |
|
2144 apply (simp add: card_Diff_singleton_if split add: split_if_asm) |
|
2145 apply (case_tac "card A", auto) |
|
2146 done |
|
2147 |
|
2148 lemma psubset_card_mono: "finite B ==> A < B ==> card A < card B" |
|
2149 apply (simp add: psubset_eq linorder_not_le [symmetric]) |
|
2150 apply (blast dest: card_seteq) |
|
2151 done |
|
2152 |
|
2153 lemma card_Un_Int: "finite A ==> finite B |
|
2154 ==> card A + card B = card (A Un B) + card (A Int B)" |
|
2155 by(simp add:card_def setsum_Un_Int) |
|
2156 |
|
2157 lemma card_Un_disjoint: "finite A ==> finite B |
|
2158 ==> A Int B = {} ==> card (A Un B) = card A + card B" |
|
2159 by (simp add: card_Un_Int) |
|
2160 |
|
2161 lemma card_Diff_subset: |
|
2162 "finite B ==> B <= A ==> card (A - B) = card A - card B" |
|
2163 by(simp add:card_def setsum_diff_nat) |
|
2164 |
|
2165 lemma card_Diff_subset_Int: |
|
2166 assumes AB: "finite (A \<inter> B)" shows "card (A - B) = card A - card (A \<inter> B)" |
|
2167 proof - |
|
2168 have "A - B = A - A \<inter> B" by auto |
|
2169 thus ?thesis |
|
2170 by (simp add: card_Diff_subset AB) |
|
2171 qed |
|
2172 |
|
2173 lemma card_Diff1_less: "finite A ==> x: A ==> card (A - {x}) < card A" |
|
2174 apply (rule Suc_less_SucD) |
|
2175 apply (simp add: card_Suc_Diff1 del:card_Diff_insert) |
|
2176 done |
|
2177 |
|
2178 lemma card_Diff2_less: |
|
2179 "finite A ==> x: A ==> y: A ==> card (A - {x} - {y}) < card A" |
|
2180 apply (case_tac "x = y") |
|
2181 apply (simp add: card_Diff1_less del:card_Diff_insert) |
|
2182 apply (rule less_trans) |
|
2183 prefer 2 apply (auto intro!: card_Diff1_less simp del:card_Diff_insert) |
|
2184 done |
|
2185 |
|
2186 lemma card_Diff1_le: "finite A ==> card (A - {x}) <= card A" |
|
2187 apply (case_tac "x : A") |
|
2188 apply (simp_all add: card_Diff1_less less_imp_le) |
|
2189 done |
|
2190 |
|
2191 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B" |
|
2192 by (erule psubsetI, blast) |
|
2193 |
|
2194 lemma insert_partition: |
|
2195 "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk> |
|
2196 \<Longrightarrow> x \<inter> \<Union> F = {}" |
|
2197 by auto |
|
2198 |
|
2199 lemma finite_psubset_induct[consumes 1, case_names psubset]: |
|
2200 assumes "finite A" and "!!A. finite A \<Longrightarrow> (!!B. finite B \<Longrightarrow> B \<subset> A \<Longrightarrow> P(B)) \<Longrightarrow> P(A)" shows "P A" |
|
2201 using assms(1) |
|
2202 proof (induct A rule: measure_induct_rule[where f=card]) |
|
2203 case (less A) |
|
2204 show ?case |
|
2205 proof(rule assms(2)[OF less(2)]) |
|
2206 fix B assume "finite B" "B \<subset> A" |
|
2207 show "P B" by(rule less(1)[OF psubset_card_mono[OF less(2) `B \<subset> A`] `finite B`]) |
|
2208 qed |
|
2209 qed |
|
2210 |
|
2211 text{* main cardinality theorem *} |
|
2212 lemma card_partition [rule_format]: |
|
2213 "finite C ==> |
|
2214 finite (\<Union> C) --> |
|
2215 (\<forall>c\<in>C. card c = k) --> |
|
2216 (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) --> |
|
2217 k * card(C) = card (\<Union> C)" |
|
2218 apply (erule finite_induct, simp) |
|
2219 apply (simp add: card_Un_disjoint insert_partition |
|
2220 finite_subset [of _ "\<Union> (insert x F)"]) |
|
2221 done |
|
2222 |
|
2223 lemma card_eq_UNIV_imp_eq_UNIV: |
|
2224 assumes fin: "finite (UNIV :: 'a set)" |
|
2225 and card: "card A = card (UNIV :: 'a set)" |
|
2226 shows "A = (UNIV :: 'a set)" |
|
2227 proof |
|
2228 show "A \<subseteq> UNIV" by simp |
|
2229 show "UNIV \<subseteq> A" |
|
2230 proof |
|
2231 fix x |
|
2232 show "x \<in> A" |
|
2233 proof (rule ccontr) |
|
2234 assume "x \<notin> A" |
|
2235 then have "A \<subset> UNIV" by auto |
|
2236 with fin have "card A < card (UNIV :: 'a set)" by (fact psubset_card_mono) |
|
2237 with card show False by simp |
|
2238 qed |
|
2239 qed |
|
2240 qed |
|
2241 |
|
2242 text{*The form of a finite set of given cardinality*} |
|
2243 |
|
2244 lemma card_eq_SucD: |
|
2245 assumes "card A = Suc k" |
|
2246 shows "\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={})" |
|
2247 proof - |
|
2248 have fin: "finite A" using assms by (auto intro: ccontr) |
|
2249 moreover have "card A \<noteq> 0" using assms by auto |
|
2250 ultimately obtain b where b: "b \<in> A" by auto |
|
2251 show ?thesis |
|
2252 proof (intro exI conjI) |
|
2253 show "A = insert b (A-{b})" using b by blast |
|
2254 show "b \<notin> A - {b}" by blast |
|
2255 show "card (A - {b}) = k" and "k = 0 \<longrightarrow> A - {b} = {}" |
|
2256 using assms b fin by(fastsimp dest:mk_disjoint_insert)+ |
|
2257 qed |
|
2258 qed |
|
2259 |
|
2260 lemma card_Suc_eq: |
|
2261 "(card A = Suc k) = |
|
2262 (\<exists>b B. A = insert b B & b \<notin> B & card B = k & (k=0 \<longrightarrow> B={}))" |
|
2263 apply(rule iffI) |
|
2264 apply(erule card_eq_SucD) |
|
2265 apply(auto) |
|
2266 apply(subst card_insert) |
|
2267 apply(auto intro:ccontr) |
|
2268 done |
|
2269 |
|
2270 lemma finite_fun_UNIVD2: |
|
2271 assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)" |
|
2272 shows "finite (UNIV :: 'b set)" |
|
2273 proof - |
|
2274 from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary))" |
|
2275 by(rule finite_imageI) |
|
2276 moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. f arbitrary)" |
|
2277 by(rule UNIV_eq_I) auto |
|
2278 ultimately show "finite (UNIV :: 'b set)" by simp |
|
2279 qed |
|
2280 |
|
2281 lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y" |
|
2282 apply (cases "finite A") |
|
2283 apply (erule finite_induct) |
|
2284 apply (auto simp add: algebra_simps) |
|
2285 done |
|
2286 |
|
2287 lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)" |
|
2288 apply (erule finite_induct) |
|
2289 apply auto |
|
2290 done |
|
2291 |
|
2292 lemma setprod_gen_delta: |
|
2293 assumes fS: "finite S" |
|
2294 shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::{comm_monoid_mult}) * c^ (card S - 1) else c^ card S)" |
|
2295 proof- |
|
2296 let ?f = "(\<lambda>k. if k=a then b k else c)" |
|
2297 {assume a: "a \<notin> S" |
|
2298 hence "\<forall> k\<in> S. ?f k = c" by simp |
|
2299 hence ?thesis using a setprod_constant[OF fS, of c] by (simp add: setprod_1 cong add: setprod_cong) } |
|
2300 moreover |
|
2301 {assume a: "a \<in> S" |
|
2302 let ?A = "S - {a}" |
|
2303 let ?B = "{a}" |
|
2304 have eq: "S = ?A \<union> ?B" using a by blast |
|
2305 have dj: "?A \<inter> ?B = {}" by simp |
|
2306 from fS have fAB: "finite ?A" "finite ?B" by auto |
|
2307 have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A" |
|
2308 apply (rule setprod_cong) by auto |
|
2309 have cA: "card ?A = card S - 1" using fS a by auto |
|
2310 have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto |
|
2311 have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" |
|
2312 using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] |
|
2313 by simp |
|
2314 then have ?thesis using a cA |
|
2315 by (simp add: fA1 ring_simps cong add: setprod_cong cong del: if_weak_cong)} |
|
2316 ultimately show ?thesis by blast |
|
2317 qed |
|
2318 |
|
2319 |
|
2320 lemma setsum_bounded: |
|
2321 assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})" |
|
2322 shows "setsum f A \<le> of_nat(card A) * K" |
|
2323 proof (cases "finite A") |
|
2324 case True |
|
2325 thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp |
|
2326 next |
|
2327 case False thus ?thesis by (simp add: setsum_def) |
|
2328 qed |
|
2329 |
|
2330 |
|
2331 lemma card_UNIV_unit: "card (UNIV :: unit set) = 1" |
|
2332 unfolding UNIV_unit by simp |
|
2333 |
|
2334 |
|
2335 subsubsection {* Cardinality of unions *} |
|
2336 |
|
2337 lemma card_UN_disjoint: |
|
2338 "finite I ==> (ALL i:I. finite (A i)) ==> |
|
2339 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) |
|
2340 ==> card (UNION I A) = (\<Sum>i\<in>I. card(A i))" |
|
2341 apply (simp add: card_def del: setsum_constant) |
|
2342 apply (subgoal_tac |
|
2343 "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I") |
|
2344 apply (simp add: setsum_UN_disjoint del: setsum_constant) |
|
2345 apply (simp cong: setsum_cong) |
|
2346 done |
|
2347 |
|
2348 lemma card_Union_disjoint: |
|
2349 "finite C ==> (ALL A:C. finite A) ==> |
|
2350 (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |
|
2351 ==> card (Union C) = setsum card C" |
|
2352 apply (frule card_UN_disjoint [of C id]) |
|
2353 apply (unfold Union_def id_def, assumption+) |
|
2354 done |
|
2355 |
|
2356 |
|
2357 subsubsection {* Cardinality of image *} |
|
2358 |
|
2359 text{*The image of a finite set can be expressed using @{term fold_image}.*} |
|
2360 lemma image_eq_fold_image: |
|
2361 "finite A ==> f ` A = fold_image (op Un) (%x. {f x}) {} A" |
|
2362 proof (induct rule: finite_induct) |
|
2363 case empty then show ?case by simp |
|
2364 next |
|
2365 interpret ab_semigroup_mult "op Un" |
|
2366 proof qed auto |
|
2367 case insert |
|
2368 then show ?case by simp |
|
2369 qed |
|
2370 |
|
2371 lemma card_image_le: "finite A ==> card (f ` A) <= card A" |
|
2372 apply (induct set: finite) |
|
2373 apply simp |
|
2374 apply (simp add: le_SucI card_insert_if) |
|
2375 done |
|
2376 |
|
2377 lemma card_image: "inj_on f A ==> card (f ` A) = card A" |
|
2378 by(simp add:card_def setsum_reindex o_def del:setsum_constant) |
|
2379 |
|
2380 lemma bij_betw_same_card: "bij_betw f A B \<Longrightarrow> card A = card B" |
|
2381 by(auto simp: card_image bij_betw_def) |
|
2382 |
|
2383 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A" |
|
2384 by (simp add: card_seteq card_image) |
|
2385 |
|
2386 lemma eq_card_imp_inj_on: |
|
2387 "[| finite A; card(f ` A) = card A |] ==> inj_on f A" |
|
2388 apply (induct rule:finite_induct) |
|
2389 apply simp |
|
2390 apply(frule card_image_le[where f = f]) |
|
2391 apply(simp add:card_insert_if split:if_splits) |
|
2392 done |
|
2393 |
|
2394 lemma inj_on_iff_eq_card: |
|
2395 "finite A ==> inj_on f A = (card(f ` A) = card A)" |
|
2396 by(blast intro: card_image eq_card_imp_inj_on) |
|
2397 |
|
2398 |
|
2399 lemma card_inj_on_le: |
|
2400 "[|inj_on f A; f ` A \<subseteq> B; finite B |] ==> card A \<le> card B" |
|
2401 apply (subgoal_tac "finite A") |
|
2402 apply (force intro: card_mono simp add: card_image [symmetric]) |
|
2403 apply (blast intro: finite_imageD dest: finite_subset) |
|
2404 done |
|
2405 |
|
2406 lemma card_bij_eq: |
|
2407 "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A; |
|
2408 finite A; finite B |] ==> card A = card B" |
|
2409 by (auto intro: le_antisym card_inj_on_le) |
|
2410 |
|
2411 |
|
2412 subsubsection {* Cardinality of products *} |
|
2413 |
|
2414 (* |
|
2415 lemma SigmaI_insert: "y \<notin> A ==> |
|
2416 (SIGMA x:(insert y A). B x) = (({y} <*> (B y)) \<union> (SIGMA x: A. B x))" |
|
2417 by auto |
|
2418 *) |
|
2419 |
|
2420 lemma card_SigmaI [simp]: |
|
2421 "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk> |
|
2422 \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))" |
|
2423 by(simp add:card_def setsum_Sigma del:setsum_constant) |
|
2424 |
|
2425 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)" |
|
2426 apply (cases "finite A") |
|
2427 apply (cases "finite B") |
|
2428 apply (auto simp add: card_eq_0_iff |
|
2429 dest: finite_cartesian_productD1 finite_cartesian_productD2) |
|
2430 done |
|
2431 |
|
2432 lemma card_cartesian_product_singleton: "card({x} <*> A) = card(A)" |
|
2433 by (simp add: card_cartesian_product) |
|
2434 |
|
2435 |
|
2436 subsubsection {* Cardinality of sums *} |
|
2437 |
|
2438 lemma card_Plus: |
|
2439 assumes "finite A" and "finite B" |
|
2440 shows "card (A <+> B) = card A + card B" |
|
2441 proof - |
|
2442 have "Inl`A \<inter> Inr`B = {}" by fast |
|
2443 with assms show ?thesis |
|
2444 unfolding Plus_def |
|
2445 by (simp add: card_Un_disjoint card_image) |
|
2446 qed |
|
2447 |
|
2448 lemma card_Plus_conv_if: |
|
2449 "card (A <+> B) = (if finite A \<and> finite B then card(A) + card(B) else 0)" |
|
2450 by(auto simp: card_def setsum_Plus simp del: setsum_constant) |
|
2451 |
|
2452 |
|
2453 subsubsection {* Cardinality of the Powerset *} |
|
2454 |
|
2455 lemma card_Pow: "finite A ==> card (Pow A) = Suc (Suc 0) ^ card A" (* FIXME numeral 2 (!?) *) |
|
2456 apply (induct set: finite) |
|
2457 apply (simp_all add: Pow_insert) |
|
2458 apply (subst card_Un_disjoint, blast) |
|
2459 apply (blast intro: finite_imageI, blast) |
|
2460 apply (subgoal_tac "inj_on (insert x) (Pow F)") |
|
2461 apply (simp add: card_image Pow_insert) |
|
2462 apply (unfold inj_on_def) |
|
2463 apply (blast elim!: equalityE) |
|
2464 done |
|
2465 |
|
2466 text {* Relates to equivalence classes. Based on a theorem of F. Kammüller. *} |
|
2467 |
|
2468 lemma dvd_partition: |
|
2469 "finite (Union C) ==> |
|
2470 ALL c : C. k dvd card c ==> |
|
2471 (ALL c1: C. ALL c2: C. c1 \<noteq> c2 --> c1 Int c2 = {}) ==> |
|
2472 k dvd card (Union C)" |
|
2473 apply(frule finite_UnionD) |
|
2474 apply(rotate_tac -1) |
|
2475 apply (induct set: finite, simp_all, clarify) |
|
2476 apply (subst card_Un_disjoint) |
|
2477 apply (auto simp add: disjoint_eq_subset_Compl) |
|
2478 done |
|
2479 |
|
2480 |
|
2481 subsubsection {* Relating injectivity and surjectivity *} |
|
2482 |
|
2483 lemma finite_surj_inj: "finite(A) \<Longrightarrow> A <= f`A \<Longrightarrow> inj_on f A" |
|
2484 apply(rule eq_card_imp_inj_on, assumption) |
|
2485 apply(frule finite_imageI) |
|
2486 apply(drule (1) card_seteq) |
|
2487 apply(erule card_image_le) |
|
2488 apply simp |
|
2489 done |
|
2490 |
|
2491 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a" |
|
2492 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f" |
|
2493 by (blast intro: finite_surj_inj subset_UNIV dest:surj_range) |
|
2494 |
|
2495 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a" |
|
2496 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f" |
|
2497 by(fastsimp simp:surj_def dest!: endo_inj_surj) |
|
2498 |
|
2499 corollary infinite_UNIV_nat[iff]: "~finite(UNIV::nat set)" |
|
2500 proof |
|
2501 assume "finite(UNIV::nat set)" |
|
2502 with finite_UNIV_inj_surj[of Suc] |
|
2503 show False by simp (blast dest: Suc_neq_Zero surjD) |
|
2504 qed |
|
2505 |
|
2506 (* Often leads to bogus ATP proofs because of reduced type information, hence noatp *) |
|
2507 lemma infinite_UNIV_char_0[noatp]: |
|
2508 "\<not> finite (UNIV::'a::semiring_char_0 set)" |
|
2509 proof |
|
2510 assume "finite (UNIV::'a set)" |
|
2511 with subset_UNIV have "finite (range of_nat::'a set)" |
|
2512 by (rule finite_subset) |
|
2513 moreover have "inj (of_nat::nat \<Rightarrow> 'a)" |
|
2514 by (simp add: inj_on_def) |
|
2515 ultimately have "finite (UNIV::nat set)" |
|
2516 by (rule finite_imageD) |
|
2517 then show "False" |
|
2518 by simp |
|
2519 qed |
|
2520 |
1063 |
2521 subsection{* A fold functional for non-empty sets *} |
1064 subsection{* A fold functional for non-empty sets *} |
2522 |
1065 |
2523 text{* Does not require start value. *} |
1066 text{* Does not require start value. *} |
2524 |
1067 |
2809 next |
1352 next |
2810 case insert thus ?case by (simp add: mult_assoc) |
1353 case insert thus ?case by (simp add: mult_assoc) |
2811 qed |
1354 qed |
2812 |
1355 |
2813 |
1356 |
2814 subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *} |
|
2815 |
|
2816 text{* |
|
2817 As an application of @{text fold1} we define infimum |
|
2818 and supremum in (not necessarily complete!) lattices |
|
2819 over (non-empty) sets by means of @{text fold1}. |
|
2820 *} |
|
2821 |
|
2822 context semilattice_inf |
|
2823 begin |
|
2824 |
|
2825 lemma below_fold1_iff: |
|
2826 assumes "finite A" "A \<noteq> {}" |
|
2827 shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" |
|
2828 proof - |
|
2829 interpret ab_semigroup_idem_mult inf |
|
2830 by (rule ab_semigroup_idem_mult_inf) |
|
2831 show ?thesis using assms by (induct rule: finite_ne_induct) simp_all |
|
2832 qed |
|
2833 |
|
2834 lemma fold1_belowI: |
|
2835 assumes "finite A" |
|
2836 and "a \<in> A" |
|
2837 shows "fold1 inf A \<le> a" |
|
2838 proof - |
|
2839 from assms have "A \<noteq> {}" by auto |
|
2840 from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis |
|
2841 proof (induct rule: finite_ne_induct) |
|
2842 case singleton thus ?case by simp |
|
2843 next |
|
2844 interpret ab_semigroup_idem_mult inf |
|
2845 by (rule ab_semigroup_idem_mult_inf) |
|
2846 case (insert x F) |
|
2847 from insert(5) have "a = x \<or> a \<in> F" by simp |
|
2848 thus ?case |
|
2849 proof |
|
2850 assume "a = x" thus ?thesis using insert |
|
2851 by (simp add: mult_ac) |
|
2852 next |
|
2853 assume "a \<in> F" |
|
2854 hence bel: "fold1 inf F \<le> a" by (rule insert) |
|
2855 have "inf (fold1 inf (insert x F)) a = inf x (inf (fold1 inf F) a)" |
|
2856 using insert by (simp add: mult_ac) |
|
2857 also have "inf (fold1 inf F) a = fold1 inf F" |
|
2858 using bel by (auto intro: antisym) |
|
2859 also have "inf x \<dots> = fold1 inf (insert x F)" |
|
2860 using insert by (simp add: mult_ac) |
|
2861 finally have aux: "inf (fold1 inf (insert x F)) a = fold1 inf (insert x F)" . |
|
2862 moreover have "inf (fold1 inf (insert x F)) a \<le> a" by simp |
|
2863 ultimately show ?thesis by simp |
|
2864 qed |
|
2865 qed |
|
2866 qed |
|
2867 |
|
2868 end |
|
2869 |
|
2870 context lattice |
|
2871 begin |
|
2872 |
|
2873 definition |
|
2874 Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900) |
|
2875 where |
|
2876 "Inf_fin = fold1 inf" |
|
2877 |
|
2878 definition |
|
2879 Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900) |
|
2880 where |
|
2881 "Sup_fin = fold1 sup" |
|
2882 |
|
2883 lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<le> \<Squnion>\<^bsub>fin\<^esub>A" |
|
2884 apply(unfold Sup_fin_def Inf_fin_def) |
|
2885 apply(subgoal_tac "EX a. a:A") |
|
2886 prefer 2 apply blast |
|
2887 apply(erule exE) |
|
2888 apply(rule order_trans) |
|
2889 apply(erule (1) fold1_belowI) |
|
2890 apply(erule (1) semilattice_inf.fold1_belowI [OF dual_semilattice]) |
|
2891 done |
|
2892 |
|
2893 lemma sup_Inf_absorb [simp]: |
|
2894 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^bsub>fin\<^esub>A) = a" |
|
2895 apply(subst sup_commute) |
|
2896 apply(simp add: Inf_fin_def sup_absorb2 fold1_belowI) |
|
2897 done |
|
2898 |
|
2899 lemma inf_Sup_absorb [simp]: |
|
2900 "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^bsub>fin\<^esub>A) = a" |
|
2901 by (simp add: Sup_fin_def inf_absorb1 |
|
2902 semilattice_inf.fold1_belowI [OF dual_semilattice]) |
|
2903 |
|
2904 end |
|
2905 |
|
2906 context distrib_lattice |
|
2907 begin |
|
2908 |
|
2909 lemma sup_Inf1_distrib: |
|
2910 assumes "finite A" |
|
2911 and "A \<noteq> {}" |
|
2912 shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}" |
|
2913 proof - |
|
2914 interpret ab_semigroup_idem_mult inf |
|
2915 by (rule ab_semigroup_idem_mult_inf) |
|
2916 from assms show ?thesis |
|
2917 by (simp add: Inf_fin_def image_def |
|
2918 hom_fold1_commute [where h="sup x", OF sup_inf_distrib1]) |
|
2919 (rule arg_cong [where f="fold1 inf"], blast) |
|
2920 qed |
|
2921 |
|
2922 lemma sup_Inf2_distrib: |
|
2923 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
|
2924 shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}" |
|
2925 using A proof (induct rule: finite_ne_induct) |
|
2926 case singleton thus ?case |
|
2927 by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def]) |
|
2928 next |
|
2929 interpret ab_semigroup_idem_mult inf |
|
2930 by (rule ab_semigroup_idem_mult_inf) |
|
2931 case (insert x A) |
|
2932 have finB: "finite {sup x b |b. b \<in> B}" |
|
2933 by(rule finite_surj[where f = "sup x", OF B(1)], auto) |
|
2934 have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}" |
|
2935 proof - |
|
2936 have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" |
|
2937 by blast |
|
2938 thus ?thesis by(simp add: insert(1) B(1)) |
|
2939 qed |
|
2940 have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
|
2941 have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)" |
|
2942 using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def]) |
|
2943 also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2) |
|
2944 also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})" |
|
2945 using insert by(simp add:sup_Inf1_distrib[OF B]) |
|
2946 also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({sup x b |b. b \<in> B} \<union> {sup a b |a b. a \<in> A \<and> b \<in> B})" |
|
2947 (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M") |
|
2948 using B insert |
|
2949 by (simp add: Inf_fin_def fold1_Un2 [OF finB _ finAB ne]) |
|
2950 also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}" |
|
2951 by blast |
|
2952 finally show ?case . |
|
2953 qed |
|
2954 |
|
2955 lemma inf_Sup1_distrib: |
|
2956 assumes "finite A" and "A \<noteq> {}" |
|
2957 shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}" |
|
2958 proof - |
|
2959 interpret ab_semigroup_idem_mult sup |
|
2960 by (rule ab_semigroup_idem_mult_sup) |
|
2961 from assms show ?thesis |
|
2962 by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1]) |
|
2963 (rule arg_cong [where f="fold1 sup"], blast) |
|
2964 qed |
|
2965 |
|
2966 lemma inf_Sup2_distrib: |
|
2967 assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" |
|
2968 shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}" |
|
2969 using A proof (induct rule: finite_ne_induct) |
|
2970 case singleton thus ?case |
|
2971 by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def]) |
|
2972 next |
|
2973 case (insert x A) |
|
2974 have finB: "finite {inf x b |b. b \<in> B}" |
|
2975 by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto) |
|
2976 have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}" |
|
2977 proof - |
|
2978 have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})" |
|
2979 by blast |
|
2980 thus ?thesis by(simp add: insert(1) B(1)) |
|
2981 qed |
|
2982 have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast |
|
2983 interpret ab_semigroup_idem_mult sup |
|
2984 by (rule ab_semigroup_idem_mult_sup) |
|
2985 have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)" |
|
2986 using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def]) |
|
2987 also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2) |
|
2988 also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})" |
|
2989 using insert by(simp add:inf_Sup1_distrib[OF B]) |
|
2990 also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({inf x b |b. b \<in> B} \<union> {inf a b |a b. a \<in> A \<and> b \<in> B})" |
|
2991 (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M") |
|
2992 using B insert |
|
2993 by (simp add: Sup_fin_def fold1_Un2 [OF finB _ finAB ne]) |
|
2994 also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}" |
|
2995 by blast |
|
2996 finally show ?case . |
|
2997 qed |
|
2998 |
|
2999 end |
|
3000 |
|
3001 |
|
3002 subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *} |
|
3003 |
|
3004 text{* |
|
3005 As an application of @{text fold1} we define minimum |
|
3006 and maximum in (not necessarily complete!) linear orders |
|
3007 over (non-empty) sets by means of @{text fold1}. |
|
3008 *} |
|
3009 |
|
3010 context linorder |
|
3011 begin |
|
3012 |
|
3013 lemma ab_semigroup_idem_mult_min: |
|
3014 "ab_semigroup_idem_mult min" |
|
3015 proof qed (auto simp add: min_def) |
|
3016 |
|
3017 lemma ab_semigroup_idem_mult_max: |
|
3018 "ab_semigroup_idem_mult max" |
|
3019 proof qed (auto simp add: max_def) |
|
3020 |
|
3021 lemma max_lattice: |
|
3022 "semilattice_inf (op \<ge>) (op >) max" |
|
3023 by (fact min_max.dual_semilattice) |
|
3024 |
|
3025 lemma dual_max: |
|
3026 "ord.max (op \<ge>) = min" |
|
3027 by (auto simp add: ord.max_def_raw min_def expand_fun_eq) |
|
3028 |
|
3029 lemma dual_min: |
|
3030 "ord.min (op \<ge>) = max" |
|
3031 by (auto simp add: ord.min_def_raw max_def expand_fun_eq) |
|
3032 |
|
3033 lemma strict_below_fold1_iff: |
|
3034 assumes "finite A" and "A \<noteq> {}" |
|
3035 shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)" |
|
3036 proof - |
|
3037 interpret ab_semigroup_idem_mult min |
|
3038 by (rule ab_semigroup_idem_mult_min) |
|
3039 from assms show ?thesis |
|
3040 by (induct rule: finite_ne_induct) |
|
3041 (simp_all add: fold1_insert) |
|
3042 qed |
|
3043 |
|
3044 lemma fold1_below_iff: |
|
3045 assumes "finite A" and "A \<noteq> {}" |
|
3046 shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)" |
|
3047 proof - |
|
3048 interpret ab_semigroup_idem_mult min |
|
3049 by (rule ab_semigroup_idem_mult_min) |
|
3050 from assms show ?thesis |
|
3051 by (induct rule: finite_ne_induct) |
|
3052 (simp_all add: fold1_insert min_le_iff_disj) |
|
3053 qed |
|
3054 |
|
3055 lemma fold1_strict_below_iff: |
|
3056 assumes "finite A" and "A \<noteq> {}" |
|
3057 shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)" |
|
3058 proof - |
|
3059 interpret ab_semigroup_idem_mult min |
|
3060 by (rule ab_semigroup_idem_mult_min) |
|
3061 from assms show ?thesis |
|
3062 by (induct rule: finite_ne_induct) |
|
3063 (simp_all add: fold1_insert min_less_iff_disj) |
|
3064 qed |
|
3065 |
|
3066 lemma fold1_antimono: |
|
3067 assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B" |
|
3068 shows "fold1 min B \<le> fold1 min A" |
|
3069 proof cases |
|
3070 assume "A = B" thus ?thesis by simp |
|
3071 next |
|
3072 interpret ab_semigroup_idem_mult min |
|
3073 by (rule ab_semigroup_idem_mult_min) |
|
3074 assume "A \<noteq> B" |
|
3075 have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast |
|
3076 have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl) |
|
3077 also have "\<dots> = min (fold1 min A) (fold1 min (B-A))" |
|
3078 proof - |
|
3079 have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`]) |
|
3080 moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *) |
|
3081 moreover have "(B-A) \<noteq> {}" using prems by blast |
|
3082 moreover have "A Int (B-A) = {}" using prems by blast |
|
3083 ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un) |
|
3084 qed |
|
3085 also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj) |
|
3086 finally show ?thesis . |
|
3087 qed |
|
3088 |
|
3089 definition |
|
3090 Min :: "'a set \<Rightarrow> 'a" |
|
3091 where |
|
3092 "Min = fold1 min" |
|
3093 |
|
3094 definition |
|
3095 Max :: "'a set \<Rightarrow> 'a" |
|
3096 where |
|
3097 "Max = fold1 max" |
|
3098 |
|
3099 lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def] |
|
3100 lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def] |
|
3101 |
|
3102 lemma Min_insert [simp]: |
|
3103 assumes "finite A" and "A \<noteq> {}" |
|
3104 shows "Min (insert x A) = min x (Min A)" |
|
3105 proof - |
|
3106 interpret ab_semigroup_idem_mult min |
|
3107 by (rule ab_semigroup_idem_mult_min) |
|
3108 from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def]) |
|
3109 qed |
|
3110 |
|
3111 lemma Max_insert [simp]: |
|
3112 assumes "finite A" and "A \<noteq> {}" |
|
3113 shows "Max (insert x A) = max x (Max A)" |
|
3114 proof - |
|
3115 interpret ab_semigroup_idem_mult max |
|
3116 by (rule ab_semigroup_idem_mult_max) |
|
3117 from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def]) |
|
3118 qed |
|
3119 |
|
3120 lemma Min_in [simp]: |
|
3121 assumes "finite A" and "A \<noteq> {}" |
|
3122 shows "Min A \<in> A" |
|
3123 proof - |
|
3124 interpret ab_semigroup_idem_mult min |
|
3125 by (rule ab_semigroup_idem_mult_min) |
|
3126 from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def) |
|
3127 qed |
|
3128 |
|
3129 lemma Max_in [simp]: |
|
3130 assumes "finite A" and "A \<noteq> {}" |
|
3131 shows "Max A \<in> A" |
|
3132 proof - |
|
3133 interpret ab_semigroup_idem_mult max |
|
3134 by (rule ab_semigroup_idem_mult_max) |
|
3135 from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def) |
|
3136 qed |
|
3137 |
|
3138 lemma Min_Un: |
|
3139 assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}" |
|
3140 shows "Min (A \<union> B) = min (Min A) (Min B)" |
|
3141 proof - |
|
3142 interpret ab_semigroup_idem_mult min |
|
3143 by (rule ab_semigroup_idem_mult_min) |
|
3144 from assms show ?thesis |
|
3145 by (simp add: Min_def fold1_Un2) |
|
3146 qed |
|
3147 |
|
3148 lemma Max_Un: |
|
3149 assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}" |
|
3150 shows "Max (A \<union> B) = max (Max A) (Max B)" |
|
3151 proof - |
|
3152 interpret ab_semigroup_idem_mult max |
|
3153 by (rule ab_semigroup_idem_mult_max) |
|
3154 from assms show ?thesis |
|
3155 by (simp add: Max_def fold1_Un2) |
|
3156 qed |
|
3157 |
|
3158 lemma hom_Min_commute: |
|
3159 assumes "\<And>x y. h (min x y) = min (h x) (h y)" |
|
3160 and "finite N" and "N \<noteq> {}" |
|
3161 shows "h (Min N) = Min (h ` N)" |
|
3162 proof - |
|
3163 interpret ab_semigroup_idem_mult min |
|
3164 by (rule ab_semigroup_idem_mult_min) |
|
3165 from assms show ?thesis |
|
3166 by (simp add: Min_def hom_fold1_commute) |
|
3167 qed |
|
3168 |
|
3169 lemma hom_Max_commute: |
|
3170 assumes "\<And>x y. h (max x y) = max (h x) (h y)" |
|
3171 and "finite N" and "N \<noteq> {}" |
|
3172 shows "h (Max N) = Max (h ` N)" |
|
3173 proof - |
|
3174 interpret ab_semigroup_idem_mult max |
|
3175 by (rule ab_semigroup_idem_mult_max) |
|
3176 from assms show ?thesis |
|
3177 by (simp add: Max_def hom_fold1_commute [of h]) |
|
3178 qed |
|
3179 |
|
3180 lemma Min_le [simp]: |
|
3181 assumes "finite A" and "x \<in> A" |
|
3182 shows "Min A \<le> x" |
|
3183 using assms by (simp add: Min_def min_max.fold1_belowI) |
|
3184 |
|
3185 lemma Max_ge [simp]: |
|
3186 assumes "finite A" and "x \<in> A" |
|
3187 shows "x \<le> Max A" |
|
3188 proof - |
|
3189 interpret semilattice_inf "op \<ge>" "op >" max |
|
3190 by (rule max_lattice) |
|
3191 from assms show ?thesis by (simp add: Max_def fold1_belowI) |
|
3192 qed |
|
3193 |
|
3194 lemma Min_ge_iff [simp, noatp]: |
|
3195 assumes "finite A" and "A \<noteq> {}" |
|
3196 shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" |
|
3197 using assms by (simp add: Min_def min_max.below_fold1_iff) |
|
3198 |
|
3199 lemma Max_le_iff [simp, noatp]: |
|
3200 assumes "finite A" and "A \<noteq> {}" |
|
3201 shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)" |
|
3202 proof - |
|
3203 interpret semilattice_inf "op \<ge>" "op >" max |
|
3204 by (rule max_lattice) |
|
3205 from assms show ?thesis by (simp add: Max_def below_fold1_iff) |
|
3206 qed |
|
3207 |
|
3208 lemma Min_gr_iff [simp, noatp]: |
|
3209 assumes "finite A" and "A \<noteq> {}" |
|
3210 shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)" |
|
3211 using assms by (simp add: Min_def strict_below_fold1_iff) |
|
3212 |
|
3213 lemma Max_less_iff [simp, noatp]: |
|
3214 assumes "finite A" and "A \<noteq> {}" |
|
3215 shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)" |
|
3216 proof - |
|
3217 interpret dual: linorder "op \<ge>" "op >" |
|
3218 by (rule dual_linorder) |
|
3219 from assms show ?thesis |
|
3220 by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max]) |
|
3221 qed |
|
3222 |
|
3223 lemma Min_le_iff [noatp]: |
|
3224 assumes "finite A" and "A \<noteq> {}" |
|
3225 shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)" |
|
3226 using assms by (simp add: Min_def fold1_below_iff) |
|
3227 |
|
3228 lemma Max_ge_iff [noatp]: |
|
3229 assumes "finite A" and "A \<noteq> {}" |
|
3230 shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)" |
|
3231 proof - |
|
3232 interpret dual: linorder "op \<ge>" "op >" |
|
3233 by (rule dual_linorder) |
|
3234 from assms show ?thesis |
|
3235 by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max]) |
|
3236 qed |
|
3237 |
|
3238 lemma Min_less_iff [noatp]: |
|
3239 assumes "finite A" and "A \<noteq> {}" |
|
3240 shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)" |
|
3241 using assms by (simp add: Min_def fold1_strict_below_iff) |
|
3242 |
|
3243 lemma Max_gr_iff [noatp]: |
|
3244 assumes "finite A" and "A \<noteq> {}" |
|
3245 shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)" |
|
3246 proof - |
|
3247 interpret dual: linorder "op \<ge>" "op >" |
|
3248 by (rule dual_linorder) |
|
3249 from assms show ?thesis |
|
3250 by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max]) |
|
3251 qed |
|
3252 |
|
3253 lemma Min_eqI: |
|
3254 assumes "finite A" |
|
3255 assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x" |
|
3256 and "x \<in> A" |
|
3257 shows "Min A = x" |
|
3258 proof (rule antisym) |
|
3259 from `x \<in> A` have "A \<noteq> {}" by auto |
|
3260 with assms show "Min A \<ge> x" by simp |
|
3261 next |
|
3262 from assms show "x \<ge> Min A" by simp |
|
3263 qed |
|
3264 |
|
3265 lemma Max_eqI: |
|
3266 assumes "finite A" |
|
3267 assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" |
|
3268 and "x \<in> A" |
|
3269 shows "Max A = x" |
|
3270 proof (rule antisym) |
|
3271 from `x \<in> A` have "A \<noteq> {}" by auto |
|
3272 with assms show "Max A \<le> x" by simp |
|
3273 next |
|
3274 from assms show "x \<le> Max A" by simp |
|
3275 qed |
|
3276 |
|
3277 lemma Min_antimono: |
|
3278 assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" |
|
3279 shows "Min N \<le> Min M" |
|
3280 using assms by (simp add: Min_def fold1_antimono) |
|
3281 |
|
3282 lemma Max_mono: |
|
3283 assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" |
|
3284 shows "Max M \<le> Max N" |
|
3285 proof - |
|
3286 interpret dual: linorder "op \<ge>" "op >" |
|
3287 by (rule dual_linorder) |
|
3288 from assms show ?thesis |
|
3289 by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max]) |
|
3290 qed |
|
3291 |
|
3292 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]: |
|
3293 "finite A \<Longrightarrow> P {} \<Longrightarrow> |
|
3294 (!!b A. finite A \<Longrightarrow> ALL a:A. a < b \<Longrightarrow> P A \<Longrightarrow> P(insert b A)) |
|
3295 \<Longrightarrow> P A" |
|
3296 proof (induct rule: finite_psubset_induct) |
|
3297 fix A :: "'a set" |
|
3298 assume IH: "!! B. finite B \<Longrightarrow> B < A \<Longrightarrow> P {} \<Longrightarrow> |
|
3299 (!!b A. finite A \<Longrightarrow> (\<forall>a\<in>A. a<b) \<Longrightarrow> P A \<Longrightarrow> P (insert b A)) |
|
3300 \<Longrightarrow> P B" |
|
3301 and "finite A" and "P {}" |
|
3302 and step: "!!b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" |
|
3303 show "P A" |
|
3304 proof (cases "A = {}") |
|
3305 assume "A = {}" thus "P A" using `P {}` by simp |
|
3306 next |
|
3307 let ?B = "A - {Max A}" let ?A = "insert (Max A) ?B" |
|
3308 assume "A \<noteq> {}" |
|
3309 with `finite A` have "Max A : A" by auto |
|
3310 hence A: "?A = A" using insert_Diff_single insert_absorb by auto |
|
3311 moreover have "finite ?B" using `finite A` by simp |
|
3312 ultimately have "P ?B" using `P {}` step IH[of ?B] by blast |
|
3313 moreover have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastsimp |
|
3314 ultimately show "P A" using A insert_Diff_single step[OF `finite ?B`] by fastsimp |
|
3315 qed |
|
3316 qed |
|
3317 |
|
3318 lemma finite_linorder_min_induct[consumes 1, case_names empty insert]: |
|
3319 "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A" |
|
3320 by(rule linorder.finite_linorder_max_induct[OF dual_linorder]) |
|
3321 |
|
3322 end |
|
3323 |
|
3324 context linordered_ab_semigroup_add |
|
3325 begin |
|
3326 |
|
3327 lemma add_Min_commute: |
|
3328 fixes k |
|
3329 assumes "finite N" and "N \<noteq> {}" |
|
3330 shows "k + Min N = Min {k + m | m. m \<in> N}" |
|
3331 proof - |
|
3332 have "\<And>x y. k + min x y = min (k + x) (k + y)" |
|
3333 by (simp add: min_def not_le) |
|
3334 (blast intro: antisym less_imp_le add_left_mono) |
|
3335 with assms show ?thesis |
|
3336 using hom_Min_commute [of "plus k" N] |
|
3337 by simp (blast intro: arg_cong [where f = Min]) |
|
3338 qed |
|
3339 |
|
3340 lemma add_Max_commute: |
|
3341 fixes k |
|
3342 assumes "finite N" and "N \<noteq> {}" |
|
3343 shows "k + Max N = Max {k + m | m. m \<in> N}" |
|
3344 proof - |
|
3345 have "\<And>x y. k + max x y = max (k + x) (k + y)" |
|
3346 by (simp add: max_def not_le) |
|
3347 (blast intro: antisym less_imp_le add_left_mono) |
|
3348 with assms show ?thesis |
|
3349 using hom_Max_commute [of "plus k" N] |
|
3350 by simp (blast intro: arg_cong [where f = Max]) |
|
3351 qed |
|
3352 |
|
3353 end |
|
3354 |
|
3355 context linordered_ab_group_add |
|
3356 begin |
|
3357 |
|
3358 lemma minus_Max_eq_Min [simp]: |
|
3359 "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)" |
|
3360 by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min) |
|
3361 |
|
3362 lemma minus_Min_eq_Max [simp]: |
|
3363 "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)" |
|
3364 by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max) |
|
3365 |
|
3366 end |
|
3367 |
|
3368 |
|
3369 subsection {* Expressing set operations via @{const fold} *} |
1357 subsection {* Expressing set operations via @{const fold} *} |
3370 |
1358 |
3371 lemma (in fun_left_comm) fun_left_comm_apply: |
1359 lemma (in fun_left_comm) fun_left_comm_apply: |
3372 "fun_left_comm (\<lambda>x. f (g x))" |
1360 "fun_left_comm (\<lambda>x. f (g x))" |
3373 proof |
1361 proof |