Moved function composition lemmas into Prod.thy

1 files changed, 0 insertions, 57 deletions

diff --git a/ProdProps.thy b/ProdProps.thy
deleted file mode 100644
index a68f79b..0000000
--- a/ProdProps.thy
+++ /dev/null
@@ -1,57 +0,0 @@
-(*  Title:  HoTT/ProdProps.thy
-    Author: Josh Chen
-
-Properties of the dependent product
-*)
-
-theory ProdProps
-  imports
-    HoTT_Methods
-    Prod
-begin
-
-
-section \<open>Composition\<close>
-
-text "
-  The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Prod>-type definitional equality, and the correct substitutions in the subgoals thereafter.
-"
-
-lemma compose_assoc:
-  assumes "A: U i" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D x"
-  shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)"
-proof (subst (0 1 2 3) compose_def)
-  show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)"
-  proof (subst Prod_eq)
-    \<comment> \<open>Todo: set the Simplifier (or other simplification methods) up to use \<open>Prod_eq\<close>!\<close>
-    
-    show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
-    proof compute
-      show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
-      proof compute
-        show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (routine lems: assms)
-      qed
-      show "\<And>x. x: B \<Longrightarrow> h`(g`x): D (g`x)" by (routine lems: assms)
-    qed (routine lems: assms)
-  qed fact
-qed
-
-
-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>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
-    show "\<And>a. a: A \<Longrightarrow> c ((\<^bold>\<lambda>x. b x)`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a"
-    by (derive lems: assms)
-  qed (routine lems: assms)
-qed (derive lems: assms)
-
-
-text "Set up the \<open>compute\<close> method to automatically simplify function compositions."
-
-lemmas compose_comp [comp]
-
-
-end