src/HOL/equalities.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 6007 91070f559b4d
child 6283 e3096df44326
permissions -rw-r--r--
tidying
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
wenzelm@5069
    15
Goal "{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
wenzelm@5069
    20
Goal "(A <= {}) = (A = {})";
paulson@2891
    21
by (Blast_tac 1);
nipkow@1531
    22
qed "subset_empty";
nipkow@1531
    23
Addsimps [subset_empty];
nipkow@1531
    24
wenzelm@5069
    25
Goalw [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
wenzelm@5069
    30
Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";
paulson@4748
    31
by (Blast_tac 1);
paulson@4748
    32
qed "Collect_disj_eq";
paulson@4748
    33
wenzelm@5069
    34
Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}";
paulson@4748
    35
by (Blast_tac 1);
paulson@4748
    36
qed "Collect_conj_eq";
paulson@4748
    37
paulson@4748
    38
nipkow@1548
    39
section "insert";
clasohm@923
    40
nipkow@1531
    41
(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
wenzelm@5069
    42
Goal "insert a A = {a} Un A";
paulson@2891
    43
by (Blast_tac 1);
nipkow@1531
    44
qed "insert_is_Un";
nipkow@1531
    45
wenzelm@5069
    46
Goal "insert a A ~= {}";
wenzelm@4089
    47
by (blast_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
paulson@5143
    54
Goal "a:A ==> insert a A = A";
paulson@2891
    55
by (Blast_tac 1);
clasohm@923
    56
qed "insert_absorb";
nipkow@4605
    57
(* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls
nipkow@4605
    58
   in case of nested inserts!
nipkow@4605
    59
*)
clasohm@923
    60
wenzelm@5069
    61
Goal "insert x (insert x A) = insert x A";
paulson@2891
    62
by (Blast_tac 1);
nipkow@1531
    63
qed "insert_absorb2";
nipkow@1531
    64
Addsimps [insert_absorb2];
nipkow@1531
    65
wenzelm@5069
    66
Goal "insert x (insert y A) = insert y (insert x A)";
paulson@2891
    67
by (Blast_tac 1);
paulson@1879
    68
qed "insert_commute";
paulson@1879
    69
wenzelm@5069
    70
Goal "(insert x A <= B) = (x:B & A <= B)";
paulson@2891
    71
by (Blast_tac 1);
clasohm@923
    72
qed "insert_subset";
nipkow@1531
    73
Addsimps[insert_subset];
nipkow@1531
    74
paulson@5143
    75
Goal "insert a A ~= insert a B ==> A ~= B";
nipkow@3222
    76
by (Blast_tac 1);
nipkow@3222
    77
qed "insert_lim";
nipkow@3222
    78
nipkow@1531
    79
(* use new B rather than (A-{a}) to avoid infinite unfolding *)
paulson@5143
    80
Goal "a:A ==> ? B. A = insert a B & a ~: B";
paulson@1553
    81
by (res_inst_tac [("x","A-{a}")] exI 1);
paulson@2891
    82
by (Blast_tac 1);
nipkow@1531
    83
qed "mk_disjoint_insert";
clasohm@923
    84
oheimb@4882
    85
bind_thm ("insert_Collect", prove_goal thy 
paulson@5590
    86
	  "insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
oheimb@4882
    87
paulson@5941
    88
Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
paulson@2891
    89
by (Blast_tac 1);
paulson@1843
    90
qed "UN_insert_distrib";
paulson@1843
    91
oheimb@1660
    92
section "``";
clasohm@923
    93
wenzelm@5069
    94
Goal "f``{} = {}";
paulson@2891
    95
by (Blast_tac 1);
clasohm@923
    96
qed "image_empty";
nipkow@1531
    97
Addsimps[image_empty];
clasohm@923
    98
wenzelm@5069
    99
Goal "f``insert a B = insert (f a) (f``B)";
paulson@2891
   100
by (Blast_tac 1);
clasohm@923
   101
qed "image_insert";
nipkow@1531
   102
Addsimps[image_insert];
clasohm@923
   103
wenzelm@5069
   104
Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
nipkow@3222
   105
by (Blast_tac 1);
nipkow@3222
   106
qed "image_UNION";
nipkow@3222
   107
wenzelm@5069
   108
Goal "(%x. x) `` Y = Y";
nipkow@3222
   109
by (Blast_tac 1);
nipkow@3222
   110
qed "image_id";
paulson@5967
   111
Addsimps [image_id];
nipkow@3222
   112
wenzelm@5069
   113
Goal "f``(g``A) = (%x. f (g x)) `` A";
paulson@3457
   114
by (Blast_tac 1);
paulson@4059
   115
qed "image_image";
nipkow@3222
   116
paulson@5143
   117
Goal "x:A ==> insert (f x) (f``A) = f``A";
paulson@2891
   118
by (Blast_tac 1);
paulson@1884
   119
qed "insert_image";
paulson@1884
   120
Addsimps [insert_image];
paulson@1884
   121
wenzelm@5069
   122
Goal "(f``A = {}) = (A = {})";
paulson@4306
   123
by (blast_tac (claset() addSEs [equalityCE]) 1);
nipkow@3415
   124
qed "image_is_empty";
nipkow@3415
   125
AddIffs [image_is_empty];
nipkow@3415
   126
nipkow@5281
   127
Goal "f `` {x. P x} = {f x | x. P x}";
paulson@5319
   128
by (Blast_tac 1);
nipkow@5281
   129
qed "image_Collect";
nipkow@5281
   130
Addsimps [image_Collect];
nipkow@5281
   131
paulson@5590
   132
Goalw [image_def] "(%x. if P x then f x else g x) `` S   \
paulson@5590
   133
\                = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";
nipkow@4686
   134
by (Simp_tac 1);
paulson@2891
   135
by (Blast_tac 1);
nipkow@1748
   136
qed "if_image_distrib";
nipkow@1748
   137
Addsimps[if_image_distrib];
nipkow@1748
   138
paulson@5590
   139
val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
oheimb@4136
   140
by (rtac set_ext 1);
oheimb@4136
   141
by (simp_tac (simpset() addsimps image_def::prems) 1);
oheimb@4136
   142
qed "image_cong";
oheimb@4136
   143
nipkow@1748
   144
nipkow@1548
   145
section "Int";
clasohm@923
   146
wenzelm@5069
   147
Goal "A Int A = A";
paulson@2891
   148
by (Blast_tac 1);
clasohm@923
   149
qed "Int_absorb";
nipkow@1531
   150
Addsimps[Int_absorb];
clasohm@923
   151
paulson@5590
   152
Goal "A Int (A Int B) = A Int B";
paulson@4609
   153
by (Blast_tac 1);
paulson@4609
   154
qed "Int_left_absorb";
paulson@4609
   155
paulson@5590
   156
Goal "A Int B = B Int A";
paulson@2891
   157
by (Blast_tac 1);
clasohm@923
   158
qed "Int_commute";
clasohm@923
   159
wenzelm@5069
   160
Goal "A Int (B Int C) = B Int (A Int C)";
paulson@4609
   161
by (Blast_tac 1);
paulson@4609
   162
qed "Int_left_commute";
paulson@4609
   163
paulson@5590
   164
Goal "(A Int B) Int C = A Int (B Int C)";
paulson@2891
   165
by (Blast_tac 1);
clasohm@923
   166
qed "Int_assoc";
clasohm@923
   167
paulson@4609
   168
(*Intersection is an AC-operator*)
paulson@4609
   169
val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
paulson@4609
   170
paulson@5143
   171
Goal "B<=A ==> A Int B = B";
paulson@4662
   172
by (Blast_tac 1);
paulson@4662
   173
qed "Int_absorb1";
paulson@4662
   174
paulson@5143
   175
Goal "A<=B ==> A Int B = A";
paulson@4662
   176
by (Blast_tac 1);
paulson@4662
   177
qed "Int_absorb2";
paulson@4662
   178
wenzelm@5069
   179
Goal "{} Int B = {}";
paulson@2891
   180
by (Blast_tac 1);
clasohm@923
   181
qed "Int_empty_left";
nipkow@1531
   182
Addsimps[Int_empty_left];
clasohm@923
   183
wenzelm@5069
   184
Goal "A Int {} = {}";
paulson@2891
   185
by (Blast_tac 1);
clasohm@923
   186
qed "Int_empty_right";
nipkow@1531
   187
Addsimps[Int_empty_right];
nipkow@1531
   188
paulson@5490
   189
Goal "(A Int B = {}) = (A <= -B)";
paulson@4306
   190
by (blast_tac (claset() addSEs [equalityCE]) 1);
paulson@3356
   191
qed "disjoint_eq_subset_Compl";
paulson@3356
   192
wenzelm@5069
   193
Goal "UNIV Int B = B";
paulson@2891
   194
by (Blast_tac 1);
nipkow@1531
   195
qed "Int_UNIV_left";
nipkow@1531
   196
Addsimps[Int_UNIV_left];
nipkow@1531
   197
wenzelm@5069
   198
Goal "A Int UNIV = A";
paulson@2891
   199
by (Blast_tac 1);
nipkow@1531
   200
qed "Int_UNIV_right";
nipkow@1531
   201
Addsimps[Int_UNIV_right];
clasohm@923
   202
wenzelm@5069
   203
Goal "A Int B = Inter{A,B}";
paulson@4634
   204
by (Blast_tac 1);
paulson@4634
   205
qed "Int_eq_Inter";
paulson@4634
   206
paulson@5590
   207
Goal "A Int (B Un C) = (A Int B) Un (A Int C)";
paulson@2891
   208
by (Blast_tac 1);
clasohm@923
   209
qed "Int_Un_distrib";
clasohm@923
   210
paulson@5590
   211
Goal "(B Un C) Int A = (B Int A) Un (C Int A)";
paulson@2891
   212
by (Blast_tac 1);
paulson@1618
   213
qed "Int_Un_distrib2";
paulson@1618
   214
wenzelm@5069
   215
Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
wenzelm@4089
   216
by (blast_tac (claset() addEs [equalityCE]) 1);
nipkow@1531
   217
qed "Int_UNIV";
nipkow@1531
   218
Addsimps[Int_UNIV];
nipkow@1531
   219
paulson@5319
   220
Goal "(C <= A Int B) = (C <= A & C <= B)";
paulson@5319
   221
by (Blast_tac 1);
paulson@5319
   222
qed "Int_subset_iff";
paulson@5319
   223
paulson@5319
   224
nipkow@1548
   225
section "Un";
clasohm@923
   226
wenzelm@5069
   227
Goal "A Un A = A";
paulson@2891
   228
by (Blast_tac 1);
clasohm@923
   229
qed "Un_absorb";
nipkow@1531
   230
Addsimps[Un_absorb];
clasohm@923
   231
wenzelm@5069
   232
Goal " A Un (A Un B) = A Un B";
nipkow@3222
   233
by (Blast_tac 1);
nipkow@3222
   234
qed "Un_left_absorb";
nipkow@3222
   235
paulson@5590
   236
Goal "A Un B = B Un A";
paulson@2891
   237
by (Blast_tac 1);
clasohm@923
   238
qed "Un_commute";
clasohm@923
   239
wenzelm@5069
   240
Goal "A Un (B Un C) = B Un (A Un C)";
nipkow@3222
   241
by (Blast_tac 1);
nipkow@3222
   242
qed "Un_left_commute";
nipkow@3222
   243
paulson@5590
   244
Goal "(A Un B) Un C = A Un (B Un C)";
paulson@2891
   245
by (Blast_tac 1);
clasohm@923
   246
qed "Un_assoc";
clasohm@923
   247
paulson@4609
   248
(*Union is an AC-operator*)
paulson@4609
   249
val Un_ac = [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute];
paulson@4609
   250
paulson@5143
   251
Goal "A<=B ==> A Un B = B";
paulson@4662
   252
by (Blast_tac 1);
paulson@4662
   253
qed "Un_absorb1";
paulson@4662
   254
paulson@5143
   255
Goal "B<=A ==> A Un B = A";
paulson@4662
   256
by (Blast_tac 1);
paulson@4662
   257
qed "Un_absorb2";
paulson@4662
   258
wenzelm@5069
   259
Goal "{} Un B = B";
paulson@2891
   260
by (Blast_tac 1);
clasohm@923
   261
qed "Un_empty_left";
nipkow@1531
   262
Addsimps[Un_empty_left];
clasohm@923
   263
wenzelm@5069
   264
Goal "A Un {} = A";
paulson@2891
   265
by (Blast_tac 1);
clasohm@923
   266
qed "Un_empty_right";
nipkow@1531
   267
Addsimps[Un_empty_right];
nipkow@1531
   268
wenzelm@5069
   269
Goal "UNIV Un B = UNIV";
paulson@2891
   270
by (Blast_tac 1);
nipkow@1531
   271
qed "Un_UNIV_left";
nipkow@1531
   272
Addsimps[Un_UNIV_left];
nipkow@1531
   273
wenzelm@5069
   274
Goal "A Un UNIV = UNIV";
paulson@2891
   275
by (Blast_tac 1);
nipkow@1531
   276
qed "Un_UNIV_right";
nipkow@1531
   277
Addsimps[Un_UNIV_right];
clasohm@923
   278
wenzelm@5069
   279
Goal "A Un B = Union{A,B}";
paulson@4634
   280
by (Blast_tac 1);
paulson@4634
   281
qed "Un_eq_Union";
paulson@4634
   282
wenzelm@5069
   283
Goal "(insert a B) Un C = insert a (B Un C)";
paulson@2891
   284
by (Blast_tac 1);
clasohm@923
   285
qed "Un_insert_left";
paulson@3384
   286
Addsimps[Un_insert_left];
clasohm@923
   287
wenzelm@5069
   288
Goal "A Un (insert a B) = insert a (A Un B)";
paulson@2891
   289
by (Blast_tac 1);
paulson@1917
   290
qed "Un_insert_right";
paulson@3384
   291
Addsimps[Un_insert_right];
paulson@1917
   292
wenzelm@5069
   293
Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \
paulson@5590
   294
\                                  else        B Int C)";
nipkow@4686
   295
by (Simp_tac 1);
paulson@3356
   296
by (Blast_tac 1);
paulson@3356
   297
qed "Int_insert_left";
paulson@3356
   298
wenzelm@5069
   299
Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \
paulson@5590
   300
\                                  else        A Int B)";
nipkow@4686
   301
by (Simp_tac 1);
paulson@3356
   302
by (Blast_tac 1);
paulson@3356
   303
qed "Int_insert_right";
paulson@3356
   304
paulson@5590
   305
Goal "A Un (B Int C) = (A Un B) Int (A Un C)";
paulson@2891
   306
by (Blast_tac 1);
clasohm@923
   307
qed "Un_Int_distrib";
clasohm@923
   308
paulson@5590
   309
Goal "(B Int C) Un A = (B Un A) Int (C Un A)";
paulson@4609
   310
by (Blast_tac 1);
paulson@4609
   311
qed "Un_Int_distrib2";
paulson@4609
   312
paulson@5590
   313
Goal "(A Int B) Un (B Int C) Un (C Int A) = \
paulson@5590
   314
\     (A Un B) Int (B Un C) Int (C Un A)";
paulson@2891
   315
by (Blast_tac 1);
clasohm@923
   316
qed "Un_Int_crazy";
clasohm@923
   317
wenzelm@5069
   318
Goal "(A<=B) = (A Un B = B)";
paulson@4306
   319
by (blast_tac (claset() addSEs [equalityCE]) 1);
clasohm@923
   320
qed "subset_Un_eq";
clasohm@923
   321
wenzelm@5069
   322
Goal "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
paulson@2891
   323
by (Blast_tac 1);
clasohm@923
   324
qed "subset_insert_iff";
clasohm@923
   325
wenzelm@5069
   326
Goal "(A Un B = {}) = (A = {} & B = {})";
wenzelm@4089
   327
by (blast_tac (claset() addEs [equalityCE]) 1);
clasohm@923
   328
qed "Un_empty";
nipkow@1531
   329
Addsimps[Un_empty];
clasohm@923
   330
paulson@5319
   331
Goal "(A Un B <= C) = (A <= C & B <= C)";
paulson@5319
   332
by (Blast_tac 1);
paulson@5319
   333
qed "Un_subset_iff";
paulson@5319
   334
paulson@5331
   335
Goal "(A - B) Un (A Int B) = A";
paulson@5331
   336
by (Blast_tac 1);
paulson@5331
   337
qed "Un_Diff_Int";
paulson@5331
   338
paulson@5319
   339
paulson@5931
   340
section "Set complement";
clasohm@923
   341
paulson@5490
   342
Goal "A Int -A = {}";
paulson@2891
   343
by (Blast_tac 1);
clasohm@923
   344
qed "Compl_disjoint";
nipkow@1531
   345
Addsimps[Compl_disjoint];
clasohm@923
   346
paulson@5490
   347
Goal "A Un -A = UNIV";
paulson@2891
   348
by (Blast_tac 1);
clasohm@923
   349
qed "Compl_partition";
clasohm@923
   350
paulson@5490
   351
Goal "- -A = (A:: 'a set)";
paulson@2891
   352
by (Blast_tac 1);
clasohm@923
   353
qed "double_complement";
nipkow@1531
   354
Addsimps[double_complement];
clasohm@923
   355
paulson@5490
   356
Goal "-(A Un B) = -A Int -B";
paulson@2891
   357
by (Blast_tac 1);
clasohm@923
   358
qed "Compl_Un";
clasohm@923
   359
paulson@5490
   360
Goal "-(A Int B) = -A Un -B";
paulson@2891
   361
by (Blast_tac 1);
clasohm@923
   362
qed "Compl_Int";
clasohm@923
   363
paulson@5490
   364
Goal "-(UN x:A. B(x)) = (INT x:A. -B(x))";
paulson@2891
   365
by (Blast_tac 1);
clasohm@923
   366
qed "Compl_UN";
clasohm@923
   367
paulson@5490
   368
Goal "-(INT x:A. B(x)) = (UN x:A. -B(x))";
paulson@2891
   369
by (Blast_tac 1);
clasohm@923
   370
qed "Compl_INT";
clasohm@923
   371
paulson@4615
   372
Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
paulson@4615
   373
clasohm@923
   374
(*Halmos, Naive Set Theory, page 16.*)
clasohm@923
   375
wenzelm@5069
   376
Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
paulson@4306
   377
by (blast_tac (claset() addSEs [equalityCE]) 1);
clasohm@923
   378
qed "Un_Int_assoc_eq";
clasohm@923
   379
clasohm@923
   380
nipkow@1548
   381
section "Union";
clasohm@923
   382
wenzelm@5069
   383
Goal "Union({}) = {}";
paulson@2891
   384
by (Blast_tac 1);
clasohm@923
   385
qed "Union_empty";
nipkow@1531
   386
Addsimps[Union_empty];
nipkow@1531
   387
wenzelm@5069
   388
Goal "Union(UNIV) = UNIV";
paulson@2891
   389
by (Blast_tac 1);
nipkow@1531
   390
qed "Union_UNIV";
nipkow@1531
   391
Addsimps[Union_UNIV];
clasohm@923
   392
wenzelm@5069
   393
Goal "Union(insert a B) = a Un Union(B)";
paulson@2891
   394
by (Blast_tac 1);
clasohm@923
   395
qed "Union_insert";
nipkow@1531
   396
Addsimps[Union_insert];
clasohm@923
   397
wenzelm@5069
   398
Goal "Union(A Un B) = Union(A) Un Union(B)";
paulson@2891
   399
by (Blast_tac 1);
clasohm@923
   400
qed "Union_Un_distrib";
nipkow@1531
   401
Addsimps[Union_Un_distrib];
clasohm@923
   402
wenzelm@5069
   403
Goal "Union(A Int B) <= Union(A) Int Union(B)";
paulson@2891
   404
by (Blast_tac 1);
clasohm@923
   405
qed "Union_Int_subset";
clasohm@923
   406
wenzelm@5069
   407
Goal "(Union M = {}) = (! A : M. A = {})"; 
paulson@4306
   408
by (blast_tac (claset() addEs [equalityCE]) 1);
paulson@4306
   409
qed "Union_empty_conv"; 
nipkow@4003
   410
AddIffs [Union_empty_conv];
nipkow@4003
   411
wenzelm@5069
   412
Goal "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
paulson@4306
   413
by (blast_tac (claset() addSEs [equalityCE]) 1);
clasohm@923
   414
qed "Union_disjoint";
clasohm@923
   415
nipkow@1548
   416
section "Inter";
nipkow@1548
   417
wenzelm@5069
   418
Goal "Inter({}) = UNIV";
paulson@2891
   419
by (Blast_tac 1);
nipkow@1531
   420
qed "Inter_empty";
nipkow@1531
   421
Addsimps[Inter_empty];
nipkow@1531
   422
wenzelm@5069
   423
Goal "Inter(UNIV) = {}";
paulson@2891
   424
by (Blast_tac 1);
nipkow@1531
   425
qed "Inter_UNIV";
nipkow@1531
   426
Addsimps[Inter_UNIV];
nipkow@1531
   427
wenzelm@5069
   428
Goal "Inter(insert a B) = a Int Inter(B)";
paulson@2891
   429
by (Blast_tac 1);
nipkow@1531
   430
qed "Inter_insert";
nipkow@1531
   431
Addsimps[Inter_insert];
nipkow@1531
   432
wenzelm@5069
   433
Goal "Inter(A) Un Inter(B) <= Inter(A Int B)";
paulson@2891
   434
by (Blast_tac 1);
paulson@1564
   435
qed "Inter_Un_subset";
nipkow@1531
   436
wenzelm@5069
   437
Goal "Inter(A Un B) = Inter(A) Int Inter(B)";
paulson@2891
   438
by (Blast_tac 1);
clasohm@923
   439
qed "Inter_Un_distrib";
clasohm@923
   440
nipkow@1548
   441
section "UN and INT";
clasohm@923
   442
clasohm@923
   443
(*Basic identities*)
clasohm@923
   444
paulson@4200
   445
val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]);
oheimb@4136
   446
