src/HOL/equalities.ML
author berghofe
Thu May 23 15:17:23 1996 +0200 (1996-05-23)
changeset 1763 fb07e359b59f
parent 1754 852093aeb0ab
child 1786 8a31d85d27b8
permissions -rw-r--r--
expanded TABs
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
clasohm@923
    13
val eq_cs = set_cs addSIs [equalityI];
clasohm@923
    14
nipkow@1548
    15
section "{}";
nipkow@1548
    16
nipkow@1531
    17
goal Set.thy "{x.False} = {}";
berghofe@1754
    18
by (Fast_tac 1);
nipkow@1531
    19
qed "Collect_False_empty";
nipkow@1531
    20
Addsimps [Collect_False_empty];
nipkow@1531
    21
nipkow@1531
    22
goal Set.thy "(A <= {}) = (A = {})";
berghofe@1754
    23
by (Fast_tac 1);
nipkow@1531
    24
qed "subset_empty";
nipkow@1531
    25
Addsimps [subset_empty];
nipkow@1531
    26
nipkow@1548
    27
section ":";
clasohm@923
    28
clasohm@923
    29
goal Set.thy "x ~: {}";
berghofe@1754
    30
by (Fast_tac 1);
clasohm@923
    31
qed "in_empty";
nipkow@1531
    32
Addsimps[in_empty];
clasohm@923
    33
clasohm@923
    34
goal Set.thy "x : insert y A = (x=y | x:A)";
berghofe@1754
    35
by (Fast_tac 1);
clasohm@923
    36
qed "in_insert";
nipkow@1531
    37
Addsimps[in_insert];
clasohm@923
    38
nipkow@1548
    39
section "insert";
clasohm@923
    40
nipkow@1531
    41
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
nipkow@1531
    42
goal Set.thy "insert a A = {a} Un A";
berghofe@1754
    43
by (Fast_tac 1);
nipkow@1531
    44
qed "insert_is_Un";
nipkow@1531
    45
nipkow@1179
    46
goal Set.thy "insert a A ~= {}";
berghofe@1754
    47
by (fast_tac (!claset addEs [equalityCE]) 1);
nipkow@1179
    48
qed"insert_not_empty";
nipkow@1531
    49
Addsimps[insert_not_empty];
nipkow@1179
    50
nipkow@1179
    51
bind_thm("empty_not_insert",insert_not_empty RS not_sym);
nipkow@1531
    52
Addsimps[empty_not_insert];
nipkow@1179
    53
clasohm@923
    54
goal Set.thy "!!a. a:A ==> insert a A = A";
berghofe@1754
    55
by (Fast_tac 1);
clasohm@923
    56
qed "insert_absorb";
clasohm@923
    57
nipkow@1531
    58
goal Set.thy "insert x (insert x A) = insert x A";
berghofe@1754
    59
by (Fast_tac 1);
nipkow@1531
    60
qed "insert_absorb2";
nipkow@1531
    61
Addsimps [insert_absorb2];
nipkow@1531
    62
clasohm@923
    63
goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
berghofe@1754
    64
by (Fast_tac 1);
clasohm@923
    65
qed "insert_subset";
nipkow@1531
    66
Addsimps[insert_subset];
nipkow@1531
    67
nipkow@1531
    68
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
nipkow@1531
    69
goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
paulson@1553
    70
by (res_inst_tac [("x","A-{a}")] exI 1);
berghofe@1754
    71
by (Fast_tac 1);
nipkow@1531
    72
qed "mk_disjoint_insert";
clasohm@923
    73
oheimb@1660
    74
section "``";
clasohm@923
    75
clasohm@923
    76
goal Set.thy "f``{} = {}";
berghofe@1754
    77
by (Fast_tac 1);
clasohm@923
    78
qed "image_empty";
nipkow@1531
    79
Addsimps[image_empty];
clasohm@923
    80
clasohm@923
    81
goal Set.thy "f``insert a B = insert (f a) (f``B)";
berghofe@1754
    82
by (Fast_tac 1);
clasohm@923
    83
qed "image_insert";
nipkow@1531
    84
Addsimps[image_insert];
clasohm@923
    85
oheimb@1660
    86
qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
berghofe@1754
    87
 (fn _ => [Fast_tac 1]);
oheimb@1660
    88
