src/HOL/equalities.ML
author nipkow
Sun Nov 16 16:18:31 1997 +0100 (1997-11-16)
changeset 4231 a73f5a63f197
parent 4200 5a2cd204f8b4
child 4306 ddbe1a9722ab
permissions -rw-r--r--
Removed
"(ALL x:f``A. P x) = (ALL x:A. P(f x))",
"(EX x:f``A. P x) = (EX x:A. P(f x))",
again, because they were already there and added
"(UN x:f``A. B x) = (UN a:A. B(f a))"
"(INT x:f``A. B x) = (INT a:A. B(f a))"
instead.
clasohm@1465
     1
(*  Title:      HOL/equalities
clasohm@923
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@923
     4
    Copyright   1994  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Equalities involving union, intersection, inclusion, etc.
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
writeln"File HOL/equalities";
clasohm@923
    10
berghofe@1754
    11
AddSIs [equalityI];
berghofe@1754
    12
nipkow@1548
    13
section "{}";
nipkow@1548
    14
paulson@4059
    15
goal thy "{x. False} = {}";
paulson@2891
    16
by (Blast_tac 1);
nipkow@1531
    17
qed "Collect_False_empty";
nipkow@1531
    18
Addsimps [Collect_False_empty];
nipkow@1531
    19
paulson@4059
    20
goal thy "(A <= {}) = (A = {})";
paulson@2891
    21
by (Blast_tac 1);
nipkow@1531
    22
qed "subset_empty";
nipkow@1531
    23
Addsimps [subset_empty];
nipkow@1531
    24
nipkow@3222
    25
goalw thy [psubset_def] "~ (A < {})";
nipkow@3222
    26
by (Blast_tac 1);
nipkow@3222
    27
qed "not_psubset_empty";
nipkow@3222
    28
AddIffs [not_psubset_empty];
nipkow@3222
    29
nipkow@1548
    30
section "insert";
clasohm@923
    31
nipkow@1531
    32
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
paulson@4059
    33
goal thy "insert a A = {a} Un A";
paulson@2891
    34
by (Blast_tac 1);
nipkow@1531
    35
qed "insert_is_Un";
nipkow@1531
    36
paulson@4059
    37
goal thy "insert a A ~= {}";
wenzelm@4089
    38
by (blast_tac (claset() addEs [equalityCE]) 1);
nipkow@1179
    39
qed"insert_not_empty";
nipkow@1531
    40
Addsimps[insert_not_empty];
nipkow@1179
    41
nipkow@1179
    42
bind_thm("empty_not_insert",insert_not_empty RS not_sym);
nipkow@1531
    43
Addsimps[empty_not_insert];
nipkow@1179
    44
paulson@4059
    45
goal thy "!!a. a:A ==> insert a A = A";
paulson@2891
    46
by (Blast_tac 1);
clasohm@923
    47
qed "insert_absorb";
clasohm@923
    48
paulson@4059
    49
goal thy "insert x (insert x A) = insert x A";
paulson@2891
    50
by (Blast_tac 1);
nipkow@1531
    51
qed "insert_absorb2";
nipkow@1531
    52
Addsimps [insert_absorb2];
nipkow@1531
    53
paulson@4059
    54
goal thy "insert x (insert y A) = insert y (insert x A)";
paulson@2891
    55
by (Blast_tac 1);
paulson@1879
    56
qed "insert_commute";
paulson@1879
    57
paulson@4059
    58
goal thy "(insert x A <= B) = (x:B & A <= B)";
paulson@2891
    59
by (Blast_tac 1);
clasohm@923
    60
qed "insert_subset";
nipkow@1531
    61
Addsimps[insert_subset];
nipkow@1531
    62
paulson@4059
    63
goal thy "!!a. insert a A ~= insert a B ==> A ~= B";
nipkow@3222
    64
by (Blast_tac 1);
nipkow@3222
    65
qed "insert_lim";
nipkow@3222
    66
nipkow@1531
    67
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
paulson@4059
    68
goal thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
paulson@1553
    69
by (res_inst_tac [("x","A-{a}")] exI 1);
paulson@2891
    70
by (Blast_tac 1);
nipkow@1531
    71
qed "mk_disjoint_insert";
clasohm@923
    72
paulson@4059
    73
goal thy
paulson@1843
    74
    "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
paulson@2891
    75
by (Blast_tac 1);
paulson@1843
    76
qed "UN_insert_distrib";
paulson@1843
    77
oheimb@1660
    78
section "``";
clasohm@923
    79
paulson@4059
    80
goal thy "f``{} = {}";
paulson@2891
    81
by (Blast_tac 1);
clasohm@923
    82
qed "image_empty";
nipkow@1531
    83
Addsimps[image_empty];
clasohm@923
    84
paulson@4059
    85
goal thy "f``insert a B = insert (f a) (f``B)";
paulson@2891
    86
by (Blast_tac 1);
clasohm@923
    87
qed "image_insert";
nipkow@1531
    88
Addsimps[image_insert];
clasohm@923
    89
paulson@4059
    90
goal thy  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
nipkow@3222
    91
by (Blast_tac 1);
nipkow@3222
    92
qed "image_UNION";
nipkow@3222
    93
paulson@4059
    94
goal thy "(%x. x) `` Y = Y";
nipkow@3222
    95
by (Blast_tac 1);
nipkow@3222
    96
qed "image_id";
nipkow@3222
    97
paulson@4059
    98
goal thy "f``(g``A) = (%x. f (g x)) `` A";
paulson@3457
    99
by (Blast_tac 1);
paulson@4059
   100
qed "image_image";
nipkow@3222
   101
paulson@4059
   102
goal thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
paulson@2891
   103
by (Blast_tac 1);
paulson@1884
   104
qed "insert_image";
paulson@1884
   105
Addsimps [insert_image];
paulson@1884
   106
paulson@4059
   107
goal thy "(f``A = {}) = (A = {})";
wenzelm@4089
   108
by (blast_tac (claset() addSEs [equalityE]) 1);
nipkow@3415
   109
qed "image_is_empty";
nipkow@3415
   110
AddIffs [image_is_empty];
nipkow@3415
   111
paulson@4059
   112
goalw thy [image_def]
berghofe@1763
   113
"(%x. if P x then f x else g x) `` S                    \
paulson@4200
   114
\ = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
paulson@2031
   115
by (split_tac [expand_if] 1);
paulson@2891
   116
by (Blast_tac 1);
nipkow@1748
   117
qed "if_image_distrib";
nipkow@1748
   118
Addsimps[if_image_distrib];
nipkow@1748
   119
oheimb@4136
   120
val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
oheimb@4136
   121
by (rtac set_ext 1);
oheimb@4136
   122
by (simp_tac (simpset() addsimps image_def::prems) 1);
oheimb@4136
   123
qed "image_cong";
oheimb@4136
   124
nipkow@1748
   125
nipkow@1548
   126
section "Int";
clasohm@923
   127
paulson@4059
   128
goal thy "A Int A = A";
paulson@2891
   129
by (Blast_tac 1);
clasohm@923
   130
qed "Int_absorb";
nipkow@1531
   131
Addsimps[Int_absorb];
clasohm@923
   132
paulson@4059
   133
goal thy "A Int B  =  B Int A";
paulson@2891
   134
by (Blast_tac 1);
clasohm@923
   135
qed "Int_commute";
clasohm@923
   136
paulson@4059
   137
goal thy "(A Int B) Int C  =  A Int (B Int C)";
paulson@2891
   138
by (Blast_tac 1);
clasohm@923
   139
qed "Int_assoc";
clasohm@923
   140
paulson@4059
   141
goal thy "{} Int B = {}";
paulson@2891
   142
by (Blast_tac 1);
clasohm@923
   143
qed "Int_empty_left";
nipkow@1531
   144
Addsimps[Int_empty_left];
clasohm@923
   145
paulson@4059
   146
goal thy "A Int {} = {}";
paulson@2891
   147
by (Blast_tac 1);
clasohm@923
   148
qed "Int_empty_right";
nipkow@1531
   149
Addsimps[Int_empty_right];
nipkow@1531
   150
paulson@4059
   151
goal thy "(A Int B = {}) = (A <= Compl B)";
wenzelm@4089
   152
by (blast_tac (claset() addSEs [equalityE]) 1);
paulson@3356
   153
qed "disjoint_eq_subset_Compl";
paulson@3356
   154
paulson@4059
   155
goal thy "UNIV Int B = B";
paulson@2891
   156
by (Blast_tac 1);
nipkow@1531
   157
qed "Int_UNIV_left";
nipkow@1531
   158
Addsimps[Int_UNIV_left];
nipkow@1531
   159
paulson@4059
   160
goal thy "A Int UNIV = A";
paulson@2891
   161
by (Blast_tac 1);
nipkow@1531
   162
qed "Int_UNIV_right";
nipkow@1531
   163
Addsimps[Int_UNIV_right];
clasohm@923
   164
paulson@4059
   165
goal thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
paulson@2891
   166
by (Blast_tac 1);
clasohm@923
   167
qed "Int_Un_distrib";
clasohm@923
   168
paulson@4059
   169
goal thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
paulson@2891
   170
by (Blast_tac 1);
paulson@1618
   171
qed "Int_Un_distrib2";
paulson@1618
   172
paulson@4059
   173
goal thy "(A<=B) = (A Int B = A)";
wenzelm@4089
   174
by (blast_tac (claset() addSEs [equalityE]) 1);
clasohm@923
   175
qed "subset_Int_eq";
clasohm@923
   176
paulson@4059
   177
goal thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
wenzelm@4089
   178
by (blast_tac (claset() addEs [equalityCE]) 1);
nipkow@1531
   179
qed "Int_UNIV";
nipkow@1531
   180
Addsimps[Int_UNIV];
nipkow@1531
   181
nipkow@1548
   182
section "Un";
clasohm@923
   183
paulson@4059
   184
goal thy "A Un A = A";
paulson@2891
   185
by (Blast_tac 1);
clasohm@923
   186
qed "Un_absorb";
nipkow@1531
   187
Addsimps[Un_absorb];
clasohm@923
   188
paulson@4059
   189
goal thy " A Un (A Un B) = A Un B";
nipkow@3222
   190
by (Blast_tac 1);
nipkow@3222
   191
qed "Un_left_absorb";
nipkow@3222
   192
paulson@4059
   193
goal thy "A Un B  =  B Un A";
paulson@2891
   194
by (Blast_tac 1);
clasohm@923
   195
qed "Un_commute";
clasohm@923
   196
paulson@4059
   197
goal thy " A Un (B Un C) = B Un (A Un C)";
nipkow@3222
   198
by (Blast_tac 1);
nipkow@3222
   199
qed "Un_left_commute";
nipkow@3222
   200
paulson@4059
   201
goal thy "(A Un B) Un C  =  A Un (B Un C)";
paulson@2891
   202
by (Blast_tac 1);
clasohm@923
   203
qed "Un_assoc";
clasohm@923
   204
paulson@4059
   205
goal thy "{} Un B = B";
paulson@2891
   206
by (Blast_tac 1);
clasohm@923
   207
qed "Un_empty_left";
nipkow@1531
   208
Addsimps[Un_empty_left];
clasohm@923
   209
paulson@4059
   210
goal thy "A Un {} = A";
paulson@2891
   211
by (Blast_tac 1);
clasohm@923
   212
qed "Un_empty_right";
nipkow@1531
   213
Addsimps[Un_empty_right];
nipkow@1531
   214
paulson@4059
   215
goal thy "UNIV Un B = UNIV";
paulson@2891
   216
by (Blast_tac 1);
nipkow@1531
   217
qed "Un_UNIV_left";
nipkow@1531
   218
Addsimps[Un_UNIV_left];
nipkow@1531
   219
paulson@4059
   220
goal thy "A Un UNIV = UNIV";
paulson@2891
   221
by (Blast_tac 1);
nipkow@1531
   222
qed "Un_UNIV_right";
nipkow@1531
   223
Addsimps[Un_UNIV_right];
clasohm@923
   224
paulson@4059
   225
goal thy "(insert a B) Un C = insert a (B Un C)";
paulson@2891
   226
by (Blast_tac 1);
clasohm@923
   227
qed "Un_insert_left";
paulson@3384
   228
Addsimps[Un_insert_left];
clasohm@923
   229
paulson@4059
   230
goal thy "A Un (insert a B) = insert a (A Un B)";
paulson@2891
   231
by (Blast_tac 1);
paulson@1917
   232
qed "Un_insert_right";
paulson@3384
   233
Addsimps[Un_insert_right];
paulson@1917
   234
paulson@4059
   235
goal thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
paulson@3356
   236
\                                          else        B Int C)";
wenzelm@4089
   237
