equalities.ML

--- a/equalities.ML	Wed May 25 12:25:40 1994 +0200
+++ b/equalities.ML	Wed May 25 12:43:50 1994 +0200
@@ -1,7 +1,7 @@
 (*  Title: 	HOL/equalities
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Equalities involving union, intersection, inclusion, etc.
 *)
@@ -10,7 +10,7 @@
 
 val eq_cs = set_cs addSIs [equalityI];
 
-(** : **)
+(** The membership relation, : **)
 
 goal Set.thy "x ~: {}";
 by(fast_tac set_cs 1);
@@ -164,9 +164,9 @@
 by (fast_tac eq_cs 1);
 val Union_Un_distrib = result();
 
-goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
-by (fast_tac eq_cs 1);
-val Union_Un_distrib = result();
+goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
+by (fast_tac set_cs 1);
+val Union_Int_subset = result();
 
 val prems = goal Set.thy
    "(Union(C) Int A = {}) = (! B:C. B Int A = {})";
@@ -179,33 +179,7 @@
 
 (** Unions and Intersections of Families **)
 
-goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
-by (fast_tac eq_cs 1);
-val UN_eq = result();
-
-(*Look: it has an EXISTENTIAL quantifier*)
-goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
-by (fast_tac eq_cs 1);
-val INT_eq = result();
-
-goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
-by (fast_tac eq_cs 1);
-val Int_Union = result();
-
-(* Devlin, page 12: Union of a family of unions **)
-goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
-by (fast_tac eq_cs 1);
-val Un_Union_image = result();
-
-goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
-by (fast_tac eq_cs 1);
-val Un_Inter = result();
-
-goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
-by (best_tac eq_cs 1);
-val Int_Inter_image = result();
-
-(** Other identities about Unions and Intersections **)
+(*Basic identities*)
 
 goal Set.thy "Union(range(f)) = (UN x.f(x))";
 by (fast_tac eq_cs 1);
@@ -223,9 +197,79 @@
 by (fast_tac eq_cs 1);
 val Inter_image_eq = result();
 
+goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
+by (fast_tac eq_cs 1);
+val UN_constant = result();
+
+goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
+by (fast_tac eq_cs 1);
+val INT_constant = result();
+
 goal Set.thy "(UN x.B) = B";
 by (fast_tac eq_cs 1);
-val constant_UN = result();
+val UN1_constant = result();
+
+goal Set.thy "(INT x.B) = B";
+by (fast_tac eq_cs 1);
+val INT1_constant = result();
+
+goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
+by (fast_tac eq_cs 1);
+val UN_eq = result();
+
+(*Look: it has an EXISTENTIAL quantifier*)
+goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
+by (fast_tac eq_cs 1);
+val INT_eq = result();
+
+(*Distributive laws...*)
+
+goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
+by (fast_tac eq_cs 1);
+val Int_Union = result();
+
+(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
+   Union of a family of unions **)
+goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
+by (fast_tac eq_cs 1);
+val Un_Union_image = result();
+
+(*Equivalent version*)
+goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
+by (fast_tac eq_cs 1);
+val UN_Un_distrib = result();
+
+goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
+by (fast_tac eq_cs 1);
+val Un_Inter = result();
+
+goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
+by (best_tac eq_cs 1);
+val Int_Inter_image = result();
+
+(*Equivalent version*)
+goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
+by (fast_tac eq_cs 1);
+val INT_Int_distrib = result();
+
+(*Halmos, Naive Set Theory, page 35.*)
+goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
+by (fast_tac eq_cs 1);
+val Int_UN_distrib = result();
+
+goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
+by (fast_tac eq_cs 1);
+val Un_INT_distrib = result();
+
+goal Set.thy
+    "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
+by (fast_tac eq_cs 1);
+val Int_UN_distrib2 = result();
+
+goal Set.thy
+    "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
+by (fast_tac eq_cs 1);
+val Un_INT_distrib2 = result();
 
 (** Simple properties of Diff -- set difference **)
 
@@ -262,12 +306,11 @@
 goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
 by (fast_tac eq_cs 1);
 val Diff_partition = result();
-(*
-goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C-A)) = A";
-by (cut_facts_tac prems 1);
+
+goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = A :: 'a set";
 by (fast_tac eq_cs 1);
-val double_complement = result();
-*)
+val double_diff = result();
+
 goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
 by (fast_tac eq_cs 1);
 val Diff_Un = result();
@@ -280,7 +323,7 @@
   [in_empty,in_insert,insert_subset,
    Int_absorb,Int_empty_left,Int_empty_right,
    Un_absorb,Un_empty_left,Un_empty_right,
-   constant_UN,image_empty,
+   UN1_constant,image_empty,
    Compl_disjoint,double_complement,
    Union_empty,Union_insert,empty_subsetI,subset_refl,
    Diff_cancel,empty_Diff,Diff_empty,Diff_disjoint];