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