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