src/HOL/equalities.ML
changeset 1531 e5eb247ad13c
parent 1465 5d7a7e439cec
child 1548 afe750876848
     1.1 --- a/src/HOL/equalities.ML	Mon Mar 04 12:28:48 1996 +0100
     1.2 +++ b/src/HOL/equalities.ML	Mon Mar 04 14:37:33 1996 +0100
     1.3 @@ -10,47 +10,81 @@
     1.4  
     1.5  val eq_cs = set_cs addSIs [equalityI];
     1.6  
     1.7 +goal Set.thy "{x.False} = {}";
     1.8 +by(fast_tac eq_cs 1);
     1.9 +qed "Collect_False_empty";
    1.10 +Addsimps [Collect_False_empty];
    1.11 +
    1.12 +goal Set.thy "(A <= {}) = (A = {})";
    1.13 +by(fast_tac eq_cs 1);
    1.14 +qed "subset_empty";
    1.15 +Addsimps [subset_empty];
    1.16 +
    1.17  (** The membership relation, : **)
    1.18  
    1.19  goal Set.thy "x ~: {}";
    1.20  by(fast_tac set_cs 1);
    1.21  qed "in_empty";
    1.22 +Addsimps[in_empty];
    1.23  
    1.24  goal Set.thy "x : insert y A = (x=y | x:A)";
    1.25  by(fast_tac set_cs 1);
    1.26  qed "in_insert";
    1.27 +Addsimps[in_insert];
    1.28  
    1.29  (** insert **)
    1.30  
    1.31 +(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
    1.32 +goal Set.thy "insert a A = {a} Un A";
    1.33 +by(fast_tac eq_cs 1);
    1.34 +qed "insert_is_Un";
    1.35 +
    1.36  goal Set.thy "insert a A ~= {}";
    1.37  by (fast_tac (set_cs addEs [equalityCE]) 1);
    1.38  qed"insert_not_empty";
    1.39 +Addsimps[insert_not_empty];
    1.40  
    1.41  bind_thm("empty_not_insert",insert_not_empty RS not_sym);
    1.42 +Addsimps[empty_not_insert];
    1.43  
    1.44  goal Set.thy "!!a. a:A ==> insert a A = A";
    1.45  by (fast_tac eq_cs 1);
    1.46  qed "insert_absorb";
    1.47  
    1.48 +goal Set.thy "insert x (insert x A) = insert x A";
    1.49 +by(fast_tac eq_cs 1);
    1.50 +qed "insert_absorb2";
    1.51 +Addsimps [insert_absorb2];
    1.52 +
    1.53  goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
    1.54  by (fast_tac set_cs 1);
    1.55  qed "insert_subset";
    1.56 +Addsimps[insert_subset];
    1.57 +
    1.58 +(* use new B rather than (A-{a}) to avoid infinite unfolding *)
    1.59 +goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
    1.60 +by(res_inst_tac [("x","A-{a}")] exI 1);
    1.61 +by(fast_tac eq_cs 1);
    1.62 +qed "mk_disjoint_insert";
    1.63  
    1.64  (** Image **)
    1.65  
    1.66  goal Set.thy "f``{} = {}";
    1.67  by (fast_tac eq_cs 1);
    1.68  qed "image_empty";
    1.69 +Addsimps[image_empty];
    1.70  
    1.71  goal Set.thy "f``insert a B = insert (f a) (f``B)";
    1.72  by (fast_tac eq_cs 1);
    1.73  qed "image_insert";
    1.74 +Addsimps[image_insert];
    1.75  
    1.76  (** Binary Intersection **)
    1.77  
    1.78  goal Set.thy "A Int A = A";
    1.79  by (fast_tac eq_cs 1);
    1.80  qed "Int_absorb";
    1.81 +Addsimps[Int_absorb];
    1.82  
    1.83  goal Set.thy "A Int B  =  B Int A";
    1.84  by (fast_tac eq_cs 1);
    1.85 @@ -63,10 +97,22 @@
    1.86  goal Set.thy "{} Int B = {}";
    1.87  by (fast_tac eq_cs 1);
    1.88  qed "Int_empty_left";
    1.89 +Addsimps[Int_empty_left];
    1.90  
    1.91  goal Set.thy "A Int {} = {}";
    1.92  by (fast_tac eq_cs 1);
    1.93  qed "Int_empty_right";
    1.94 +Addsimps[Int_empty_right];
    1.95 +
    1.96 +goal Set.thy "UNIV Int B = B";
    1.97 +by (fast_tac eq_cs 1);
    1.98 +qed "Int_UNIV_left";
    1.99 +Addsimps[Int_UNIV_left];
   1.100 +
   1.101 +goal Set.thy "A Int UNIV = A";
   1.102 +by (fast_tac eq_cs 1);
   1.103 +qed "Int_UNIV_right";
   1.104 +Addsimps[Int_UNIV_right];
   1.105  
   1.106  goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
   1.107  by (fast_tac eq_cs 1);
   1.108 @@ -76,11 +122,17 @@
   1.109  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   1.110  qed "subset_Int_eq";
   1.111  
   1.112 +goal Set.thy "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
   1.113 +by (fast_tac (eq_cs addEs [equalityCE]) 1);
   1.114 +qed "Int_UNIV";
   1.115 +Addsimps[Int_UNIV];
   1.116 +
   1.117  (** Binary Union **)
   1.118  
   1.119  goal Set.thy "A Un A = A";
   1.120  by (fast_tac eq_cs 1);
   1.121  qed "Un_absorb";
   1.122 +Addsimps[Un_absorb];
   1.123  
   1.124  goal Set.thy "A Un B  =  B Un A";
   1.125  by (fast_tac eq_cs 1);
   1.126 @@ -93,10 +145,22 @@
   1.127  goal Set.thy "{} Un B = B";
   1.128  by(fast_tac eq_cs 1);
   1.129  qed "Un_empty_left";
   1.130 +Addsimps[Un_empty_left];
   1.131  
   1.132  goal Set.thy "A Un {} = A";
   1.133  by(fast_tac eq_cs 1);
   1.134  qed "Un_empty_right";
   1.135 +Addsimps[Un_empty_right];
   1.136 +
   1.137 +goal Set.thy "UNIV Un B = UNIV";
   1.138 +by(fast_tac eq_cs 1);
   1.139 +qed "Un_UNIV_left";
   1.140 +Addsimps[Un_UNIV_left];
   1.141 +
   1.142 +goal Set.thy "A Un UNIV = UNIV";
   1.143 +by(fast_tac eq_cs 1);
   1.144 +qed "Un_UNIV_right";
   1.145 +Addsimps[Un_UNIV_right];
   1.146  
   1.147  goal Set.thy "insert a B Un C = insert a (B Un C)";
   1.148  by(fast_tac eq_cs 1);
   1.149 @@ -122,20 +186,23 @@
   1.150  goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
   1.151  by (fast_tac (eq_cs addEs [equalityCE]) 1);
   1.152  qed "Un_empty";
   1.153 +Addsimps[Un_empty];
   1.154  
   1.155  (** Simple properties of Compl -- complement of a set **)
   1.156  
   1.157  goal Set.thy "A Int Compl(A) = {}";
   1.158  by (fast_tac eq_cs 1);
   1.159  qed "Compl_disjoint";
   1.160 +Addsimps[Compl_disjoint];
   1.161  
   1.162 -goal Set.thy "A Un Compl(A) = {x.True}";
   1.163 +goal Set.thy "A Un Compl(A) = UNIV";
   1.164  by (fast_tac eq_cs 1);
   1.165  qed "Compl_partition";
   1.166  
   1.167  goal Set.thy "Compl(Compl(A)) = A";
   1.168  by (fast_tac eq_cs 1);
   1.169  qed "double_complement";
   1.170 +Addsimps[double_complement];
   1.171  
   1.172  goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
   1.173  by (fast_tac eq_cs 1);
   1.174 @@ -165,14 +232,22 @@
   1.175  goal Set.thy "Union({}) = {}";
   1.176  by (fast_tac eq_cs 1);
   1.177  qed "Union_empty";
   1.178 +Addsimps[Union_empty];
   1.179 +
   1.180 +goal Set.thy "Union(UNIV) = UNIV";
   1.181 +by (fast_tac eq_cs 1);
   1.182 +qed "Union_UNIV";
   1.183 +Addsimps[Union_UNIV];
   1.184  
   1.185  goal Set.thy "Union(insert a B) = a Un Union(B)";
   1.186  by (fast_tac eq_cs 1);
   1.187  qed "Union_insert";
   1.188 +Addsimps[Union_insert];
   1.189  
   1.190  goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
   1.191  by (fast_tac eq_cs 1);
   1.192  qed "Union_Un_distrib";
   1.193 +Addsimps[Union_Un_distrib];
   1.194  
   1.195  goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
   1.196  by (fast_tac set_cs 1);
   1.197 @@ -183,6 +258,28 @@
   1.198  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   1.199  qed "Union_disjoint";
   1.200  
   1.201 +goal Set.thy "Inter({}) = UNIV";
   1.202 +by (fast_tac eq_cs 1);
   1.203 +qed "Inter_empty";
   1.204 +Addsimps[Inter_empty];
   1.205 +
   1.206 +goal Set.thy "Inter(UNIV) = {}";
   1.207 +by (fast_tac eq_cs 1);
   1.208 +qed "Inter_UNIV";
   1.209 +Addsimps[Inter_UNIV];
   1.210 +
   1.211 +goal Set.thy "Inter(insert a B) = a Int Inter(B)";
   1.212 +by (fast_tac eq_cs 1);
   1.213 +qed "Inter_insert";
   1.214 +Addsimps[Inter_insert];
   1.215 +
   1.216 +(* Why does fast_tac fail???
   1.217 +goal Set.thy "Inter(A Int B) = Inter(A) Int Inter(B)";
   1.218 +by (fast_tac eq_cs 1);
   1.219 +qed "Inter_Int_distrib";
   1.220 +Addsimps[Inter_Int_distrib];
   1.221 +*)
   1.222 +
   1.223  goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
   1.224  by (best_tac eq_cs 1);
   1.225  qed "Inter_Un_distrib";
   1.226 @@ -194,10 +291,32 @@
   1.227  goal Set.thy "(UN x:{}. B x) = {}";
   1.228  by (fast_tac eq_cs 1);
   1.229  qed "UN_empty";
   1.230 +Addsimps[UN_empty];
   1.231 +
   1.232 +goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
   1.233 +by (fast_tac eq_cs 1);
   1.234 +qed "UN_UNIV";
   1.235 +Addsimps[UN_UNIV];
   1.236 +
   1.237 +goal Set.thy "(INT x:{}. B x) = UNIV";
   1.238 +by (fast_tac eq_cs 1);
   1.239 +qed "INT_empty";
   1.240 +Addsimps[INT_empty];
   1.241 +
   1.242 +goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
   1.243 +by (fast_tac eq_cs 1);
   1.244 +qed "INT_UNIV";
   1.245 +Addsimps[INT_UNIV];
   1.246  
   1.247  goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
   1.248  by (fast_tac eq_cs 1);
   1.249  qed "UN_insert";
   1.250 +Addsimps[UN_insert];
   1.251 +
   1.252 +goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
   1.253 +by (fast_tac eq_cs 1);
   1.254 +qed "INT_insert";
   1.255 +Addsimps[INT_insert];
   1.256  
   1.257  goal Set.thy "Union(range(f)) = (UN x.f(x))";
   1.258  by (fast_tac eq_cs 1);
   1.259 @@ -226,10 +345,12 @@
   1.260  goal Set.thy "(UN x.B) = B";
   1.261  by (fast_tac eq_cs 1);
   1.262  qed "UN1_constant";
   1.263 +Addsimps[UN1_constant];
   1.264  
   1.265  goal Set.thy "(INT x.B) = B";
   1.266  by (fast_tac eq_cs 1);
   1.267  qed "INT1_constant";
   1.268 +Addsimps[INT1_constant];
   1.269  
   1.270  goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
   1.271  by (fast_tac eq_cs 1);
   1.272 @@ -294,14 +415,27 @@
   1.273  goal Set.thy "A-A = {}";
   1.274  by (fast_tac eq_cs 1);
   1.275  qed "Diff_cancel";
   1.276 +Addsimps[Diff_cancel];
   1.277  
   1.278  goal Set.thy "{}-A = {}";
   1.279  by (fast_tac eq_cs 1);
   1.280  qed "empty_Diff";
   1.281 +Addsimps[empty_Diff];
   1.282  
   1.283  goal Set.thy "A-{} = A";
   1.284  by (fast_tac eq_cs 1);
   1.285  qed "Diff_empty";
   1.286 +Addsimps[Diff_empty];
   1.287 +
   1.288 +goal Set.thy "A-UNIV = {}";
   1.289 +by (fast_tac eq_cs 1);
   1.290 +qed "Diff_UNIV";
   1.291 +Addsimps[Diff_UNIV];
   1.292 +
   1.293 +goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
   1.294 +by(fast_tac eq_cs 1);
   1.295 +qed "Diff_insert0";
   1.296 +Addsimps [Diff_insert0];
   1.297  
   1.298  (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
   1.299  goal Set.thy "A - insert a B = A - B - {a}";
   1.300 @@ -313,6 +447,16 @@
   1.301  by (fast_tac eq_cs 1);
   1.302  qed "Diff_insert2";
   1.303  
   1.304 +goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
   1.305 +by(simp_tac (!simpset setloop split_tac[expand_if]) 1);
   1.306 +by(fast_tac eq_cs 1);
   1.307 +qed "insert_Diff_if";
   1.308 +
   1.309 +goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
   1.310 +by(fast_tac eq_cs 1);
   1.311 +qed "insert_Diff1";
   1.312 +Addsimps [insert_Diff1];
   1.313 +
   1.314  val prems = goal Set.thy "a:A ==> insert a (A-{a}) = A";
   1.315  by (fast_tac (eq_cs addSIs prems) 1);
   1.316  qed "insert_Diff";
   1.317 @@ -320,6 +464,7 @@
   1.318  goal Set.thy "A Int (B-A) = {}";
   1.319  by (fast_tac eq_cs 1);
   1.320  qed "Diff_disjoint";
   1.321 +Addsimps[Diff_disjoint];
   1.322  
   1.323  goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
   1.324  by (fast_tac eq_cs 1);
   1.325 @@ -337,13 +482,20 @@
   1.326  by (fast_tac eq_cs 1);
   1.327  qed "Diff_Int";
   1.328  
   1.329 -Addsimps
   1.330 -  [in_empty,in_insert,insert_subset,
   1.331 -   insert_not_empty,empty_not_insert,
   1.332 -   Int_absorb,Int_empty_left,Int_empty_right,
   1.333 -   Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
   1.334 -   UN_empty, UN_insert,
   1.335 -   UN1_constant,image_empty,
   1.336 -   Compl_disjoint,double_complement,
   1.337 -   Union_empty,Union_insert,empty_subsetI,subset_refl,
   1.338 -   Diff_cancel,empty_Diff,Diff_empty,Diff_disjoint];
   1.339 +(* Congruence rule for set comprehension *)
   1.340 +val prems = goal Set.thy
   1.341 +  "[| !!x. P x = Q x; !!x. Q x ==> f x = g x |] ==> \
   1.342 +\  {f x |x. P x} = {g x|x. Q x}";
   1.343 +by(simp_tac (!simpset addsimps prems) 1);
   1.344 +br set_ext 1;
   1.345 +br iffI 1;
   1.346 +by(fast_tac (eq_cs addss (!simpset addsimps prems)) 1);
   1.347 +be CollectE 1;
   1.348 +be exE 1;
   1.349 +by(Asm_simp_tac 1);
   1.350 +be conjE 1;
   1.351 +by(rtac exI 1 THEN rtac conjI 1 THEN atac 2);
   1.352 +by(asm_simp_tac (!simpset addsimps prems) 1);
   1.353 +qed "Collect_cong1";
   1.354 +
   1.355 +Addsimps[subset_UNIV, empty_subsetI, subset_refl];