# HG changeset patch
# User paulson
# Date 888228978 -3600
# Node ID f5f957ab73eb0c280868641b173f3758f129756d
# Parent  ecf8f17f6fe07bd992e464d782c9a88bd55e5fb5
New laws for union

diff -r ecf8f17f6fe0 -r f5f957ab73eb src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Feb 23 11:15:40 1998 +0100
+++ b/src/HOL/equalities.ML	Mon Feb 23 11:16:18 1998 +0100
@@ -413,6 +413,11 @@
 qed "UN_empty2";
 Addsimps[UN_empty2];
 
+goal thy "(UN x:A. {x}) = A";
+by (Blast_tac 1);
+qed "UN_singleton";
+Addsimps [UN_singleton];
+
 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";
@@ -609,6 +614,16 @@
 by (Blast_tac 1);
 qed "double_diff";
 
+goal thy "A Un (B-A) = A Un B";
+by (Blast_tac 1);
+qed "Un_Diff_cancel";
+
+goal thy "(B-A) Un A = B Un A";
+by (Blast_tac 1);
+qed "Un_Diff_cancel2";
+
+Addsimps [Un_Diff_cancel, Un_Diff_cancel2];
+
 goal thy "A - (B Un C) = (A-B) Int (A-C)";
 by (Blast_tac 1);
 qed "Diff_Un";
@@ -625,6 +640,10 @@
 by (Blast_tac 1);
 qed "Int_Diff";
 
+goal thy "(A-B) Int C = (A Int C) - (B Int C)";
+by (Blast_tac 1);
+qed "Diff_Int_distrib";
+
 
 section "Miscellany";