# HG changeset patch
# User lcp
# Date 789958886 -3600
# Node ID ce99db6728ba60db6591409b2354b9f0051f7b88
# Parent  28a593f4b600dd9b9b9b7c1f101419bd517844f0
Proved comp_lam.

diff -r 28a593f4b600 -r ce99db6728ba src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Jan 13 02:00:43 1995 +0100
+++ b/src/ZF/Perm.ML	Fri Jan 13 02:01:26 1995 +0100
@@ -330,6 +330,18 @@
 		      apply_Pair,apply_type] 1));
 qed "comp_fun_apply";
 
+(*Simplifies compositions of lambda-abstractions*)
+val [prem] = goal Perm.thy
+    "[| !!x. x:A ==> b(x): B 	\
+\    |] ==> (lam y:B.c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
+by (resolve_tac [fun_extension] 1);
+by (resolve_tac [comp_fun] 1);
+by (resolve_tac [lam_funtype] 2);
+by (typechk_tac (prem::ZF_typechecks));
+by (asm_simp_tac (ZF_ss addsimps [comp_fun_apply]
+             setsolver type_auto_tac [lam_type, lam_funtype, prem]) 1);
+qed "comp_lam";
+
 goal Perm.thy "!!f g. [| g: inj(A,B);  f: inj(B,C) |] ==> (f O g) : inj(A,C)";
 by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
     f_imp_injective 1);