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