# HG changeset patch
# User lcp
# Date 777056983 -7200
# Node ID 5fbfa997f1b03c3cc8164bdd08248feed5993ea7
# Parent  9d62c7e0869953c9089c6e8ddb6f51500a26ddfc
ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
they can be proved trivially using eq_cs
ZF/domrange/XXX_empty: renamed XXX_0

diff -r 9d62c7e08699 -r 5fbfa997f1b0 src/ZF/domrange.ML
--- a/src/ZF/domrange.ML	Tue Aug 16 19:06:14 1994 +0200
+++ b/src/ZF/domrange.ML	Tue Aug 16 19:09:43 1994 +0200
@@ -57,21 +57,8 @@
   [ (rtac (domain_iff RS iffD1 RS exE) 1),
     (REPEAT (ares_tac prems 1)) ]);
 
-val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A"
- (fn _ =>
-  [ (REPEAT (eresolve_tac [domainE,SigmaE2] 1
-     ORELSE ares_tac [domainI,equalityI,subsetI,SigmaI] 1)) ]);
-
-val domain_empty = prove_goal ZF.thy "domain(0) = 0"
- (fn _ =>
-  [ (REPEAT (eresolve_tac [domainE,emptyE] 1
-     ORELSE ares_tac [equalityI,subsetI] 1)) ]);
-
 val domain_subset = prove_goal ZF.thy "domain(Sigma(A,B)) <= A"
- (fn _ =>
-  [ (rtac subsetI 1),
-    (etac domainE 1),
-    (etac SigmaD1 1) ]);
+ (fn _ => [ (rtac subsetI 1), (etac domainE 1), (etac SigmaD1 1) ]);
 
 
 (*** range ***)
@@ -86,17 +73,6 @@
     (resolve_tac prems 1),
     (etac converseD 1) ]);
 
-val range_of_prod = prove_goalw ZF.thy [range_def]
-    "!!a A B. a:A ==> range(A*B) = B"
- (fn _ =>
-  [ (rtac (converse_of_prod RS ssubst) 1),
-    (etac domain_of_prod 1) ]);
-
-val range_empty = prove_goalw ZF.thy [range_def] "range(0) = 0"
- (fn _ =>
-  [ (rtac (converse_empty RS ssubst) 1),
-    (rtac domain_empty 1) ]);
-
 val range_subset = prove_goalw ZF.thy [range_def] "range(A*B) <= B"
  (fn _ =>
   [ (rtac (converse_of_prod RS ssubst) 1),
@@ -128,10 +104,6 @@
   [ (rtac (major RS UnE) 1),
     (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);
 
-val field_of_prod = prove_goal ZF.thy "field(A*A) = A"
- (fn _ =>
-  [ (fast_tac (pair_cs addIs  [fieldCI,equalityI] addSEs [fieldE]) 1) ]);
-
 val field_subset = prove_goal ZF.thy "field(A*B) <= A Un B"
  (fn _ => [ (fast_tac (pair_cs addIs  [fieldCI] addSEs [fieldE]) 1) ]);
 
diff -r 9d62c7e08699 -r 5fbfa997f1b0 src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Tue Aug 16 19:06:14 1994 +0200
+++ b/src/ZF/equalities.ML	Tue Aug 16 19:09:43 1994 +0200
@@ -296,7 +296,17 @@
 by (fast_tac eq_cs 1);
 val SUM_eq_UN = result();
 
-(** Domain, Range and Field **)
+(** Domain **)
+
+val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A"
+ (fn _ => [ fast_tac eq_cs 1 ]);
+
+val domain_0 = prove_goal ZF.thy "domain(0) = 0"
+ (fn _ => [ fast_tac eq_cs 1 ]);
+
+val domain_cons = prove_goal ZF.thy
+    "domain(cons(<a,b>,r)) = cons(a, domain(r))"
+ (fn _ => [ fast_tac eq_cs 1 ]);
 
 goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
 by (fast_tac eq_cs 1);
@@ -310,6 +320,19 @@
 by (fast_tac eq_cs 1);
 val domain_diff_subset = result();
 
+(** Range **)
+
+val range_of_prod = prove_goal ZF.thy
+    "!!a A B. a:A ==> range(A*B) = B"
+ (fn _ => [ fast_tac eq_cs 1 ]);
+
+val range_0 = prove_goal ZF.thy "range(0) = 0"
+ (fn _ => [ fast_tac eq_cs 1 ]); 
+
+val range_cons = prove_goal ZF.thy
+    "range(cons(<a,b>,r)) = cons(b, range(r))"
+ (fn _ => [ fast_tac eq_cs 1 ]);
+
 goal ZF.thy "range(A Un B) = range(A) Un range(B)";
 by (fast_tac eq_cs 1);
 val range_Un_eq = result();
@@ -322,6 +345,18 @@
 by (fast_tac eq_cs 1);
 val range_diff_subset = result();
 
+(** Field **)
+
+val field_of_prod = prove_goal ZF.thy "field(A*A) = A"
+ (fn _ => [ fast_tac eq_cs 1 ]); 
+
+val field_0 = prove_goal ZF.thy "field(0) = 0"
+ (fn _ => [ fast_tac eq_cs 1 ]); 
+
+val field_cons = prove_goal ZF.thy
+    "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
+ (fn _ => [ rtac equalityI 1, ALLGOALS (fast_tac ZF_cs) ]);
+
 goal ZF.thy "field(A Un B) = field(A) Un field(B)";
 by (fast_tac eq_cs 1);
 val field_Un_eq = result();
@@ -339,7 +374,7 @@
 
 goal ZF.thy "r``0 = 0";
 by (fast_tac eq_cs 1);
-val image_empty = result();
+val image_0 = result();
 
 goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
 by (fast_tac eq_cs 1);
@@ -362,7 +397,7 @@
 
 goal ZF.thy "r-``0 = 0";
 by (fast_tac eq_cs 1);
-val vimage_empty = result();
+val vimage_0 = result();
 
 goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
 by (fast_tac eq_cs 1);