src/HOL/equalities.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5238 c449f23728df
child 5281 f4d16517b360
permissions -rw-r--r--
even more tidying of Goal commands
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 
oheimb@4882
    86
	"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
oheimb@4882
    87
paulson@5278
    88
Goal "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
paulson@2891
    89
by (Blast_tac 1);
paulson@1843
    90
qed "UN_insert_distrib";
paulson@1843
    91
oheimb@1660
    92
section "``";
clasohm@923
    93
wenzelm@5069
    94
Goal "f``{} = {}";
paulson@2891
    95
by (Blast_tac 1);
clasohm@923
    96
qed "image_empty";
nipkow@1531
    97
Addsimps[image_empty];
clasohm@923
    98
wenzelm@5069
    99
Goal "f``insert a B = insert (f a) (f``B)";
paulson@2891
   100
by (Blast_tac 1);
clasohm@923
   101
qed "image_insert";
nipkow@1531
   102
Addsimps[image_insert];
clasohm@923
   103
wenzelm@5069
   104
Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
nipkow@3222
   105
by (Blast_tac 1);
nipkow@3222
   106
qed "image_UNION";
nipkow@3222
   107
wenzelm@5069
   108
Goal "(%x. x) `` Y = Y";
nipkow@3222
   109
by (Blast_tac 1);
nipkow@3222
   110
qed "image_id";
nipkow@3222
   111
wenzelm@5069
   112
Goal "f``(g``A) = (%x. f (g x)) `` A";
paulson@3457
   113
by (Blast_tac 1);
paulson@4059
   114
qed "image_image";
nipkow@3222
   115
paulson@5143
   116
Goal "x:A ==> insert (f x) (f``A) = f``A";
paulson@2891
   117
by (Blast_tac 1);
paulson@1884
   118
qed "insert_image";
paulson@1884
   119
Addsimps [insert_image];
paulson@1884
   120
wenzelm@5069
   121
Goal "(f``A = {}) = (A = {})";
paulson@4306
   122
by (blast_tac (claset() addSEs [equalityCE]) 1);
nipkow@3415
   123
qed "image_is_empty";
nipkow@3415
   124
AddIffs [image_is_empty];
nipkow@3415
   125
wenzelm@5069
   126
Goalw [image_def]
berghofe@1763
   127
"(%x. if P x then f x else g x) `` S                    \
paulson@4200
   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
oheimb@4136
   134
val prems= goal thy "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";
oheimb@4136
   135
by (rtac set_ext 1);
oheimb@4136
   136
by (simp_tac (simpset() addsimps image_def::prems) 1);
oheimb@4136
   137
qed "image_cong";
oheimb@4136
   138
nipkow@1748
   139
nipkow@1548
   140
section "Int";
clasohm@923
   141
wenzelm@5069
   142
Goal "A Int A = A";
paulson@2891
   143
by (Blast_tac 1);
clasohm@923
   144
qed "Int_absorb";
nipkow@1531
   145
Addsimps[Int_absorb];
clasohm@923
   146
wenzelm@5069
   147
Goal " A Int (A Int B) = A Int B";
paulson@4609
   148
by (Blast_tac 1);
paulson@4609
   149
qed "Int_left_absorb";
paulson@4609
   150
wenzelm@5069
   151
Goal "A Int B  =  B Int A";
paulson@2891
   152
by (Blast_tac 1);
clasohm@923
   153
qed "Int_commute";
clasohm@923
   154
wenzelm@5069
   155
Goal "A Int (B Int C) = B Int (A Int C)";
paulson@4609
   156
by (Blast_tac 1);
paulson@4609
   157
qed "Int_left_commute";
paulson@4609
   158
wenzelm@5069
   159
Goal "(A Int B) Int C  =  A Int (B Int C)";
paulson@2891
   160
by (Blast_tac 1);
clasohm@923
   161
qed "Int_assoc";
clasohm@923
   162
paulson@4609
   163
(*Intersection is an AC-operator*)
paulson@4609
   164
val Int_ac = [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute];
paulson@4609
   165
paulson@5143
   166
Goal "B<=A ==> A Int B = B";
paulson@4662
   167
by (Blast_tac 1);
paulson@4662
   168
qed "Int_absorb1";
paulson@4662
   169
paulson@5143
   170
