Method "quantify" converts product inhabitation into Pure universal statements. Also misc. cleanups.

1 files changed, 74 insertions, 21 deletions

diff --git a/Equal.thy b/Equal.thy
index 99ff268..1d8f6ae 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -1,52 +1,105 @@
-(*
-Title:  Equal.thy
-Author: Joshua Chen
-Date:   2018
+(********
+Isabelle/HoTT: Equality
+Feb 2019
 
-Equality type
-*)
+********)
 
 theory Equal
-imports HoTT_Base
+imports Prod HoTT_Methods
 
 begin
 
 
-section \<open>Basic definitions\<close>
+section \<open>Type definitions\<close>
 
 axiomatization
-  Equal    :: "[t, t, t] \<Rightarrow> t" and
-  refl     :: "t \<Rightarrow> t" and
-  indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t"  ("(1ind\<^sub>=)")
+  Eq    :: "[t, t, t] \<Rightarrow> t" and
+  refl  :: "t \<Rightarrow> t" and
+  indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"
 
 syntax
-  "_equal" :: "[t, t, t] \<Rightarrow> t"        ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
-  "_equal_ascii" :: "[t, t, t] \<Rightarrow> t"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
-
+  "_Eq" :: "[t, t, t] \<Rightarrow> t"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
 translations
-  "a =[A] b" \<rightleftharpoons> "CONST Equal A a b"
-  "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b"
+  "a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b"
 
 axiomatization where
-  Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i" and
+  Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =[A] b: U i" and
 
-  Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a" and
+  Equal_intro: "a: A \<Longrightarrow> (refl a): a =[A] a" and
 
   Equal_elim: "\<lbrakk>
-    p: x =\<^sub>A y;
+    p: x =[A] y;
     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 =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= 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 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 =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= 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 (refl a) \<equiv> f a"
 
 lemmas Equal_form [form]
 lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim
 lemmas Equal_comp [comp]
 
 
+section \<open>Path induction\<close>
+
+text \<open>We set up rudimentary automation of path induction:\<close>
+
+method path_ind for x y p :: t =
+  (rule Equal_elim[where ?x=x and ?y=y and ?p=p]; (fact | assumption)?)
+
+
+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"
+
+lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A 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"
+unfolding inv_def by derive
+
+declare
+  inv_type [intro]
+  inv_comp [comp]
+
+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)
+  fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" .
+qed (routine add: assms)
+
+
+syntax "_pathcomp" :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 110)
+translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q"
+
+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)
+
+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)
+
+lemma pathcomp_comp:
+  assumes "A: U i" and "a: A"
+  shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
+unfolding pathcomp_def by (derive lems: assms)
+
+declare
+  pathcomp_type [intro]
+  pathcomp_trans [intro]
+  pathcomp_comp [comp]
+
 end