Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/equalities.ML
author wenzelm
Wed, 24 Nov 1999 13:35:31 +0100
changeset 8030 af8db1872960
parent 8026 636884ec8f13
child 8121 4a53041acb28
permissions -rw-r--r--
prove_goal thy; 
     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 (*supersedes Collect_False_empty*)

    16 Goal "{s. P} = (if P then UNIV else {})";

    17 by (Force_tac 1);

    18 qed "Collect_const";

    19 Addsimps [Collect_const];

    20 

    21 Goal "(A <= {}) = (A = {})";

    22 by (Blast_tac 1);

    23 qed "subset_empty";

    24 Addsimps [subset_empty];

    25 

    26 Goalw [psubset_def] "~ (A < {})";

    27 by (Blast_tac 1);

    28 qed "not_psubset_empty";

    29 AddIffs [not_psubset_empty];

    30 

    31 Goal "(Collect P = {}) = (!x. ~ P x)";

    32 by Auto_tac;

    33 qed "Collect_empty_eq";

    34 Addsimps[Collect_empty_eq];

    35 

    36 Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";

    37 by (Blast_tac 1);

    38 qed "Collect_disj_eq";

    39 

    40 Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}";

    41 by (Blast_tac 1);

    42 qed "Collect_conj_eq";

    43 

    44 Goal "{x. ALL y. P x y} = (INT y. {x. P x y})";

    45 by (Blast_tac 1);

    46 qed "Collect_all_eq";

    47 

    48 Goal "{x. ALL y: A. P x y} = (INT y: A. {x. P x y})";

    49 by (Blast_tac 1);

    50 qed "Collect_ball_eq";

    51 

    52 Goal "{x. EX y. P x y} = (UN y. {x. P x y})";

    53 by (Blast_tac 1);

    54 qed "Collect_ex_eq";

    55 

    56 Goal "{x. EX y: A. P x y} = (UN y: A. {x. P x y})";

    57 by (Blast_tac 1);

    58 qed "Collect_bex_eq";

    59 

    60 

    61 section "insert";

    62 

    63 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)

    64 Goal "insert a A = {a} Un A";

    65 by (Blast_tac 1);

    66 qed "insert_is_Un";

    67 

    68 Goal "insert a A ~= {}";

    69 by (blast_tac (claset() addEs [equalityCE]) 1);

    70 qed"insert_not_empty";

    71 Addsimps[insert_not_empty];

    72 

    73 bind_thm("empty_not_insert",insert_not_empty RS not_sym);

    74 Addsimps[empty_not_insert];

    75 

    76 Goal "a:A ==> insert a A = A";

    77 by (Blast_tac 1);

    78 qed "insert_absorb";

    79 (* Addsimps [insert_absorb] causes recursive calls

    80    when there are nested inserts, with QUADRATIC running time

    81 *)

    82 

    83 Goal "insert x (insert x A) = insert x A";

    84 by (Blast_tac 1);

    85 qed "insert_absorb2";

    86 Addsimps [insert_absorb2];

    87 

    88 Goal "insert x (insert y A) = insert y (insert x A)";

    89 by (Blast_tac 1);

    90 qed "insert_commute";

    91 

    92 Goal "(insert x A <= B) = (x:B & A <= B)";

    93 by (Blast_tac 1);

    94 qed "insert_subset";

    95 Addsimps[insert_subset];

    96 

    97 Goal "insert a A ~= insert a B ==> A ~= B";

    98 by (Blast_tac 1);

    99 qed "insert_lim";

   100 

   101 (* use new B rather than (A-{a}) to avoid infinite unfolding *)

   102 Goal "a:A ==> ? B. A = insert a B & a ~: B";

   103 by (res_inst_tac [("x","A-{a}")] exI 1);

   104 by (Blast_tac 1);

   105 qed "mk_disjoint_insert";

   106 

   107 bind_thm ("insert_Collect", prove_goal thy 

   108 	  "insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));

   109 

   110 Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";

   111 by (Blast_tac 1);

   112 qed "UN_insert_distrib";

   113 

   114 section "``";

   115 

   116 Goal "f``{} = {}";

   117 by (Blast_tac 1);

   118 qed "image_empty";

   119 Addsimps[image_empty];

   120 

   121 Goal "f``insert a B = insert (f a) (f``B)";

   122 by (Blast_tac 1);

   123 qed "image_insert";

   124 Addsimps[image_insert];

   125 

   126 Goal "x:A ==> (%x. c) `` A = {c}";

   127 by (Blast_tac 1);

   128 qed "image_constant";

   129 

   130 Goal "f``(g``A) = (%x. f (g x)) `` A";

   131 by (Blast_tac 1);

   132 qed "image_image";

   133 

   134 Goal "x:A ==> insert (f x) (f``A) = f``A";

   135 by (Blast_tac 1);

   136 qed "insert_image";

   137 Addsimps [insert_image];

   138 

   139 Goal "(f``A = {}) = (A = {})";

   140 by (blast_tac (claset() addSEs [equalityCE]) 1);

   141 qed "image_is_empty";

   142 AddIffs [image_is_empty];

   143 

   144 Goal "f `` {x. P x} = {f x | x. P x}";

   145 by (Blast_tac 1);

   146 qed "image_Collect";

   147 Addsimps [image_Collect];

   148 

   149 Goalw [image_def] "(%x. if P x then f x else g x) `` S   \

   150 \                = (f `` (S Int {x. P x})) Un (g `` (S Int {x. ~(P x)}))";

   151 by (Simp_tac 1);

   152 by (Blast_tac 1);

   153 qed "if_image_distrib";

   154 Addsimps[if_image_distrib];

   155 

   156 val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f``M = g``N";

   157 by (simp_tac (simpset() addsimps image_def::prems) 1);

   158 qed "image_cong";

   159 

   160 

   161 section "range";

   162 

   163 Goal "{u. ? x. u = f x} = range f";

   164 by Auto_tac;

   165 qed "full_SetCompr_eq";

   166 

   167 

   168 section "Int";

   169 

   170 Goal "A Int A = A";

   171 by (Blast_tac 1);

   172 qed "Int_absorb";

   173 Addsimps[Int_absorb];

   174 

   175 Goal "A Int (A Int B) = A Int B";

   176 by (Blast_tac 1);

   177 qed "Int_left_absorb";

   178 

   179 Goal "A Int B = B Int A";

   180 by (Blast_tac 1);

   181 qed "Int_commute";

   182 

   183 Goal "A Int (B Int C) = B Int (A Int C)";

   184 by (Blast_tac 1);

   185 qed "Int_left_commute";

   186 

   187 Goal "(A Int B) Int C = A Int (B Int C)";

   188 by (Blast_tac 1);

   189 qed "Int_assoc";

   190 

   191 (*Intersection is an AC-operator*)

   192 bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]);

   193 

   194 Goal "B<=A ==> A Int B = B";

   195 by (Blast_tac 1);

   196 qed "Int_absorb1";

   197 

   198 Goal "A<=B ==> A Int B = A";

   199 by (Blast_tac 1);

   200 qed "Int_absorb2";

   201 

   202 Goal "{} Int B = {}";

   203 by (Blast_tac 1);

   204 qed "Int_empty_left";

   205 Addsimps[Int_empty_left];

   206 

   207 Goal "A Int {} = {}";

   208 by (Blast_tac 1);

   209 qed "Int_empty_right";

   210 Addsimps[Int_empty_right];

   211 

   212 Goal "(A Int B = {}) = (A <= -B)";

   213 by (blast_tac (claset() addSEs [equalityCE]) 1);

   214 qed "disjoint_eq_subset_Compl";

   215 

   216 Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";

   217 by  (Blast_tac 1);

   218 qed "disjoint_iff_not_equal";

   219 

   220 Goal "UNIV Int B = B";

   221 by (Blast_tac 1);

   222 qed "Int_UNIV_left";

   223 Addsimps[Int_UNIV_left];

   224 

   225 Goal "A Int UNIV = A";

   226 by (Blast_tac 1);

   227 qed "Int_UNIV_right";

   228 Addsimps[Int_UNIV_right];

   229 

   230 Goal "A Int B = Inter{A,B}";

   231 by (Blast_tac 1);

   232 qed "Int_eq_Inter";

   233 

   234 Goal "A Int (B Un C) = (A Int B) Un (A Int C)";

   235 by (Blast_tac 1);

   236 qed "Int_Un_distrib";

   237 

   238 Goal "(B Un C) Int A = (B Int A) Un (C Int A)";

   239 by (Blast_tac 1);

   240 qed "Int_Un_distrib2";

   241 

   242 Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";

   243 by (blast_tac (claset() addEs [equalityCE]) 1);

   244 qed "Int_UNIV";

   245 Addsimps[Int_UNIV];

   246 

   247 Goal "(C <= A Int B) = (C <= A & C <= B)";

   248 by (Blast_tac 1);

   249 qed "Int_subset_iff";

   250 

   251 Goal "(x : A Int {x. P x}) = (x : A & P x)";

   252 by (Blast_tac 1);

   253 qed "Int_Collect";

   254 

   255 section "Un";

   256 

   257 Goal "A Un A = A";

   258 by (Blast_tac 1);

   259 qed "Un_absorb";

   260 Addsimps[Un_absorb];

   261 

   262 Goal " A Un (A Un B) = A Un B";

   263 by (Blast_tac 1);

   264 qed "Un_left_absorb";

   265 

   266 Goal "A Un B = B Un A";

   267 by (Blast_tac 1);

   268 qed "Un_commute";

   269 

   270 Goal "A Un (B Un C) = B Un (A Un C)";

   271 by (Blast_tac 1);

   272 qed "Un_left_commute";

   273 

   274 Goal "(A Un B) Un C = A Un (B Un C)";

   275 by (Blast_tac 1);

   276 qed "Un_assoc";

   277 

   278 (*Union is an AC-operator*)

   279 bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]);

   280 

   281 Goal "A<=B ==> A Un B = B";

   282 by (Blast_tac 1);

   283 qed "Un_absorb1";

   284 

   285 Goal "B<=A ==> A Un B = A";

   286 by (Blast_tac 1);

   287 qed "Un_absorb2";

   288 

   289 Goal "{} Un B = B";

   290 by (Blast_tac 1);

   291 qed "Un_empty_left";

   292 Addsimps[Un_empty_left];

   293 

   294 Goal "A Un {} = A";

   295 by (Blast_tac 1);

   296 qed "Un_empty_right";

   297 Addsimps[Un_empty_right];

   298 

   299 Goal "UNIV Un B = UNIV";

   300 by (Blast_tac 1);

   301 qed "Un_UNIV_left";

   302 Addsimps[Un_UNIV_left];

   303 

   304 Goal "A Un UNIV = UNIV";

   305 by (Blast_tac 1);

   306 qed "Un_UNIV_right";

   307 Addsimps[Un_UNIV_right];

   308 

   309 Goal "A Un B = Union{A,B}";

   310 by (Blast_tac 1);

   311 qed "Un_eq_Union";

   312 

   313 Goal "(insert a B) Un C = insert a (B Un C)";

   314 by (Blast_tac 1);

   315 qed "Un_insert_left";

   316 Addsimps[Un_insert_left];

   317 

   318 Goal "A Un (insert a B) = insert a (A Un B)";

   319 by (Blast_tac 1);

   320 qed "Un_insert_right";

   321 Addsimps[Un_insert_right];

   322 

   323 Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \

   324 \                                  else        B Int C)";

   325 by (Simp_tac 1);

   326 by (Blast_tac 1);

   327 qed "Int_insert_left";

   328 

   329 Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \

   330 \                                  else        A Int B)";

   331 by (Simp_tac 1);

   332 by (Blast_tac 1);

   333 qed "Int_insert_right";

   334 

   335 Goal "A Un (B Int C) = (A Un B) Int (A Un C)";

   336 by (Blast_tac 1);

   337 qed "Un_Int_distrib";

   338 

   339 Goal "(B Int C) Un A = (B Un A) Int (C Un A)";

   340 by (Blast_tac 1);

   341 qed "Un_Int_distrib2";

   342 

   343 Goal "(A Int B) Un (B Int C) Un (C Int A) = \

   344 \     (A Un B) Int (B Un C) Int (C Un A)";

   345 by (Blast_tac 1);

   346 qed "Un_Int_crazy";

   347 

   348 Goal "(A<=B) = (A Un B = B)";

   349 by (blast_tac (claset() addSEs [equalityCE]) 1);

   350 qed "subset_Un_eq";

   351 

   352 Goal "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";

   353 by (Blast_tac 1);

   354 qed "subset_insert_iff";

   355 

   356 Goal "(A Un B = {}) = (A = {} & B = {})";

   357 by (blast_tac (claset() addEs [equalityCE]) 1);

   358 qed "Un_empty";

   359 Addsimps[Un_empty];

   360 

   361 Goal "(A Un B <= C) = (A <= C & B <= C)";

   362 by (Blast_tac 1);

   363 qed "Un_subset_iff";

   364 

   365 Goal "(A - B) Un (A Int B) = A";

   366 by (Blast_tac 1);

   367 qed "Un_Diff_Int";

   368 

   369 

   370 section "Set complement";

   371 

   372 Goal "A Int (-A) = {}";

   373 by (Blast_tac 1);

   374 qed "Compl_disjoint";

   375 Addsimps[Compl_disjoint];

   376 

   377 Goal "A Un (-A) = UNIV";

   378 by (Blast_tac 1);

   379 qed "Compl_partition";

   380 

   381 Goal "- (-A) = (A:: 'a set)";

   382 by (Blast_tac 1);

   383 qed "double_complement";

   384 Addsimps[double_complement];

   385 

   386 Goal "-(A Un B) = (-A) Int (-B)";

   387 by (Blast_tac 1);

   388 qed "Compl_Un";

   389 

   390 Goal "-(A Int B) = (-A) Un (-B)";

   391 by (Blast_tac 1);

   392 qed "Compl_Int";

   393 

   394 Goal "-(UN x:A. B(x)) = (INT x:A. -B(x))";

   395 by (Blast_tac 1);

   396 qed "Compl_UN";

   397 

   398 Goal "-(INT x:A. B(x)) = (UN x:A. -B(x))";

   399 by (Blast_tac 1);

   400 qed "Compl_INT";

   401 

   402 Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];

   403 

   404 (*Halmos, Naive Set Theory, page 16.*)

   405 

   406 Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";

   407 by (blast_tac (claset() addSEs [equalityCE]) 1);

   408 qed "Un_Int_assoc_eq";

   409 

   410 

   411 section "Union";

   412 

   413 Goal "Union({}) = {}";

   414 by (Blast_tac 1);

   415 qed "Union_empty";

   416 Addsimps[Union_empty];

   417 

   418 Goal "Union(UNIV) = UNIV";

   419 by (Blast_tac 1);

   420 qed "Union_UNIV";

   421 Addsimps[Union_UNIV];

   422 

   423 Goal "Union(insert a B) = a Un Union(B)";

   424 by (Blast_tac 1);

   425 qed "Union_insert";

   426 Addsimps[Union_insert];

   427 

   428 Goal "Union(A Un B) = Union(A) Un Union(B)";

   429 by (Blast_tac 1);

   430 qed "Union_Un_distrib";

   431 Addsimps[Union_Un_distrib];

   432 

   433 Goal "Union(A Int B) <= Union(A) Int Union(B)";

   434 by (Blast_tac 1);

   435 qed "Union_Int_subset";

   436 

   437 Goal "(Union M = {}) = (! A : M. A = {})"; 

   438 by (blast_tac (claset() addEs [equalityCE]) 1);

   439 qed "Union_empty_conv"; 

   440 AddIffs [Union_empty_conv];

   441 

   442 Goal "(Union(C) Int A = {}) = (! B:C. B Int A = {})";

   443 by (blast_tac (claset() addSEs [equalityCE]) 1);

   444 qed "Union_disjoint";

   445 

   446 section "Inter";

   447 

   448 Goal "Inter({}) = UNIV";

   449 by (Blast_tac 1);

   450 qed "Inter_empty";

   451 Addsimps[Inter_empty];

   452 

   453 Goal "Inter(UNIV) = {}";

   454 by (Blast_tac 1);

   455 qed "Inter_UNIV";

   456 Addsimps[Inter_UNIV];

   457 

   458 Goal "Inter(insert a B) = a Int Inter(B)";

   459 by (Blast_tac 1);

   460 qed "Inter_insert";

   461 Addsimps[Inter_insert];

   462 

   463 Goal "Inter(A) Un Inter(B) <= Inter(A Int B)";

   464 by (Blast_tac 1);

   465 qed "Inter_Un_subset";

   466 

   467 Goal "Inter(A Un B) = Inter(A) Int Inter(B)";

   468 by (Blast_tac 1);

   469 qed "Inter_Un_distrib";

   470 

   471 section "UN and INT";

   472 

   473 (*Basic identities*)

   474 

   475 bind_thm ("not_empty", prove_goal thy "(A ~= {}) = (? x. x:A)" (K [Blast_tac 1]));

   476 

   477 Goal "(UN x:{}. B x) = {}";

   478 by (Blast_tac 1);

   479 qed "UN_empty";

   480 Addsimps[UN_empty];

   481 

   482 Goal "(UN x:A. {}) = {}";

   483 by (Blast_tac 1);

   484 qed "UN_empty2";

   485 Addsimps[UN_empty2];

   486 

   487 Goal "(UN x:A. {x}) = A";

   488 by (Blast_tac 1);

   489 qed "UN_singleton";

   490 Addsimps [UN_singleton];

   491 

   492 Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";

   493 by (Blast_tac 1);

   494 qed "UN_absorb";

   495 

   496 Goal "(INT x:{}. B x) = UNIV";

   497 by (Blast_tac 1);

   498 qed "INT_empty";

   499 Addsimps[INT_empty];

   500 

   501 Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";

   502 by (Blast_tac 1);

   503 qed "INT_absorb";

   504 

   505 Goal "(UN x:insert a A. B x) = B a Un UNION A B";

   506 by (Blast_tac 1);

   507 qed "UN_insert";

   508 Addsimps[UN_insert];

   509 

   510 Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)";

   511 by (Blast_tac 1);

   512 qed "UN_Un";

   513 

   514 Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)";

   515 by (Blast_tac 1);

   516 qed "UN_UN_flatten";

   517 

   518 Goal "((UN i:I. A i) <= B) = (ALL i:I. A i <= B)";

   519 by (Blast_tac 1);

   520 qed "UN_subset_iff";

   521 

   522 Goal "(B <= (INT i:I. A i)) = (ALL i:I. B <= A i)";

   523 by (Blast_tac 1);

   524 qed "INT_subset_iff";

   525 

   526 Goal "(INT x:insert a A. B x) = B a Int INTER A B";

   527 by (Blast_tac 1);

   528 qed "INT_insert";

   529 Addsimps[INT_insert];

   530 

   531 Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)";

   532 by (Blast_tac 1);

   533 qed "INT_Un";

   534 

   535 Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";

   536 by (Blast_tac 1);

   537 qed "INT_insert_distrib";

   538 

   539 Goal "Union(B``A) = (UN x:A. B(x))";

   540 by (Blast_tac 1);

   541 qed "Union_image_eq";

   542 Addsimps [Union_image_eq];

   543 

   544 Goal "f `` Union S = (UN x:S. f `` x)";

   545 by (Blast_tac 1);

   546 qed "image_Union_eq";

   547 

   548 Goal "Inter(B``A) = (INT x:A. B(x))";

   549 by (Blast_tac 1);

   550 qed "Inter_image_eq";

   551 Addsimps [Inter_image_eq];

   552 

   553 Goal "u: A ==> (UN y:A. c) = c";

   554 by (Blast_tac 1);

   555 qed "UN_constant";

   556 Addsimps[UN_constant];

   557 

   558 Goal "u: A ==> (INT y:A. c) = c";

   559 by (Blast_tac 1);

   560 qed "INT_constant";

   561 Addsimps[INT_constant];

   562 

   563 Goal "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";

   564 by (Blast_tac 1);

   565 qed "UN_eq";

   566 

   567 (*Look: it has an EXISTENTIAL quantifier*)

   568 Goal "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";

   569 by (Blast_tac 1);

   570 qed "INT_eq";

   571 

   572 

   573 (*Distributive laws...*)

   574 

   575 Goal "A Int Union(B) = (UN C:B. A Int C)";

   576 by (Blast_tac 1);

   577 qed "Int_Union";

   578 

   579 Goal "Union(B) Int A = (UN C:B. C Int A)";

   580 by (Blast_tac 1);

   581 qed "Int_Union2";

   582 

   583 (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 

   584    Union of a family of unions **)

   585 Goal "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";

   586 by (Blast_tac 1);

   587 qed "Un_Union_image";

   588 

   589 (*Equivalent version*)

   590 Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";

   591 by (Blast_tac 1);

   592 qed "UN_Un_distrib";

   593 

   594 Goal "A Un Inter(B) = (INT C:B. A Un C)";

   595 by (Blast_tac 1);

   596 qed "Un_Inter";

   597 

   598 Goal "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";

   599 by (Blast_tac 1);

   600 qed "Int_Inter_image";

   601 

   602 (*Equivalent version*)

   603 Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";

   604 by (Blast_tac 1);

   605 qed "INT_Int_distrib";

   606 

   607 (*Halmos, Naive Set Theory, page 35.*)

   608 Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";

   609 by (Blast_tac 1);

   610 qed "Int_UN_distrib";

   611 

   612 Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";

   613 by (Blast_tac 1);

   614 qed "Un_INT_distrib";

   615 

   616 Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";

   617 by (Blast_tac 1);

   618 qed "Int_UN_distrib2";

   619 

   620 Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";

   621 by (Blast_tac 1);

   622 qed "Un_INT_distrib2";

   623 

   624 

   625 section"Bounded quantifiers";

   626 

   627 (** The following are not added to the default simpset because

   628     (a) they duplicate the body and (b) there are no similar rules for Int. **)

   629 

   630 Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";

   631 by (Blast_tac 1);

   632 qed "ball_Un";

   633 

   634 Goal "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";

   635 by (Blast_tac 1);

   636 qed "bex_Un";

   637 

   638 Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)";

   639 by (Blast_tac 1);

   640 qed "ball_UN";

   641 

   642 Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)";

   643 by (Blast_tac 1);

   644 qed "bex_UN";

   645 

   646 

   647 section "-";

   648 

   649 Goal "A-B = A Int (-B)";

   650 by (Blast_tac 1);

   651 qed "Diff_eq";

   652 

   653 Goal "(A-B = {}) = (A<=B)";

   654 by (Blast_tac 1);

   655 qed "Diff_eq_empty_iff";

   656 Addsimps[Diff_eq_empty_iff];

   657 

   658 Goal "A-A = {}";

   659 by (Blast_tac 1);

   660 qed "Diff_cancel";

   661 Addsimps[Diff_cancel];

   662 

   663 Goal "A Int B = {} ==> A-B = A";

   664 by (blast_tac (claset() addEs [equalityE]) 1);

   665 qed "Diff_triv";

   666 

   667 Goal "{}-A = {}";

   668 by (Blast_tac 1);

   669 qed "empty_Diff";

   670 Addsimps[empty_Diff];

   671 

   672 Goal "A-{} = A";

   673 by (Blast_tac 1);

   674 qed "Diff_empty";

   675 Addsimps[Diff_empty];

   676 

   677 Goal "A-UNIV = {}";

   678 by (Blast_tac 1);

   679 qed "Diff_UNIV";

   680 Addsimps[Diff_UNIV];

   681 

   682 Goal "x~:A ==> A - insert x B = A-B";

   683 by (Blast_tac 1);

   684 qed "Diff_insert0";

   685 Addsimps [Diff_insert0];

   686 

   687 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)

   688 Goal "A - insert a B = A - B - {a}";

   689 by (Blast_tac 1);

   690 qed "Diff_insert";

   691 

   692 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)

   693 Goal "A - insert a B = A - {a} - B";

   694 by (Blast_tac 1);

   695 qed "Diff_insert2";

   696 

   697 Goal "insert x A - B = (if x:B then A-B else insert x (A-B))";

   698 by (Simp_tac 1);

   699 by (Blast_tac 1);

   700 qed "insert_Diff_if";

   701 

   702 Goal "x:B ==> insert x A - B = A-B";

   703 by (Blast_tac 1);

   704 qed "insert_Diff1";

   705 Addsimps [insert_Diff1];

   706 

   707 Goal "a:A ==> insert a (A-{a}) = A";

   708 by (Blast_tac 1);

   709 qed "insert_Diff";

   710 

   711 Goal "x ~: A ==> (insert x A) - {x} = A";

   712 by Auto_tac;

   713 qed "Diff_insert_absorb";

   714 

   715 Goal "A Int (B-A) = {}";

   716 by (Blast_tac 1);

   717 qed "Diff_disjoint";

   718 Addsimps[Diff_disjoint];

   719 

   720 Goal "A<=B ==> A Un (B-A) = B";

   721 by (Blast_tac 1);

   722 qed "Diff_partition";

   723 

   724 Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";

   725 by (Blast_tac 1);

   726 qed "double_diff";

   727 

   728 Goal "A Un (B-A) = A Un B";

   729 by (Blast_tac 1);

   730 qed "Un_Diff_cancel";

   731 

   732 Goal "(B-A) Un A = B Un A";

   733 by (Blast_tac 1);

   734 qed "Un_Diff_cancel2";

   735 

   736 Addsimps [Un_Diff_cancel, Un_Diff_cancel2];

   737 

   738 Goal "A - (B Un C) = (A-B) Int (A-C)";

   739 by (Blast_tac 1);

   740 qed "Diff_Un";

   741 

   742 Goal "A - (B Int C) = (A-B) Un (A-C)";

   743 by (Blast_tac 1);

   744 qed "Diff_Int";

   745 

   746 Goal "(A Un B) - C = (A - C) Un (B - C)";

   747 by (Blast_tac 1);

   748 qed "Un_Diff";

   749 

   750 Goal "(A Int B) - C = A Int (B - C)";

   751 by (Blast_tac 1);

   752 qed "Int_Diff";

   753 

   754 Goal "C Int (A-B) = (C Int A) - (C Int B)";

   755 by (Blast_tac 1);

   756 qed "Diff_Int_distrib";

   757 

   758 Goal "(A-B) Int C = (A Int C) - (B Int C)";

   759 by (Blast_tac 1);

   760 qed "Diff_Int_distrib2";

   761 

   762 Goal "A - (- B) = A Int B";

   763 by Auto_tac;

   764 qed "Diff_Compl";

   765 Addsimps [Diff_Compl];

   766 

   767 

   768 section "Quantification over type \"bool\"";

   769 

   770 Goal "(ALL b::bool. P b) = (P True & P False)";

   771 by Auto_tac;

   772 by (case_tac "b" 1);

   773 by Auto_tac;

   774 qed "all_bool_eq";

   775 

   776 bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec);

   777 

   778 Goal "(EX b::bool. P b) = (P True | P False)";

   779 by Auto_tac;

   780 by (case_tac "b" 1);

   781 by Auto_tac;

   782 qed "ex_bool_eq";

   783 

   784 Goal "A Un B = (UN b. if b then A else B)";

   785 by (auto_tac(claset(), simpset() addsimps [split_if_mem2]));

   786 qed "Un_eq_UN";

   787 

   788 Goal "(UN b::bool. A b) = (A True Un A False)";

   789 by Auto_tac;

   790 by (case_tac "b" 1);

   791 by Auto_tac;

   792 qed "UN_bool_eq";

   793 

   794 Goal "(INT b::bool. A b) = (A True Int A False)";

   795 by Auto_tac;

   796 by (case_tac "b" 1);

   797 by Auto_tac;

   798 qed "INT_bool_eq";

   799 

   800 

   801 section "Pow";

   802 

   803 Goalw [Pow_def] "Pow {} = {{}}";

   804 by Auto_tac;

   805 qed "Pow_empty";

   806 Addsimps [Pow_empty];

   807 

   808 Goal "Pow (insert a A) = Pow A Un (insert a `` Pow A)";

   809 by Safe_tac;

   810 by (etac swap 1);

   811 by (res_inst_tac [("x", "x-{a}")] image_eqI 1);

   812 by (ALLGOALS Blast_tac);

   813 qed "Pow_insert";

   814 

   815 Goal "Pow (- A) = {-B |B. A: Pow B}";

   816 by Safe_tac;

   817 by (Blast_tac 2);

   818 by (res_inst_tac [("x", "-x")] exI 1);

   819 by (ALLGOALS Blast_tac);

   820 qed "Pow_Compl";

   821 

   822 Goal "Pow UNIV = UNIV";

   823 by (Blast_tac 1);

   824 qed "Pow_UNIV";

   825 Addsimps [Pow_UNIV];

   826 

   827 Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";

   828 by (Blast_tac 1);

   829 qed "Un_Pow_subset";

   830 

   831 Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";

   832 by (Blast_tac 1);

   833 qed "UN_Pow_subset";

   834 

   835 Goal "A <= Pow(Union(A))";

   836 by (Blast_tac 1);

   837 qed "subset_Pow_Union";

   838 

   839 Goal "Union(Pow(A)) = A";

   840 by (Blast_tac 1);

   841 qed "Union_Pow_eq";

   842 

   843 Goal "Pow(A Int B) = Pow(A) Int Pow(B)";

   844 by (Blast_tac 1);

   845 qed "Pow_Int_eq";

   846 

   847 Goal "Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))";

   848 by (Blast_tac 1);

   849 qed "Pow_INT_eq";

   850 

   851 Addsimps [Union_Pow_eq, Pow_Int_eq];

   852 

   853 

   854 section "Miscellany";

   855 

   856 Goal "(A = B) = ((A <= (B::'a set)) & (B<=A))";

   857 by (Blast_tac 1);

   858 qed "set_eq_subset";

   859 

   860 Goal "A <= B =  (! t. t:A --> t:B)";

   861 by (Blast_tac 1);

   862 qed "subset_iff";

   863 

   864 Goalw [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";

   865 by (Blast_tac 1);

   866 qed "subset_iff_psubset_eq";

   867 

   868 Goal "(!x. x ~: A) = (A={})";

   869 by (Blast_tac 1);

   870 qed "all_not_in_conv";

   871 AddIffs [all_not_in_conv];

   872 

   873 

   874 (** for datatypes **)

   875 Goal "f x ~= f y ==> x ~= y";

   876 by (Fast_tac 1);

   877 qed "distinct_lemma";

   878 

   879 

   880 (** Miniscoping: pushing in big Unions and Intersections **)

   881 local

   882   fun prover s = prove_goal thy s (fn _ => [Blast_tac 1])

   883 in

   884 val UN_simps = map prover 

   885     ["!!C. c: C ==> (UN x:C. insert a (B x)) = insert a (UN x:C. B x)",

   886      "!!C. c: C ==> (UN x:C. A x Un B)   = ((UN x:C. A x) Un B)",

   887      "!!C. c: C ==> (UN x:C. A Un B x)   = (A Un (UN x:C. B x))",

   888      "(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",

   889      "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",

   890      "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",

   891      "(UN x:C. A - B x)    = (A - (INT x:C. B x))",

   892      "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",

   893      "(UN z: UNION A B. C z) = (UN  x:A. UN z: B(x). C z)",

   894      "(UN x:f``A. B x)     = (UN a:A. B(f a))"];

   895 

   896 val INT_simps = map prover

   897     ["!!C. c: C ==> (INT x:C. A x Int B) = ((INT x:C. A x) Int B)",

   898      "!!C. c: C ==> (INT x:C. A Int B x) = (A Int (INT x:C. B x))",

   899      "!!C. c: C ==> (INT x:C. A x - B)   = ((INT x:C. A x) - B)",

   900      "!!C. c: C ==> (INT x:C. A - B x)   = (A - (UN x:C. B x))",

   901      "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",

   902      "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",

   903      "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))",

   904      "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",

   905      "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",

   906      "(INT x:f``A. B x)    = (INT a:A. B(f a))"];

   907 

   908 

   909 val ball_simps = map prover

   910     ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",

   911      "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",

   912      "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",

   913      "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",

   914      "(ALL x:{}. P x) = True",

   915      "(ALL x:UNIV. P x) = (ALL x. P x)",

   916      "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",

   917      "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",

   918      "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",

   919      "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",

   920      "(ALL x:f``A. P x) = (ALL x:A. P(f x))",

   921      "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];

   922 

   923 val ball_conj_distrib = 

   924     prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";

   925 

   926 val bex_simps = map prover

   927     ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",

   928      "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",

   929      "(EX x:{}. P x) = False",

   930      "(EX x:UNIV. P x) = (EX x. P x)",

   931      "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",

   932      "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",

   933      "(EX x: UNION A B. P x) = (EX a:A. EX x: B a.  P x)",

   934      "(EX x:Collect Q. P x) = (EX x. Q x & P x)",

   935      "(EX x:f``A. P x) = (EX x:A. P(f x))",

   936      "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];

   937 

   938 val bex_disj_distrib = 

   939     prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";

   940 

   941 end;

   942 

   943 bind_thms ("UN_simps", UN_simps);

   944 bind_thms ("INT_simps", INT_simps);

   945 bind_thms ("ball_simps", ball_simps);

   946 bind_thms ("bex_simps", bex_simps);

   947 bind_thm ("ball_conj_distrib", ball_conj_distrib);

   948 bind_thm ("bex_disj_distrib", bex_disj_distrib);

   949 

   950 Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);
wneuper/isa