Goal "A<=B ==> A Int B = A";
paulson@4662
   171
by (Blast_tac 1);
paulson@4662
   172
qed "Int_absorb2";
paulson@4662
   173
wenzelm@5069
   174
Goal "{} Int B = {}";
paulson@2891
   175
by (Blast_tac 1);
clasohm@923
   176
qed "Int_empty_left";
nipkow@1531
   177
Addsimps[Int_empty_left];
clasohm@923
   178
wenzelm@5069
   179
Goal "A Int {} = {}";
paulson@2891
   180
by (Blast_tac 1);
clasohm@923
   181
qed "Int_empty_right";
nipkow@1531
   182
Addsimps[Int_empty_right];
nipkow@1531
   183
wenzelm@5069
   184
Goal "(A Int B = {}) = (A <= Compl B)";
paulson@4306
   185
by (blast_tac (claset() addSEs [equalityCE]) 1);
paulson@3356
   186
qed "disjoint_eq_subset_Compl";
paulson@3356
   187
wenzelm@5069
   188
Goal "UNIV Int B = B";
paulson@2891
   189
by (Blast_tac 1);
nipkow@1531
   190
qed "Int_UNIV_left";
nipkow@1531
   191
Addsimps[Int_UNIV_left];
nipkow@1531
   192
wenzelm@5069
   193
Goal "A Int UNIV = A";
paulson@2891
   194
by (Blast_tac 1);
nipkow@1531
   195
qed "Int_UNIV_right";
nipkow@1531
   196
Addsimps[Int_UNIV_right];
clasohm@923
   197
wenzelm@5069
   198
Goal "A Int B = Inter{A,B}";
paulson@4634
   199
by (Blast_tac 1);
paulson@4634
   200
qed "Int_eq_Inter";
paulson@4634
   201
wenzelm@5069
   202
Goal "A Int (B Un C)  =  (A Int B) Un (A Int C)";
paulson@2891
   203
by (Blast_tac 1);
clasohm@923
   204
qed "Int_Un_distrib";
clasohm@923
   205
wenzelm@5069
   206
Goal "(B Un C) Int A =  (B Int A) Un (C Int A)";
paulson@2891
   207
by (Blast_tac 1);
paulson@1618
   208
qed "Int_Un_distrib2";
paulson@1618
   209
wenzelm@5069
   210
Goal "(A<=B) = (A Int B = A)";
paulson@4306
   211
by (blast_tac (claset() addSEs [equalityCE]) 1);
clasohm@923
   212
qed "subset_Int_eq";
clasohm@923
   213
wenzelm@5069
   214
Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
wenzelm@4089
   215
by (blast_tac (claset() addEs [equalityCE]) 1);
nipkow@1531
   216
qed "Int_UNIV";
nipkow@1531
   217
Addsimps[Int_UNIV];
nipkow@1531
   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
wenzelm@5069
   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
wenzelm@5069
   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@4306
   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@4306
   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
wenzelm@5069
   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
wenzelm@5069
   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@5278
   307
Goal "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
paulson@2891
   308
by (Blast_tac 1);
clasohm@923
   309
qed "Un_Int_crazy";
clasohm@923
   310
wenzelm@5069
   311
Goal "(A<=B) = (A Un B = B)";
paulson@4306
   312
by (blast_tac (claset() addSEs [equalityCE]) 1);
clasohm@923
   313
qed "subset_Un_eq";
clasohm@923
   314
wenzelm@5069
   315
Goal "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
paulson@2891
   316
by (Blast_tac 1);
clasohm@923
   317
qed "subset_insert_iff";
clasohm@923
   318
wenzelm@5069
   319
Goal "(A Un B = {}) = (A = {} & B = {})";
wenzelm@4089
   320
by (blast_tac (claset() addEs [equalityCE]) 1);
clasohm@923
   321
qed "Un_empty";
nipkow@1531
   322
Addsimps[Un_empty];
clasohm@923
   323
nipkow@1548
   324
section "Compl";
clasohm@923
   325
wenzelm@5069
   326
Goal "A Int Compl(A) = {}";
paulson@2891
   327
by (Blast_tac 1);
clasohm@923
   328
qed "Compl_disjoint";
nipkow@1531
   329
Addsimps[Compl_disjoint];
clasohm@923
   330
wenzelm@5069
   331
