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