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