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