From 31ff82301c71c51957d08965d2e4451d375860d8 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 17 Aug 2018 18:39:12 +0200 Subject: Properties of function composition --- ProdProps.thy | 29 +++++------------------------ 1 file changed, 5 insertions(+), 24 deletions(-) (limited to 'ProdProps.thy') diff --git a/ProdProps.thy b/ProdProps.thy index 2145bf9..7071b39 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -39,35 +39,16 @@ proof (subst (0 1 2 3) compose_def) qed -lemma compose_comp': +lemma compose_comp: assumes "A: U(i)" and "\x. x: A \ b(x): B" and "\x. x: B \ c(x): C(x)" shows "(\<^bold>\x. c(x)) \ (\<^bold>\x. b(x)) \ \<^bold>\x. c(b(x))" proof (subst compose_def, subst Prod_eq) - show "\x. x: A \ (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`x) \ \<^bold>\x. c (b x)" + show "\a. a: A \ (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c (b x))`a" proof compute - - - -text "However we can derive a variant with more explicit premises:" - -lemma compose_comp: - assumes - "A: U(i)" "B: U(i)" "C: B \ U(i)" and - "\x. x: A \ b(x): B" and - "\x. x: B \ c(x): C(x)" - shows "(\<^bold>\x. c(x)) \ (\<^bold>\x. b(x)) \ \<^bold>\x. c(b(x))" -proof (subst compose_def) - show "\<^bold>\x. (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`x) \ \<^bold>\x. c(b(x))" - proof - show "\a. a: A \ (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`a) \ c(b(a))" - proof compute - show "\a. a: A \ c((\<^bold>\x. b(x))`a) \ c(b(a))" by compute (simple lems: assms) - qed (simple lems: assms) - qed fact + show "\a. a: A \ c((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c(b(x)))`a" + by compute (simple lems: assms, compute?)+ + qed (simple lems: assms) qed (simple lems: assms) -lemmas compose_comps [comp] = compose_def compose_comp - - end -- cgit v1.2.3