ZF/domrange/domain_of_prod, domain_empty, etc: moved to equalities.ML where
authorlcp
Tue Aug 16 19:09:43 1994 +0200 (1994-08-16 ago)
changeset 5365fbfa997f1b0
parent 535 9d62c7e08699
child 537 3a84f846e649
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
src/ZF/domrange.ML
src/ZF/equalities.ML
     1.1 --- a/src/ZF/domrange.ML	Tue Aug 16 19:06:14 1994 +0200
     1.2 +++ b/src/ZF/domrange.ML	Tue Aug 16 19:09:43 1994 +0200
     1.3 @@ -57,21 +57,8 @@
     1.4    [ (rtac (domain_iff RS iffD1 RS exE) 1),
     1.5      (REPEAT (ares_tac prems 1)) ]);
     1.6  
     1.7 -val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A"
     1.8 - (fn _ =>
     1.9 -  [ (REPEAT (eresolve_tac [domainE,SigmaE2] 1
    1.10 -     ORELSE ares_tac [domainI,equalityI,subsetI,SigmaI] 1)) ]);
    1.11 -
    1.12 -val domain_empty = prove_goal ZF.thy "domain(0) = 0"
    1.13 - (fn _ =>
    1.14 -  [ (REPEAT (eresolve_tac [domainE,emptyE] 1
    1.15 -     ORELSE ares_tac [equalityI,subsetI] 1)) ]);
    1.16 -
    1.17  val domain_subset = prove_goal ZF.thy "domain(Sigma(A,B)) <= A"
    1.18 - (fn _ =>
    1.19 -  [ (rtac subsetI 1),
    1.20 -    (etac domainE 1),
    1.21 -    (etac SigmaD1 1) ]);
    1.22 + (fn _ => [ (rtac subsetI 1), (etac domainE 1), (etac SigmaD1 1) ]);
    1.23  
    1.24  
    1.25  (*** range ***)
    1.26 @@ -86,17 +73,6 @@
    1.27      (resolve_tac prems 1),
    1.28      (etac converseD 1) ]);
    1.29  
    1.30 -val range_of_prod = prove_goalw ZF.thy [range_def]
    1.31 -    "!!a A B. a:A ==> range(A*B) = B"
    1.32 - (fn _ =>
    1.33 -  [ (rtac (converse_of_prod RS ssubst) 1),
    1.34 -    (etac domain_of_prod 1) ]);
    1.35 -
    1.36 -val range_empty = prove_goalw ZF.thy [range_def] "range(0) = 0"
    1.37 - (fn _ =>
    1.38 -  [ (rtac (converse_empty RS ssubst) 1),
    1.39 -    (rtac domain_empty 1) ]);
    1.40 -
    1.41  val range_subset = prove_goalw ZF.thy [range_def] "range(A*B) <= B"
    1.42   (fn _ =>
    1.43    [ (rtac (converse_of_prod RS ssubst) 1),
    1.44 @@ -128,10 +104,6 @@
    1.45    [ (rtac (major RS UnE) 1),
    1.46      (REPEAT (eresolve_tac (prems@[domainE,rangeE]) 1)) ]);
    1.47  
    1.48 -val field_of_prod = prove_goal ZF.thy "field(A*A) = A"
    1.49 - (fn _ =>
    1.50 -  [ (fast_tac (pair_cs addIs  [fieldCI,equalityI] addSEs [fieldE]) 1) ]);
    1.51 -
    1.52  val field_subset = prove_goal ZF.thy "field(A*B) <= A Un B"
    1.53   (fn _ => [ (fast_tac (pair_cs addIs  [fieldCI] addSEs [fieldE]) 1) ]);
    1.54  
     2.1 --- a/src/ZF/equalities.ML	Tue Aug 16 19:06:14 1994 +0200
     2.2 +++ b/src/ZF/equalities.ML	Tue Aug 16 19:09:43 1994 +0200
     2.3 @@ -296,7 +296,17 @@
     2.4  by (fast_tac eq_cs 1);
     2.5  val SUM_eq_UN = result();
     2.6  
     2.7 -(** Domain, Range and Field **)
     2.8 +(** Domain **)
     2.9 +
    2.10 +val domain_of_prod = prove_goal ZF.thy "!!A B. b:B ==> domain(A*B) = A"
    2.11 + (fn _ => [ fast_tac eq_cs 1 ]);
    2.12 +
    2.13 +val domain_0 = prove_goal ZF.thy "domain(0) = 0"
    2.14 + (fn _ => [ fast_tac eq_cs 1 ]);
    2.15 +
    2.16 +val domain_cons = prove_goal ZF.thy
    2.17 +    "domain(cons(<a,b>,r)) = cons(a, domain(r))"
    2.18 + (fn _ => [ fast_tac eq_cs 1 ]);
    2.19  
    2.20  goal ZF.thy "domain(A Un B) = domain(A) Un domain(B)";
    2.21  by (fast_tac eq_cs 1);
    2.22 @@ -310,6 +320,19 @@
    2.23  by (fast_tac eq_cs 1);
    2.24  val domain_diff_subset = result();
    2.25  
    2.26 +(** Range **)
    2.27 +
    2.28 +val range_of_prod = prove_goal ZF.thy
    2.29 +    "!!a A B. a:A ==> range(A*B) = B"
    2.30 + (fn _ => [ fast_tac eq_cs 1 ]);
    2.31 +
    2.32 +val range_0 = prove_goal ZF.thy "range(0) = 0"
    2.33 + (fn _ => [ fast_tac eq_cs 1 ]); 
    2.34 +
    2.35 +val range_cons = prove_goal ZF.thy
    2.36 +    "range(cons(<a,b>,r)) = cons(b, range(r))"
    2.37 + (fn _ => [ fast_tac eq_cs 1 ]);
    2.38 +
    2.39  goal ZF.thy "range(A Un B) = range(A) Un range(B)";
    2.40  by (fast_tac eq_cs 1);
    2.41  val range_Un_eq = result();
    2.42 @@ -322,6 +345,18 @@
    2.43  by (fast_tac eq_cs 1);
    2.44  val range_diff_subset = result();
    2.45  
    2.46 +(** Field **)
    2.47 +
    2.48 +val field_of_prod = prove_goal ZF.thy "field(A*A) = A"
    2.49 + (fn _ => [ fast_tac eq_cs 1 ]); 
    2.50 +
    2.51 +val field_0 = prove_goal ZF.thy "field(0) = 0"
    2.52 + (fn _ => [ fast_tac eq_cs 1 ]); 
    2.53 +
    2.54 +val field_cons = prove_goal ZF.thy
    2.55 +    "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
    2.56 + (fn _ => [ rtac equalityI 1, ALLGOALS (fast_tac ZF_cs) ]);
    2.57 +
    2.58  goal ZF.thy "field(A Un B) = field(A) Un field(B)";
    2.59  by (fast_tac eq_cs 1);
    2.60  val field_Un_eq = result();
    2.61 @@ -339,7 +374,7 @@
    2.62  
    2.63  goal ZF.thy "r``0 = 0";
    2.64  by (fast_tac eq_cs 1);
    2.65 -val image_empty = result();
    2.66 +val image_0 = result();
    2.67  
    2.68  goal ZF.thy "r``(A Un B) = (r``A) Un (r``B)";
    2.69  by (fast_tac eq_cs 1);
    2.70 @@ -362,7 +397,7 @@
    2.71  
    2.72  goal ZF.thy "r-``0 = 0";
    2.73  by (fast_tac eq_cs 1);
    2.74 -val vimage_empty = result();
    2.75 +val vimage_0 = result();
    2.76  
    2.77  goal ZF.thy "r-``(A Un B) = (r-``A) Un (r-``B)";
    2.78  by (fast_tac eq_cs 1);