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