Goal "A Un Compl(A) = UNIV";
paulson@2891
   332
by (Blast_tac 1);
clasohm@923
   333
qed "Compl_partition";
clasohm@923
   334
wenzelm@5069
   335
Goal "Compl(Compl(A)) = A";
paulson@2891
   336
by (Blast_tac 1);
clasohm@923
   337
qed "double_complement";
nipkow@1531
   338
Addsimps[double_complement];
clasohm@923
   339
wenzelm@5069
   340
Goal "Compl(A Un B) = Compl(A) Int Compl(B)";
paulson@2891
   341
by (Blast_tac 1);
clasohm@923
   342
qed "Compl_Un";
clasohm@923
   343
wenzelm@5069
   344
Goal "Compl(A Int B) = Compl(A) Un Compl(B)";
paulson@2891
   345
by (Blast_tac 1);
clasohm@923
   346
qed "Compl_Int";
clasohm@923
   347
wenzelm@5069
   348
Goal "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
paulson@2891
   349
by (Blast_tac 1);
clasohm@923
   350
qed "Compl_UN";
clasohm@923
   351
wenzelm@5069
   352
Goal "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
paulson@2891
   353
by (Blast_tac 1);
clasohm@923
   354
qed "Compl_INT";
clasohm@923
   355
paulson@4615
   356
Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
paulson@4615
   357
clasohm@923
   358
(*Halmos, Naive Set Theory, page 16.*)
clasohm@923
   359
wenzelm@5069
   360
Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
paulson@4306
   361
by (blast_tac (claset() addSEs [equalityCE]) 1);
clasohm@923
   362
qed "Un_Int_assoc_eq";
clasohm@923
   363
clasohm@923
   364
nipkow@1548
   365
section "Union";
clasohm@923
   366
wenzelm@5069
   367
Goal "Union({}) = {}";
paulson@2891
   368
by (Blast_tac 1);
clasohm@923
   369
qed "Union_empty";
nipkow@1531
   370
Addsimps[Union_empty];
nipkow@1531
   371
wenzelm@5069
   372
Goal "Union(UNIV) = UNIV";
paulson@2891
   373
by (Blast_tac 1);
nipkow@1531
   374
qed "Union_UNIV";
nipkow@1531
   375
Addsimps[Union_UNIV];
clasohm@923
   376
wenzelm@5069
   377
Goal "Union(insert a B) = a Un Union(B)";
paulson@2891
   378
by (Blast_tac 1);
clasohm@923
   379
qed "Union_insert";
nipkow@1531
   380
Addsimps[Union_insert];
clasohm@923
   381
wenzelm@5069
   382
Goal "Union(A Un B) = Union(A) Un Union(B)";
paulson@2891
   383
by (Blast_tac 1);
clasohm@923
   384
qed "Union_Un_distrib";
nipkow@1531
   385
Addsimps[Union_Un_distrib];
clasohm@923
   386
wenzelm@5069
   387
Goal "Union(A Int B) <= Union(A) Int Union(B)";
paulson@2891
   388
by (Blast_tac 1);
clasohm@923
   389
qed "Union_Int_subset";
clasohm@923
   390
wenzelm@5069
   391
Goal "(Union M = {}) = (! A : M. A = {})"; 
paulson@4306
   392
by (blast_tac (claset() addEs [equalityCE]) 1);
paulson@4306
   393
qed "Union_empty_conv"; 
nipkow@4003
   394
AddIffs [Union_empty_conv];
nipkow@4003
   395
wenzelm@5069
   396
Goal "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
paulson@4306
   397
by (blast_tac (claset() addSEs [equalityCE]) 1);
clasohm@923
   398
qed "Union_disjoint";
clasohm@923
   399
nipkow@1548
   400
section "Inter";
nipkow@1548
   401
wenzelm@5069
   402
Goal "Inter({}) = UNIV";
paulson@2891
   403
by (Blast_tac 1);
nipkow@1531
   404
qed "Inter_empty";
nipkow@1531
   405
Addsimps[Inter_empty];
nipkow@1531
   406
wenzelm@5069
   407
Goal "Inter(UNIV) = {}";
paulson@2891
   408
by (Blast_tac 1);
nipkow@1531
   409
qed "Inter_UNIV";
nipkow@1531
   410
