# HG changeset patch
# User lcp
# Date 777547643 -7200
# Node ID 13c30ac40f8fb36b823ba1f406dd0000acba46b2
# Parent  0b03ce5b62f7ad3478b24a2226029911b8241b86
ZF/upair/consE', UnE': new

diff -r 0b03ce5b62f7 -r 13c30ac40f8f src/ZF/upair.ML
--- a/src/ZF/upair.ML	Mon Aug 22 11:11:17 1994 +0200
+++ b/src/ZF/upair.ML	Mon Aug 22 11:27:23 1994 +0200
@@ -52,6 +52,17 @@
     (etac UpairE 1),
     (REPEAT (EVERY1 [resolve_tac prems, etac subst, assume_tac])) ]);
 
+(*Stronger version of the rule above*)
+val UnE' = prove_goal ZF.thy
+    "[| c : A Un B;  c:A ==> P;  [| c:B;  c~:A |] ==> P |] ==> P"
+ (fn major::prems =>
+  [(rtac (major RS UnE) 1),
+   (eresolve_tac prems 1),
+   (rtac classical 1),
+   (eresolve_tac prems 1),
+   (swap_res_tac prems 1),
+   (etac notnotD 1)]);
+
 val Un_iff = prove_goal ZF.thy "c : A Un B <-> (c:A | c:B)"
  (fn _ => [ (fast_tac (lemmas_cs addIs [UnI1,UnI2] addSEs [UnE]) 1) ]);
 
@@ -125,6 +136,17 @@
   [ (rtac (major RS UnE) 1),
     (REPEAT (eresolve_tac (prems @ [UpairE]) 1)) ]);
 
+(*Stronger version of the rule above*)
+val consE' = prove_goal ZF.thy
+    "[| a : cons(b,A);  a=b ==> P;  [| a:A;  a~=b |] ==> P |] ==> P"
+ (fn major::prems =>
+  [(rtac (major RS consE) 1),
+   (eresolve_tac prems 1),
+   (rtac classical 1),
+   (eresolve_tac prems 1),
+   (swap_res_tac prems 1),
+   (etac notnotD 1)]);
+
 val cons_iff = prove_goal ZF.thy "a : cons(b,A) <-> (a=b | a:A)"
  (fn _ => [ (fast_tac (lemmas_cs addIs [consI1,consI2] addSEs [consE]) 1) ]);