# HG changeset patch
# User paulson
# Date 828610895 -7200
# Node ID 581165679095cd958a8c8375a4f891b264a42f1b
# Parent  d3484e841d1e244cafc81611335e6604d6887d76
Added more _iff rewrites for Compl, Un, Int

diff -r d3484e841d1e -r 581165679095 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Apr 04 10:24:38 1996 +0200
+++ b/src/HOL/Set.ML	Thu Apr 04 11:41:35 1996 +0200
@@ -187,6 +187,9 @@
 
 val ComplE = make_elim ComplD;
 
+qed_goal "Compl_iff" Set.thy "(c : Compl(A)) = (c~:A)"
+ (fn _ => [ (fast_tac (HOL_cs addSIs [ComplI] addSEs [ComplE]) 1) ]);
+
 
 section "Binary union -- Un";
 
@@ -211,6 +214,9 @@
 by (REPEAT (eresolve_tac prems 1));
 qed "UnE";
 
+qed_goal "Un_iff" Set.thy "(c : A Un B) = (c:A | c:B)"
+ (fn _ => [ (fast_tac (HOL_cs addSIs [UnCI] addSEs [UnE]) 1) ]);
+
 
 section "Binary intersection -- Int";
 
@@ -234,6 +240,9 @@
 by (rtac (major RS IntD2) 1);
 qed "IntE";
 
+qed_goal "Int_iff" Set.thy "(c : A Int B) = (c:A & c:B)"
+ (fn _ => [ (fast_tac (HOL_cs addSIs [IntI] addSEs [IntE]) 1) ]);
+
 
 section "Set difference";
 
@@ -276,6 +285,9 @@
  (fn [major,minor]=>
   [ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
 
+qed_goal "empty_iff" Set.thy "(c : {}) = False"
+ (fn _ => [ (fast_tac (HOL_cs addSEs [emptyE]) 1) ]);
+
 
 section "Augmenting a set -- insert";