diff options
author | Josh Chen | 2018-08-13 10:37:20 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-13 10:37:20 +0200 |
commit | 962fc96123039b53b9c6946796e909fb50ec9004 (patch) | |
tree | 16f7d456fef26b6eb549200515a274e8ed3fc388 /EqualProps.thy | |
parent | 7a89ec1e72f61179767c6488177c6d12e69388c5 (diff) |
rcompose done
Diffstat (limited to '')
-rw-r--r-- | EqualProps.thy | 78 |
1 files changed, 60 insertions, 18 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 9d23a99..d645fb6 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -15,20 +15,20 @@ begin section \<open>Symmetry / Path inverse\<close> -definition inv :: "[Term, Term] \<Rightarrow> (Term \<Rightarrow> Term)" ("(1inv[_,/ _])") - where "inv[x,y] \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) x y p" +axiomatization inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) + where inv_def: "inv \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) p" lemma inv_type: - assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "inv[x,y](p): y =\<^sub>A x" + assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x" unfolding inv_def -proof +proof (rule Equal_elim[where ?x=x and ?y=y]) \<comment> \<open>Path induction\<close> show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> y =\<^sub>A x: U(i)" using assms(1) .. show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. qed (fact assms)+ -lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) \<equiv> refl(a)" +lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)" unfolding inv_def proof show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. @@ -38,24 +38,66 @@ qed (fact assms) section \<open>Transitivity / Path composition\<close> -text "``Raw'' composition function, of type \<open>\<Prod>x,y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close>." +text " + Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. +" + +axiomatization rcompose :: Term where + rcompose_def: "rcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" + -definition rcompose :: "Term \<Rightarrow> Term" ("(1rcompose[_])") - where "rcompose[A] \<equiv> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:A. \<^bold>\<lambda>p:(x =\<^sub>A y). indEqual[A] - (\<lambda>x y _. \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z) - (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>p:(x =\<^sub>A z). indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<lambda>x. refl(x)) x z p) - x y p" +lemma rcompose_type: + assumes "A: U(i)" + shows "rcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" +unfolding rcompose_def +proof + show "\<And>x. x: A \<Longrightarrow> + \<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + proof + show "\<And>x y. \<lbrakk>x: A ; y: A\<rbrakk> \<Longrightarrow> + \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" + proof + { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y" + show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z" + proof (rule Equal_elim[where ?x=x and ?y=y]) + show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)" + proof + show "\<And>x y z. \<lbrakk>x: A; y: A; z: A\<rbrakk> \<Longrightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)" + by (rule Prod_form Equal_form assms | assumption)+ + qed (rule assms) + + show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>z p. ind\<^sub>= refl p: \<Prod>z:A. x =\<^sub>A z \<rightarrow> x =\<^sub>A z" + proof + show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>p. ind\<^sub>= refl p: x =\<^sub>A z \<rightarrow> x =\<^sub>A z" + proof + { fix x z p assume asm: "x: A" "z: A" "p: x =\<^sub>A z" + show "ind\<^sub>= refl p: x =[A] z" + proof (rule Equal_elim[where ?x=x and ?y=z]) + show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms) + show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. + qed (fact asm)+ } + show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> x =\<^sub>A z: U(i)" by standard (rule assms) + qed + qed (rule assms) + qed (rule asm)+ } + show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms) + qed + qed (rule assms) +qed (fact assms) +corollary + assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" + shows "rcompose`x`y`p`z`q: x =\<^sub>A z" + by standard+ (rule rcompose_type assms)+ -definition compose :: "[Term, Term, Term] \<Rightarrow> [Term, Term] \<Rightarrow> Term" ("(1compose[ _,/ _,/ _])") - where "compose[x,y,z] \<equiv> \<lambda>p." +axiomatization compose :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where + compose_comp: "\<lbrakk> + A: U(i); + x: A; y: A; z: A; + p: x =\<^sub>A y; q: y =\<^sub>A z + \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rcompose`x`y`p`z`q" -lemma compose_type: - assumes "A : U(i)" and "x : A" and "y : A" and "z : A" - shows "compose[A,x,y,z] : x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z" - unfolding rcompose_def - by (derive lems: assms) lemma compose_comp: assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" |