nipkow@1748
    89
goalw Set.thy [image_def]
berghofe@1763
    90
"(%x. if P x then f x else g x) `` S                    \
nipkow@1748
    91
\ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
nipkow@1748
    92
by(split_tac [expand_if] 1);
berghofe@1754
    93
by(Fast_tac 1);
nipkow@1748
    94
qed "if_image_distrib";
nipkow@1748
    95
Addsimps[if_image_distrib];
nipkow@1748
    96
nipkow@1748
    97
oheimb@1660
    98
section "range";
oheimb@1660
    99
oheimb@1660
   100
qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
berghofe@1754
   101
 (fn _ => [Fast_tac 1]);
oheimb@1660
   102
oheimb@1660
   103
qed_goalw "image_range" Set.thy [image_def, range_def]
oheimb@1660
   104
 "f``range g = range (%x. f (g x))" (fn _ => [
berghofe@1763
   105
        rtac Collect_cong 1,
berghofe@1763
   106
        Fast_tac 1]);
oheimb@1660
   107
nipkow@1548
   108
section "Int";
clasohm@923
   109
clasohm@923
   110
goal Set.thy "A Int A = A";
berghofe@1754
   111
by (Fast_tac 1);
clasohm@923
   112
qed "Int_absorb";
nipkow@1531
   113
Addsimps[Int_absorb];
clasohm@923
   114
clasohm@923
   115
goal Set.thy "A Int B  =  B Int A";
berghofe@1754
   116
by (Fast_tac 1);
clasohm@923
   117
qed "Int_commute";
clasohm@923
   118
clasohm@923
   119
goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
berghofe@1754
   120
by (Fast_tac 1);
clasohm@923
   121
qed "Int_assoc";
clasohm@923
   122
clasohm@923
   123
goal Set.thy "{} Int B = {}";
berghofe@1754
   124
by (Fast_tac 1);
clasohm@923
   125
qed "Int_empty_left";
nipkow@1531
   126
Addsimps[Int_empty_left];
clasohm@923
   127
clasohm@923
   128
goal Set.thy "A Int {} = {}";
berghofe@1754
   129
by (Fast_tac 1);
clasohm@923
   130
qed "Int_empty_right";
nipkow@1531
   131
Addsimps[Int_empty_right];
nipkow@1531
   132
nipkow@1531
   133
goal Set.thy "UNIV Int B = B";
berghofe@1754
   134
by (Fast_tac 1);
nipkow@1531
   135
qed "Int_UNIV_left";
nipkow@1531
   136
Addsimps[Int_UNIV_left];
nipkow@1531
   137
nipkow@1531
   138
goal Set.thy "A Int UNIV = A";
berghofe@1754
   139
by (Fast_tac 1);
nipkow@1531
   140
qed "Int_UNIV_right";
nipkow@1531
   141
Addsimps[Int_UNIV_right];
clasohm@923
   142
clasohm@923
   143
goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
berghofe@1754
   144
by (Fast_tac 1);
clasohm@923
   145
qed "Int_Un_distrib";
clasohm@923
   146
paulson@1618
   147
goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
berghofe@1754
   148
by (Fast_tac 1);
paulson@1618
   149
qed "Int_Un_distrib2";
paulson@1618
   150
clasohm@923
   151
goal Set.thy "(A<=B) = (A Int B = A)";
berghofe@1754
   152
by (fast_tac (!claset addSEs [equalityE]) 1);
clasohm@923
   153
qed "subset_Int_eq";
clasohm@923
   154
nipkow@1531
   155
goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
berghofe@1754
   156
by (fast_tac (!claset addEs [equalityCE]) 1);
nipkow@1531
   157
qed "Int_UNIV";
nipkow@1531
   158
Addsimps[Int_UNIV];
nipkow@1531
   159
nipkow@1548
   160
section "Un";
clasohm@923
   161
clasohm@923
   162
goal Set.thy "A Un A = A";
berghofe@1754
   163
by (Fast_tac 1);
clasohm@923
   164
qed "Un_absorb";
nipkow@1531
   165
Addsimps[Un_absorb];
clasohm@923
   166
clasohm@923
   167
goal Set.thy "A Un B  =  B Un A";
berghofe@1754
   168
by (Fast_tac 1);
clasohm@923
   169