Addsimps[Inter_UNIV];
nipkow@1531
   411
wenzelm@5069
   412
Goal "Inter(insert a B) = a Int Inter(B)";
paulson@2891
   413
by (Blast_tac 1);
nipkow@1531
   414
qed "Inter_insert";
nipkow@1531
   415
Addsimps[Inter_insert];
nipkow@1531
   416
wenzelm@5069
   417
Goal "Inter(A) Un Inter(B) <= Inter(A Int B)";
paulson@2891
   418
by (Blast_tac 1);
paulson@1564
   419
qed "Inter_Un_subset";
nipkow@1531
   420
wenzelm@5069
   421
Goal "Inter(A Un B) = Inter(A) Int Inter(B)";
paulson@2891
   422
by (Blast_tac 1);
clasohm@923
   423
qed "Inter_Un_distrib";
clasohm@923
   424
nipkow@1548
   425
section "UN and INT";
clasohm@923
   426
clasohm@923
   427
(*Basic identities*)
clasohm@923
   428
paulson@4200
   429
val not_empty = prove_goal Set.thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]);
oheimb@4136
   430
(*Addsimps[not_empty];*)
oheimb@4136
   431
wenzelm@5069
   432
Goal "(UN x:{}. B x) = {}";
paulson@2891
   433
by (Blast_tac 1);
nipkow@1179
   434
qed "UN_empty";
nipkow@1531
   435
Addsimps[UN_empty];
nipkow@1531
   436
wenzelm@5069
   437
Goal "(UN x:A. {}) = {}";
paulson@3457
   438
by (Blast_tac 1);
nipkow@3222
   439
qed "UN_empty2";
nipkow@3222
   440
Addsimps[UN_empty2];
nipkow@3222
   441
wenzelm@5069
   442
Goal "(UN x:A. {x}) = A";
paulson@4645
   443
by (Blast_tac 1);
paulson@4645
   444
qed "UN_singleton";
paulson@4645
   445
Addsimps [UN_singleton];
paulson@4645
   446
paulson@5143
   447
Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
paulson@4634
   448
by (Blast_tac 1);
paulson@4634
   449
qed "UN_absorb";
paulson@4634
   450
wenzelm@5069
   451
Goal "(INT x:{}. B x) = UNIV";
paulson@2891
   452
by (Blast_tac 1);
nipkow@1531
   453
qed "INT_empty";
nipkow@1531
   454
Addsimps[INT_empty];
nipkow@1531
   455
paulson@5143
   456
Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
paulson@4634
   457
by (Blast_tac 1);
paulson@4634
   458
qed "INT_absorb";
paulson@4634
   459
wenzelm@5069
   460
Goal "(UN x:insert a A. B x) = B a Un UNION A B";
paulson@2891
   461
by (Blast_tac 1);
nipkow@1179
   462
qed "UN_insert";
nipkow@1531
   463
Addsimps[UN_insert];
nipkow@1531
   464
wenzelm@5069
   465
Goal "(UN i: A Un B. M i) = ((UN i: A. M i) Un (UN i:B. M i))";
nipkow@3222
   466
by (Blast_tac 1);
nipkow@3222
   467
qed "UN_Un";
nipkow@3222
   468
wenzelm@5069
   469
Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)";
paulson@4771
   470
by (Blast_tac 1);
paulson@4771
   471
qed "UN_UN_flatten";
paulson@4771
   472
wenzelm@5069
   473
Goal "(INT x:insert a A. B x) = B a Int INTER A B";
paulson@2891
   474
by (Blast_tac 1);
nipkow@1531
   475
qed "INT_insert";
nipkow@1531
   476
Addsimps[INT_insert];
nipkow@1179
   477
paulson@5148
   478
Goal "A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
paulson@2891
   479
by (Blast_tac 1);
paulson@2021
   480
qed "INT_insert_distrib";
paulson@2021
   481
wenzelm@5069
   482
Goal "Union(B``A) = (UN x:A. B(x))";
paulson@2891
   483
by (Blast_tac 1);
clasohm@923
   484
qed "Union_image_eq";
clasohm@923
   485
wenzelm@5069
   486
Goal "Inter(B``A) = (INT x:A. B(x))";
paulson@2891
   487
by (Blast_tac 1);
clasohm@923
   488
qed "Inter_image_eq";
clasohm@923
   489
