From 9d21e7e4ca3f22055acf72f15f19d4c9248882ca Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 5 Feb 2019 18:29:37 +0100
Subject: Basic type inference for composed lambda terms!

---
 Prod.thy | 29 +++++++++++------------------
 1 file changed, 11 insertions(+), 18 deletions(-)

diff --git a/Prod.thy b/Prod.thy
index 4c572ce..a28c52a 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -67,7 +67,7 @@ lemmas Prod_form [form]
 lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim
 lemmas Prod_comp [comp] = Prod_cmp Prod_uniq
 
-section \<open>Additional definitions\<close>
+section \<open>Function composition\<close>
 
 definition compose :: "[t, t, t] \<Rightarrow> t"
 where "compose A g f \<equiv> ,\\x: A. g`(f`x)"
@@ -81,10 +81,12 @@ let fun compose_tr ctxt tms =
   let
     val g :: f :: _ = tms |> map (Typing.tm_of_ptm ctxt)
     val dom =
-      case Typing.get_typing f (Typing.typing_assms ctxt) of
-        SOME (Const ("Prod.Prod", _) $ T $ _) => T
-      | SOME _ => Exn.error "Can't compose with a non-function"
-      | NONE => Exn.error "Cannot infer domain of composition—please state this explicitly"
+      case f of
+        Const ("Prod.lam", _) $ T $ _ => T
+      | _ => (case Typing.get_typing f (Typing.typing_assms ctxt) of
+               SOME (Const ("Prod.Prod", _) $ T $ _) => T
+             | SOME _ => Exn.error "Can't compose with a non-function"
+             | NONE => Exn.error "Cannot infer domain of composition: please state this explicitly")
   in
     @{const compose} $ dom $ g $ f
   end
@@ -94,24 +96,15 @@ end
 \<close>
 
 lemma compose_assoc:
-  assumes "A: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: TT x: C. D x" "(,\\(x: A). b x): TT x: A. D x"
-  shows "(h o g) o f \<equiv> h o (g o f)"
-(* (derive lems: assms Prod_intro_eq) *)
-sorry
+  assumes "A: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: TT x: C. D x"
+  shows "compose A (compose B h g) f \<equiv> compose A h (compose A g f)"
+by (derive lems: assms Prod_intro_eq)
 
 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 "(,\\x: B. c x) o (,\\x: A. b x) \<equiv> ,\\x: A. c (b x)"
-ML_prf \<open>
-Assumption.all_assms_of @{context};
-nth (Assumption.all_assms_of @{context}) 1 |> Thm.term_of;
-Assumption.all_prems_of @{context};
-nth (Assumption.all_prems_of @{context}) 0 |> Thm.prop_of;
-typing_assms @{context}
-\<close>
-(*by (derive lems: assms Prod_intro_eq)*)
+by (derive lems: assms Prod_intro_eq)
 
 abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> ,\\x: A. x"
 
-
 end
-- 
cgit v1.2.3