qed "Un_commute";
clasohm@923
   170
clasohm@923
   171
goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
berghofe@1754
   172
by (Fast_tac 1);
clasohm@923
   173
qed "Un_assoc";
clasohm@923
   174
clasohm@923
   175
goal Set.thy "{} Un B = B";
berghofe@1754
   176
by (Fast_tac 1);
clasohm@923
   177
qed "Un_empty_left";
nipkow@1531
   178
Addsimps[Un_empty_left];
clasohm@923
   179
clasohm@923
   180
goal Set.thy "A Un {} = A";
berghofe@1754
   181
by (Fast_tac 1);
clasohm@923
   182
qed "Un_empty_right";
nipkow@1531
   183
Addsimps[Un_empty_right];
nipkow@1531
   184
nipkow@1531
   185
goal Set.thy "UNIV Un B = UNIV";
berghofe@1754
   186
by (Fast_tac 1);
nipkow@1531
   187
qed "Un_UNIV_left";
nipkow@1531
   188
Addsimps[Un_UNIV_left];
nipkow@1531
   189
nipkow@1531
   190
goal Set.thy "A Un UNIV = UNIV";
berghofe@1754
   191
by (Fast_tac 1);
nipkow@1531
   192
qed "Un_UNIV_right";
nipkow@1531
   193
Addsimps[Un_UNIV_right];
clasohm@923
   194
clasohm@923
   195
goal Set.thy "insert a B Un C = insert a (B Un C)";
berghofe@1754
   196
by (Fast_tac 1);
clasohm@923
   197
qed "Un_insert_left";
clasohm@923
   198
clasohm@923
   199
goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
berghofe@1754
   200
by (Fast_tac 1);
clasohm@923
   201
qed "Un_Int_distrib";
clasohm@923
   202
clasohm@923
   203
goal Set.thy
clasohm@923
   204
 "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
berghofe@1754
   205
by (Fast_tac 1);
clasohm@923
   206
qed "Un_Int_crazy";
clasohm@923
   207
clasohm@923
   208
goal Set.thy "(A<=B) = (A Un B = B)";
berghofe@1754
   209
by (fast_tac (!claset addSEs [equalityE]) 1);
clasohm@923
   210
qed "subset_Un_eq";
clasohm@923
   211
clasohm@923
   212
goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
berghofe@1754
   213
by (Fast_tac 1);
clasohm@923
   214
qed "subset_insert_iff";
clasohm@923
   215
clasohm@923
   216
goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
berghofe@1754
   217
by (fast_tac (!claset addEs [equalityCE]) 1);
clasohm@923
   218
qed "Un_empty";
nipkow@1531
   219
Addsimps[Un_empty];
clasohm@923
   220
nipkow@1548
   221
section "Compl";
clasohm@923
   222
clasohm@923
   223
goal Set.thy "A Int Compl(A) = {}";
berghofe@1754
   224
by (Fast_tac 1);
clasohm@923
   225
qed "Compl_disjoint";
nipkow@1531
   226
Addsimps[Compl_disjoint];
clasohm@923
   227
nipkow@1531
   228
goal Set.thy "A Un Compl(A) = UNIV";
berghofe@1754
   229
by (Fast_tac 1);
clasohm@923
   230
qed "Compl_partition";
clasohm@923
   231
clasohm@923
   232
goal Set.thy "Compl(Compl(A)) = A";
berghofe@1754
   233
by (Fast_tac 1);
clasohm@923
   234
qed "double_complement";
nipkow@1531
   235
Addsimps[double_complement];
clasohm@923
   236
clasohm@923
   237
goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
berghofe@1754
   238
by (Fast_tac 1);
clasohm@923
   239
qed "Compl_Un";
clasohm@923
   240
clasohm@923
   241
goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
berghofe@1754
   242
by (Fast_tac 1);
clasohm@923
   243
qed "Compl_Int";
clasohm@923
   244
clasohm@923
   245
goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
berghofe@1754
   246
by (Fast_tac 1);
clasohm@923
   247
qed "Compl_UN";
clasohm@923
   248
clasohm@923
   249
goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
berghofe@1754
   250
by (Fast_tac 1);
clasohm@923
   251
qed "Compl_INT";
clasohm@923
   252
clasohm@923
   253
(*Halmos, Naive Set Theory, page 16.*)
clasohm@923
   254