paulson@5143
   490
Goal "A~={} ==> (UN y:A. c) = c";
paulson@2891
   491
by (Blast_tac 1);
clasohm@923
   492
qed "UN_constant";
paulson@4159
   493
Addsimps[UN_constant];
clasohm@923
   494
paulson@5143
   495
Goal "A~={} ==> (INT y:A. c) = c";
paulson@2891
   496
by (Blast_tac 1);
clasohm@923
   497
qed "INT_constant";
paulson@4159
   498
Addsimps[INT_constant];
clasohm@923
   499
wenzelm@5069
   500
Goal "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
paulson@2891
   501
by (Blast_tac 1);
clasohm@923
   502
qed "UN_eq";
clasohm@923
   503
clasohm@923
   504
(*Look: it has an EXISTENTIAL quantifier*)
wenzelm@5069
   505
Goal "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
paulson@2891
   506
by (Blast_tac 1);
clasohm@923
   507
qed "INT_eq";
clasohm@923
   508
wenzelm@5069
   509
Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
nipkow@3222
   510
by (Blast_tac 1);
nipkow@3222
   511
qed "UNION_o";
nipkow@3222
   512
nipkow@3222
   513
clasohm@923
   514
(*Distributive laws...*)
clasohm@923
   515
wenzelm@5069
   516
Goal "A Int Union(B) = (UN C:B. A Int C)";
paulson@2891
   517
by (Blast_tac 1);
clasohm@923
   518
qed "Int_Union";
clasohm@923
   519
wenzelm@5069
   520
Goal "Union(B) Int A = (UN C:B. C Int A)";
paulson@4674
   521
by (Blast_tac 1);
paulson@4674
   522
qed "Int_Union2";
paulson@4674
   523
paulson@4306
   524
(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
clasohm@923
   525
   Union of a family of unions **)
wenzelm@5069
   526
Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
paulson@2891
   527
by (Blast_tac 1);
clasohm@923
   528
qed "Un_Union_image";
clasohm@923
   529
clasohm@923
   530
(*Equivalent version*)
wenzelm@5069
   531
Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
paulson@2891
   532
by (Blast_tac 1);
clasohm@923
   533
qed "UN_Un_distrib";
clasohm@923
   534
wenzelm@5069
   535
Goal "A Un Inter(B) = (INT C:B. A Un C)";
paulson@2891
   536
by (Blast_tac 1);
clasohm@923
   537
qed "Un_Inter";
clasohm@923
   538
wenzelm@5069
   539
Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
paulson@2891
   540
by (Blast_tac 1);
clasohm@923
   541
qed "Int_Inter_image";
clasohm@923
   542
clasohm@923
   543
(*Equivalent version*)
wenzelm@5069
   544
Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
paulson@2891
   545
by (Blast_tac 1);
clasohm@923
   546
qed "INT_Int_distrib";
clasohm@923
   547
clasohm@923
   548
(*Halmos, Naive Set Theory, page 35.*)
wenzelm@5069
   549
Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
paulson@2891
   550
by (Blast_tac 1);
clasohm@923
   551
qed "Int_UN_distrib";
clasohm@923
   552
wenzelm@5069
   553
Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
paulson@2891
   554
by (Blast_tac 1);
clasohm@923
   555
qed "Un_INT_distrib";
clasohm@923
   556
paulson@5278
   557
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
   558
by (Blast_tac 1);
clasohm@923
   559
qed "Int_UN_distrib2";
clasohm@923
   560
paulson@5278
   561
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
   562
by (Blast_tac 1);
clasohm@923
   563
qed "Un_INT_distrib2";
clasohm@923
   564
nipkow@2512
   565
nipkow@2512
   566
section"Bounded quantifiers";
nipkow@2512
   567
nipkow@3860
   568
(** The following are not added to the default simpset because
nipkow@3860
   569
    (a) they duplicate the body and (b) there are no similar rules for Int. **)
nipkow@2512
   570
wenzelm@5069
   571
Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
paulson@2891
   572
by (Blast_tac 1);
paulson@2519
   573
qed "ball_Un";
paulson@2519
   574
wenzelm@5069
   575
Goal "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
paulson@2891
   576
by (Blast_tac 1);
paulson@2519
   577
qed "bex_Un";
nipkow@2512
   578