wenzelm@5069
   447
Goal "(UN x:{}. B x) = {}";
paulson@2891
   448
by (Blast_tac 1);
nipkow@1179
   449
qed "UN_empty";
nipkow@1531
   450
Addsimps[UN_empty];
nipkow@1531
   451
wenzelm@5069
   452
Goal "(UN x:A. {}) = {}";
paulson@3457
   453
by (Blast_tac 1);
nipkow@3222
   454
qed "UN_empty2";
nipkow@3222
   455
Addsimps[UN_empty2];
nipkow@3222
   456
wenzelm@5069
   457
Goal "(UN x:A. {x}) = A";
paulson@4645
   458
by (Blast_tac 1);
paulson@4645
   459
qed "UN_singleton";
paulson@4645
   460
Addsimps [UN_singleton];
paulson@4645
   461
paulson@5143
   462
Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
paulson@4634
   463
by (Blast_tac 1);
paulson@4634
   464
qed "UN_absorb";
paulson@4634
   465
wenzelm@5069
   466
Goal "(INT x:{}. B x) = UNIV";
paulson@2891
   467
by (Blast_tac 1);
nipkow@1531
   468
qed "INT_empty";
nipkow@1531
   469
Addsimps[INT_empty];
nipkow@1531
   470
paulson@5143
   471
Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
paulson@4634
   472
