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