From 7f932806cf445db589c32429f396d6ccbc086476 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 17 Feb 2019 23:15:02 +0100 Subject: Dependent elimator for Eq now has the correct form. Cleaned up theorems --- Equal.thy | 124 ++++++++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 104 insertions(+), 20 deletions(-) diff --git a/Equal.thy b/Equal.thy index 1d8f6ae..c10e1c2 100644 --- a/Equal.thy +++ b/Equal.thy @@ -15,7 +15,7 @@ section \Type definitions\ axiomatization Eq :: "[t, t, t] \ t" and refl :: "t \ t" and - indEq :: "[[t, t, t] \ t, t \ t, t] \ t" + indEq :: "[[t, t, t] \ t, t \ t, t, t, t] \ t" syntax "_Eq" :: "[t, t, t] \ t" ("(3_ =[_]/ _)" [101, 0, 101] 100) @@ -32,12 +32,12 @@ axiomatization where x: A; y: A; \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f p : C x y p" and + \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f x y p : C x y p" and Equal_comp: "\ a: A; \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f (refl a) \ f a" + \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f a a (refl a) \ f a" lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim @@ -56,13 +56,29 @@ section \Properties of equality\ subsection \Symmetry (path inverse)\ -definition inv :: "[t, t] \ t" -where "inv A p \ indEq (\x y. ^(y =[A] x)) (\x. refl x) p" +definition inv :: "[t, t, t, t] \ t" +where "inv A x y p \ indEq (\x y. ^(y =[A] x)) (\x. refl x) x y p" -lemma inv_type: "\A: U i; x: A; y: A; p: x =[A] y\ \ inv A p: y =[A] x" +syntax "_inv" :: "t \ t" ("~_" [1000]) + +text \Pretty-printing switch for path inverse:\ + +ML \val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\ + +print_translation \ +let fun inv_tr' ctxt [A, x, y, p] = + if Config.get ctxt pretty_inv + then Syntax.const @{syntax_const "_inv"} $ p + else @{const inv} $ A $ x $ y $ p +in + [(@{const_syntax inv}, inv_tr')] +end +\ + +lemma inv_type: "\A: U i; x: A; y: A; p: x =[A] y\ \ inv A x y p: y =[A] x" unfolding inv_def by derive -lemma inv_comp: "\A: U i; a: A\ \ inv A (refl a) \ refl a" +lemma inv_comp: "\A: U i; a: A\ \ inv A a a (refl a) \ refl a" unfolding inv_def by derive declare @@ -74,32 +90,100 @@ subsection \Transitivity (path composition)\ schematic_goal transitivity: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" shows "?p: \z: A. y =[A]z \ x =[A] z" -proof (path_ind x y p, quantify 2) +proof (path_ind x y p, quantify_all) fix x z show "\p. p: x =[A] z \ p: x =[A] z" . qed (routine add: assms) +definition pathcomp :: "[t, t, t, t, t, t] \ t" +where + "pathcomp A x y z p q \ + (indEq (\x y _. \z: A. y =[A] z \ x =[A] z) (\x. \y: A. id (x =[A] y)) x y p)`z`q" -syntax "_pathcomp" :: "[t, t] \ t" (infixl "\" 110) -translations "p \ q" \ "CONST pathcomp`p`q" +syntax "_pathcomp" :: "[t, t] \ t" (infixl "*" 110) -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" - shows "pathcomp: x =\<^sub>A y \ (y =\<^sub>A z) \ (x =\<^sub>A z)" -unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms) +text \Pretty-printing switch for path composition:\ + +ML \val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\ -corollary pathcomp_trans: - assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "p \ q: x =\<^sub>A z" -by (routine add: assms pathcomp_type) +print_translation \ +let fun pathcomp_tr' ctxt [A, x, y, z, p, q] = + if Config.get ctxt pretty_pathcomp + then Syntax.const @{syntax_const "_pathcomp"} $ p $ q + else @{const pathcomp} $ A $ x $ y $ z $ p $ q +in + [(@{const_syntax pathcomp}, pathcomp_tr')] +end +\ + +lemma pathcomp_type: + assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" + shows "pathcomp A x y z p q: x =[A] z" +unfolding pathcomp_def by (routine add: transitivity assms) lemma pathcomp_comp: assumes "A: U i" and "a: A" - shows "(refl a) \ (refl a) \ refl a" + shows "pathcomp A a a a (refl a) (refl a) \ refl a" unfolding pathcomp_def by (derive lems: assms) declare pathcomp_type [intro] - pathcomp_trans [intro] pathcomp_comp [comp] + +section \Higher groupoid structure of types\ + +schematic_goal pathcomp_idr: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p" +proof (path_ind x y p) + show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal pathcomp_idl: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p" +proof (path_ind x y p) + show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal pathcomp_invl: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)" +proof (path_ind x y p) + show + "\x. x: A \ refl(refl x): + pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal pathcomp_right_inv: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)" +proof (path_ind x y p) + show + "\x. x: A \ refl(refl x): + pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal inv_involutive: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: inv A y x (inv A x y p) =[x =[A] y] p" +proof (path_ind x y p) + show "\x. x: A \ refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal pathcomp_assoc: + fixes x y p + assumes "A: U i" "x: A" "y: A" "z: A" "w: A" and "p: x =[A] y" "q: y =[A] z" "r: z =[A] w" + shows + "?a: + pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] + pathcomp A x z w (pathcomp A x y z p q) r" +proof + fix x y p + end -- cgit v1.2.3