diff options
| author | Josh Chen | 2018-07-07 23:03:33 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-07-07 23:03:33 +0200 |
| commit | decb363a30a30c1875bf4b93bc544c28edf3149e (patch) | |
| tree | d4b8c2d5fa1b1146815c58c4630de75b6768f7c6 /EqualProps.thy | |
| parent | 8541c7d0748d06676e5eb52d61cf468858d590e2 (diff) | |
Library snapshot. Methods written, everything nicely organized.
Diffstat (limited to 'EqualProps.thy')
| -rw-r--r-- | EqualProps.thy | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index 2807587..cb267c6 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -22,22 +22,14 @@ definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") lemma inv_type: assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" - by (derive lems: assms unfolds: inv_def) + unfolding inv_def + by (derive lems: assms) lemma inv_comp: assumes "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)" - -proof - - have "inv[A,a,a]`refl(a) \<equiv> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a)" - by (derive lems: assms unfolds: inv_def) - - also have "indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" - by (simple lems: assms) - - finally show "inv[A,a,a]`refl(a) \<equiv> refl(a)" . -qed + unfolding inv_def by (simplify lems: assms) section \<open>Transitivity / Path composition\<close> @@ -50,6 +42,7 @@ definition rcompose :: "Term \<Rightarrow> Term" ("(1rcompose[_])") (\<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" + 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>." abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") @@ -59,14 +52,15 @@ abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compo 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" - by (derive lems: assms unfolds: rcompose_def) + 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)" - -sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close> + unfolding rcompose_def + by (simplify lems: assms) lemmas Equal_simps [intro] = inv_comp compose_comp |