diff options
Diffstat (limited to 'EqualProps.thy')
-rw-r--r-- | EqualProps.thy | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 2a13ed2..f3b355a 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -48,17 +48,17 @@ 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 reqcompose :: Term where - reqcompose_def: "reqcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" +axiomatization rpathcomp :: Term where + rpathcomp_def: "rpathcomp \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p" text " More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: " -lemma reqcompose_type: +lemma rpathcomp_type: assumes "A: U(i)" - shows "reqcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" -unfolding reqcompose_def + shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" +unfolding rpathcomp_def proof fix x assume 1: "x: A" show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" @@ -85,17 +85,17 @@ qed fact corollary assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "reqcompose`x`y`p`z`q: x =\<^sub>A z" - by (simple lems: assms reqcompose_type) + shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" + by (simple lems: assms rpathcomp_type) text " The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule. " -lemma reqcompose_comp: +lemma rpathcomp_comp: assumes "A: U(i)" and "a: A" - shows "reqcompose`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" -unfolding reqcompose_def + shows "rpathcomp`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" +unfolding rpathcomp_def proof compute { fix x assume 1: "x: A" show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" @@ -197,28 +197,28 @@ qed fact text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." -axiomatization eqcompose :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where - eqcompose_def: "\<lbrakk> +axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 60) where + pathcomp_def: "\<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> reqcompose`x`y`p`z`q" + \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q" -lemma eqcompose_type: +lemma pathcomp_type: assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" shows "p \<bullet> q: x =\<^sub>A z" -proof (subst eqcompose_def) +proof (subst pathcomp_def) show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ -qed (simple lems: assms reqcompose_type) +qed (simple lems: assms rpathcomp_type) -lemma eqcompose_comp: +lemma pathcomp_comp: assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)" -by (subst eqcompose_def) (simple lems: assms reqcompose_comp) +by (subst pathcomp_def) (simple lems: assms rpathcomp_comp) -lemmas EqualProps_rules [intro] = inv_type eqcompose_type -lemmas EqualProps_comps [comp] = inv_comp eqcompose_comp +lemmas EqualProps_rules [intro] = inv_type pathcomp_type +lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp end
\ No newline at end of file |