From 73e7023a301753e91dfdc9ba49c4bcff91dbddc3 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 28 Feb 2019 18:42:59 +0100 Subject: tweak mixfix priorities --- Prod.thy | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) (limited to 'Prod.thy') diff --git a/Prod.thy b/Prod.thy index 48f0151..0bd037d 100644 --- a/Prod.thy +++ b/Prod.thy @@ -96,17 +96,26 @@ in end \ -lemma compose_assoc: - assumes "A: U i" and "f: A \ B" and "g: B \ C" and "h: \x: C. D x" - shows "(h o[B] g) o[A] f \ h o[A] g o[A] f" -unfolding compose_def by (derive lems: assms cong) +lemma compose_type: + assumes + "A: U i" and "B: U i" and "C: B \ U i" and + "f: A \ B" and "g: \x: B. C x" + shows "g o[A] f: \x: A. C (f`x)" +unfolding compose_def by (derive lems: assms) lemma compose_comp: assumes "A: U i" and "\x. x: A \ b x: B" and "\x. x: B \ c x: C x" shows "(\x: B. c x) o[A] (\x: A. b x) \ \x: A. c (b x)" unfolding compose_def by (derive lems: assms cong) -declare compose_comp [comp] +declare + compose_type [intro] + compose_comp [comp] + +lemma compose_assoc: + assumes "A: U i" and "f: A \ B" and "g: B \ C" and "h: \x: C. D x" + shows "(h o[B] g) o[A] f \ h o[A] g o[A] f" +unfolding compose_def by (derive lems: assms cong) abbreviation id :: "t \ t" where "id A \ \x: A. x" -- cgit v1.2.3