by (Blast_tac 1);
paulson@4634
   473
qed "INT_absorb";
paulson@4634
   474
wenzelm@5069
   475
Goal "(UN x:insert a A. B x) = B a Un UNION A B";
paulson@2891
   476
by (Blast_tac 1);
nipkow@1179
   477
qed "UN_insert";
nipkow@1531
   478
Addsimps[UN_insert];
nipkow@1531
   479
paulson@5999
   480
Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)";
nipkow@3222
   481
by (Blast_tac 1);
nipkow@3222
   482
qed "UN_Un";
nipkow@3222
   483
wenzelm@5069
   484
Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)";
paulson@4771
   485
by (Blast_tac 1);
paulson@4771
   486
qed "UN_UN_flatten";
paulson@4771
   487
wenzelm@5069
   488
Goal "(INT x:insert a A. B x) = B a Int INTER A B";
paulson@2891
   489
by (Blast_tac 1);
nipkow@1531
   490
qed "INT_insert";
nipkow@1531
   491
Addsimps[INT_insert];
nipkow@1179
   492
paulson@5999
   493
Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)";
paulson@5999
   494
by (Blast_tac 1);
paulson@5999
   495
qed "INT_Un";
paulson@5999
   496
paulson@5941
   497
Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
paulson@2891
   498
by (Blast_tac 1);
paulson@2021
   499
