diff options
| -rw-r--r-- | Equal.thy | 124 |
1 files changed, 104 insertions, 20 deletions
@@ -15,7 +15,7 @@ section \<open>Type definitions\<close> axiomatization Eq :: "[t, t, t] \<Rightarrow> t" and refl :: "t \<Rightarrow> t" and - indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" + indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t, t, t] \<Rightarrow> t" syntax "_Eq" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) @@ -32,12 +32,12 @@ axiomatization where x: A; y: A; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f p : C x y p" and + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f x y p : C x y p" and Equal_comp: "\<lbrakk> a: A; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f (refl a) \<equiv> f a" + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f a a (refl a) \<equiv> f a" lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim @@ -56,13 +56,29 @@ section \<open>Properties of equality\<close> subsection \<open>Symmetry (path inverse)\<close> -definition inv :: "[t, t] \<Rightarrow> t" -where "inv A p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) p" +definition inv :: "[t, t, t, t] \<Rightarrow> t" +where "inv A x y p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) x y p" -lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A p: y =[A] x" +syntax "_inv" :: "t \<Rightarrow> t" ("~_" [1000]) + +text \<open>Pretty-printing switch for path inverse:\<close> + +ML \<open>val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\<close> + +print_translation \<open> +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 +\<close> + +lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A x y p: y =[A] x" unfolding inv_def by derive -lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A (refl a) \<equiv> refl a" +lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A a a (refl a) \<equiv> refl a" unfolding inv_def by derive declare @@ -74,32 +90,100 @@ subsection \<open>Transitivity (path composition)\<close> schematic_goal transitivity: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z" -proof (path_ind x y p, quantify 2) +proof (path_ind x y p, quantify_all) fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" . qed (routine add: assms) +definition pathcomp :: "[t, t, t, t, t, t] \<Rightarrow> t" +where + "pathcomp A x y z p q \<equiv> + (indEq (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z) (\<lambda>x. \<lambda>y: A. id (x =[A] y)) x y p)`z`q" -syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 110) -translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q" +syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "*" 110) -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" - shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)" -unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms) +text \<open>Pretty-printing switch for path composition:\<close> + +ML \<open>val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\<close> -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 \<bullet> q: x =\<^sub>A z" -by (routine add: assms pathcomp_type) +print_translation \<open> +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 +\<close> + +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) \<bullet> (refl a) \<equiv> refl a" + shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a" unfolding pathcomp_def by (derive lems: assms) declare pathcomp_type [intro] - pathcomp_trans [intro] pathcomp_comp [comp] + +section \<open>Higher groupoid structure of types\<close> + +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 "\<And>x. x: A \<Longrightarrow> 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 "\<And>x. x: A \<Longrightarrow> 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 + "\<And>x. x: A \<Longrightarrow> 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 + "\<And>x. x: A \<Longrightarrow> 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 "\<And>x. x: A \<Longrightarrow> 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 |