# HG changeset patch
# User lcp
# Date 777112403 -7200
# Node ID b4fe3da03449501b0b00750dccd63c909c0b1a6b
# Parent  3a84f846e64979f6fa8cbfb23227a5c1e7333275
ZF/func/fun_extend3: new
ZF/func/cons_fun_eq: simplified proof

diff -r 3a84f846e649 -r b4fe3da03449 src/ZF/func.ML
--- a/src/ZF/func.ML	Wed Aug 17 10:31:35 1994 +0200
+++ b/src/ZF/func.ML	Wed Aug 17 10:33:23 1994 +0200
@@ -374,6 +374,11 @@
 by (fast_tac eq_cs 1);
 val fun_extend = result();
 
+goal ZF.thy
+    "!!f A B. [| f: A->B;  c~:A;  b: B |] ==> cons(<c,b>,f) : cons(c,A) -> B";
+by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 1);
+val fun_extend3 = result();
+
 goal ZF.thy "!!f A B. [| f: A->B;  a:A;  c~:A |] ==> cons(<c,b>,f)`a = f`a";
 by (rtac (apply_Pair RS consI2 RS apply_equality) 1);
 by (rtac fun_extend 3);
@@ -386,23 +391,20 @@
 by (REPEAT (assume_tac 1));
 val fun_extend_apply2 = result();
 
+(*For Finite.ML.  Inclusion of right into left is easy*)
 goal ZF.thy
     "!!c. c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})";
-by (safe_tac eq_cs);
-(*Inclusion of right into left is easy*)
-by (fast_tac (ZF_cs addEs [fun_extend RS fun_weaken_type]) 2);
+by (safe_tac (eq_cs addSEs [fun_extend3]));
 (*Inclusion of left into right*)
 by (subgoal_tac "restrict(x, A) : A -> B" 1);
 by (fast_tac (ZF_cs addEs [restrict_type2]) 2);
 by (rtac UN_I 1 THEN assume_tac 1);
 by (rtac UN_I 1 THEN fast_tac (ZF_cs addEs [apply_type]) 1);
-by (subgoal_tac "x = cons(<c, x ` c>, restrict(x, A))" 1);
-by (fast_tac ZF_cs 1);
-(*Proving the lemma*)
+by (simp_tac (FOL_ss addsimps cons_iff::mem_simps) 1);
 by (resolve_tac [fun_extension] 1 THEN REPEAT (ares_tac [fun_extend] 1));
 by (etac consE 1);
 by (ALLGOALS 
     (asm_simp_tac (FOL_ss addsimps [restrict, fun_extend_apply1, 
-				   fun_extend_apply2])));
+				    fun_extend_apply2])));
 val cons_fun_eq = result();