From 57d183c7955fb54b3eb6dd431f5aec338131266b Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 22 Feb 2019 23:45:50 +0100 Subject: Cleanups and reorganization --- Equal.thy | 219 -------------------------------------------------------------- 1 file changed, 219 deletions(-) delete mode 100644 Equal.thy (limited to 'Equal.thy') diff --git a/Equal.thy b/Equal.thy deleted file mode 100644 index 17c1c99..0000000 --- a/Equal.thy +++ /dev/null @@ -1,219 +0,0 @@ -(******** -Isabelle/HoTT: Equality -Feb 2019 - -********) - -theory Equal -imports Prod HoTT_Methods - -begin - - -section \Type definitions\ - -axiomatization - Eq :: "[t, t, t] \ t" and - refl :: "t \ t" and - indEq :: "[[t, t, t] \ t, t \ t, t, t, t] \ t" - -syntax - "_Eq" :: "[t, t, t] \ t" ("(3_ =[_]/ _)" [101, 0, 101] 100) -translations - "a =[A] b" \ "(CONST Eq) A a b" - -axiomatization where - Eq_form: "\A: U i; a: A; b: A\ \ a =[A] b: U i" and - - Eq_intro: "a: A \ (refl a): a =[A] a" and - - Eq_elim: "\ - p: x =[A] y; - a: A; - b: 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 a b p : C a b p" and - - Eq_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 a a (refl a) \ f a" - -lemmas Eq_form [form] -lemmas Eq_routine [intro] = Eq_form Eq_intro Eq_elim -lemmas Eq_comp [comp] - - -section \Path induction\ - -text \We set up rudimentary automation of path induction:\ - -method path_ind for a b p :: t = - (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (fact | assumption)?) - - -section \Properties of equality\ - -subsection \Symmetry (path inverse)\ - -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" - -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 a a (refl a) \ refl a" -unfolding inv_def by derive - -declare - inv_type [intro] - inv_comp [comp] - -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_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) - -text \Pretty-printing switch for path composition:\ - -ML \val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\ - -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_cmp: - assumes "A: U i" and "a: A" - shows "pathcomp A a a a (refl a) (refl a) \ refl a" -unfolding pathcomp_def by (derive lems: assms) - -lemmas pathcomp_type [intro] -lemmas pathcomp_comp [comp] = pathcomp_cmp - - -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_invr: - 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 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 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) - -declare[[pretty_pathcomp=false]] - -schematic_goal pathcomp_assoc: - assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x =[A] y" - shows - "?a: \q: y =[A] z. \r: z =[A] w. - 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 (path_ind x y p) - oops - schematic_goal l: - assumes "A: U i" "x: A" "z: A" "w: A" "q: x =[A] z" - shows - "?a: \r: z =[A] w. pathcomp A x x w (refl x) (pathcomp A y z w q r) =[x =[A] w] - pathcomp A x z w (pathcomp A x x z (refl x) q) r" - proof (path_ind x z q) - oops - schematic_goal l': - assumes "A: U i" "x: A" "w: A" "r: x =[A] w" - shows - "?a: pathcomp A x x w (refl x) (pathcomp A x x w (refl x) r) =[x =[A] w] - pathcomp A x x w (pathcomp A x x x (refl x) (refl x)) r" - proof (path_ind x w r) - show "\x. x: A \ refl(refl x): - pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x] - pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)" - by (derive lems: assms) - qed (routine add: assms) - -(* Possible todo: - implement a custom version of schematic_goal/theorem that exports the derived proof term. -*) - -definition l'_prftm :: "[t, t, t, t] \ t" -where "l'_prftm A x w r\ - indEq - (\a b c. pathcomp A a a b (refl a) (pathcomp A a a b (refl a) c) =[a =[A] b] - pathcomp A a a b (pathcomp A a a a (refl a) (refl a)) c) - (\x. refl (refl x)) x w r" - - -end -- cgit v1.2.3