qed "INT_insert_distrib";
paulson@2021
   500
wenzelm@5069
   501
Goal "Union(B``A) = (UN x:A. B(x))";
paulson@2891
   502
by (Blast_tac 1);
clasohm@923
   503
qed "Union_image_eq";
clasohm@923
   504
wenzelm@5069
   505
Goal "Inter(B``A) = (INT x:A. B(x))";
paulson@2891
   506
by (Blast_tac 1);
clasohm@923
   507
qed "Inter_image_eq";
clasohm@923
   508
paulson@5941
   509
Goal "u: A ==> (UN y:A. c) = c";
paulson@2891
   510
by (Blast_tac 1);
clasohm@923
   511
qed "UN_constant";
paulson@4159
   512
Addsimps[UN_constant];
clasohm@923
   513
paulson@5941
   514
Goal "u: A ==> (INT y:A. c) = c";
paulson@2891
   515
by (Blast_tac 1);
clasohm@923
   516
qed "INT_constant";
paulson@4159
   517
Addsimps[INT_constant];
clasohm@923
   518
wenzelm@5069
   519
Goal "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
paulson@2891
   520
by (Blast_tac 1);
clasohm@923
   521
qed "UN_eq";
clasohm@923
   522
clasohm@923
   523
(*Look: it has an EXISTENTIAL quantifier*)
wenzelm@5069
   524
