1(* Title: ZF/equalities.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4*) 5 6section\<open>Basic Equalities and Inclusions\<close> 7 8theory equalities imports pair begin 9 10text\<open>These cover union, intersection, converse, domain, range, etc. Philippe 11de Groote proved many of the inclusions.\<close> 12 13lemma in_mono: "A\<subseteq>B ==> x\<in>A \<longrightarrow> x\<in>B" 14by blast 15 16lemma the_eq_0 [simp]: "(THE x. False) = 0" 17by (blast intro: the_0) 18 19subsection\<open>Bounded Quantifiers\<close> 20text \<open>\medskip 21 22 The following are not added to the default simpset because 23 (a) they duplicate the body and (b) there are no similar rules for \<open>Int\<close>.\<close> 24 25lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))" 26 by blast 27 28lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))" 29 by blast 30 31lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))" 32 by blast 33 34lemma bex_UN: "(\<exists>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>z\<in>B(x). P(z))" 35 by blast 36 37subsection\<open>Converse of a Relation\<close> 38 39lemma converse_iff [simp]: "<a,b>\<in> converse(r) \<longleftrightarrow> <b,a>\<in>r" 40by (unfold converse_def, blast) 41 42lemma converseI [intro!]: "<a,b>\<in>r ==> <b,a>\<in>converse(r)" 43by (unfold converse_def, blast) 44 45lemma converseD: "<a,b> \<in> converse(r) ==> <b,a> \<in> r" 46by (unfold converse_def, blast) 47 48lemma converseE [elim!]: 49 "[| yx \<in> converse(r); 50 !!x y. [| yx=<y,x>; <x,y>\<in>r |] ==> P |] 51 ==> P" 52by (unfold converse_def, blast) 53 54lemma converse_converse: "r\<subseteq>Sigma(A,B) ==> converse(converse(r)) = r" 55by blast 56 57lemma converse_type: "r\<subseteq>A*B ==> converse(r)\<subseteq>B*A" 58by blast 59 60lemma converse_prod [simp]: "converse(A*B) = B*A" 61by blast 62 63lemma converse_empty [simp]: "converse(0) = 0" 64by blast 65 66lemma converse_subset_iff: 67 "A \<subseteq> Sigma(X,Y) ==> converse(A) \<subseteq> converse(B) \<longleftrightarrow> A \<subseteq> B" 68by blast 69 70 71subsection\<open>Finite Set Constructions Using \<^term>\<open>cons\<close>\<close> 72 73lemma cons_subsetI: "[| a\<in>C; B\<subseteq>C |] ==> cons(a,B) \<subseteq> C" 74by blast 75 76lemma subset_consI: "B \<subseteq> cons(a,B)" 77by blast 78 79lemma cons_subset_iff [iff]: "cons(a,B)\<subseteq>C \<longleftrightarrow> a\<in>C & B\<subseteq>C" 80by blast 81 82(*A safe special case of subset elimination, adding no new variables 83 [| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *) 84lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE] 85 86lemma subset_empty_iff: "A\<subseteq>0 \<longleftrightarrow> A=0" 87by blast 88 89lemma subset_cons_iff: "C\<subseteq>cons(a,B) \<longleftrightarrow> C\<subseteq>B | (a\<in>C & C-{a} \<subseteq> B)" 90by blast 91 92(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) 93lemma cons_eq: "{a} \<union> B = cons(a,B)" 94by blast 95 96lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))" 97by blast 98 99lemma cons_absorb: "a: B ==> cons(a,B) = B" 100by blast 101 102lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B" 103by blast 104 105lemma Diff_cons_eq: "cons(a,B) - C = (if a\<in>C then B-C else cons(a,B-C))" 106by auto 107 108lemma equal_singleton: "[| a: C; \<And>y. y \<in>C \<Longrightarrow> y=b |] ==> C = {b}" 109by blast 110 111lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)" 112by blast 113 114(** singletons **) 115 116lemma singleton_subsetI: "a\<in>C ==> {a} \<subseteq> C" 117by blast 118 119lemma singleton_subsetD: "{a} \<subseteq> C ==> a\<in>C" 120by blast 121 122 123(** succ **) 124 125lemma subset_succI: "i \<subseteq> succ(i)" 126by blast 127 128(*But if j is an ordinal or is transitive, then @{term"i\<in>j"} implies @{term"i\<subseteq>j"}! 129 See @{text"Ord_succ_subsetI}*) 130lemma succ_subsetI: "[| i\<in>j; i\<subseteq>j |] ==> succ(i)\<subseteq>j" 131by (unfold succ_def, blast) 132 133lemma succ_subsetE: 134 "[| succ(i) \<subseteq> j; [| i\<in>j; i\<subseteq>j |] ==> P |] ==> P" 135by (unfold succ_def, blast) 136 137lemma succ_subset_iff: "succ(a) \<subseteq> B \<longleftrightarrow> (a \<subseteq> B & a \<in> B)" 138by (unfold succ_def, blast) 139 140 141subsection\<open>Binary Intersection\<close> 142 143(** Intersection is the greatest lower bound of two sets **) 144 145lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A & C \<subseteq> B" 146by blast 147 148lemma Int_lower1: "A \<inter> B \<subseteq> A" 149by blast 150 151lemma Int_lower2: "A \<inter> B \<subseteq> B" 152by blast 153 154lemma Int_greatest: "[| C\<subseteq>A; C\<subseteq>B |] ==> C \<subseteq> A \<inter> B" 155by blast 156 157lemma Int_cons: "cons(a,B) \<inter> C \<subseteq> cons(a, B \<inter> C)" 158by blast 159 160lemma Int_absorb [simp]: "A \<inter> A = A" 161by blast 162 163lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B" 164by blast 165 166lemma Int_commute: "A \<inter> B = B \<inter> A" 167by blast 168 169lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)" 170by blast 171 172lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)" 173by blast 174 175(*Intersection is an AC-operator*) 176lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute 177 178lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B" 179 by blast 180 181lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A" 182 by blast 183 184lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)" 185by blast 186 187lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)" 188by blast 189 190lemma subset_Int_iff: "A\<subseteq>B \<longleftrightarrow> A \<inter> B = A" 191by (blast elim!: equalityE) 192 193lemma subset_Int_iff2: "A\<subseteq>B \<longleftrightarrow> B \<inter> A = A" 194by (blast elim!: equalityE) 195 196lemma Int_Diff_eq: "C\<subseteq>A ==> (A-B) \<inter> C = C-B" 197by blast 198 199lemma Int_cons_left: 200 "cons(a,A) \<inter> B = (if a \<in> B then cons(a, A \<inter> B) else A \<inter> B)" 201by auto 202 203lemma Int_cons_right: 204 "A \<inter> cons(a, B) = (if a \<in> A then cons(a, A \<inter> B) else A \<inter> B)" 205by auto 206 207lemma cons_Int_distrib: "cons(x, A \<inter> B) = cons(x, A) \<inter> cons(x, B)" 208by auto 209 210subsection\<open>Binary Union\<close> 211 212(** Union is the least upper bound of two sets *) 213 214lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C & B \<subseteq> C" 215by blast 216 217lemma Un_upper1: "A \<subseteq> A \<union> B" 218by blast 219 220lemma Un_upper2: "B \<subseteq> A \<union> B" 221by blast 222 223lemma Un_least: "[| A\<subseteq>C; B\<subseteq>C |] ==> A \<union> B \<subseteq> C" 224by blast 225 226lemma Un_cons: "cons(a,B) \<union> C = cons(a, B \<union> C)" 227by blast 228 229lemma Un_absorb [simp]: "A \<union> A = A" 230by blast 231 232lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B" 233by blast 234 235lemma Un_commute: "A \<union> B = B \<union> A" 236by blast 237 238lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)" 239by blast 240 241lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)" 242by blast 243 244(*Union is an AC-operator*) 245lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute 246 247lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B" 248 by blast 249 250lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A" 251 by blast 252 253lemma Un_Int_distrib: "(A \<inter> B) \<union> C = (A \<union> C) \<inter> (B \<union> C)" 254by blast 255 256lemma subset_Un_iff: "A\<subseteq>B \<longleftrightarrow> A \<union> B = B" 257by (blast elim!: equalityE) 258 259lemma subset_Un_iff2: "A\<subseteq>B \<longleftrightarrow> B \<union> A = B" 260by (blast elim!: equalityE) 261 262lemma Un_empty [iff]: "(A \<union> B = 0) \<longleftrightarrow> (A = 0 & B = 0)" 263by blast 264 265lemma Un_eq_Union: "A \<union> B = \<Union>({A, B})" 266by blast 267 268subsection\<open>Set Difference\<close> 269 270lemma Diff_subset: "A-B \<subseteq> A" 271by blast 272 273lemma Diff_contains: "[| C\<subseteq>A; C \<inter> B = 0 |] ==> C \<subseteq> A-B" 274by blast 275 276lemma subset_Diff_cons_iff: "B \<subseteq> A - cons(c,C) \<longleftrightarrow> B\<subseteq>A-C & c \<notin> B" 277by blast 278 279lemma Diff_cancel: "A - A = 0" 280by blast 281 282lemma Diff_triv: "A \<inter> B = 0 ==> A - B = A" 283by blast 284 285lemma empty_Diff [simp]: "0 - A = 0" 286by blast 287 288lemma Diff_0 [simp]: "A - 0 = A" 289by blast 290 291lemma Diff_eq_0_iff: "A - B = 0 \<longleftrightarrow> A \<subseteq> B" 292by (blast elim: equalityE) 293 294(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) 295lemma Diff_cons: "A - cons(a,B) = A - B - {a}" 296by blast 297 298(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) 299lemma Diff_cons2: "A - cons(a,B) = A - {a} - B" 300by blast 301 302lemma Diff_disjoint: "A \<inter> (B-A) = 0" 303by blast 304 305lemma Diff_partition: "A\<subseteq>B ==> A \<union> (B-A) = B" 306by blast 307 308lemma subset_Un_Diff: "A \<subseteq> B \<union> (A - B)" 309by blast 310 311lemma double_complement: "[| A\<subseteq>B; B\<subseteq>C |] ==> B-(C-A) = A" 312by blast 313 314lemma double_complement_Un: "(A \<union> B) - (B-A) = A" 315by blast 316 317lemma Un_Int_crazy: 318 "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)" 319apply blast 320done 321 322lemma Diff_Un: "A - (B \<union> C) = (A-B) \<inter> (A-C)" 323by blast 324 325lemma Diff_Int: "A - (B \<inter> C) = (A-B) \<union> (A-C)" 326by blast 327 328lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)" 329by blast 330 331lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)" 332by blast 333 334lemma Diff_Int_distrib: "C \<inter> (A-B) = (C \<inter> A) - (C \<inter> B)" 335by blast 336 337lemma Diff_Int_distrib2: "(A-B) \<inter> C = (A \<inter> C) - (B \<inter> C)" 338by blast 339 340(*Halmos, Naive Set Theory, page 16.*) 341lemma Un_Int_assoc_iff: "(A \<inter> B) \<union> C = A \<inter> (B \<union> C) \<longleftrightarrow> C\<subseteq>A" 342by (blast elim!: equalityE) 343 344 345subsection\<open>Big Union and Intersection\<close> 346 347(** Big Union is the least upper bound of a set **) 348 349lemma Union_subset_iff: "\<Union>(A) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. x \<subseteq> C)" 350by blast 351 352lemma Union_upper: "B\<in>A ==> B \<subseteq> \<Union>(A)" 353by blast 354 355lemma Union_least: "[| !!x. x\<in>A ==> x\<subseteq>C |] ==> \<Union>(A) \<subseteq> C" 356by blast 357 358lemma Union_cons [simp]: "\<Union>(cons(a,B)) = a \<union> \<Union>(B)" 359by blast 360 361lemma Union_Un_distrib: "\<Union>(A \<union> B) = \<Union>(A) \<union> \<Union>(B)" 362by blast 363 364lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>(A) \<inter> \<Union>(B)" 365by blast 366 367lemma Union_disjoint: "\<Union>(C) \<inter> A = 0 \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = 0)" 368by (blast elim!: equalityE) 369 370lemma Union_empty_iff: "\<Union>(A) = 0 \<longleftrightarrow> (\<forall>B\<in>A. B=0)" 371by blast 372 373lemma Int_Union2: "\<Union>(B) \<inter> A = (\<Union>C\<in>B. C \<inter> A)" 374by blast 375 376(** Big Intersection is the greatest lower bound of a nonempty set **) 377 378lemma Inter_subset_iff: "A\<noteq>0 ==> C \<subseteq> \<Inter>(A) \<longleftrightarrow> (\<forall>x\<in>A. C \<subseteq> x)" 379by blast 380 381lemma Inter_lower: "B\<in>A ==> \<Inter>(A) \<subseteq> B" 382by blast 383 384lemma Inter_greatest: "[| A\<noteq>0; !!x. x\<in>A ==> C\<subseteq>x |] ==> C \<subseteq> \<Inter>(A)" 385by blast 386 387(** Intersection of a family of sets **) 388 389lemma INT_lower: "x\<in>A ==> (\<Inter>x\<in>A. B(x)) \<subseteq> B(x)" 390by blast 391 392lemma INT_greatest: "[| A\<noteq>0; !!x. x\<in>A ==> C\<subseteq>B(x) |] ==> C \<subseteq> (\<Inter>x\<in>A. B(x))" 393by force 394 395lemma Inter_0 [simp]: "\<Inter>(0) = 0" 396by (unfold Inter_def, blast) 397 398lemma Inter_Un_subset: 399 "[| z\<in>A; z\<in>B |] ==> \<Inter>(A) \<union> \<Inter>(B) \<subseteq> \<Inter>(A \<inter> B)" 400by blast 401 402(* A good challenge: Inter is ill-behaved on the empty set *) 403lemma Inter_Un_distrib: 404 "[| A\<noteq>0; B\<noteq>0 |] ==> \<Inter>(A \<union> B) = \<Inter>(A) \<inter> \<Inter>(B)" 405by blast 406 407lemma Union_singleton: "\<Union>({b}) = b" 408by blast 409 410lemma Inter_singleton: "\<Inter>({b}) = b" 411by blast 412 413lemma Inter_cons [simp]: 414 "\<Inter>(cons(a,B)) = (if B=0 then a else a \<inter> \<Inter>(B))" 415by force 416 417subsection\<open>Unions and Intersections of Families\<close> 418 419lemma subset_UN_iff_eq: "A \<subseteq> (\<Union>i\<in>I. B(i)) \<longleftrightarrow> A = (\<Union>i\<in>I. A \<inter> B(i))" 420by (blast elim!: equalityE) 421 422lemma UN_subset_iff: "(\<Union>x\<in>A. B(x)) \<subseteq> C \<longleftrightarrow> (\<forall>x\<in>A. B(x) \<subseteq> C)" 423by blast 424 425lemma UN_upper: "x\<in>A ==> B(x) \<subseteq> (\<Union>x\<in>A. B(x))" 426by (erule RepFunI [THEN Union_upper]) 427 428lemma UN_least: "[| !!x. x\<in>A ==> B(x)\<subseteq>C |] ==> (\<Union>x\<in>A. B(x)) \<subseteq> C" 429by blast 430 431lemma Union_eq_UN: "\<Union>(A) = (\<Union>x\<in>A. x)" 432by blast 433 434lemma Inter_eq_INT: "\<Inter>(A) = (\<Inter>x\<in>A. x)" 435by (unfold Inter_def, blast) 436 437lemma UN_0 [simp]: "(\<Union>i\<in>0. A(i)) = 0" 438by blast 439 440lemma UN_singleton: "(\<Union>x\<in>A. {x}) = A" 441by blast 442 443lemma UN_Un: "(\<Union>i\<in> A \<union> B. C(i)) = (\<Union>i\<in> A. C(i)) \<union> (\<Union>i\<in>B. C(i))" 444by blast 445 446lemma INT_Un: "(\<Inter>i\<in>I \<union> J. A(i)) = 447 (if I=0 then \<Inter>j\<in>J. A(j) 448 else if J=0 then \<Inter>i\<in>I. A(i) 449 else ((\<Inter>i\<in>I. A(i)) \<inter> (\<Inter>j\<in>J. A(j))))" 450by (simp, blast intro!: equalityI) 451 452lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B(y)). C(x)) = (\<Union>y\<in>A. \<Union>x\<in> B(y). C(x))" 453by blast 454 455(*Halmos, Naive Set Theory, page 35.*) 456lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A(i)) = (\<Union>i\<in>I. B \<inter> A(i))" 457by blast 458 459lemma Un_INT_distrib: "I\<noteq>0 ==> B \<union> (\<Inter>i\<in>I. A(i)) = (\<Inter>i\<in>I. B \<union> A(i))" 460by auto 461 462lemma Int_UN_distrib2: 463 "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) = (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))" 464by blast 465 466lemma Un_INT_distrib2: "[| I\<noteq>0; J\<noteq>0 |] ==> 467 (\<Inter>i\<in>I. A(i)) \<union> (\<Inter>j\<in>J. B(j)) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A(i) \<union> B(j))" 468by auto 469 470lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A=0 then 0 else c)" 471by force 472 473lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A=0 then 0 else c)" 474by force 475 476lemma UN_RepFun [simp]: "(\<Union>y\<in> RepFun(A,f). B(y)) = (\<Union>x\<in>A. B(f(x)))" 477by blast 478 479lemma INT_RepFun [simp]: "(\<Inter>x\<in>RepFun(A,f). B(x)) = (\<Inter>a\<in>A. B(f(a)))" 480by (auto simp add: Inter_def) 481 482lemma INT_Union_eq: 483 "0 \<notin> A ==> (\<Inter>x\<in> \<Union>(A). B(x)) = (\<Inter>y\<in>A. \<Inter>x\<in>y. B(x))" 484apply (subgoal_tac "\<forall>x\<in>A. x\<noteq>0") 485 prefer 2 apply blast 486apply (force simp add: Inter_def ball_conj_distrib) 487done 488 489lemma INT_UN_eq: 490 "(\<forall>x\<in>A. B(x) \<noteq> 0) 491 ==> (\<Inter>z\<in> (\<Union>x\<in>A. B(x)). C(z)) = (\<Inter>x\<in>A. \<Inter>z\<in> B(x). C(z))" 492apply (subst INT_Union_eq, blast) 493apply (simp add: Inter_def) 494done 495 496 497(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 498 Union of a family of unions **) 499 500lemma UN_Un_distrib: 501 "(\<Union>i\<in>I. A(i) \<union> B(i)) = (\<Union>i\<in>I. A(i)) \<union> (\<Union>i\<in>I. B(i))" 502by blast 503 504lemma INT_Int_distrib: 505 "I\<noteq>0 ==> (\<Inter>i\<in>I. A(i) \<inter> B(i)) = (\<Inter>i\<in>I. A(i)) \<inter> (\<Inter>i\<in>I. B(i))" 506by (blast elim!: not_emptyE) 507 508lemma UN_Int_subset: 509 "(\<Union>z\<in>I \<inter> J. A(z)) \<subseteq> (\<Union>z\<in>I. A(z)) \<inter> (\<Union>z\<in>J. A(z))" 510by blast 511 512(** Devlin, page 12, exercise 5: Complements **) 513 514lemma Diff_UN: "I\<noteq>0 ==> B - (\<Union>i\<in>I. A(i)) = (\<Inter>i\<in>I. B - A(i))" 515by (blast elim!: not_emptyE) 516 517lemma Diff_INT: "I\<noteq>0 ==> B - (\<Inter>i\<in>I. A(i)) = (\<Union>i\<in>I. B - A(i))" 518by (blast elim!: not_emptyE) 519 520 521(** Unions and Intersections with General Sum **) 522 523(*Not suitable for rewriting: LOOPS!*) 524lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) \<union> Sigma(B,C)" 525by blast 526 527(*Not suitable for rewriting: LOOPS!*) 528lemma Sigma_cons2: "A * cons(b,B) = A*{b} \<union> A*B" 529by blast 530 531lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) \<union> Sigma(A,B)" 532by blast 533 534lemma Sigma_succ2: "A * succ(B) = A*{B} \<union> A*B" 535by blast 536 537lemma SUM_UN_distrib1: 538 "(\<Sum>x \<in> (\<Union>y\<in>A. C(y)). B(x)) = (\<Union>y\<in>A. \<Sum>x\<in>C(y). B(x))" 539by blast 540 541lemma SUM_UN_distrib2: 542 "(\<Sum>i\<in>I. \<Union>j\<in>J. C(i,j)) = (\<Union>j\<in>J. \<Sum>i\<in>I. C(i,j))" 543by blast 544 545lemma SUM_Un_distrib1: 546 "(\<Sum>i\<in>I \<union> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<union> (\<Sum>j\<in>J. C(j))" 547by blast 548 549lemma SUM_Un_distrib2: 550 "(\<Sum>i\<in>I. A(i) \<union> B(i)) = (\<Sum>i\<in>I. A(i)) \<union> (\<Sum>i\<in>I. B(i))" 551by blast 552 553(*First-order version of the above, for rewriting*) 554lemma prod_Un_distrib2: "I * (A \<union> B) = I*A \<union> I*B" 555by (rule SUM_Un_distrib2) 556 557lemma SUM_Int_distrib1: 558 "(\<Sum>i\<in>I \<inter> J. C(i)) = (\<Sum>i\<in>I. C(i)) \<inter> (\<Sum>j\<in>J. C(j))" 559by blast 560 561lemma SUM_Int_distrib2: 562 "(\<Sum>i\<in>I. A(i) \<inter> B(i)) = (\<Sum>i\<in>I. A(i)) \<inter> (\<Sum>i\<in>I. B(i))" 563by blast 564 565(*First-order version of the above, for rewriting*) 566lemma prod_Int_distrib2: "I * (A \<inter> B) = I*A \<inter> I*B" 567by (rule SUM_Int_distrib2) 568 569(*Cf Aczel, Non-Well-Founded Sets, page 115*) 570lemma SUM_eq_UN: "(\<Sum>i\<in>I. A(i)) = (\<Union>i\<in>I. {i} * A(i))" 571by blast 572 573lemma times_subset_iff: 574 "(A'*B' \<subseteq> A*B) \<longleftrightarrow> (A' = 0 | B' = 0 | (A'\<subseteq>A) & (B'\<subseteq>B))" 575by blast 576 577lemma Int_Sigma_eq: 578 "(\<Sum>x \<in> A'. B'(x)) \<inter> (\<Sum>x \<in> A. B(x)) = (\<Sum>x \<in> A' \<inter> A. B'(x) \<inter> B(x))" 579by blast 580 581(** Domain **) 582 583lemma domain_iff: "a: domain(r) \<longleftrightarrow> (\<exists>y. <a,y>\<in> r)" 584by (unfold domain_def, blast) 585 586lemma domainI [intro]: "<a,b>\<in> r ==> a: domain(r)" 587by (unfold domain_def, blast) 588 589lemma domainE [elim!]: 590 "[| a \<in> domain(r); !!y. <a,y>\<in> r ==> P |] ==> P" 591by (unfold domain_def, blast) 592 593lemma domain_subset: "domain(Sigma(A,B)) \<subseteq> A" 594by blast 595 596lemma domain_of_prod: "b\<in>B ==> domain(A*B) = A" 597by blast 598 599lemma domain_0 [simp]: "domain(0) = 0" 600by blast 601 602lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))" 603by blast 604 605lemma domain_Un_eq [simp]: "domain(A \<union> B) = domain(A) \<union> domain(B)" 606by blast 607 608lemma domain_Int_subset: "domain(A \<inter> B) \<subseteq> domain(A) \<inter> domain(B)" 609by blast 610 611lemma domain_Diff_subset: "domain(A) - domain(B) \<subseteq> domain(A - B)" 612by blast 613 614lemma domain_UN: "domain(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. domain(B(x)))" 615by blast 616 617lemma domain_Union: "domain(\<Union>(A)) = (\<Union>x\<in>A. domain(x))" 618by blast 619 620 621(** Range **) 622 623lemma rangeI [intro]: "<a,b>\<in> r ==> b \<in> range(r)" 624apply (unfold range_def) 625apply (erule converseI [THEN domainI]) 626done 627 628lemma rangeE [elim!]: "[| b \<in> range(r); !!x. <x,b>\<in> r ==> P |] ==> P" 629by (unfold range_def, blast) 630 631lemma range_subset: "range(A*B) \<subseteq> B" 632apply (unfold range_def) 633apply (subst converse_prod) 634apply (rule domain_subset) 635done 636 637lemma range_of_prod: "a\<in>A ==> range(A*B) = B" 638by blast 639 640lemma range_0 [simp]: "range(0) = 0" 641by blast 642 643lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))" 644by blast 645 646lemma range_Un_eq [simp]: "range(A \<union> B) = range(A) \<union> range(B)" 647by blast 648 649lemma range_Int_subset: "range(A \<inter> B) \<subseteq> range(A) \<inter> range(B)" 650by blast 651 652lemma range_Diff_subset: "range(A) - range(B) \<subseteq> range(A - B)" 653by blast 654 655lemma domain_converse [simp]: "domain(converse(r)) = range(r)" 656by blast 657 658lemma range_converse [simp]: "range(converse(r)) = domain(r)" 659by blast 660 661 662(** Field **) 663 664lemma fieldI1: "<a,b>\<in> r ==> a \<in> field(r)" 665by (unfold field_def, blast) 666 667lemma fieldI2: "<a,b>\<in> r ==> b \<in> field(r)" 668by (unfold field_def, blast) 669 670lemma fieldCI [intro]: 671 "(~ <c,a>\<in>r ==> <a,b>\<in> r) ==> a \<in> field(r)" 672apply (unfold field_def, blast) 673done 674 675lemma fieldE [elim!]: 676 "[| a \<in> field(r); 677 !!x. <a,x>\<in> r ==> P; 678 !!x. <x,a>\<in> r ==> P |] ==> P" 679by (unfold field_def, blast) 680 681lemma field_subset: "field(A*B) \<subseteq> A \<union> B" 682by blast 683 684lemma domain_subset_field: "domain(r) \<subseteq> field(r)" 685apply (unfold field_def) 686apply (rule Un_upper1) 687done 688 689lemma range_subset_field: "range(r) \<subseteq> field(r)" 690apply (unfold field_def) 691apply (rule Un_upper2) 692done 693 694lemma domain_times_range: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> domain(r)*range(r)" 695by blast 696 697lemma field_times_field: "r \<subseteq> Sigma(A,B) ==> r \<subseteq> field(r)*field(r)" 698by blast 699 700lemma relation_field_times_field: "relation(r) ==> r \<subseteq> field(r)*field(r)" 701by (simp add: relation_def, blast) 702 703lemma field_of_prod: "field(A*A) = A" 704by blast 705 706lemma field_0 [simp]: "field(0) = 0" 707by blast 708 709lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))" 710by blast 711 712lemma field_Un_eq [simp]: "field(A \<union> B) = field(A) \<union> field(B)" 713by blast 714 715lemma field_Int_subset: "field(A \<inter> B) \<subseteq> field(A) \<inter> field(B)" 716by blast 717 718lemma field_Diff_subset: "field(A) - field(B) \<subseteq> field(A - B)" 719by blast 720 721lemma field_converse [simp]: "field(converse(r)) = field(r)" 722by blast 723 724(** The Union of a set of relations is a relation -- Lemma for fun_Union **) 725lemma rel_Union: "(\<forall>x\<in>S. \<exists>A B. x \<subseteq> A*B) ==> 726 \<Union>(S) \<subseteq> domain(\<Union>(S)) * range(\<Union>(S))" 727by blast 728 729(** The Union of 2 relations is a relation (Lemma for fun_Un) **) 730lemma rel_Un: "[| r \<subseteq> A*B; s \<subseteq> C*D |] ==> (r \<union> s) \<subseteq> (A \<union> C) * (B \<union> D)" 731by blast 732 733lemma domain_Diff_eq: "[| <a,c> \<in> r; c\<noteq>b |] ==> domain(r-{<a,b>}) = domain(r)" 734by blast 735 736lemma range_Diff_eq: "[| <c,b> \<in> r; c\<noteq>a |] ==> range(r-{<a,b>}) = range(r)" 737by blast 738 739 740subsection\<open>Image of a Set under a Function or Relation\<close> 741 742lemma image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. <x,b>\<in>r)" 743by (unfold image_def, blast) 744 745lemma image_singleton_iff: "b \<in> r``{a} \<longleftrightarrow> <a,b>\<in>r" 746by (rule image_iff [THEN iff_trans], blast) 747 748lemma imageI [intro]: "[| <a,b>\<in> r; a\<in>A |] ==> b \<in> r``A" 749by (unfold image_def, blast) 750 751lemma imageE [elim!]: 752 "[| b: r``A; !!x.[| <x,b>\<in> r; x\<in>A |] ==> P |] ==> P" 753by (unfold image_def, blast) 754 755lemma image_subset: "r \<subseteq> A*B ==> r``C \<subseteq> B" 756by blast 757 758lemma image_0 [simp]: "r``0 = 0" 759by blast 760 761lemma image_Un [simp]: "r``(A \<union> B) = (r``A) \<union> (r``B)" 762by blast 763 764lemma image_UN: "r `` (\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. r `` B(x))" 765by blast 766 767lemma Collect_image_eq: 768 "{z \<in> Sigma(A,B). P(z)} `` C = (\<Union>x \<in> A. {y \<in> B(x). x \<in> C & P(<x,y>)})" 769by blast 770 771lemma image_Int_subset: "r``(A \<inter> B) \<subseteq> (r``A) \<inter> (r``B)" 772by blast 773 774lemma image_Int_square_subset: "(r \<inter> A*A)``B \<subseteq> (r``B) \<inter> A" 775by blast 776 777lemma image_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)``B = (r``B) \<inter> A" 778by blast 779 780 781(*Image laws for special relations*) 782lemma image_0_left [simp]: "0``A = 0" 783by blast 784 785lemma image_Un_left: "(r \<union> s)``A = (r``A) \<union> (s``A)" 786by blast 787 788lemma image_Int_subset_left: "(r \<inter> s)``A \<subseteq> (r``A) \<inter> (s``A)" 789by blast 790 791 792subsection\<open>Inverse Image of a Set under a Function or Relation\<close> 793 794lemma vimage_iff: 795 "a \<in> r-``B \<longleftrightarrow> (\<exists>y\<in>B. <a,y>\<in>r)" 796by (unfold vimage_def image_def converse_def, blast) 797 798lemma vimage_singleton_iff: "a \<in> r-``{b} \<longleftrightarrow> <a,b>\<in>r" 799by (rule vimage_iff [THEN iff_trans], blast) 800 801lemma vimageI [intro]: "[| <a,b>\<in> r; b\<in>B |] ==> a \<in> r-``B" 802by (unfold vimage_def, blast) 803 804lemma vimageE [elim!]: 805 "[| a: r-``B; !!x.[| <a,x>\<in> r; x\<in>B |] ==> P |] ==> P" 806apply (unfold vimage_def, blast) 807done 808 809lemma vimage_subset: "r \<subseteq> A*B ==> r-``C \<subseteq> A" 810apply (unfold vimage_def) 811apply (erule converse_type [THEN image_subset]) 812done 813 814lemma vimage_0 [simp]: "r-``0 = 0" 815by blast 816 817lemma vimage_Un [simp]: "r-``(A \<union> B) = (r-``A) \<union> (r-``B)" 818by blast 819 820lemma vimage_Int_subset: "r-``(A \<inter> B) \<subseteq> (r-``A) \<inter> (r-``B)" 821by blast 822 823(*NOT suitable for rewriting*) 824lemma vimage_eq_UN: "f -``B = (\<Union>y\<in>B. f-``{y})" 825by blast 826 827lemma function_vimage_Int: 828 "function(f) ==> f-``(A \<inter> B) = (f-``A) \<inter> (f-``B)" 829by (unfold function_def, blast) 830 831lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)" 832by (unfold function_def, blast) 833 834lemma function_image_vimage: "function(f) ==> f `` (f-`` A) \<subseteq> A" 835by (unfold function_def, blast) 836 837lemma vimage_Int_square_subset: "(r \<inter> A*A)-``B \<subseteq> (r-``B) \<inter> A" 838by blast 839 840lemma vimage_Int_square: "B\<subseteq>A ==> (r \<inter> A*A)-``B = (r-``B) \<inter> A" 841by blast 842 843 844 845(*Invese image laws for special relations*) 846lemma vimage_0_left [simp]: "0-``A = 0" 847by blast 848 849lemma vimage_Un_left: "(r \<union> s)-``A = (r-``A) \<union> (s-``A)" 850by blast 851 852lemma vimage_Int_subset_left: "(r \<inter> s)-``A \<subseteq> (r-``A) \<inter> (s-``A)" 853by blast 854 855 856(** Converse **) 857 858lemma converse_Un [simp]: "converse(A \<union> B) = converse(A) \<union> converse(B)" 859by blast 860 861lemma converse_Int [simp]: "converse(A \<inter> B) = converse(A) \<inter> converse(B)" 862by blast 863 864lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)" 865by blast 866 867lemma converse_UN [simp]: "converse(\<Union>x\<in>A. B(x)) = (\<Union>x\<in>A. converse(B(x)))" 868by blast 869 870(*Unfolding Inter avoids using excluded middle on A=0*) 871lemma converse_INT [simp]: 872 "converse(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. converse(B(x)))" 873apply (unfold Inter_def, blast) 874done 875 876 877subsection\<open>Powerset Operator\<close> 878 879lemma Pow_0 [simp]: "Pow(0) = {0}" 880by blast 881 882lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) \<union> {cons(a,X) . X: Pow(A)}" 883apply (rule equalityI, safe) 884apply (erule swap) 885apply (rule_tac a = "x-{a}" in RepFun_eqI, auto) 886done 887 888lemma Un_Pow_subset: "Pow(A) \<union> Pow(B) \<subseteq> Pow(A \<union> B)" 889by blast 890 891lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow(B(x))) \<subseteq> Pow(\<Union>x\<in>A. B(x))" 892by blast 893 894lemma subset_Pow_Union: "A \<subseteq> Pow(\<Union>(A))" 895by blast 896 897lemma Union_Pow_eq [simp]: "\<Union>(Pow(A)) = A" 898by blast 899 900lemma Union_Pow_iff: "\<Union>(A) \<in> Pow(B) \<longleftrightarrow> A \<in> Pow(Pow(B))" 901by blast 902 903lemma Pow_Int_eq [simp]: "Pow(A \<inter> B) = Pow(A) \<inter> Pow(B)" 904by blast 905 906lemma Pow_INT_eq: "A\<noteq>0 ==> Pow(\<Inter>x\<in>A. B(x)) = (\<Inter>x\<in>A. Pow(B(x)))" 907by (blast elim!: not_emptyE) 908 909 910subsection\<open>RepFun\<close> 911 912lemma RepFun_subset: "[| !!x. x\<in>A ==> f(x) \<in> B |] ==> {f(x). x\<in>A} \<subseteq> B" 913by blast 914 915lemma RepFun_eq_0_iff [simp]: "{f(x).x\<in>A}=0 \<longleftrightarrow> A=0" 916by blast 917 918lemma RepFun_constant [simp]: "{c. x\<in>A} = (if A=0 then 0 else {c})" 919by force 920 921 922subsection\<open>Collect\<close> 923 924lemma Collect_subset: "Collect(A,P) \<subseteq> A" 925by blast 926 927lemma Collect_Un: "Collect(A \<union> B, P) = Collect(A,P) \<union> Collect(B,P)" 928by blast 929 930lemma Collect_Int: "Collect(A \<inter> B, P) = Collect(A,P) \<inter> Collect(B,P)" 931by blast 932 933lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)" 934by blast 935 936lemma Collect_cons: "{x\<in>cons(a,B). P(x)} = 937 (if P(a) then cons(a, {x\<in>B. P(x)}) else {x\<in>B. P(x)})" 938by (simp, blast) 939 940lemma Int_Collect_self_eq: "A \<inter> Collect(A,P) = Collect(A,P)" 941by blast 942 943lemma Collect_Collect_eq [simp]: 944 "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))" 945by blast 946 947lemma Collect_Int_Collect_eq: 948 "Collect(A,P) \<inter> Collect(A,Q) = Collect(A, %x. P(x) & Q(x))" 949by blast 950 951lemma Collect_Union_eq [simp]: 952 "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))" 953by blast 954 955lemma Collect_Int_left: "{x\<in>A. P(x)} \<inter> B = {x \<in> A \<inter> B. P(x)}" 956by blast 957 958lemma Collect_Int_right: "A \<inter> {x\<in>B. P(x)} = {x \<in> A \<inter> B. P(x)}" 959by blast 960 961lemma Collect_disj_eq: "{x\<in>A. P(x) | Q(x)} = Collect(A, P) \<union> Collect(A, Q)" 962by blast 963 964lemma Collect_conj_eq: "{x\<in>A. P(x) & Q(x)} = Collect(A, P) \<inter> Collect(A, Q)" 965by blast 966 967lemmas subset_SIs = subset_refl cons_subsetI subset_consI 968 Union_least UN_least Un_least 969 Inter_greatest Int_greatest RepFun_subset 970 Un_upper1 Un_upper2 Int_lower1 Int_lower2 971 972ML \<open> 973val subset_cs = 974 claset_of (\<^context> 975 delrules [@{thm subsetI}, @{thm subsetCE}] 976 addSIs @{thms subset_SIs} 977 addIs [@{thm Union_upper}, @{thm Inter_lower}] 978 addSEs [@{thm cons_subsetE}]); 979 980val ZF_cs = claset_of (\<^context> delrules [@{thm equalityI}]); 981\<close> 982 983end 984 985