wenzelm@5069
   579
Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)";
paulson@4771
   580
by (Blast_tac 1);
paulson@4771
   581
qed "ball_UN";
paulson@4771
   582
wenzelm@5069
   583
Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)";
paulson@4771
   584
by (Blast_tac 1);
paulson@4771
   585
qed "bex_UN";
paulson@4771
   586
nipkow@2512
   587
nipkow@1548
   588
section "-";
clasohm@923
   589
wenzelm@5069
   590
Goal "A-B = A Int Compl B";
paulson@4609
   591
by (Blast_tac 1);
paulson@4662
   592
qed "Diff_eq";
paulson@4609
   593
wenzelm@5069
   594
Goal "A-A = {}";
paulson@2891
   595
by (Blast_tac 1);
clasohm@923
   596
qed "Diff_cancel";
nipkow@1531
   597
Addsimps[Diff_cancel];
clasohm@923
   598
paulson@5143
   599
Goal "A Int B = {} ==> A-B = A";
paulson@4674
   600
by (blast_tac (claset() addEs [equalityE]) 1);
paulson@4674
   601
qed "Diff_triv";
paulson@4674
   602
wenzelm@5069
   603
Goal "{}-A = {}";
paulson@2891
   604
by (Blast_tac 1);
clasohm@923
   605
qed "empty_Diff";
nipkow@1531
   606
Addsimps[empty_Diff];
clasohm@923
   607
wenzelm@5069
   608
Goal "A-{} = A";
paulson@2891
   609
by (Blast_tac 1);
clasohm@923
   610
qed "Diff_empty";
nipkow@1531
   611
Addsimps[Diff_empty];
nipkow@1531
   612
wenzelm@5069
   613
Goal "A-UNIV = {}";
paulson@2891
   614
by (Blast_tac 1);
nipkow@1531
   615
qed "Diff_UNIV";
nipkow@1531
   616
Addsimps[Diff_UNIV];
nipkow@1531
   617
paulson@5143
   618
Goal "x~:A ==> A - insert x B = A-B";
paulson@2891
   619
by (Blast_tac 1);
nipkow@1531
   620
qed "Diff_insert0";
nipkow@1531
   621
Addsimps [Diff_insert0];
clasohm@923
   622
clasohm@923
   623
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
wenzelm@5069
   624
Goal "A - insert a B = A - B - {a}";
paulson@2891
   625
by (Blast_tac 1);
clasohm@923
   626
qed "Diff_insert";
clasohm@923
   627
clasohm@923
   628