Goal "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
paulson@2891
   525
by (Blast_tac 1);
clasohm@923
   526
qed "INT_eq";
clasohm@923
   527
nipkow@3222
   528
clasohm@923
   529
(*Distributive laws...*)
clasohm@923
   530
wenzelm@5069
   531
Goal "A Int Union(B) = (UN C:B. A Int C)";
paulson@2891
   532
by (Blast_tac 1);
clasohm@923
   533
qed "Int_Union";
clasohm@923
   534
wenzelm@5069
   535
Goal "Union(B) Int A = (UN C:B. C Int A)";
paulson@4674
   536
by (Blast_tac 1);
paulson@4674
   537
qed "Int_Union2";
paulson@4674
   538
paulson@4306
   539
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
clasohm@923
   540
   Union of a family of unions **)
wenzelm@5069
   541
Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
paulson@2891
   542
by (Blast_tac 1);
clasohm@923
   543
qed "Un_Union_image";
clasohm@923
   544
clasohm@923
   545
(*Equivalent version*)
wenzelm@5069
   546
Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
paulson@2891
   547
by (Blast_tac 1);
clasohm@923
   548
qed "UN_Un_distrib";
clasohm@923
   549
wenzelm@5069
   550
Goal "A Un Inter(B) = (INT C:B. A Un C)";
paulson@2891
   551