clasohm@923
   255
goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
berghofe@1754
   256
by (fast_tac (!claset addSEs [equalityE]) 1);
clasohm@923
   257
qed "Un_Int_assoc_eq";
clasohm@923
   258
clasohm@923
   259
nipkow@1548
   260
section "Union";
clasohm@923
   261
clasohm@923
   262
goal Set.thy "Union({}) = {}";
berghofe@1754
   263
by (Fast_tac 1);
clasohm@923
   264
qed "Union_empty";
nipkow@1531
   265
Addsimps[Union_empty];
nipkow@1531
   266
nipkow@1531
   267
goal Set.thy "Union(UNIV) = UNIV";
berghofe@1754
   268
by (Fast_tac 1);
nipkow@1531
   269
qed "Union_UNIV";
nipkow@1531
   270
Addsimps[Union_UNIV];
clasohm@923
   271
clasohm@923
   272
goal Set.thy "Union(insert a B) = a Un Union(B)";
berghofe@1754
   273
by (Fast_tac 1);
clasohm@923
   274
qed "Union_insert";
nipkow@1531
   275
Addsimps[Union_insert];
clasohm@923
   276
clasohm@923
   277
goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
berghofe@1754
   278
by (Fast_tac 1);
clasohm@923
   279
qed "Union_Un_distrib";
nipkow@1531
   280
Addsimps[Union_Un_distrib];
clasohm@923
   281
clasohm@923
   282
goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
berghofe@1754
   283
by (Fast_tac 1);
clasohm@923
   284
qed "Union_Int_subset";
clasohm@923
   285
clasohm@923
   286
val prems = goal Set.thy
clasohm@923
   287
   "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
berghofe@1754
   288
by (fast_tac (!claset addSEs [equalityE]) 1);
clasohm@923
   289
qed "Union_disjoint";
clasohm@923
   290
nipkow@1548
   291
section "Inter";
nipkow@1548
   292
nipkow@1531
   293
goal Set.thy "Inter({}) = UNIV";
berghofe@1754
   294
by (Fast_tac 1);
nipkow@1531
   295
qed "Inter_empty";
nipkow@1531
   296
Addsimps[Inter_empty];
nipkow@1531
   297
nipkow@1531
   298
goal Set.thy "Inter(UNIV) = {}";
berghofe@1754
   299
by (Fast_tac 1);
nipkow@1531
   300
qed "Inter_UNIV";
nipkow@1531
   301
Addsimps[Inter_UNIV];
nipkow@1531
   302
nipkow@1531
   303
goal Set.thy "Inter(insert a B) = a Int Inter(B)";
berghofe@1754
   304
by (Fast_tac 1);
nipkow@1531
   305
qed "Inter_insert";
nipkow@1531
   306
Addsimps[Inter_insert];
nipkow@1531
   307
paulson@1564
   308
goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
berghofe@1754
   309
by (Fast_tac 1);
paulson@1564
   310
qed "Inter_Un_subset";
nipkow@1531
   311
clasohm@923
   312
goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
clasohm@923
   313
by (best_tac eq_cs 1);
clasohm@923
   314
qed "Inter_Un_distrib";
clasohm@923
   315
nipkow@1548
   316
section "UN and INT";
clasohm@923
   317
clasohm@923
   318
(*Basic identities*)
clasohm@923
   319
nipkow@1179
   320
goal Set.thy "(UN x:{}. B x) = {}";
berghofe@1754
   321
by (Fast_tac 1);
nipkow@1179
   322
qed "UN_empty";
nipkow@1531
   323
Addsimps[UN_empty];
nipkow@1531
   324
nipkow@1531
   325
goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
berghofe@1754
   326
by (Fast_tac 1);
nipkow@1531
   327
qed "UN_UNIV";
nipkow@1531
   328
Addsimps[UN_UNIV];
nipkow@1531
   329
nipkow@1531
   330
goal Set.thy "(INT x:{}. B x) = UNIV";
berghofe@1754
   331
by (Fast_tac 1);
nipkow@1531
   332
qed "INT_empty";
nipkow@1531
   333
Addsimps[INT_empty];
nipkow@1531
   334
nipkow@1531
   335
goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
berghofe@1754
   336
by (Fast_tac 1);
nipkow@1531
   337
