# HG changeset patch
# User paulson
# Date 887896885 -3600
# Node ID 83d364462ce16477c79c3060eb964b277f092862
# Parent  d4a0749737152ae687a9ac68803d01fd31f9e4ce
Four new Union/Intersection laws

diff -r d4a074973715 -r 83d364462ce1 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Feb 18 18:42:54 1998 +0100
+++ b/src/HOL/equalities.ML	Thu Feb 19 15:01:25 1998 +0100
@@ -176,6 +176,10 @@
 qed "Int_UNIV_right";
 Addsimps[Int_UNIV_right];
 
+goal thy "A Int B = Inter{A,B}";
+by (Blast_tac 1);
+qed "Int_eq_Inter";
+
 goal thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
 by (Blast_tac 1);
 qed "Int_Un_distrib";
@@ -239,6 +243,10 @@
 qed "Un_UNIV_right";
 Addsimps[Un_UNIV_right];
 
+goal thy "A Un B = Union{A,B}";
+by (Blast_tac 1);
+qed "Un_eq_Union";
+
 goal thy "(insert a B) Un C = insert a (B Un C)";
 by (Blast_tac 1);
 qed "Un_insert_left";
@@ -405,11 +413,19 @@
 qed "UN_empty2";
 Addsimps[UN_empty2];
 
+goal thy "!!k. k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
+by (Blast_tac 1);
+qed "UN_absorb";
+
 goal thy "(INT x:{}. B x) = UNIV";
 by (Blast_tac 1);
 qed "INT_empty";
 Addsimps[INT_empty];
 
+goal thy "!!k. k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
+by (Blast_tac 1);
+qed "INT_absorb";
+
 goal thy "(UN x:insert a A. B x) = B a Un UNION A B";
 by (Blast_tac 1);
 qed "UN_insert";