by (Blast_tac 1);
clasohm@923
   552
qed "Un_Inter";
clasohm@923
   553
wenzelm@5069
   554
Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
paulson@2891
   555
by (Blast_tac 1);
clasohm@923
   556
qed "Int_Inter_image";
clasohm@923
   557
clasohm@923
   558
(*Equivalent version*)
wenzelm@5069
   559
Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
paulson@2891
   560
by (Blast_tac 1);
clasohm@923
   561
qed "INT_Int_distrib";
clasohm@923
   562
clasohm@923
   563
(*Halmos, Naive Set Theory, page 35.*)
wenzelm@5069
   564
Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
paulson@2891
   565
by (Blast_tac 1);
clasohm@923
   566
qed "Int_UN_distrib";
clasohm@923
   567
wenzelm@5069
   568
Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
paulson@2891
   569
by (Blast_tac 1);
clasohm@923
   570
qed "Un_INT_distrib";
clasohm@923
   571
paulson@5278
   572
Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
paulson@2891
   573
by (Blast_tac 1);
clasohm@923
   574
qed "Int_UN_distrib2";
clasohm@923
   575
paulson@5278
   576
Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
paulson@2891
   577
by (Blast_tac 1);
clasohm@923
   578
qed "Un_INT_distrib2";
clasohm@923
   579
nipkow@2512
   580
nipkow@2512
   581
section"Bounded quantifiers";
nipkow@2512
   582
nipkow@3860
   583
(** The following are not added to the default simpset because
nipkow@3860
   584
    (a) they duplicate the body and (b) there are no similar rules for Int. **)
nipkow@2512
   585
wenzelm@5069
   586
Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
paulson@2891
   587
by (Blast_tac 1);
paulson@2519
   588
qed "ball_Un";
paulson@2519
   589
wenzelm@5069
   590
Goal "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
paulson@2891
   591
by (Blast_tac 1);
paulson@2519
   592
qed "bex_Un";
nipkow@2512
   593
wenzelm@5069
   594
Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)";
paulson@4771
   595
by (Blast_tac 1);
paulson@4771
   596
qed "ball_UN";
paulson@4771
   597
wenzelm@5069
   598
Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)";
paulson@4771
   599
by (Blast_tac 1);
paulson@4771
   600
qed "bex_UN";
paulson@4771
   601
nipkow@2512
   602
nipkow@1548
   603
section "-";
clasohm@923
   604
paulson@5490
   605
Goal "A-B = A Int -B";
paulson@4609
   606
by (Blast_tac 1);
paulson@4662
   607
qed "Diff_eq";
paulson@4609
   608
wenzelm@5069
   609
Goal "A-A = {}";
paulson@2891
   610
by (Blast_tac 1);
clasohm@923
   611
qed "Diff_cancel";
nipkow@1531
   612
Addsimps[Diff_cancel];
clasohm@923
   613
paulson@5143
   614
Goal "A Int B = {} ==> A-B = A";
paulson@4674
   615
by (blast_tac (claset() addEs [equalityE]) 1);
paulson@4674
   616
qed "Diff_triv";
paulson@4674
   617
wenzelm@5069
   618
Goal "{}-A = {}";
paulson@2891
   619
by (Blast_tac 1);
clasohm@923
   620
qed "empty_Diff";
nipkow@1531
   621
Addsimps[empty_Diff];
clasohm@923
   622
wenzelm@5069
   623
Goal "A-{} = A";
paulson@2891
   624
by (Blast_tac 1);
clasohm@923
   625
qed "Diff_empty";
nipkow@1531
   626
Addsimps[Diff_empty];
nipkow@1531
   627
wenzelm@5069
   628
Goal "A-UNIV = {}";
paulson@2891
   629
by (Blast_tac 1);
nipkow@1531
   630
qed "Diff_UNIV";
nipkow@1531
   631
Addsimps[Diff_UNIV];
nipkow@1531
   632
paulson@5143
   633
Goal "x~:A ==> A - insert x B = A-B";
paulson@2891
   634
by (Blast_tac 1);
nipkow@1531
   635
qed "Diff_insert0";
nipkow@1531
   636
Addsimps [Diff_insert0];
clasohm@923
   637
clasohm@923
   638
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
wenzelm@5069
   639