by (simp_tac (simpset() addsplits [expand_if]) 1);
paulson@3356
   238
by (Blast_tac 1);
paulson@3356
   239
qed "Int_insert_left";
paulson@3356
   240
paulson@4059
   241
goal thy "A Int (insert a B) = (if a:A then insert a (A Int B) \
paulson@3356
   242
\                                          else        A Int B)";
wenzelm@4089
   243
by (simp_tac (simpset() addsplits [expand_if]) 1);
paulson@3356
   244
by (Blast_tac 1);
paulson@3356
   245
qed "Int_insert_right";
paulson@3356
   246
paulson@4059
   247
goal thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
paulson@2891
   248
by (Blast_tac 1);
clasohm@923
   249
qed "Un_Int_distrib";
clasohm@923
   250
paulson@4059
   251
goal thy
clasohm@923
   252
 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
paulson@2891
   253
by (Blast_tac 1);
clasohm@923
   254
qed "Un_Int_crazy";
clasohm@923
   255
paulson@4059
   256
goal thy "(A<=B) = (A Un B = B)";
wenzelm@4089
   257
by (blast_tac (claset() addSEs [equalityE]) 1);
clasohm@923
   258
qed "subset_Un_eq";
clasohm@923
   259
paulson@4059
   260
goal thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
paulson@2891
   261
