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