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