by (Blast_tac 1);
clasohm@923
   262
qed "subset_insert_iff";
clasohm@923
   263
paulson@4059
   264
goal thy "(A Un B = {}) = (A = {} & B = {})";
wenzelm@4089
   265
by (blast_tac (claset() addEs [equalityCE]) 1);
clasohm@923
   266
qed "Un_empty";
nipkow@1531
   267
Addsimps[Un_empty];
clasohm@923
   268
nipkow@1548
   269
section "Compl";
clasohm@923
   270
paulson@4059
   271
goal thy "A Int Compl(A) = {}";
paulson@2891
   272
by (Blast_tac 1);
clasohm@923
   273
qed "Compl_disjoint";
nipkow@1531
   274
Addsimps[Compl_disjoint];
clasohm@923
   275
paulson@4059
   276
goal thy "A Un Compl(A) = UNIV";
paulson@2891
   277
by (Blast_tac 1);
clasohm@923
   278
qed "Compl_partition";
clasohm@923
   279
paulson@4059
   280
goal thy "Compl(Compl(A)) = A";
paulson@2891
   281
by (Blast_tac 1);
clasohm@923
   282
qed "double_complement";
nipkow@1531
   283
Addsimps[double_complement];
clasohm@923
   284
paulson@4059
   285
goal thy "Compl(A Un B) = Compl(A) Int Compl(B)";
paulson@2891
   286
