# HG changeset patch
# User paulson
# Date 951128179 -3600
# Node ID 2ae7f9b2c0bf6cee8d27a35d80de5266670319dc
# Parent  4bc79ed1233bda7cdfc27e7e4a0bea148167ee57
simplified some proofs

diff -r 4bc79ed1233b -r 2ae7f9b2c0bf src/ZF/AC/AC2_AC6.ML
--- a/src/ZF/AC/AC2_AC6.ML	Mon Feb 21 11:15:43 2000 +0100
+++ b/src/ZF/AC/AC2_AC6.ML	Mon Feb 21 11:16:19 2000 +0100
@@ -14,8 +14,7 @@
 (* AC1 ==> AC2                                                            *)
 (* ********************************************************************** *)
 
-Goal "[| B:A; f:(PROD X:A. X); 0~:A |]  \
-\               ==> {f`B} <= B Int {f`C. C:A}";
+Goal "[| f:(PROD X:A. X);  B:A;  0~:A |] ==> {f`B} <= B Int {f`C. C:A}";
 by (fast_tac (claset() addSEs [apply_type]) 1);
 val lemma1 = result();
 
@@ -47,15 +46,14 @@
 by (rtac subst_elem 1);
 by (fast_tac (claset() addSIs [the_equality]
                 addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2);
-by (fast_tac (claset() addSEs [equalityE, make_elim singleton_subsetD]) 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
 val lemma2 = result();
 
 Goal "ALL D:{E*{E}. E:A}. EX y. D Int C = {y}  \
 \       ==> (lam x:A. fst(THE z. (x*{x} Int C = {z}))) :  \
 \               (PROD X:A. X) ";
-by (fast_tac (claset() addSEs [lemma2]
-                addSIs [lam_type, RepFunI, fst_type]
-                addSDs [bspec]) 1);
+by (fast_tac (claset() addSEs [lemma2] 
+                       addSIs [lam_type, RepFunI, fst_type]) 1);
 val lemma3 = result();
 
 Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1";
@@ -90,7 +88,7 @@
 val lemma1 = result();
 
 Goal "domain(UN z:A. {z}*f(z)) = {a:A. f(a)~=0}";
-by (fast_tac (claset() addSIs [not_emptyI] addDs [range_type]) 1);
+by (Blast_tac 1);
 val lemma2 = result();
 
 Goal "x:A ==> (UN z:A. {z}*f(z))``{x} = f(x)";
@@ -102,7 +100,7 @@
 by (REPEAT (eresolve_tac [allE,impE] 1));
 by (etac lemma1 1);
 by (asm_full_simp_tac (simpset() addsimps [lemma2, lemma3]
-                        addcongs [Pi_cong]) 1);
+                                 addcongs [Pi_cong]) 1);
 qed "AC4_AC3";
 
 (* ********************************************************************** *)
@@ -116,10 +114,7 @@
 val lemma = result();
 
 Goalw AC_defs "AC3 ==> AC1";
-by (REPEAT (resolve_tac [allI, impI] 1));
-by (REPEAT (eresolve_tac [allE, ballE] 1));
-by (fast_tac (claset() addSIs [id_type]) 2);
-by (fast_tac (claset() addEs [lemma RS subst]) 1);
+by (fast_tac (claset() addSIs [id_type] addEs [lemma RS subst]) 1);
 qed "AC3_AC1";
 
 (* ********************************************************************** *)
@@ -152,14 +147,8 @@
 val lemma1 = result();
 
 Goalw [range_def] "R <= A*B ==> range(lam x:R. fst(x)) = domain(R)";
-by (rtac equalityI 1);
-by (fast_tac (claset() addSEs [lamE]
-                addEs [subst_elem]
-                addSDs [Pair_fst_snd_eq]) 1);
-by (rtac subsetI 1);
-by (etac domainE 1);
-by (rtac domainI 1);
-by (fast_tac (claset() addSEs [lamI RS subst_elem] addIs [fst_conv RS ssubst]) 1);
+by (force_tac (claset() addIs [lamI RS subst_elem] addSEs [lamE], 
+	       simpset()) 1);
 val lemma2 = result();
 
 Goal "[| EX f: A->C. P(f,domain(f)); A=B |] ==>  EX f: B->C. P(f,B)";
@@ -171,16 +160,11 @@
 Goal "[| R <= A*B; g: C->R; ALL x:C. (lam z:R. fst(z))` (g`x) = x |] \
 \               ==> (lam x:C. snd(g`x)): (PROD x:C. R``{x})";
 by (rtac lam_type 1);
-by (dtac apply_type 1 THEN (assume_tac 1));
-by (dtac bspec 1 THEN (assume_tac 1));
-by (rtac imageI 1);
-by (resolve_tac [subsetD RS Pair_fst_snd_eq RSN (2, subst_elem)] 1
-        THEN (REPEAT (assume_tac 1)));
-by (Asm_full_simp_tac 1);
+by (force_tac (claset() addDs [apply_type], simpset()) 1);
 val lemma4 = result();
 
 Goalw AC_defs "AC5 ==> AC4";
-by (REPEAT (resolve_tac [allI,impI] 1));
+by (Clarify_tac 1);
 by (REPEAT (eresolve_tac [allE,ballE] 1));
 by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2));
 by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1));
@@ -195,4 +179,3 @@
 Goalw AC_defs "AC1 <-> AC6";
 by (Blast_tac 1);
 qed "AC1_iff_AC6";
-