src/HOL/equalities.ML
author berghofe
Thu May 23 15:17:23 1996 +0200 (1996-05-23)
changeset 1763 fb07e359b59f
parent 1754 852093aeb0ab
child 1786 8a31d85d27b8
permissions -rw-r--r--
expanded TABs
     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 val eq_cs = set_cs addSIs [equalityI];
    14 
    15 section "{}";
    16 
    17 goal Set.thy "{x.False} = {}";
    18 by (Fast_tac 1);
    19 qed "Collect_False_empty";
    20 Addsimps [Collect_False_empty];
    21 
    22 goal Set.thy "(A <= {}) = (A = {})";
    23 by (Fast_tac 1);
    24 qed "subset_empty";
    25 Addsimps [subset_empty];
    26 
    27 section ":";
    28 
    29 goal Set.thy "x ~: {}";
    30 by (Fast_tac 1);
    31 qed "in_empty";
    32 Addsimps[in_empty];
    33 
    34 goal Set.thy "x : insert y A = (x=y | x:A)";
    35 by (Fast_tac 1);
    36 qed "in_insert";
    37 Addsimps[in_insert];
    38 
    39 section "insert";
    40 
    41 (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    42 goal Set.thy "insert a A = {a} Un A";
    43 by (Fast_tac 1);
    44 qed "insert_is_Un";
    45 
    46 goal Set.thy "insert a A ~= {}";
    47 by (fast_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 Set.thy "!!a. a:A ==> insert a A = A";
    55 by (Fast_tac 1);
    56 qed "insert_absorb";
    57 
    58 goal Set.thy "insert x (insert x A) = insert x A";
    59 by (Fast_tac 1);
    60 qed "insert_absorb2";
    61 Addsimps [insert_absorb2];
    62 
    63 goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
    64 by (Fast_tac 1);
    65 qed "insert_subset";
    66 Addsimps[insert_subset];
    67 
    68 (* use new B rather than (A-{a}) to avoid infinite unfolding *)
    69 goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
    70 by (res_inst_tac [("x","A-{a}")] exI 1);
    71 by (Fast_tac 1);
    72 qed "mk_disjoint_insert";
    73 
    74 section "``";
    75 
    76 goal Set.thy "f``{} = {}";
    77 by (Fast_tac 1);
    78 qed "image_empty";
    79 Addsimps[image_empty];
    80 
    81 goal Set.thy "f``insert a B = insert (f a) (f``B)";
    82 by (Fast_tac 1);
    83 qed "image_insert";
    84 Addsimps[image_insert];
    85 
    86 qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
    87  (fn _ => [Fast_tac 1]);
    88 
    89 goalw Set.thy [image_def]
    90 "(%x. if P x then f x else g x) `` S                    \
    91 \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
    92 by(split_tac [expand_if] 1);
    93 by(Fast_tac 1);
    94 qed "if_image_distrib";
    95 Addsimps[if_image_distrib];
    96 
    97 
    98 section "range";
    99 
   100 qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
   101  (fn _ => [Fast_tac 1]);
   102 
   103 qed_goalw "image_range" Set.thy [image_def, range_def]
   104  "f``range g = range (%x. f (g x))" (fn _ => [
   105         rtac Collect_cong 1,
   106         Fast_tac 1]);
   107 
   108 section "Int";
   109 
   110 goal Set.thy "A Int A = A";
   111 by (Fast_tac 1);
   112 qed "Int_absorb";
   113 Addsimps[Int_absorb];
   114 
   115 goal Set.thy "A Int B  =  B Int A";
   116 by (Fast_tac 1);
   117 qed "Int_commute";
   118 
   119 goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
   120 by (Fast_tac 1);
   121 qed "Int_assoc";
   122 
   123 goal Set.thy "{} Int B = {}";
   124 by (Fast_tac 1);
   125 qed "Int_empty_left";
   126 Addsimps[Int_empty_left];
   127 
   128 goal Set.thy "A Int {} = {}";
   129 by (Fast_tac 1);
   130 qed "Int_empty_right";
   131 Addsimps[Int_empty_right];
   132 
   133 goal Set.thy "UNIV Int B = B";
   134 by (Fast_tac 1);
   135 qed "Int_UNIV_left";
   136 Addsimps[Int_UNIV_left];
   137 
   138 goal Set.thy "A Int UNIV = A";
   139 by (Fast_tac 1);
   140 qed "Int_UNIV_right";
   141 Addsimps[Int_UNIV_right];
   142 
   143 goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
   144 by (Fast_tac 1);
   145 qed "Int_Un_distrib";
   146 
   147 goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
   148 by (Fast_tac 1);
   149 qed "Int_Un_distrib2";
   150 
   151 goal Set.thy "(A<=B) = (A Int B = A)";
   152 by (fast_tac (!claset addSEs [equalityE]) 1);
   153 qed "subset_Int_eq";
   154 
   155 goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
   156 by (fast_tac (!claset addEs [equalityCE]) 1);
   157 qed "Int_UNIV";
   158 Addsimps[Int_UNIV];
   159 
   160 section "Un";
   161 
   162 goal Set.thy "A Un A = A";
   163 by (Fast_tac 1);
   164 qed "Un_absorb";
   165 Addsimps[Un_absorb];
   166 
   167 goal Set.thy "A Un B  =  B Un A";
   168 by (Fast_tac 1);
   169 qed "Un_commute";
   170 
   171 goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
   172 by (Fast_tac 1);
   173 qed "Un_assoc";
   174 
   175 goal Set.thy "{} Un B = B";
   176 by (Fast_tac 1);
   177 qed "Un_empty_left";
   178 Addsimps[Un_empty_left];
   179 
   180 goal Set.thy "A Un {} = A";
   181 by (Fast_tac 1);
   182 qed "Un_empty_right";
   183 Addsimps[Un_empty_right];
   184 
   185 goal Set.thy "UNIV Un B = UNIV";
   186 by (Fast_tac 1);
   187 qed "Un_UNIV_left";
   188 Addsimps[Un_UNIV_left];
   189 
   190 goal Set.thy "A Un UNIV = UNIV";
   191 by (Fast_tac 1);
   192 qed "Un_UNIV_right";
   193 Addsimps[Un_UNIV_right];
   194 
   195 goal Set.thy "insert a B Un C = insert a (B Un C)";
   196 by (Fast_tac 1);
   197 qed "Un_insert_left";
   198 
   199 goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
   200 by (Fast_tac 1);
   201 qed "Un_Int_distrib";
   202 
   203 goal Set.thy
   204  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
   205 by (Fast_tac 1);
   206 qed "Un_Int_crazy";
   207 
   208 goal Set.thy "(A<=B) = (A Un B = B)";
   209 by (fast_tac (!claset addSEs [equalityE]) 1);
   210 qed "subset_Un_eq";
   211 
   212 goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
   213 by (Fast_tac 1);
   214 qed "subset_insert_iff";
   215 
   216 goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
   217 by (fast_tac (!claset addEs [equalityCE]) 1);
   218 qed "Un_empty";
   219 Addsimps[Un_empty];
   220 
   221 section "Compl";
   222 
   223 goal Set.thy "A Int Compl(A) = {}";
   224 by (Fast_tac 1);
   225 qed "Compl_disjoint";
   226 Addsimps[Compl_disjoint];
   227 
   228 goal Set.thy "A Un Compl(A) = UNIV";
   229 by (Fast_tac 1);
   230 qed "Compl_partition";
   231 
   232 goal Set.thy "Compl(Compl(A)) = A";
   233 by (Fast_tac 1);
   234 qed "double_complement";
   235 Addsimps[double_complement];
   236 
   237 goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
   238 by (Fast_tac 1);
   239 qed "Compl_Un";
   240 
   241 goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
   242 by (Fast_tac 1);
   243 qed "Compl_Int";
   244 
   245 goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
   246 by (Fast_tac 1);
   247 qed "Compl_UN";
   248 
   249 goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
   250 by (Fast_tac 1);
   251 qed "Compl_INT";
   252 
   253 (*Halmos, Naive Set Theory, page 16.*)
   254 
   255 goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
   256 by (fast_tac (!claset addSEs [equalityE]) 1);
   257 qed "Un_Int_assoc_eq";
   258 
   259 
   260 section "Union";
   261 
   262 goal Set.thy "Union({}) = {}";
   263 by (Fast_tac 1);
   264 qed "Union_empty";
   265 Addsimps[Union_empty];
   266 
   267 goal Set.thy "Union(UNIV) = UNIV";
   268 by (Fast_tac 1);
   269 qed "Union_UNIV";
   270 Addsimps[Union_UNIV];
   271 
   272 goal Set.thy "Union(insert a B) = a Un Union(B)";
   273 by (Fast_tac 1);
   274 qed "Union_insert";
   275 Addsimps[Union_insert];
   276 
   277 goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
   278 by (Fast_tac 1);
   279 qed "Union_Un_distrib";
   280 Addsimps[Union_Un_distrib];
   281 
   282 goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
   283 by (Fast_tac 1);
   284 qed "Union_Int_subset";
   285 
   286 val prems = goal Set.thy
   287    "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
   288 by (fast_tac (!claset addSEs [equalityE]) 1);
   289 qed "Union_disjoint";
   290 
   291 section "Inter";
   292 
   293 goal Set.thy "Inter({}) = UNIV";
   294 by (Fast_tac 1);
   295 qed "Inter_empty";
   296 Addsimps[Inter_empty];
   297 
   298 goal Set.thy "Inter(UNIV) = {}";
   299 by (Fast_tac 1);
   300 qed "Inter_UNIV";
   301 Addsimps[Inter_UNIV];
   302 
   303 goal Set.thy "Inter(insert a B) = a Int Inter(B)";
   304 by (Fast_tac 1);
   305 qed "Inter_insert";
   306 Addsimps[Inter_insert];
   307 
   308 goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
   309 by (Fast_tac 1);
   310 qed "Inter_Un_subset";
   311 
   312 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
   313 by (best_tac eq_cs 1);
   314 qed "Inter_Un_distrib";
   315 
   316 section "UN and INT";
   317 
   318 (*Basic identities*)
   319 
   320 goal Set.thy "(UN x:{}. B x) = {}";
   321 by (Fast_tac 1);
   322 qed "UN_empty";
   323 Addsimps[UN_empty];
   324 
   325 goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
   326 by (Fast_tac 1);
   327 qed "UN_UNIV";
   328 Addsimps[UN_UNIV];
   329 
   330 goal Set.thy "(INT x:{}. B x) = UNIV";
   331 by (Fast_tac 1);
   332 qed "INT_empty";
   333 Addsimps[INT_empty];
   334 
   335 goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
   336 by (Fast_tac 1);
   337 qed "INT_UNIV";
   338 Addsimps[INT_UNIV];
   339 
   340 goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
   341 by (Fast_tac 1);
   342 qed "UN_insert";
   343 Addsimps[UN_insert];
   344 
   345 goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
   346 by (Fast_tac 1);
   347 qed "INT_insert";
   348 Addsimps[INT_insert];
   349 
   350 goal Set.thy "Union(range(f)) = (UN x.f(x))";
   351 by (Fast_tac 1);
   352 qed "Union_range_eq";
   353 
   354 goal Set.thy "Inter(range(f)) = (INT x.f(x))";
   355 by (Fast_tac 1);
   356 qed "Inter_range_eq";
   357 
   358 goal Set.thy "Union(B``A) = (UN x:A. B(x))";
   359 by (Fast_tac 1);
   360 qed "Union_image_eq";
   361 
   362 goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
   363 by (Fast_tac 1);
   364 qed "Inter_image_eq";
   365 
   366 goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
   367 by (Fast_tac 1);
   368 qed "UN_constant";
   369 
   370 goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
   371 by (Fast_tac 1);
   372 qed "INT_constant";
   373 
   374 goal Set.thy "(UN x.B) = B";
   375 by (Fast_tac 1);
   376 qed "UN1_constant";
   377 Addsimps[UN1_constant];
   378 
   379 goal Set.thy "(INT x.B) = B";
   380 by (Fast_tac 1);
   381 qed "INT1_constant";
   382 Addsimps[INT1_constant];
   383 
   384 goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
   385 by (Fast_tac 1);
   386 qed "UN_eq";
   387 
   388 (*Look: it has an EXISTENTIAL quantifier*)
   389 goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
   390 by (Fast_tac 1);
   391 qed "INT_eq";
   392 
   393 (*Distributive laws...*)
   394 
   395 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
   396 by (Fast_tac 1);
   397 qed "Int_Union";
   398 
   399 (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
   400    Union of a family of unions **)
   401 goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
   402 by (Fast_tac 1);
   403 qed "Un_Union_image";
   404 
   405 (*Equivalent version*)
   406 goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
   407 by (Fast_tac 1);
   408 qed "UN_Un_distrib";
   409 
   410 goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
   411 by (Fast_tac 1);
   412 qed "Un_Inter";
   413 
   414 goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
   415 by (best_tac eq_cs 1);
   416 qed "Int_Inter_image";
   417 
   418 (*Equivalent version*)
   419 goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
   420 by (Fast_tac 1);
   421 qed "INT_Int_distrib";
   422 
   423 (*Halmos, Naive Set Theory, page 35.*)
   424 goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
   425 by (Fast_tac 1);
   426 qed "Int_UN_distrib";
   427 
   428 goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
   429 by (Fast_tac 1);
   430 qed "Un_INT_distrib";
   431 
   432 goal Set.thy
   433     "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
   434 by (Fast_tac 1);
   435 qed "Int_UN_distrib2";
   436 
   437 goal Set.thy
   438     "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
   439 by (Fast_tac 1);
   440 qed "Un_INT_distrib2";
   441 
   442 section "-";
   443 
   444 goal Set.thy "A-A = {}";
   445 by (Fast_tac 1);
   446 qed "Diff_cancel";
   447 Addsimps[Diff_cancel];
   448 
   449 goal Set.thy "{}-A = {}";
   450 by (Fast_tac 1);
   451 qed "empty_Diff";
   452 Addsimps[empty_Diff];
   453 
   454 goal Set.thy "A-{} = A";
   455 by (Fast_tac 1);
   456 qed "Diff_empty";
   457 Addsimps[Diff_empty];
   458 
   459 goal Set.thy "A-UNIV = {}";
   460 by (Fast_tac 1);
   461 qed "Diff_UNIV";
   462 Addsimps[Diff_UNIV];
   463 
   464 goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
   465 by (Fast_tac 1);
   466 qed "Diff_insert0";
   467 Addsimps [Diff_insert0];
   468 
   469 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   470 goal Set.thy "A - insert a B = A - B - {a}";
   471 by (Fast_tac 1);
   472 qed "Diff_insert";
   473 
   474 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   475 goal Set.thy "A - insert a B = A - {a} - B";
   476 by (Fast_tac 1);
   477 qed "Diff_insert2";
   478 
   479 goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
   480 by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
   481 by (Fast_tac 1);
   482 qed "insert_Diff_if";
   483 
   484 goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
   485 by (Fast_tac 1);
   486 qed "insert_Diff1";
   487 Addsimps [insert_Diff1];
   488 
   489 val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
   490 by (fast_tac (!claset addSIs prems) 1);
   491 qed "insert_Diff";
   492 
   493 goal Set.thy "A Int (B-A) = {}";
   494 by (Fast_tac 1);
   495 qed "Diff_disjoint";
   496 Addsimps[Diff_disjoint];
   497 
   498 goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
   499 by (Fast_tac 1);
   500 qed "Diff_partition";
   501 
   502 goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
   503 by (Fast_tac 1);
   504 qed "double_diff";
   505 
   506 goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
   507 by (Fast_tac 1);
   508 qed "Diff_Un";
   509 
   510 goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
   511 by (Fast_tac 1);
   512 qed "Diff_Int";
   513 
   514 Addsimps[subset_UNIV, empty_subsetI, subset_refl];