by (Blast_tac 1);
clasohm@923
   287
qed "Compl_Un";
clasohm@923
   288
paulson@4059
   289
goal thy "Compl(A Int B) = Compl(A) Un Compl(B)";
paulson@2891
   290
by (Blast_tac 1);
clasohm@923
   291
qed "Compl_Int";
clasohm@923
   292
paulson@4059
   293
goal thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
paulson@2891
   294
by (Blast_tac 1);
clasohm@923
   295
qed "Compl_UN";
clasohm@923
   296
paulson@4059
   297
goal thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
paulson@2891
   298
by (Blast_tac 1);
clasohm@923
   299
qed "Compl_INT";
clasohm@923
   300
clasohm@923
   301
(*Halmos, Naive Set Theory, page 16.*)
clasohm@923
   302
paulson@4059
   303
goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
wenzelm@4089
   304
by (blast_tac (claset() addSEs [equalityE]) 1);
clasohm@923
   305
qed "Un_Int_assoc_eq";
clasohm@923
   306
clasohm@923
   307
nipkow@1548
   308
section "Union";
clasohm@923
   309
paulson@4059
   310
goal thy "Union({}) = {}";
paulson@2891
   311
by (Blast_tac 1);
clasohm@923
   312
qed "Union_empty";
nipkow@1531
   313
Addsimps[Union_empty];
nipkow@1531
   314
paulson@4059
   315
goal thy "Union(UNIV) = UNIV";
paulson@2891
   316
by (Blast_tac 1);
nipkow@1531
   317
qed "Union_UNIV";
nipkow@1531
   318
Addsimps[Union_UNIV];
clasohm@923
   319
paulson@4059
   320
goal thy "Union(insert a B) = a Un Union(B)";
paulson@2891
   321
by (Blast_tac 1);
clasohm@923
   322
qed "Union_insert";
nipkow@1531
   323
Addsimps[Union_insert];
clasohm@923
   324
paulson@4059
   325
goal thy "Union(A Un B) = Union(A) Un Union(B)";
paulson@2891
   326
by (Blast_tac 1);
clasohm@923
   327
