diff options
author | Josh Chen | 2018-08-12 13:04:16 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-12 13:04:16 +0200 |
commit | 7a89ec1e72f61179767c6488177c6d12e69388c5 (patch) | |
tree | a305bd9d92d6a51dec49b4c741dc77323ff3ab0c /EqualProps.thy | |
parent | 25225e0c637a43319fef6889dabc222df05bfd3c (diff) |
Commit before testing polymorphic equality eliminator
Diffstat (limited to 'EqualProps.thy')
-rw-r--r-- | EqualProps.thy | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 17c7fa6..9d23a99 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -15,20 +15,25 @@ begin section \<open>Symmetry / Path inverse\<close> -definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") - where "inv[A,x,y] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) x y p" +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" lemma inv_type: - assumes "A : U(i)" and "x : A" and "y : A" shows "inv[A,x,y] : x =\<^sub>A y \<rightarrow> y =\<^sub>A x" - unfolding inv_def - by (derive lems: assms) + 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" +unfolding inv_def +proof + 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)+ -corollary assumes "x =\<^sub>A y : U(i)" and "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" - by (derive lems: inv_type assms) -lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)" - unfolding inv_def by (simplify lems: assms) +lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) \<equiv> refl(a)" +unfolding inv_def +proof + show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. + show "\<And>x. x: A \<Longrightarrow> x =\<^sub>A x: U(i)" using assms(1) .. +qed (fact assms) section \<open>Transitivity / Path composition\<close> @@ -42,10 +47,8 @@ definition rcompose :: "Term \<Rightarrow> Term" ("(1rcompose[_])") x y p" -text "``Natural'' composition function, of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>." - -abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") - where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:(x =\<^sub>A y). \<^bold>\<lambda>q:(y =\<^sub>A z). rcompose[A]`x`y`p`z`q" +definition compose :: "[Term, Term, Term] \<Rightarrow> [Term, Term] \<Rightarrow> Term" ("(1compose[ _,/ _,/ _])") + where "compose[x,y,z] \<equiv> \<lambda>p." lemma compose_type: |