Goal "A - insert a B = A - B - {a}";
paulson@2891
   640
by (Blast_tac 1);
clasohm@923
   641
qed "Diff_insert";
clasohm@923
   642
clasohm@923
   643
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
wenzelm@5069
   644
Goal "A - insert a B = A - {a} - B";
paulson@2891
   645
by (Blast_tac 1);
clasohm@923
   646
qed "Diff_insert2";
clasohm@923
   647
wenzelm@5069
   648
Goal "insert x A - B = (if x:B then A-B else insert x (A-B))";
nipkow@4686
   649
by (Simp_tac 1);
paulson@2891
   650
by (Blast_tac 1);
nipkow@1531
   651
qed "insert_Diff_if";
nipkow@1531
   652
paulson@5143
   653
Goal "x:B ==> insert x A - B = A-B";
paulson@2891
   654
by (Blast_tac 1);
nipkow@1531
   655
qed "insert_Diff1";
nipkow@1531
   656
Addsimps [insert_Diff1];
nipkow@1531
   657
paulson@5143
   658
Goal "a:A ==> insert a (A-{a}) = A";
paulson@2922
   659
by (Blast_tac 1);
clasohm@923
   660
qed "insert_Diff";
clasohm@923
   661
wenzelm@5069
   662
Goal "A Int (B-A) = {}";
paulson@2891
   663
by (Blast_tac 1);
clasohm@923
   664
qed "Diff_disjoint";
nipkow@1531
   665
Addsimps[Diff_disjoint];
clasohm@923
   666
paulson@5143
   667
Goal "A<=B ==> A Un (B-A) = B";
paulson@2891
   668
by (Blast_tac 1);
clasohm@923
   669
qed "Diff_partition";
clasohm@923
   670
paulson@5143
   671
Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
paulson@2891
   672
by (Blast_tac 1);
clasohm@923
   673
qed "double_diff";
clasohm@923
   674
wenzelm@5069
   675
Goal "A Un (B-A) = A Un B";
paulson@4645
   676
by (Blast_tac 1);
paulson@4645
   677
qed "Un_Diff_cancel";
paulson@4645
   678
wenzelm@5069
   679
Goal "(B-A) Un A = B Un A";
paulson@4645
   680
by (Blast_tac 1);
paulson@4645
   681
qed "Un_Diff_cancel2";
paulson@4645
   682
paulson@4645
   683
Addsimps [Un_Diff_cancel, Un_Diff_cancel2];
paulson@4645
   684
wenzelm@5069
   685
Goal "A - (B Un C) = (A-B) Int (A-C)";
paulson@2891
   686
by (Blast_tac 1);
clasohm@923
   687
qed "Diff_Un";
clasohm@923
   688
wenzelm@5069
   689
Goal "A - (B Int C) = (A-B) Un (A-C)";
paulson@2891
   690
by (Blast_tac 1);
clasohm@923
   691
qed "Diff_Int";
clasohm@923
   692
wenzelm@5069
   693
Goal "(A Un B) - C = (A - C) Un (B - C)";
nipkow@3222
   694
by (Blast_tac 1);
nipkow@3222
   695
qed "Un_Diff";
nipkow@3222
   696
wenzelm@5069
   697
Goal "(A Int B) - C = A Int (B - C)";
nipkow@3222
   698
by (Blast_tac 1);
nipkow@3222
   699
qed "Int_Diff";
nipkow@3222
   700
wenzelm@5069
   701
Goal "C Int (A-B) = (C Int A) - (C Int B)";
paulson@4748
   702
by (Blast_tac 1);
paulson@4748
   703
qed "Diff_Int_distrib";
paulson@4748
   704
wenzelm@5069
   705
Goal "(A-B) Int C = (A Int C) - (B Int C)";
paulson@4645
   706
by (Blast_tac 1);
paulson@4748
   707
qed "Diff_Int_distrib2";
paulson@4645
   708
paulson@5632
   709
Goal "A - - B = A Int B";
paulson@5632
   710
by Auto_tac;
paulson@5632
   711
qed "Diff_Compl";
paulson@5632
   712
Addsimps [Diff_Compl];
paulson@5632
   713
nipkow@3222
   714
paulson@5238
   715
section "Quantification over type \"bool\"";
paulson@5238
   716
paulson@5238
   717
Goal "(ALL b::bool. P b) = (P True & P False)";
paulson@5238
   718
by Auto_tac;
paulson@5238
   719
by (case_tac "b" 1);
paulson@5238
   720
by Auto_tac;
paulson@5238
   721
qed "all_bool_eq";
paulson@5238
   722
berghofe@5762
   723
bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec);
berghofe@5762
   724
paulson@5238
   725
Goal "(EX b::bool. P b) = (P True | P False)";
paulson@5238
   726
by Auto_tac;
paulson@5238
   727
by (case_tac "b" 1);
paulson@5238
   728
by Auto_tac;
paulson@5238
   729
qed "ex_bool_eq";
paulson@5238
   730
paulson@5238
   731
Goal "A Un B = (UN b. if b then A else B)";
oheimb@5521
   732