qed "Union_Un_distrib";
nipkow@1531
   328
Addsimps[Union_Un_distrib];
clasohm@923
   329
paulson@4059
   330
goal thy "Union(A Int B) <= Union(A) Int Union(B)";
paulson@2891
   331
by (Blast_tac 1);
clasohm@923
   332
qed "Union_Int_subset";
clasohm@923
   333
paulson@4059
   334
goal thy "(Union M = {}) = (! A : M. A = {})"; 
wenzelm@4089
   335
by (blast_tac (claset() addEs [equalityE]) 1);
nipkow@4003
   336
qed"Union_empty_conv"; 
nipkow@4003
   337
AddIffs [Union_empty_conv];
nipkow@4003
   338
paulson@4159
   339
goal thy "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
wenzelm@4089
   340
by (blast_tac (claset() addSEs [equalityE]) 1);
clasohm@923
   341
qed "Union_disjoint";
clasohm@923
   342
nipkow@1548
   343
section "Inter";
nipkow@1548
   344
paulson@4059
   345
goal thy "Inter({}) = UNIV";
paulson@2891
   346
by (Blast_tac 1);
nipkow@1531
   347
qed "Inter_empty";
nipkow@1531
   348
Addsimps[Inter_empty];
nipkow@1531
   349
paulson@4059
   350
goal thy "Inter(UNIV) = {}";
paulson@2891
   351
by (Blast_tac 1);
nipkow@1531
   352
qed "Inter_UNIV";
nipkow@1531
   353
Addsimps[Inter_UNIV];
nipkow@1531
   354
paulson@4059
   355
goal thy "Inter(insert a B) = a Int Inter(B)";
paulson@2891
   356
by (Blast_tac 1);
nipkow@1531
   357
qed "Inter_insert";
nipkow@1531
   358
Addsimps[Inter_insert];
nipkow@1531
   359
paulson@4059
   360
goal thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
paulson@2891
   361
by (Blast_tac 1);
paulson@1564
   362
qed "Inter_Un_subset";
nipkow@1531
   363
paulson@4059
   364
goal thy "Inter(A Un B) = Inter(A) Int Inter(B)";
paulson@2891
   365
by (Blast_tac 1);
clasohm@923
   366
qed "Inter_Un_distrib";
clasohm@923
   367
nipkow@1548
   368
section "UN and INT";
clasohm@923
   369
clasohm@923
   370
(*Basic identities*)
clasohm@923
   371
paulson@4200
   372
val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]);
oheimb@4136
   373
(*Addsimps[not_empty];*)
oheimb@4136
   374
paulson@4059
   375
goal thy "(UN x:{}. B x) = {}";
paulson@2891
   376
by (Blast_tac 1);
nipkow@1179
   377
qed "UN_empty";
nipkow@1531
   378
Addsimps[UN_empty];
nipkow@1531
   379
paulson@4059
   380
goal thy "(UN x:A. {}) = {}";
paulson@3457
   381
by (Blast_tac 1);
nipkow@3222
   382
qed "UN_empty2";
nipkow@3222
   383
Addsimps[UN_empty2];
nipkow@3222
   384
paulson@4059
   385
goal thy "(INT x:{}. B x) = UNIV";
paulson@2891
   386
by (Blast_tac 1);
nipkow@1531
   387
qed "INT_empty";
nipkow@1531
   388
Addsimps[INT_empty];
nipkow@1531
   389
paulson@4059
   390
goal thy "(UN x:insert a A. B x) = B a Un UNION A B";
paulson@2891
   391
by (Blast_tac 1);
nipkow@1179
   392
qed "UN_insert";
nipkow@1531
   393
Addsimps[UN_insert];
nipkow@1531
   394
paulson@4059
   395
goal thy "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
nipkow@3222
   396
by (Blast_tac 1);
nipkow@3222
   397
qed "UN_Un";
nipkow@3222
   398
paulson@4059
   399
goal thy "(INT x:insert a A. B x) = B a Int INTER A B";
paulson@2891
   400
by (Blast_tac 1);
nipkow@1531
   401
qed "INT_insert";
nipkow@1531
   402
Addsimps[INT_insert];
nipkow@1179
   403
paulson@4059
   404
goal thy
paulson@2021
   405
    "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
paulson@2891
   406
by (Blast_tac 1);
paulson@2021
   407
qed "INT_insert_distrib";
paulson@2021
   408
paulson@4059
   409
