diff options
author | Josh Chen | 2018-08-15 17:17:34 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-15 17:17:34 +0200 |
commit | ca8e7a2681c133abdd082cfa29d6994fa73f2d47 (patch) | |
tree | c5986f543ca354275d2044214199f96eed9b65ec /Prod.thy | |
parent | 257561ff4036d0eb5b51e649f2590b61e08d6fc5 (diff) |
Rename to distinguish function and path composition; function composition proofs, which have issues...
Diffstat (limited to '')
-rw-r--r-- | Prod.thy | 26 |
1 files changed, 18 insertions, 8 deletions
@@ -68,21 +68,31 @@ 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> +section \<open>Function composition\<close> + +axiomatization compose :: "[Term, Term] \<Rightarrow> Term" (infixr "o" 70) + +syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70) +translations "g \<circ> f" \<rightleftharpoons> "g o f" + +axiomatization where + compose_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))" + compose_comp: "\<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 \<equiv> \<^bold>\<lambda>x. g`(f`x)" + +lemmas compose_rules [intro] = compose_type +lemmas compose_comps [comp] = compose_comp section \<open>Unit type\<close> |