From b01b8ee0f3472cb728f09463d0620ac8b8066bcb Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 Mar 2019 14:41:16 +0100
Subject: More progress. I think we are reaching the limit of what can be
 conveniently proved with the current implementation.

---
 Prod.thy | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

(limited to 'Prod.thy')

diff --git a/Prod.thy b/Prod.thy
index 75db657..a35138c 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -119,8 +119,36 @@ unfolding compose_def by (derive lems: assms cong)
 
 abbreviation id :: "t \<Rightarrow> t"  ("(id _)" [115] 114)  where "id A \<equiv> \<lambda>x: A. x"
 
-lemma id_type [intro]: "\<And>A. A: U i \<Longrightarrow> id A: A \<rightarrow> A" by derive
-
+lemma id_type: "\<And>A. A: U i \<Longrightarrow> id A: A \<rightarrow> A" by derive
+
+lemma id_compl:
+  assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B"
+  shows "id B o[A] f \<equiv> f"
+unfolding compose_def proof -
+  {
+  fix x assume [intro]: "x: A"
+  have "(id B)`(f`x) \<equiv> f`x" by derive
+  }
+  hence "\<lambda>x: A. (id B)`(f`x) \<equiv> \<lambda>x: A. f`x" by (derive lems: cong) derive
+  also have "\<lambda>x: A. f`x \<equiv> f" by derive
+  finally show "\<lambda>(x: A). (id B)`(f`x) \<equiv> f" by simp
+qed
+
+lemma id_compr:
+  assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B"
+  shows "f o[A] id A \<equiv> f"
+unfolding compose_def proof -
+  {
+  fix x assume [intro]: "x: A"
+  have "f`((id A)`x) \<equiv> f`x" by derive
+  }
+  hence "\<lambda>x: A. f`((id A)`x) \<equiv> \<lambda>x: A. f`x" by (derive lems: cong) derive
+  also have "\<lambda>x: A. f`x \<equiv> f" by derive
+  finally show "\<lambda>x: A. f`((id A)`x) \<equiv> f" by simp
+qed
+
+declare id_type [intro]
+lemmas id_comp [comp] = id_compl id_compr
 
 section \<open>Universal quantification\<close>
 
-- 
cgit v1.2.3