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