diff options
| -rw-r--r-- | Prod.thy | 29 |
1 files changed, 11 insertions, 18 deletions
@@ -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 |