by(auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
paulson@5238
   733
qed "Un_eq_UN";
paulson@5238
   734
paulson@5238
   735
Goal "(UN b::bool. A b) = (A True Un A False)";
paulson@5238
   736
by Auto_tac;
paulson@5238
   737
by (case_tac "b" 1);
paulson@5238
   738
by Auto_tac;
paulson@5238
   739
qed "UN_bool_eq";
paulson@5238
   740
paulson@5238
   741
Goal "(INT b::bool. A b) = (A True Int A False)";
paulson@5238
   742
by Auto_tac;
paulson@5238
   743
by (case_tac "b" 1);
paulson@5238
   744
by Auto_tac;
paulson@5238
   745
qed "INT_bool_eq";
paulson@5238
   746
paulson@5238
   747
nipkow@3222
   748
section "Miscellany";
nipkow@3222
   749
wenzelm@5069
   750
Goal "(A = B) = ((A <= (B::'a set)) & (B<=A))";
nipkow@3222
   751
by (Blast_tac 1);
nipkow@3222
   752
qed "set_eq_subset";
nipkow@3222
   753
wenzelm@5069
   754
Goal "A <= B =  (! t. t:A --> t:B)";
nipkow@3222
   755
by (Blast_tac 1);
nipkow@3222
   756
qed "subset_iff";
nipkow@3222
   757
wenzelm@5069
   758
Goalw [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
nipkow@3222
   759
by (Blast_tac 1);
nipkow@3222
   760
qed "subset_iff_psubset_eq";
paulson@2021
   761
wenzelm@5069
   762
Goal "(!x. x ~: A) = (A={})";
wenzelm@4423
   763
by (Blast_tac 1);
nipkow@3896
   764
qed "all_not_in_conv";
nipkow@3907
   765
AddIffs [all_not_in_conv];
nipkow@3896
   766
wenzelm@5069
   767
Goalw [Pow_def] "Pow {} = {{}}";
paulson@4477
   768
by Auto_tac;
paulson@3348
   769
qed "Pow_empty";
paulson@3348
   770
Addsimps [Pow_empty];
paulson@3348
   771
wenzelm@5069
   772
Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
paulson@3724
   773
by Safe_tac;
paulson@3457
   774
by (etac swap 1);
paulson@3348
   775
by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
paulson@3348
   776
by (ALLGOALS Blast_tac);
paulson@3348
   777
qed "Pow_insert";
paulson@3348
   778
paulson@6007
   779
Goal "Pow UNIV = UNIV";
paulson@6007
   780
by (Blast_tac 1);
paulson@6007
   781
qed "Pow_UNIV";
paulson@6007
   782
Addsimps [Pow_UNIV];
paulson@6007
   783
berghofe@5189
   784
(** for datatypes **)
berghofe@5189
   785
Goal "f x ~= f y ==> x ~= y";
berghofe@5189
   786
by (Fast_tac 1);
berghofe@5189
   787
qed "distinct_lemma";
berghofe@5189
   788
paulson@2021
   789
paulson@2021
   790
(** Miniscoping: pushing in big Unions and Intersections **)
paulson@2021
   791
local
paulson@4059
   792
  fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
paulson@2021
   793
in
paulson@2513
   794
val UN_simps = map prover 
paulson@5941
   795
    ["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
paulson@5941
   796
     "!!C. c: C ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
paulson@5941
   797
     "!!C. c: C ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
paulson@4159
   798
     "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
paulson@4159
   799
     "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
paulson@4159
   800
     "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
nipkow@4231
   801
     "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
nipkow@4231
   802
     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
paulson@2513
   803
paulson@2513
   804
val INT_simps = map prover
paulson@5941
   805
    ["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
paulson@5941
   806
     "!!C. c: C ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
paulson@5941
   807
     "!!C. c: C ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
paulson@5941
   808
     "!!C. c: C ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
paulson@4159
   809
     "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
paulson@4159
   810
     "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
nipkow@4231
   811
     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
nipkow@4231
   812
     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
paulson@2513
   813
paulson@2513
   814
paulson@2513
   815
val ball_simps = map prover
paulson@2513
   816
    ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
paulson@2513
   817
     "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
paulson@3422
   818
     "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
paulson@3422
   819
     "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
paulson@2513
   820
     "(ALL x:{}. P x) = True",
oheimb@4136
   821
     "(ALL x:UNIV. P x) = (ALL x. P x)",
paulson@2513
   822
     "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
paulson@2513
   823
     "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
paulson@5233
   824
     "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
nipkow@3860
   825
     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
nipkow@3860
   826
     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
nipkow@3860
   827
     "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
paulson@2513
   828
paulson@2513
   829
val ball_conj_distrib = 
paulson@2513
   830
    prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
paulson@2513
   831
paulson@2513
   832
val bex_simps = map prover
paulson@2513
   833
    ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
paulson@2513
   834
     "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
paulson@2513
   835
     "(EX x:{}. P x) = False",
oheimb@4136
   836
     "(EX x:UNIV. P x) = (EX x. P x)",
paulson@2513
   837
     "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
paulson@2513
   838
     "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
paulson@5233
   839
     "(EX x: UNION A B. P x) = (EX a:A. EX x: B a.  P x)",
nipkow@3860
   840
     "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
nipkow@3860
   841
     "(EX x:f``A. P x) = (EX x:A. P(f x))",
nipkow@3860
   842
     "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
paulson@2513
   843
paulson@3426
   844
val bex_disj_distrib = 
paulson@2513
   845
    prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
paulson@2513
   846
paulson@2021
   847
end;
paulson@2021
   848
paulson@4159
   849
Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);