diff options
Diffstat (limited to 'EqualProps.thy')
-rw-r--r-- | EqualProps.thy | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index cb267c6..43b4eb5 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -19,16 +19,14 @@ 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" -lemma inv_type: - assumes "p : x =\<^sub>A y" - shows "inv[A,x,y]`p : y =\<^sub>A x" +lemma inv_type: assumes "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) - -lemma inv_comp: - assumes "a : A" - shows "inv[A,a,a]`refl(a) \<equiv> refl(a)" +corollary assumes "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 : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by (simplify lems: assms) @@ -43,27 +41,24 @@ definition rcompose :: "Term \<Rightarrow> Term" ("(1rcompose[_])") x y p" -text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>." +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" lemma compose_type: - assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z" - shows "compose[A,x,y,z]`p`q : x =\<^sub>A z" +assumes "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 : A" - shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" +lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" unfolding rcompose_def by (simplify lems: assms) -lemmas Equal_simps [intro] = inv_comp compose_comp +lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp +lemmas EqualProps_comps [comp] = inv_comp compose_comp end
\ No newline at end of file |