# HG changeset patch
# User paulson
# Date 949490729 -3600
# Node ID 1ffd9ec372398a981928559fb644bc7847754823
# Parent  ee74d384321433953172ed2656a76ced1dd84713
new lemma fun_cons_restrict_eq

diff -r ee74d3843214 -r 1ffd9ec37239 src/ZF/func.ML
--- a/src/ZF/func.ML	Wed Feb 02 11:42:17 2000 +0100
+++ b/src/ZF/func.ML	Wed Feb 02 12:25:29 2000 +0100
@@ -314,6 +314,7 @@
 Goalw [restrict_def, lam_def] "domain(restrict(f,C)) = C";
 by (Blast_tac 1);
 qed "domain_restrict";
+Addsimps [domain_restrict];
 
 Goalw [restrict_def]
     "A<=C ==> restrict(lam x:C. b(x), A) = (lam x:A. b(x))";
@@ -322,6 +323,12 @@
 by (Asm_simp_tac 1);
 qed "restrict_lam_eq";
 
+Goal "f : cons(a, b) -> B ==> f = cons(<a, f ` a>, restrict(f, b))";
+by (rtac equalityI 1);
+by (blast_tac (claset() addIs [apply_Pair, impOfSubs restrict_subset]) 2);
+by (auto_tac (claset() addSDs [Pi_memberD],
+	       simpset() addsimps [restrict_def, lam_def]));
+qed "fun_cons_restrict_eq";
 
 
 (*** Unions of functions ***)