(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
wenzelm@5069
   629
Goal "A - insert a B = A - {a} - B";
paulson@2891
   630
by (Blast_tac 1);
clasohm@923
   631
qed "Diff_insert2";
clasohm@923
   632
wenzelm@5069
   633
Goal "insert x A - B = (if x:B then A-B else insert x (A-B))";
nipkow@4686
   634
by (Simp_tac 1);
paulson@2891
   635
by (Blast_tac 1);
nipkow@1531
   636
qed "insert_Diff_if";
nipkow@1531
   637
paulson@5143
   638
Goal "x:B ==> insert x A - B = A-B";
paulson@2891
   639
by (Blast_tac 1);
nipkow@1531
   640
qed "insert_Diff1";
nipkow@1531
   641
Addsimps [insert_Diff1];
nipkow@1531
   642
paulson@5143
   643
Goal "a:A ==> insert a (A-{a}) = A";
paulson@2922
   644
by (Blast_tac 1);
clasohm@923
   645
qed "insert_Diff";
clasohm@923
   646
wenzelm@5069
   647
Goal "A Int (B-A) = {}";
paulson@2891
   648
by (Blast_tac 1);
clasohm@923
   649
qed "Diff_disjoint";
nipkow@1531
   650
Addsimps[Diff_disjoint];
clasohm@923
   651
paulson@5143
   652
Goal "A<=B ==> A Un (B-A) = B";
paulson@2891
   653
by (Blast_tac 1);
clasohm@923
   654
qed "Diff_partition";
clasohm@923
   655
paulson@5143
   656
Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
paulson@2891
   657
by (Blast_tac 1);
clasohm@923
   658
qed "double_diff";
clasohm@923
   659
wenzelm@5069
   660
Goal "A Un (B-A) = A Un B";
paulson@4645
   661
by (Blast_tac 1);
paulson@4645
   662
qed "Un_Diff_cancel";
paulson@4645
   663
wenzelm@5069
   664
Goal "(B-A) Un A = B Un A";
paulson@4645
   665
by (Blast_tac 1);
paulson@4645
   666
qed "Un_Diff_cancel2";
paulson@4645
   667
paulson@4645
   668
Addsimps [Un_Diff_cancel, Un_Diff_cancel2];
paulson@4645
   669
wenzelm@5069
   670
Goal "A - (B Un C) = (A-B) Int (A-C)";
paulson@2891
   671
by (Blast_tac 1);
clasohm@923
   672
qed "Diff_Un";
clasohm@923
   673
wenzelm@5069
   674
Goal "A - (B Int C) = (A-B) Un (A-C)";
paulson@2891
   675
by (Blast_tac 1);
clasohm@923
   676
qed "Diff_Int";
clasohm@923
   677
wenzelm@5069
   678
Goal "(A Un B) - C = (A - C) Un (B - C)";
nipkow@3222
   679
by (Blast_tac 1);
nipkow@3222
   680
qed "Un_Diff";
nipkow@3222
   681
wenzelm@5069
   682
Goal "(A Int B) - C = A Int (B - C)";
nipkow@3222
   683
by (Blast_tac 1);
nipkow@3222
   684
qed "Int_Diff";
nipkow@3222
   685
wenzelm@5069
   686
Goal "C Int (A-B) = (C Int A) - (C Int B)";
paulson@4748
   687
by (Blast_tac 1);
paulson@4748
   688
qed "Diff_Int_distrib";
paulson@4748
   689
wenzelm@5069
   690
Goal "(A-B) Int C = (A Int C) - (B Int C)";
paulson@4645
   691
by (Blast_tac 1);
paulson@4748
   692
qed "Diff_Int_distrib2";
paulson@4645
   693
nipkow@3222
   694
paulson@5238
   695
section "Quantification over type \"bool\"";
paulson@5238
   696
paulson@5238
   697
Goal "(ALL b::bool. P b) = (P True & P False)";
paulson@5238
   698
by Auto_tac;
paulson@5238
   699
by (case_tac "b" 1);
paulson@5238
   700
by Auto_tac;
paulson@5238
   701
qed "all_bool_eq";
paulson@5238
   702
paulson@5238
   703
Goal "(EX b::bool. P b) = (P True | P False)";
paulson@5238
   704
by Auto_tac;
paulson@5238
   705
by (case_tac "b" 1);
paulson@5238
   706
by Auto_tac;
paulson@5238
   707
qed "ex_bool_eq";
paulson@5238
   708
paulson@5238
   709
Goal "A Un B = (UN b. if b then A else B)";
paulson@5238
   710
by Auto_tac;
paulson@5238
   711
by (asm_full_simp_tac (simpset() addsimps [split_if_mem2]) 1);
paulson@5238
   712
qed "Un_eq_UN";
paulson@5238
   713
paulson@5238
   714
Goal "(UN b::bool. A b) = (A True Un A False)";
paulson@5238
   715
by Auto_tac;
paulson@5238
   716
by (case_tac "b" 1);
paulson@5238
   717
by Auto_tac;
paulson@5238
   718
qed "UN_bool_eq";
paulson@5238
   719
paulson@5238
   720
Goal "(INT b::bool. A b) = (A True Int A False)";
paulson@5238
   721
by Auto_tac;
paulson@5238
   722
by (case_tac "b" 1);
paulson@5238
   723
by Auto_tac;
paulson@5238
   724
qed "INT_bool_eq";
paulson@5238
   725
paulson@5238
   726
nipkow@3222
   727
section "Miscellany";
nipkow@3222
   728
wenzelm@5069
   729
Goal "(A = B) = ((A <= (B::'a set)) & (B<=A))";
nipkow@3222
   730
by (Blast_tac 1);
nipkow@3222
   731
qed "set_eq_subset";
nipkow@3222
   732
wenzelm@5069
   733
Goal "A <= B =  (! t. t:A --> t:B)";
nipkow@3222
   734
by (Blast_tac 1);
nipkow@3222
   735
qed "subset_iff";
nipkow@3222
   736
wenzelm@5069
   737
Goalw [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
nipkow@3222
   738
by (Blast_tac 1);
nipkow@3222
   739
qed "subset_iff_psubset_eq";
paulson@2021
   740
wenzelm@5069
   741
Goal "(!x. x ~: A) = (A={})";
wenzelm@4423
   742
by (Blast_tac 1);
nipkow@3896
   743
qed "all_not_in_conv";
nipkow@3907
   744
AddIffs [all_not_in_conv];
nipkow@3896
   745
wenzelm@5069
   746
Goalw [Pow_def] "Pow {} = {{}}";
paulson@4477
   747
by Auto_tac;
paulson@3348
   748
qed "Pow_empty";
paulson@3348
   749
Addsimps [Pow_empty];
paulson@3348
   750
wenzelm@5069
   751
Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
paulson@3724
   752
by Safe_tac;
paulson@3457
   753
by (etac swap 1);
paulson@3348
   754
by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
paulson@3348
   755
by (ALLGOALS Blast_tac);
paulson@3348
   756
qed "Pow_insert";
paulson@3348
   757
berghofe@5189
   758
(** for datatypes **)
berghofe@5189
   759
Goal "f x ~= f y ==> x ~= y";
berghofe@5189
   760
by (Fast_tac 1);
berghofe@5189
   761
qed "distinct_lemma";
berghofe@5189
   762
paulson@2021
   763
paulson@2021
   764
(** Miniscoping: pushing in big Unions and Intersections **)
paulson@2021
   765
local
paulson@4059
   766
  fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])
