diff options
author | Josh Chen | 2018-08-15 00:00:09 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-15 00:00:09 +0200 |
commit | e94784953a751b0720689b686e607c95ba0f0592 (patch) | |
tree | 981da8fdd9e7f15da99674db247d07eaaaad0278 /Prod.thy | |
parent | e6473c383b479610cee4c0119e5811a12a938cf9 (diff) |
Function composition, rename path composition to differentiate the two.
Diffstat (limited to 'Prod.thy')
-rw-r--r-- | Prod.thy | 16 |
1 files changed, 16 insertions, 0 deletions
@@ -68,6 +68,22 @@ lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 lemmas Prod_comps [comp] = Prod_comp Prod_uniq +subsection \<open>Composition\<close> + +axiomatization fncompose :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70) where + fncompose_type: "\<lbrakk> + g: \<Prod>x:B. C(x); + f: A \<rightarrow> B; + (\<Prod>x:B. C(x)): U(i); + A \<rightarrow> B: U(i) + \<rbrakk> \<Longrightarrow> g \<circ> f: \<Prod>x:A. C(f`x)" +and + fncompose_comp: "\<lbrakk> + A: U(i); + \<And>x. x: A \<Longrightarrow> b(x): B; + \<And>x. x: A \<Longrightarrow> c(x): C(x) + \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))" + section \<open>Unit type\<close> |