# HG changeset patch
# User lcp
# Date 755171748 -3600
# Node ID 320f6bdb593a5a595ec623ace4a69e4bbb9d1fca
# Parent  b63888ea0b28fa1ad3973feb2a31008ce3b86b3d
ZF/ord/Ord_Un,Ord_Int,Un_upper1_le,Un_upper2_le: new

diff -r b63888ea0b28 -r 320f6bdb593a src/ZF/Ord.ML
--- a/src/ZF/Ord.ML	Mon Dec 06 09:35:35 1993 +0100
+++ b/src/ZF/Ord.ML	Mon Dec 06 10:55:48 1993 +0100
@@ -157,6 +157,14 @@
 by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
 val Ord_succ_iff = result();
 
+goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
+by (fast_tac (ZF_cs addSIs [Transset_Un]) 1);
+val Ord_Un = result();
+
+goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
+by (fast_tac (ZF_cs addSIs [Transset_Int]) 1);
+val Ord_Int = result();
+
 val nonempty::prems = goal Ord.thy
     "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
@@ -443,6 +451,16 @@
 
 (** Union and Intersection **)
 
+goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i Un j";
+by (rtac (Un_upper1 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper1_le = result();
+
+goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j le i Un j";
+by (rtac (Un_upper2 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper2_le = result();
+
 (*Replacing k by succ(k') yields the similar rule for le!*)
 goal Ord.thy "!!i j k. [| i<k;  j<k |] ==> i Un j < k";
 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
diff -r b63888ea0b28 -r 320f6bdb593a src/ZF/ord.ML
--- a/src/ZF/ord.ML	Mon Dec 06 09:35:35 1993 +0100
+++ b/src/ZF/ord.ML	Mon Dec 06 10:55:48 1993 +0100
@@ -157,6 +157,14 @@
 by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
 val Ord_succ_iff = result();
 
+goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
+by (fast_tac (ZF_cs addSIs [Transset_Un]) 1);
+val Ord_Un = result();
+
+goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
+by (fast_tac (ZF_cs addSIs [Transset_Int]) 1);
+val Ord_Int = result();
+
 val nonempty::prems = goal Ord.thy
     "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
@@ -443,6 +451,16 @@
 
 (** Union and Intersection **)
 
+goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i Un j";
+by (rtac (Un_upper1 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper1_le = result();
+
+goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j le i Un j";
+by (rtac (Un_upper2 RS subset_imp_le) 1);
+by (REPEAT (ares_tac [Ord_Un] 1));
+val Un_upper2_le = result();
+
 (*Replacing k by succ(k') yields the similar rule for le!*)
 goal Ord.thy "!!i j k. [| i<k;  j<k |] ==> i Un j < k";
 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);