paulson@2021
   767
in
paulson@2513
   768
val UN_simps = map prover 
paulson@4159
   769
    ["!!C. C ~= {} ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",
paulson@4159
   770
     "!!C. C ~= {} ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",
paulson@4159
   771
     "!!C. C ~= {} ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",
paulson@4159
   772
     "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
paulson@4159
   773
     "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
paulson@4159
   774
     "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
nipkow@4231
   775
     "(UN x:C. A - B x)    = (A - (INT x:C. B x))",
nipkow@4231
   776
     "(UN x:f``A. B x)     = (UN a:A. B(f a))"];
paulson@2513
   777
paulson@2513
   778
val INT_simps = map prover
paulson@4159
   779
    ["!!C. C ~= {} ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",
paulson@4159
   780
     "!!C. C ~= {} ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",
paulson@4159
   781
     "!!C. C ~= {} ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",
paulson@4159
   782
     "!!C. C ~= {} ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",
paulson@4159
   783
     "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
paulson@4159
   784
     "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
nipkow@4231
   785
     "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",
nipkow@4231
   786
     "(INT x:f``A. B x)    = (INT a:A. B(f a))"];
paulson@2513
   787
paulson@2513
   788
paulson@2513
   789
val ball_simps = map prover
paulson@2513
   790
    ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
paulson@2513
   791
     "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
paulson@3422
   792
     "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
paulson@3422
   793
     "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
paulson@2513
   794
     "(ALL x:{}. P x) = True",
oheimb@4136
   795
     "(ALL x:UNIV. P x) = (ALL x. P x)",
paulson@2513
   796
     "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
paulson@2513
   797
     "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
paulson@5233
   798
     "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
nipkow@3860
   799
     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
nipkow@3860
   800
     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
nipkow@3860
   801
     "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
paulson@2513
   802
paulson@2513
   803
val ball_conj_distrib = 
paulson@2513
   804
    prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
paulson@2513
   805
paulson@2513
   806
val bex_simps = map prover
paulson@2513
   807
    ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
paulson@2513
   808
     "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
paulson@2513
   809
     "(EX x:{}. P x) = False",
oheimb@4136
   810
     "(EX x:UNIV. P x) = (EX x. P x)",
paulson@2513
   811
     "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
paulson@2513
   812
     "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
paulson@5233
   813
     "(EX x: UNION A B. P x) = (EX a:A. EX x: B a.  P x)",
nipkow@3860
   814
     "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
nipkow@3860
   815
     "(EX x:f``A. P x) = (EX x:A. P(f x))",
nipkow@3860
   816
     "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
paulson@2513
   817
paulson@3426
   818
val bex_disj_distrib = 
paulson@2513
   819
    prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
paulson@2513
   820
paulson@2021
   821
end;
paulson@2021
   822
paulson@4159
   823
Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);