src/HOL/equalities.ML
 author clasohm Tue Jan 30 15:24:36 1996 +0100 (1996-01-30 ago) changeset 1465 5d7a7e439cec parent 1264 3eb91524b938 child 1531 e5eb247ad13c 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 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];
```