goal thy "Union(B``A) = (UN x:A. B(x))";
paulson@2891
   410
by (Blast_tac 1);
clasohm@923
   411
qed "Union_image_eq";
clasohm@923
   412
paulson@4059
   413
goal thy "Inter(B``A) = (INT x:A. B(x))";
paulson@2891
   414
by (Blast_tac 1);
clasohm@923
   415
qed "Inter_image_eq";
clasohm@923
   416
paulson@4159
   417
goal thy "!!A. A~={} ==> (UN y:A. c) = c";
paulson@2891
   418
by (Blast_tac 1);
clasohm@923
   419
qed "UN_constant";
paulson@4159
   420
Addsimps[UN_constant];
clasohm@923
   421
paulson@4159
   422
goal thy "!!A. A~={} ==> (INT y:A. c) = c";
paulson@2891
   423
by (Blast_tac 1);
clasohm@923
   424
qed "INT_constant";
paulson@4159
   425
Addsimps[INT_constant];
clasohm@923
   426
paulson@4059
   427
goal thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
paulson@2891
   428
by (Blast_tac 1);
clasohm@923
   429
qed "UN_eq";
clasohm@923
   430
clasohm@923
   431
(*Look: it has an EXISTENTIAL quantifier*)
paulson@4059
   432
goal thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
paulson@2891
   433
by (Blast_tac 1);
clasohm@923
   434
qed "INT_eq";
clasohm@923
   435
paulson@4059
   436
goalw thy [o_def] "UNION A (g o f) = UNION (f``A) g";
nipkow@3222
   437
by (Blast_tac 1);
nipkow@3222
   438
qed "UNION_o";
nipkow@3222
   439
nipkow@3222
   440
clasohm@923
   441
(*Distributive laws...*)
clasohm@923
   442
paulson@4059
   443
goal thy "A Int Union(B) = (UN C:B. A Int C)";
paulson@2891
   444
by (Blast_tac 1);
clasohm@923
   445
qed "Int_Union";
clasohm@923
   446
nipkow@2912
   447
(* Devlin, Setdamentals of Contemporary Set Theory, page 12, exercise 5: 
clasohm@923
   448
   Union of a family of unions **)
paulson@4059
   449
goal thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
paulson@2891
   450
by (Blast_tac 1);
clasohm@923
   451
qed "Un_Union_image";
clasohm@923
   452
clasohm@923
   453
(*Equivalent version*)
paulson@4059
   454
goal thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
paulson@2891
   455
by (Blast_tac 1);
clasohm@923
   456
qed "UN_Un_distrib";
clasohm@923
   457
paulson@4059
   458
goal thy "A Un Inter(B) = (INT C:B. A Un C)";
paulson@2891
   459
by (Blast_tac 1);
clasohm@923
   460
qed "Un_Inter";
clasohm@923
   461
paulson@4059
   462
goal thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
paulson@2891
   463
by (Blast_tac 1);
clasohm@923
   464
qed "Int_Inter_image";
clasohm@923
   465
clasohm@923
   466
(*Equivalent version*)
paulson@4059
   467
goal thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
paulson@2891
   468
by (Blast_tac 1);
clasohm@923
   469
qed "INT_Int_distrib";
clasohm@923
   470
clasohm@923
   471
(*Halmos, Naive Set Theory, page 35.*)
paulson@4059
   472
goal thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
paulson@2891
   473
by (Blast_tac 1);
clasohm@923
   474
qed "Int_UN_distrib";
clasohm@923
   475
paulson@4059
   476
goal thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
paulson@2891
   477
by (Blast_tac 1);
clasohm@923
   478
qed "Un_INT_distrib";
clasohm@923
   479
paulson@4059
   480
goal thy
clasohm@923
   481
    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
paulson@2891
   482
by (Blast_tac 1);
clasohm@923
   483
qed "Int_UN_distrib2";
clasohm@923
   484
paulson@4059
   485
goal thy
clasohm@923
   486
    "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
paulson@2891
   487
by (Blast_tac 1);
clasohm@923
   488
qed "Un_INT_distrib2";
clasohm@923
   489
nipkow@2512
   490
nipkow@2512
   491
section"Bounded quantifiers";
nipkow@2512
   492
nipkow@3860
   493
(** The following are not added to the default simpset because
nipkow@3860
   494
    (a) they duplicate the body and (b) there are no similar rules for Int. **)
nipkow@2512
   495
paulson@4059
   496
goal thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
paulson@2891
   497
