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 "\<And>x. x: A \<Longrightarrow> b(x): B" and "\<And>x. x: B \<Longrightarrow> c(x): C(x)"
   shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))"
 proof (subst compose_def, subst Prod_eq)
-  show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`x) \<equiv> \<^bold>\<lambda>x. c (b x)"
+  show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`a) \<equiv> (\<^bold>\<lambda>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 \<longrightarrow> U(i)" and
-    "\<And>x. x: A \<Longrightarrow> b(x): B" and
-    "\<And>x. x: B \<Longrightarrow> c(x): C(x)"
-  shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))"
-proof (subst compose_def)
-  show "\<^bold>\<lambda>x. (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))"
-  proof
-    show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`a) \<equiv> c(b(a))"
-    proof compute
-      show "\<And>a. a: A \<Longrightarrow> c((\<^bold>\<lambda>x. b(x))`a) \<equiv> c(b(a))" by compute (simple lems: assms)
-    qed (simple lems: assms)
-  qed fact
+    show "\<And>a. a: A \<Longrightarrow> c((\<^bold>\<lambda>x. b(x))`a) \<equiv> (\<^bold>\<lambda>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

