aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Prod.thy29
1 files 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