by (Blast_tac 1);
paulson@2519
   498
qed "ball_Un";
paulson@2519
   499
paulson@4059
   500
goal thy "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
paulson@2891
   501
by (Blast_tac 1);
paulson@2519
   502
qed "bex_Un";
nipkow@2512
   503
nipkow@2512
   504
nipkow@1548
   505
section "-";
clasohm@923
   506
paulson@4059
   507
goal thy "A-A = {}";
paulson@2891
   508
by (Blast_tac 1);
clasohm@923
   509
qed "Diff_cancel";
nipkow@1531
   510
Addsimps[Diff_cancel];
clasohm@923
   511
paulson@4059
   512
goal thy "{}-A = {}";
paulson@2891
   513
by (Blast_tac 1);
clasohm@923
   514
qed "empty_Diff";
nipkow@1531
   515
Addsimps[empty_Diff];
clasohm@923
   516
paulson@4059
   517
goal thy "A-{} = A";
paulson@2891
   518
by (Blast_tac 1);
clasohm@923
   519
qed "Diff_empty";
nipkow@1531
   520
Addsimps[Diff_empty];
nipkow@1531
   521
paulson@4059
   522
goal thy "A-UNIV = {}";
paulson@2891
   523
by (Blast_tac 1);
nipkow@1531
   524
qed "Diff_UNIV";
nipkow@1531
   525
Addsimps[Diff_UNIV];
nipkow@1531
   526
paulson@4059
   527
goal thy "!!x. x~:A ==> A - insert x B = A-B";
paulson@2891
   528
by (Blast_tac 1);
nipkow@1531
   529
qed "Diff_insert0";
nipkow@1531
   530
Addsimps [Diff_insert0];
clasohm@923
   531
clasohm@923
   532
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
paulson@4059
   533
goal thy "A - insert a B = A - B - {a}";
paulson@2891
   534
by (Blast_tac 1);
clasohm@923
   535
qed "Diff_insert";
clasohm@923
   536
clasohm@923
   537
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
paulson@4059
   538
goal thy "A - insert a B = A - {a} - B";
paulson@2891
   539
by (Blast_tac 1);
clasohm@923
   540
qed "Diff_insert2";
clasohm@923
   541
paulson@4059
   542
goal thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
wenzelm@4089
   543
by (simp_tac (simpset() addsplits [expand_if]) 1);
paulson@2891
   544
by (Blast_tac 1);
nipkow@1531
   545
qed "insert_Diff_if";
nipkow@1531
   546
paulson@4059
   547
goal thy "!!x. x:B ==> insert x A - B = A-B";
paulson@2891
   548
by (Blast_tac 1);
nipkow@1531
   549
qed "insert_Diff1";
nipkow@1531
   550
Addsimps [insert_Diff1];
nipkow@1531
   551
paulson@4059
   552
goal thy "!!a. a:A ==> insert a (A-{a}) = A";
paulson@2922
   553
by (Blast_tac 1);
clasohm@923
   554
qed "insert_Diff";
clasohm@923
   555
paulson@4059
   556
goal thy "A Int (B-A) = {}";
paulson@2891
   557
by (Blast_tac 1);
clasohm@923
   558
qed "Diff_disjoint";
nipkow@1531
   559
Addsimps[Diff_disjoint];
clasohm@923
   560
paulson@4059
   561
goal thy "!!A. A<=B ==> A Un (B-A) = B";
paulson@2891
   562
by (Blast_tac 1);
clasohm@923
   563
qed "Diff_partition";
clasohm@923
   564
paulson@4059
   565
goal thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
paulson@2891
   566
by (Blast_tac 1);
clasohm@923
   567
qed "double_diff";
clasohm@923
   568
paulson@4059
   569
goal thy "A - (B Un C) = (A-B) Int (A-C)";
paulson@2891
   570
by (Blast_tac 1);
clasohm@923
   571
qed "Diff_Un";
clasohm@923
   572
paulson@4059
   573
goal thy "A - (B Int C) = (A-B) Un (A-C)";
paulson@2891
   574
by (Blast_tac 1);
clasohm@923
   575
qed "Diff_Int";
clasohm@923
   576
paulson@4059
   577
goal thy "(A Un B) - C = (A - C) Un (B - C)";
nipkow@3222
   578
by (Blast_tac 1);
nipkow@3222
   579
qed "Un_Diff";
nipkow@3222
   580
paulson@4059
   581
