equalities.ML

 (*  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.
 *)
 
 writeln"File HOL/equalities";
 
 val eq_cs = set_cs addSIs [equalityI];
 
-(** : **)
+(** The membership relation, : **)
 
 goal Set.thy "x ~: {}";
 by(fast_tac set_cs 1);
 val in_empty = 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 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 = {})";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 val Union_disjoint = result();

 by (best_tac eq_cs 1);
 val Inter_Un_distrib = result();
 
 (** Unions and Intersections of Families **)
 
+(*Basic identities*)
+
+goal Set.thy "Union(range(f)) = (UN x.f(x))";
+by (fast_tac eq_cs 1);
+val Union_range_eq = result();
+
+goal Set.thy "Inter(range(f)) = (INT x.f(x))";
+by (fast_tac eq_cs 1);
+val Inter_range_eq = result();
+
+goal Set.thy "Union(B``A) = (UN x:A. B(x))";
+by (fast_tac eq_cs 1);
+val Union_image_eq = result();
+
+goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
+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 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, page 12: Union of a family of unions **)
+(* 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();
 
-(** Other identities about Unions and Intersections **)
-
-goal Set.thy "Union(range(f)) = (UN x.f(x))";
-by (fast_tac eq_cs 1);
-val Union_range_eq = result();
-
-goal Set.thy "Inter(range(f)) = (INT x.f(x))";
-by (fast_tac eq_cs 1);
-val Inter_range_eq = result();
-
-goal Set.thy "Union(B``A) = (UN x:A. B(x))";
-by (fast_tac eq_cs 1);
-val Union_image_eq = result();
-
-goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
-by (fast_tac eq_cs 1);
-val Inter_image_eq = result();
-
-goal Set.thy "(UN x.B) = B";
-by (fast_tac eq_cs 1);
-val constant_UN = 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 **)
 
 goal Set.thy "A-A = {}";
 by (fast_tac eq_cs 1);

 val Diff_disjoint = result();
 
 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);
-by (fast_tac eq_cs 1);
-val double_complement = result();
-*)
+
+goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = A :: 'a set";
+by (fast_tac eq_cs 1);
+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();
 
 goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";

 
 val set_ss = set_ss addsimps
   [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];