src/HOL/equalities.ML
changeset 923 ff1574a81019
child 1179 7678408f9751
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/equalities.ML	Fri Mar 03 12:02:25 1995 +0100
     1.3 @@ -0,0 +1,333 @@
     1.4 +(*  Title: 	HOL/equalities
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +Equalities involving union, intersection, inclusion, etc.
    1.10 +*)
    1.11 +
    1.12 +writeln"File HOL/equalities";
    1.13 +
    1.14 +val eq_cs = set_cs addSIs [equalityI];
    1.15 +
    1.16 +(** The membership relation, : **)
    1.17 +
    1.18 +goal Set.thy "x ~: {}";
    1.19 +by(fast_tac set_cs 1);
    1.20 +qed "in_empty";
    1.21 +
    1.22 +goal Set.thy "x : insert y A = (x=y | x:A)";
    1.23 +by(fast_tac set_cs 1);
    1.24 +qed "in_insert";
    1.25 +
    1.26 +(** insert **)
    1.27 +
    1.28 +goal Set.thy "!!a. a:A ==> insert a A = A";
    1.29 +by (fast_tac eq_cs 1);
    1.30 +qed "insert_absorb";
    1.31 +
    1.32 +goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
    1.33 +by (fast_tac set_cs 1);
    1.34 +qed "insert_subset";
    1.35 +
    1.36 +(** Image **)
    1.37 +
    1.38 +goal Set.thy "f``{} = {}";
    1.39 +by (fast_tac eq_cs 1);
    1.40 +qed "image_empty";
    1.41 +
    1.42 +goal Set.thy "f``insert a B = insert (f a) (f``B)";
    1.43 +by (fast_tac eq_cs 1);
    1.44 +qed "image_insert";
    1.45 +
    1.46 +(** Binary Intersection **)
    1.47 +
    1.48 +goal Set.thy "A Int A = A";
    1.49 +by (fast_tac eq_cs 1);
    1.50 +qed "Int_absorb";
    1.51 +
    1.52 +goal Set.thy "A Int B  =  B Int A";
    1.53 +by (fast_tac eq_cs 1);
    1.54 +qed "Int_commute";
    1.55 +
    1.56 +goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
    1.57 +by (fast_tac eq_cs 1);
    1.58 +qed "Int_assoc";
    1.59 +
    1.60 +goal Set.thy "{} Int B = {}";
    1.61 +by (fast_tac eq_cs 1);
    1.62 +qed "Int_empty_left";
    1.63 +
    1.64 +goal Set.thy "A Int {} = {}";
    1.65 +by (fast_tac eq_cs 1);
    1.66 +qed "Int_empty_right";
    1.67 +
    1.68 +goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
    1.69 +by (fast_tac eq_cs 1);
    1.70 +qed "Int_Un_distrib";
    1.71 +
    1.72 +goal Set.thy "(A<=B) = (A Int B = A)";
    1.73 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
    1.74 +qed "subset_Int_eq";
    1.75 +
    1.76 +(** Binary Union **)
    1.77 +
    1.78 +goal Set.thy "A Un A = A";
    1.79 +by (fast_tac eq_cs 1);
    1.80 +qed "Un_absorb";
    1.81 +
    1.82 +goal Set.thy "A Un B  =  B Un A";
    1.83 +by (fast_tac eq_cs 1);
    1.84 +qed "Un_commute";
    1.85 +
    1.86 +goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
    1.87 +by (fast_tac eq_cs 1);
    1.88 +qed "Un_assoc";
    1.89 +
    1.90 +goal Set.thy "{} Un B = B";
    1.91 +by(fast_tac eq_cs 1);
    1.92 +qed "Un_empty_left";
    1.93 +
    1.94 +goal Set.thy "A Un {} = A";
    1.95 +by(fast_tac eq_cs 1);
    1.96 +qed "Un_empty_right";
    1.97 +
    1.98 +goal Set.thy "insert a B Un C = insert a (B Un C)";
    1.99 +by(fast_tac eq_cs 1);
   1.100 +qed "Un_insert_left";
   1.101 +
   1.102 +goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
   1.103 +by (fast_tac eq_cs 1);
   1.104 +qed "Un_Int_distrib";
   1.105 +
   1.106 +goal Set.thy
   1.107 + "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
   1.108 +by (fast_tac eq_cs 1);
   1.109 +qed "Un_Int_crazy";
   1.110 +
   1.111 +goal Set.thy "(A<=B) = (A Un B = B)";
   1.112 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
   1.113 +qed "subset_Un_eq";
   1.114 +
   1.115 +goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
   1.116 +by (fast_tac eq_cs 1);
   1.117 +qed "subset_insert_iff";
   1.118 +
   1.119 +goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
   1.120 +by (fast_tac (eq_cs addEs [equalityCE]) 1);
   1.121 +qed "Un_empty";
   1.122 +
   1.123 +(** Simple properties of Compl -- complement of a set **)
   1.124 +
   1.125 +goal Set.thy "A Int Compl(A) = {}";
   1.126 +by (fast_tac eq_cs 1);
   1.127 +qed "Compl_disjoint";
   1.128 +
   1.129 +goal Set.thy "A Un Compl(A) = {x.True}";
   1.130 +by (fast_tac eq_cs 1);
   1.131 +qed "Compl_partition";
   1.132 +
   1.133 +goal Set.thy "Compl(Compl(A)) = A";
   1.134 +by (fast_tac eq_cs 1);
   1.135 +qed "double_complement";
   1.136 +
   1.137 +goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
   1.138 +by (fast_tac eq_cs 1);
   1.139 +qed "Compl_Un";
   1.140 +
   1.141 +goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
   1.142 +by (fast_tac eq_cs 1);
   1.143 +qed "Compl_Int";
   1.144 +
   1.145 +goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
   1.146 +by (fast_tac eq_cs 1);
   1.147 +qed "Compl_UN";
   1.148 +
   1.149 +goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
   1.150 +by (fast_tac eq_cs 1);
   1.151 +qed "Compl_INT";
   1.152 +
   1.153 +(*Halmos, Naive Set Theory, page 16.*)
   1.154 +
   1.155 +goal Set.thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
   1.156 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
   1.157 +qed "Un_Int_assoc_eq";
   1.158 +
   1.159 +
   1.160 +(** Big Union and Intersection **)
   1.161 +
   1.162 +goal Set.thy "Union({}) = {}";
   1.163 +by (fast_tac eq_cs 1);
   1.164 +qed "Union_empty";
   1.165 +
   1.166 +goal Set.thy "Union(insert a B) = a Un Union(B)";
   1.167 +by (fast_tac eq_cs 1);
   1.168 +qed "Union_insert";
   1.169 +
   1.170 +goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
   1.171 +by (fast_tac eq_cs 1);
   1.172 +qed "Union_Un_distrib";
   1.173 +
   1.174 +goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
   1.175 +by (fast_tac set_cs 1);
   1.176 +qed "Union_Int_subset";
   1.177 +
   1.178 +val prems = goal Set.thy
   1.179 +   "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
   1.180 +by (fast_tac (eq_cs addSEs [equalityE]) 1);
   1.181 +qed "Union_disjoint";
   1.182 +
   1.183 +goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
   1.184 +by (best_tac eq_cs 1);
   1.185 +qed "Inter_Un_distrib";
   1.186 +
   1.187 +(** Unions and Intersections of Families **)
   1.188 +
   1.189 +(*Basic identities*)
   1.190 +
   1.191 +goal Set.thy "Union(range(f)) = (UN x.f(x))";
   1.192 +by (fast_tac eq_cs 1);
   1.193 +qed "Union_range_eq";
   1.194 +
   1.195 +goal Set.thy "Inter(range(f)) = (INT x.f(x))";
   1.196 +by (fast_tac eq_cs 1);
   1.197 +qed "Inter_range_eq";
   1.198 +
   1.199 +goal Set.thy "Union(B``A) = (UN x:A. B(x))";
   1.200 +by (fast_tac eq_cs 1);
   1.201 +qed "Union_image_eq";
   1.202 +
   1.203 +goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
   1.204 +by (fast_tac eq_cs 1);
   1.205 +qed "Inter_image_eq";
   1.206 +
   1.207 +goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
   1.208 +by (fast_tac eq_cs 1);
   1.209 +qed "UN_constant";
   1.210 +
   1.211 +goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
   1.212 +by (fast_tac eq_cs 1);
   1.213 +qed "INT_constant";
   1.214 +
   1.215 +goal Set.thy "(UN x.B) = B";
   1.216 +by (fast_tac eq_cs 1);
   1.217 +qed "UN1_constant";
   1.218 +
   1.219 +goal Set.thy "(INT x.B) = B";
   1.220 +by (fast_tac eq_cs 1);
   1.221 +qed "INT1_constant";
   1.222 +
   1.223 +goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
   1.224 +by (fast_tac eq_cs 1);
   1.225 +qed "UN_eq";
   1.226 +
   1.227 +(*Look: it has an EXISTENTIAL quantifier*)
   1.228 +goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
   1.229 +by (fast_tac eq_cs 1);
   1.230 +qed "INT_eq";
   1.231 +
   1.232 +(*Distributive laws...*)
   1.233 +
   1.234 +goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
   1.235 +by (fast_tac eq_cs 1);
   1.236 +qed "Int_Union";
   1.237 +
   1.238 +(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
   1.239 +   Union of a family of unions **)
   1.240 +goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
   1.241 +by (fast_tac eq_cs 1);
   1.242 +qed "Un_Union_image";
   1.243 +
   1.244 +(*Equivalent version*)
   1.245 +goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
   1.246 +by (fast_tac eq_cs 1);
   1.247 +qed "UN_Un_distrib";
   1.248 +
   1.249 +goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
   1.250 +by (fast_tac eq_cs 1);
   1.251 +qed "Un_Inter";
   1.252 +
   1.253 +goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
   1.254 +by (best_tac eq_cs 1);
   1.255 +qed "Int_Inter_image";
   1.256 +
   1.257 +(*Equivalent version*)
   1.258 +goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
   1.259 +by (fast_tac eq_cs 1);
   1.260 +qed "INT_Int_distrib";
   1.261 +
   1.262 +(*Halmos, Naive Set Theory, page 35.*)
   1.263 +goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
   1.264 +by (fast_tac eq_cs 1);
   1.265 +qed "Int_UN_distrib";
   1.266 +
   1.267 +goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
   1.268 +by (fast_tac eq_cs 1);
   1.269 +qed "Un_INT_distrib";
   1.270 +
   1.271 +goal Set.thy
   1.272 +    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
   1.273 +by (fast_tac eq_cs 1);
   1.274 +qed "Int_UN_distrib2";
   1.275 +
   1.276 +goal Set.thy
   1.277 +    "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
   1.278 +by (fast_tac eq_cs 1);
   1.279 +qed "Un_INT_distrib2";
   1.280 +
   1.281 +(** Simple properties of Diff -- set difference **)
   1.282 +
   1.283 +goal Set.thy "A-A = {}";
   1.284 +by (fast_tac eq_cs 1);
   1.285 +qed "Diff_cancel";
   1.286 +
   1.287 +goal Set.thy "{}-A = {}";
   1.288 +by (fast_tac eq_cs 1);
   1.289 +qed "empty_Diff";
   1.290 +
   1.291 +goal Set.thy "A-{} = A";
   1.292 +by (fast_tac eq_cs 1);
   1.293 +qed "Diff_empty";
   1.294 +
   1.295 +(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   1.296 +goal Set.thy "A - insert a B = A - B - {a}";
   1.297 +by (fast_tac eq_cs 1);
   1.298 +qed "Diff_insert";
   1.299 +
   1.300 +(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   1.301 +goal Set.thy "A - insert a B = A - {a} - B";
   1.302 +by (fast_tac eq_cs 1);
   1.303 +qed "Diff_insert2";
   1.304 +
   1.305 +val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
   1.306 +by (fast_tac (eq_cs addSIs prems) 1);
   1.307 +qed "insert_Diff";
   1.308 +
   1.309 +goal Set.thy "A Int (B-A) = {}";
   1.310 +by (fast_tac eq_cs 1);
   1.311 +qed "Diff_disjoint";
   1.312 +
   1.313 +goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
   1.314 +by (fast_tac eq_cs 1);
   1.315 +qed "Diff_partition";
   1.316 +
   1.317 +goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
   1.318 +by (fast_tac eq_cs 1);
   1.319 +qed "double_diff";
   1.320 +
   1.321 +goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
   1.322 +by (fast_tac eq_cs 1);
   1.323 +qed "Diff_Un";
   1.324 +
   1.325 +goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
   1.326 +by (fast_tac eq_cs 1);
   1.327 +qed "Diff_Int";
   1.328 +
   1.329 +val set_ss = set_ss addsimps
   1.330 +  [in_empty,in_insert,insert_subset,
   1.331 +   Int_absorb,Int_empty_left,Int_empty_right,
   1.332 +   Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
   1.333 +   UN1_constant,image_empty,
   1.334 +   Compl_disjoint,double_complement,
   1.335 +   Union_empty,Union_insert,empty_subsetI,subset_refl,
   1.336 +   Diff_cancel,empty_Diff,Diff_empty,Diff_disjoint];