goal thy "(A Int B) - C = (A - C) Int (B - C)";
nipkow@3222
   582
by (Blast_tac 1);
nipkow@3222
   583
qed "Int_Diff";
nipkow@3222
   584
nipkow@3222
   585
nipkow@3222
   586
section "Miscellany";
nipkow@3222
   587
paulson@4059
   588
goal thy "(A = B) = ((A <= (B::'a set)) & (B<=A))";
nipkow@3222
   589
by (Blast_tac 1);
nipkow@3222
   590
qed "set_eq_subset";
nipkow@3222
   591
paulson@4059
   592
goal thy "A <= B =  (! t. t:A --> t:B)";
nipkow@3222
   593
by (Blast_tac 1);
nipkow@3222
   594
qed "subset_iff";
nipkow@3222
   595
nipkow@3222
   596
goalw thy [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
nipkow@3222
   597
by (Blast_tac 1);
nipkow@3222
   598
qed "subset_iff_psubset_eq";
paulson@2021
   599
paulson@4059
   600
goal thy "(!x. x ~: A) = (A={})";
nipkow@3896
   601
by(Blast_tac 1);
nipkow@3896
   602
qed "all_not_in_conv";
nipkow@3907
   603
AddIffs [all_not_in_conv];
nipkow@3896
   604
paulson@4059
   605
goalw thy [Pow_def] "Pow {} = {{}}";
paulson@3348
   606
by (Auto_tac());
paulson@3348
   607
qed "Pow_empty";
paulson@3348
   608
Addsimps [Pow_empty];
paulson@3348
   609
paulson@4059
   610
goal thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
paulson@3724
   611
by Safe_tac;
paulson@3457
   612
by (etac swap 1);
paulson@3348
   613
by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
paulson@3348
   614
by (ALLGOALS Blast_tac);
paulson@3348
   615
qed "Pow_insert";
paulson@3348
   616
paulson@2021
   617
paulson@2021
   618
(** Miniscoping: pushing in big Unions and Intersections **)
paulson@2021
   619
local
paulson@4059
   620
  fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
paulson@2021
   621
in
paulson@2513
   622
val UN_simps = map prover 
paulson@4159
   623
    ["!!C. C ~= {} ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
paulson@4159
   624
     "!!C. C ~= {} ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
paulson@4159
   625
     "!!C. C ~= {} ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
paulson@4159
   626
     "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
paulson@4159
   627
     "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
paulson@4159
   628
     "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
nipkow@4231
   629
     "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
nipkow@4231
   630
     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
paulson@2513
   631
paulson@2513
   632
val INT_simps = map prover
paulson@4159
   633
    ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
paulson@4159
   634
     "!!C. C ~= {} ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
paulson@4159
   635
     "!!C. C ~= {} ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
paulson@4159
   636
     "!!C. C ~= {} ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
paulson@4159
   637
     "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
paulson@4159
   638
     "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
nipkow@4231
   639
     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
nipkow@4231
   640
     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
paulson@2513
   641
paulson@2513
   642
paulson@2513
   643
val ball_simps = map prover
paulson@2513
   644
    ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
paulson@2513
   645
     "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
paulson@3422
   646
     "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
paulson@3422
   647
     "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
paulson@2513
   648
     "(ALL x:{}. P x) = True",
oheimb@4136
   649
     "(ALL x:UNIV. P x) = (ALL x. P x)",
paulson@2513
   650
     "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
paulson@2513
   651
     "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
nipkow@3860
   652
     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
nipkow@3860
   653
     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
nipkow@3860
   654
     "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
paulson@2513
   655
paulson@2513
   656
val ball_conj_distrib = 
paulson@2513
   657
    prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
paulson@2513
   658
paulson@2513
   659
val bex_simps = map prover
paulson@2513
   660
    ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
paulson@2513
   661
     "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
paulson@2513
   662
     "(EX x:{}. P x) = False",
oheimb@4136
   663
     "(EX x:UNIV. P x) = (EX x. P x)",
paulson@2513
   664
     "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
paulson@2513
   665
     "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
nipkow@3860
   666
     "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
nipkow@3860
   667
     "(EX x:f``A. P x) = (EX x:A. P(f x))",
nipkow@3860
   668
     "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
paulson@2513
   669
paulson@3426
   670
val bex_disj_distrib = 
paulson@2513
   671
    prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
paulson@2513
   672
paulson@2021
   673
end;
paulson@2021
   674
paulson@4159
   675
Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);