src/HOL/equalities.ML
author clasohm
Wed Oct 04 13:10:03 1995 +0100 (1995-10-04 ago)
changeset 1264 3eb91524b938
parent 1179 7678408f9751
child 1465 5d7a7e439cec
permissions -rw-r--r--
added local simpsets; removed IOA from 'make test'
     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 val eq_cs = set_cs addSIs [equalityI];
    12 
    13 (** The membership relation, : **)
    14 
    15 goal Set.thy "x ~: {}";
    16 by(fast_tac set_cs 1);
    17 qed "in_empty";
    18 
    19 goal Set.thy "x : insert y A = (x=y | x:A)";
    20 by(fast_tac set_cs 1);
    21 qed "in_insert";
    22 
    23 (** insert **)
    24 
    25 goal Set.thy "insert a A ~= {}";
    26 by (fast_tac (set_cs addEs [equalityCE]) 1);
    27 qed"insert_not_empty";
    28 
    29 bind_thm("empty_not_insert",insert_not_empty RS not_sym);
    30 
    31 goal Set.thy "!!a. a:A ==> insert a A = A";
    32 by (fast_tac eq_cs 1);
    33 qed "insert_absorb";
    34 
    35 goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
    36 by (fast_tac set_cs 1);
    37 qed "insert_subset";
    38 
    39 (** Image **)
    40 
    41 goal Set.thy "f``{} = {}";
    42 by (fast_tac eq_cs 1);
    43 qed "image_empty";
    44 
    45 goal Set.thy "f``insert a B = insert (f a) (f``B)";
    46 by (fast_tac eq_cs 1);
    47 qed "image_insert";
    48 
    49 (** Binary Intersection **)
    50 
    51 goal Set.thy "A Int A = A";
    52 by (fast_tac eq_cs 1);
    53 qed "Int_absorb";
    54 
    55 goal Set.thy "A Int B  =  B Int A";
    56 by (fast_tac eq_cs 1);
    57 qed "Int_commute";
    58 
    59 goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
    60 by (fast_tac eq_cs 1);
    61 qed "Int_assoc";
    62 
    63 goal Set.thy "{} Int B = {}";
    64 by (fast_tac eq_cs 1);
    65 qed "Int_empty_left";
    66 
    67 goal Set.thy "A Int {} = {}";
    68 by (fast_tac eq_cs 1);
    69 qed "Int_empty_right";
    70 
    71 goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
    72 by (fast_tac eq_cs 1);
    73 qed "Int_Un_distrib";
    74 
    75 goal Set.thy "(A<=B) = (A Int B = A)";
    76 by (fast_tac (eq_cs addSEs [equalityE]) 1);
    77 qed "subset_Int_eq";
    78 
    79 (** Binary Union **)
    80 
    81 goal Set.thy "A Un A = A";
    82 by (fast_tac eq_cs 1);
    83 qed "Un_absorb";
    84 
    85 goal Set.thy "A Un B  =  B Un A";
    86 by (fast_tac eq_cs 1);
    87 qed "Un_commute";
    88 
    89 goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
    90 by (fast_tac eq_cs 1);
    91 qed "Un_assoc";
    92 
    93 goal Set.thy "{} Un B = B";
    94 by(fast_tac eq_cs 1);
    95 qed "Un_empty_left";
    96 
    97 goal Set.thy "A Un {} = A";
    98 by(fast_tac eq_cs 1);
    99 qed "Un_empty_right";
   100 
   101 goal Set.thy "insert a B Un C = insert a (B Un C)";
   102 by(fast_tac eq_cs 1);
   103 qed "Un_insert_left";
   104 
   105 goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
   106 by (fast_tac eq_cs 1);
   107 qed "Un_Int_distrib";
   108 
   109 goal Set.thy
   110  "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
   111 by (fast_tac eq_cs 1);
   112 qed "Un_Int_crazy";
   113 
   114 goal Set.thy "(A<=B) = (A Un B = B)";
   115 by (fast_tac (eq_cs addSEs [equalityE]) 1);
   116 qed "subset_Un_eq";
   117 
   118 goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
   119 by (fast_tac eq_cs 1);
   120 qed "subset_insert_iff";
   121 
   122 goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
   123 by (fast_tac (eq_cs addEs [equalityCE]) 1);
   124 qed "Un_empty";
   125 
   126 (** Simple properties of Compl -- complement of a set **)
   127 
   128 goal Set.thy "A Int Compl(A) = {}";
   129 by (fast_tac eq_cs 1);
   130 qed "Compl_disjoint";
   131 
   132 goal Set.thy "A Un Compl(A) = {x.True}";
   133 by (fast_tac eq_cs 1);
   134 qed "Compl_partition";
   135 
   136 goal Set.thy "Compl(Compl(A)) = A";
   137 by (fast_tac eq_cs 1);
   138 qed "double_complement";
   139 
   140 goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
   141 by (fast_tac eq_cs 1);
   142 qed "Compl_Un";
   143 
   144 goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
   145 by (fast_tac eq_cs 1);
   146 qed "Compl_Int";
   147 
   148 goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
   149 by (fast_tac eq_cs 1);
   150 qed "Compl_UN";
   151 
   152 goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
   153 by (fast_tac eq_cs 1);
   154 qed "Compl_INT";
   155 
   156 (*Halmos, Naive Set Theory, page 16.*)
   157 
   158 goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
   159 by (fast_tac (eq_cs addSEs [equalityE]) 1);
   160 qed "Un_Int_assoc_eq";
   161 
   162 
   163 (** Big Union and Intersection **)
   164 
   165 goal Set.thy "Union({}) = {}";
   166 by (fast_tac eq_cs 1);
   167 qed "Union_empty";
   168 
   169 goal Set.thy "Union(insert a B) = a Un Union(B)";
   170 by (fast_tac eq_cs 1);
   171 qed "Union_insert";
   172 
   173 goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
   174 by (fast_tac eq_cs 1);
   175 qed "Union_Un_distrib";
   176 
   177 goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
   178 by (fast_tac set_cs 1);
   179 qed "Union_Int_subset";
   180 
   181 val prems = goal Set.thy
   182    "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
   183 by (fast_tac (eq_cs addSEs [equalityE]) 1);
   184 qed "Union_disjoint";
   185 
   186 goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
   187 by (best_tac eq_cs 1);
   188 qed "Inter_Un_distrib";
   189 
   190 (** Unions and Intersections of Families **)
   191 
   192 (*Basic identities*)
   193 
   194 goal Set.thy "(UN x:{}. B x) = {}";
   195 by (fast_tac eq_cs 1);
   196 qed "UN_empty";
   197 
   198 goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
   199 by (fast_tac eq_cs 1);
   200 qed "UN_insert";
   201 
   202 goal Set.thy "Union(range(f)) = (UN x.f(x))";
   203 by (fast_tac eq_cs 1);
   204 qed "Union_range_eq";
   205 
   206 goal Set.thy "Inter(range(f)) = (INT x.f(x))";
   207 by (fast_tac eq_cs 1);
   208 qed "Inter_range_eq";
   209 
   210 goal Set.thy "Union(B``A) = (UN x:A. B(x))";
   211 by (fast_tac eq_cs 1);
   212 qed "Union_image_eq";
   213 
   214 goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
   215 by (fast_tac eq_cs 1);
   216 qed "Inter_image_eq";
   217 
   218 goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
   219 by (fast_tac eq_cs 1);
   220 qed "UN_constant";
   221 
   222 goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
   223 by (fast_tac eq_cs 1);
   224 qed "INT_constant";
   225 
   226 goal Set.thy "(UN x.B) = B";
   227 by (fast_tac eq_cs 1);
   228 qed "UN1_constant";
   229 
   230 goal Set.thy "(INT x.B) = B";
   231 by (fast_tac eq_cs 1);
   232 qed "INT1_constant";
   233 
   234 goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
   235 by (fast_tac eq_cs 1);
   236 qed "UN_eq";
   237 
   238 (*Look: it has an EXISTENTIAL quantifier*)
   239 goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
   240 by (fast_tac eq_cs 1);
   241 qed "INT_eq";
   242 
   243 (*Distributive laws...*)
   244 
   245 goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
   246 by (fast_tac eq_cs 1);
   247 qed "Int_Union";
   248 
   249 (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
   250    Union of a family of unions **)
   251 goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
   252 by (fast_tac eq_cs 1);
   253 qed "Un_Union_image";
   254 
   255 (*Equivalent version*)
   256 goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
   257 by (fast_tac eq_cs 1);
   258 qed "UN_Un_distrib";
   259 
   260 goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
   261 by (fast_tac eq_cs 1);
   262 qed "Un_Inter";
   263 
   264 goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
   265 by (best_tac eq_cs 1);
   266 qed "Int_Inter_image";
   267 
   268 (*Equivalent version*)
   269 goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
   270 by (fast_tac eq_cs 1);
   271 qed "INT_Int_distrib";
   272 
   273 (*Halmos, Naive Set Theory, page 35.*)
   274 goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
   275 by (fast_tac eq_cs 1);
   276 qed "Int_UN_distrib";
   277 
   278 goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
   279 by (fast_tac eq_cs 1);
   280 qed "Un_INT_distrib";
   281 
   282 goal Set.thy
   283     "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
   284 by (fast_tac eq_cs 1);
   285 qed "Int_UN_distrib2";
   286 
   287 goal Set.thy
   288     "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
   289 by (fast_tac eq_cs 1);
   290 qed "Un_INT_distrib2";
   291 
   292 (** Simple properties of Diff -- set difference **)
   293 
   294 goal Set.thy "A-A = {}";
   295 by (fast_tac eq_cs 1);
   296 qed "Diff_cancel";
   297 
   298 goal Set.thy "{}-A = {}";
   299 by (fast_tac eq_cs 1);
   300 qed "empty_Diff";
   301 
   302 goal Set.thy "A-{} = A";
   303 by (fast_tac eq_cs 1);
   304 qed "Diff_empty";
   305 
   306 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   307 goal Set.thy "A - insert a B = A - B - {a}";
   308 by (fast_tac eq_cs 1);
   309 qed "Diff_insert";
   310 
   311 (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   312 goal Set.thy "A - insert a B = A - {a} - B";
   313 by (fast_tac eq_cs 1);
   314 qed "Diff_insert2";
   315 
   316 val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
   317 by (fast_tac (eq_cs addSIs prems) 1);
   318 qed "insert_Diff";
   319 
   320 goal Set.thy "A Int (B-A) = {}";
   321 by (fast_tac eq_cs 1);
   322 qed "Diff_disjoint";
   323 
   324 goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
   325 by (fast_tac eq_cs 1);
   326 qed "Diff_partition";
   327 
   328 goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
   329 by (fast_tac eq_cs 1);
   330 qed "double_diff";
   331 
   332 goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
   333 by (fast_tac eq_cs 1);
   334 qed "Diff_Un";
   335 
   336 goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
   337 by (fast_tac eq_cs 1);
   338 qed "Diff_Int";
   339 
   340 Addsimps
   341   [in_empty,in_insert,insert_subset,
   342    insert_not_empty,empty_not_insert,
   343    Int_absorb,Int_empty_left,Int_empty_right,
   344    Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
   345    UN_empty, UN_insert,
   346    UN1_constant,image_empty,
   347    Compl_disjoint,double_complement,
   348    Union_empty,Union_insert,empty_subsetI,subset_refl,
   349    Diff_cancel,empty_Diff,Diff_empty,Diff_disjoint];