qed "INT_UNIV";
nipkow@1531
   338
Addsimps[INT_UNIV];
nipkow@1179
   339
nipkow@1179
   340
goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
berghofe@1754
   341
by (Fast_tac 1);
nipkow@1179
   342
qed "UN_insert";
nipkow@1531
   343
Addsimps[UN_insert];
nipkow@1531
   344
nipkow@1531
   345
goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
berghofe@1754
   346
by (Fast_tac 1);
nipkow@1531
   347
qed "INT_insert";
nipkow@1531
   348
Addsimps[INT_insert];
nipkow@1179
   349
clasohm@923
   350
goal Set.thy "Union(range(f)) = (UN x.f(x))";
berghofe@1754
   351
by (Fast_tac 1);
clasohm@923
   352
qed "Union_range_eq";
clasohm@923
   353
clasohm@923
   354
goal Set.thy "Inter(range(f)) = (INT x.f(x))";
berghofe@1754
   355
by (Fast_tac 1);
clasohm@923
   356
qed "Inter_range_eq";
clasohm@923
   357
clasohm@923
   358
goal Set.thy "Union(B``A) = (UN x:A. B(x))";
berghofe@1754
   359
by (Fast_tac 1);
clasohm@923
   360
qed "Union_image_eq";
clasohm@923
   361
clasohm@923
   362
goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
berghofe@1754
   363
by (Fast_tac 1);
clasohm@923
   364
qed "Inter_image_eq";
clasohm@923
   365
clasohm@923
   366
goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
berghofe@1754
   367
by (Fast_tac 1);
clasohm@923
   368
qed "UN_constant";
clasohm@923
   369
clasohm@923
   370
goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
berghofe@1754
   371
by (Fast_tac 1);
clasohm@923
   372
qed "INT_constant";
clasohm@923
   373
clasohm@923
   374
goal Set.thy "(UN x.B) = B";
berghofe@1754
   375
by (Fast_tac 1);
clasohm@923
   376
qed "UN1_constant";
nipkow@1531
   377
Addsimps[UN1_constant];
clasohm@923
   378
clasohm@923
   379
goal Set.thy "(INT x.B) = B";
berghofe@1754
   380
by (Fast_tac 1);
clasohm@923
   381
qed "INT1_constant";
nipkow@1531
   382
Addsimps[INT1_constant];
clasohm@923
   383
clasohm@923
   384
goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
berghofe@1754
   385
by (Fast_tac 1);
clasohm@923
   386
qed "UN_eq";
clasohm@923
   387
clasohm@923
   388
(*Look: it has an EXISTENTIAL quantifier*)
clasohm@923
   389
goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
berghofe@1754
   390
by (Fast_tac 1);
clasohm@923
   391
qed "INT_eq";
clasohm@923
   392
clasohm@923
   393
(*Distributive laws...*)
clasohm@923
   394
clasohm@923
   395
goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
berghofe@1754
   396
by (Fast_tac 1);
clasohm@923
   397
qed "Int_Union";
clasohm@923
   398
clasohm@923
   399
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
clasohm@923
   400
   Union of a family of unions **)
clasohm@923
   401
goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
berghofe@1754
   402
by (Fast_tac 1);
clasohm@923
   403
qed "Un_Union_image";
clasohm@923
   404
clasohm@923
   405
(*Equivalent version*)
clasohm@923
   406
goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
berghofe@1754
   407
by (Fast_tac 1);
clasohm@923
   408
qed "UN_Un_distrib";
clasohm@923
   409
clasohm@923
   410
goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
berghofe@1754
   411
by (Fast_tac 1);
clasohm@923
   412
qed "Un_Inter";
clasohm@923
   413
clasohm@923
   414
goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
clasohm@923
   415
by (best_tac eq_cs 1);
clasohm@923
   416
qed "Int_Inter_image";
clasohm@923
   417
clasohm@923
   418
(*Equivalent version*)
clasohm@923
   419
goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
berghofe@1754
   420
by (Fast_tac 1);
clasohm@923
   421
qed "INT_Int_distrib";
clasohm@923
   422
clasohm@923
   423
(*Halmos, Naive Set Theory, page 35.*)
clasohm@923
   424
goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
berghofe@1754
   425
by (Fast_tac 1);
clasohm@923
   426
qed "Int_UN_distrib";
clasohm@923
   427
clasohm@923
   428
goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
berghofe@1754
   429
by (Fast_tac 1);
clasohm@923
   430
qed "Un_INT_distrib";
clasohm@923
   431
clasohm@923
   432
goal Set.thy
clasohm@923
   433
    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
berghofe@1754
   434
by (Fast_tac 1);
clasohm@923
   435
qed "Int_UN_distrib2";
clasohm@923
   436
clasohm@923
   437
goal Set.thy
clasohm@923
   438
    "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
berghofe@1754
   439
by (Fast_tac 1);
clasohm@923
   440
qed "Un_INT_distrib2";
clasohm@923
   441
nipkow@1548
   442
section "-";
clasohm@923
   443
clasohm@923
   444
goal Set.thy "A-A = {}";
berghofe@1754
   445
by (Fast_tac 1);
clasohm@923
   446
qed "Diff_cancel";
nipkow@1531
   447
Addsimps[Diff_cancel];
clasohm@923
   448
clasohm@923
   449
goal Set.thy "{}-A = {}";
berghofe@1754
   450
by (Fast_tac 1);
clasohm@923
   451
qed "empty_Diff";
nipkow@1531
   452
Addsimps[empty_Diff];
clasohm@923
   453
clasohm@923
   454
goal Set.thy "A-{} = A";
berghofe@1754
   455
by (Fast_tac 1);
clasohm@923
   456
qed "Diff_empty";
nipkow@1531
   457
Addsimps[Diff_empty];
nipkow@1531
   458
nipkow@1531
   459
goal Set.thy "A-UNIV = {}";
berghofe@1754
   460
by (Fast_tac 1);
nipkow@1531
   461
qed "Diff_UNIV";
nipkow@1531
   462
Addsimps[Diff_UNIV];
nipkow@1531
   463
nipkow@1531
   464
goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
berghofe@1754
   465
by (Fast_tac 1);
nipkow@1531
   466
qed "Diff_insert0";
nipkow@1531
   467
Addsimps [Diff_insert0];
clasohm@923
   468
clasohm@923
   469
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
clasohm@923
   470
goal Set.thy "A - insert a B = A - B - {a}";
berghofe@1754
   471
by (Fast_tac 1);
clasohm@923
   472
qed "Diff_insert";
clasohm@923
   473
clasohm@923
   474
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
clasohm@923
   475
goal Set.thy "A - insert a B = A - {a} - B";
berghofe@1754
   476
by (Fast_tac 1);
clasohm@923
   477
qed "Diff_insert2";
clasohm@923
   478
nipkow@1531
   479
goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
paulson@1553
   480
by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
berghofe@1754
   481
by (Fast_tac 1);
nipkow@1531
   482
qed "insert_Diff_if";
nipkow@1531
   483
nipkow@1531
   484
goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
berghofe@1754
   485
by (Fast_tac 1);
nipkow@1531
   486
qed "insert_Diff1";
nipkow@1531
   487
Addsimps [insert_Diff1];
nipkow@1531
   488
clasohm@923
   489
val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
berghofe@1754
   490
by (fast_tac (!claset addSIs prems) 1);
clasohm@923
   491
qed "insert_Diff";
clasohm@923
   492
clasohm@923
   493
goal Set.thy "A Int (B-A) = {}";
berghofe@1754
   494
by (Fast_tac 1);
clasohm@923
   495
qed "Diff_disjoint";
nipkow@1531
   496
Addsimps[Diff_disjoint];
clasohm@923
   497
clasohm@923
   498
goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
berghofe@1754
   499
by (Fast_tac 1);
clasohm@923
   500
qed "Diff_partition";
clasohm@923
   501
clasohm@923
   502
goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
berghofe@1754
   503
by (Fast_tac 1);
clasohm@923
   504
qed "double_diff";
clasohm@923
   505
clasohm@923
   506
goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
berghofe@1754
   507
by (Fast_tac 1);
clasohm@923
   508
qed "Diff_Un";
clasohm@923
   509
clasohm@923
   510
goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
berghofe@1754
   511
by (Fast_tac 1);
clasohm@923
   512
qed "Diff_Int";
clasohm@923
   513
nipkow@1531
   514
Addsimps[subset_UNIV, empty_subsetI, subset_refl];