From 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 11 Sep 2018 08:59:16 +0200
Subject: Go back to higher-order application notation

---
 EqualProps.thy | 85 +++++++++++++++++++++++++++++-----------------------------
 1 file changed, 43 insertions(+), 42 deletions(-)

(limited to 'EqualProps.thy')

diff --git a/EqualProps.thy b/EqualProps.thy
index c114d37..708eb33 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -14,7 +14,7 @@ begin
 
 section \<open>Symmetry / Path inverse\<close>
 
-definition inv :: "Term \<Rightarrow> Term"  ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl(x)) p"
+definition inv :: "Term \<Rightarrow> Term"  ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p"
 
 text "
   In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use.
@@ -22,7 +22,7 @@ text "
 "
 
 lemma inv_type:
-  assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x"
+  assumes "A : U i" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x"
 unfolding inv_def
 by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms)
   \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close>
@@ -33,7 +33,7 @@ text "
 "
 
 lemma inv_comp:
-  assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)"
+  assumes "A : U i " and "a : A" shows "(refl a)\<inverse> \<equiv> refl a"
 unfolding inv_def
 proof compute
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
@@ -46,14 +46,14 @@ text "
   Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>.
 "
 
-definition rpathcomp :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. refl(x)) q) p"
+definition rpathcomp :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
 
 text "
   More complicated proofs---the nested path inductions require more explicit step-by-step rule applications:
 "
 
 lemma rpathcomp_type:
-  assumes "A: U(i)"
+  assumes "A: U i"
   shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
 unfolding rpathcomp_def
 proof
@@ -81,7 +81,7 @@ proof
 qed fact
 
 corollary
-  assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
+  assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
   shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z"
   by (routine lems: assms rpathcomp_type)
 
@@ -90,11 +90,11 @@ text "
 "
 
 lemma rpathcomp_comp:
-  assumes "A: U(i)" and "a: A"
-  shows "rpathcomp`a`a`refl(a)`a`refl(a) \<equiv> refl(a)"
+  assumes "A: U i" and "a: A"
+  shows "rpathcomp`a`a`(refl a)`a`(refl a) \<equiv> refl a"
 unfolding rpathcomp_def
 proof compute
-  { fix x assume 1: "x: A"
+  fix x assume 1: "x: A"
   show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
   proof
     fix y assume 2: "y: A"
@@ -114,11 +114,11 @@ proof compute
         qed (rule assms)
       qed (routine lems: assms 1 2 3)
     qed (routine lems: assms 1 2)
-  qed (rule assms) }
+  qed (rule assms)
 
-  show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \<equiv> refl(a)"
+  next show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \<equiv> refl a"
   proof compute
-    { fix y assume 1: "y: A"
+    fix y assume 1: "y: A"
     show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)"
     proof
       fix p assume 2: "p: a =\<^sub>A y"
@@ -135,11 +135,11 @@ proof compute
           qed (routine lems: assms 3 4)
         qed fact
       qed (routine lems: assms 1 2)
-    qed (routine lems: assms 1) }
+    qed (routine lems: assms 1)
     
-    show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \<equiv> refl(a)"
+    next show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \<equiv> refl a"
     proof compute
-      { fix p assume 1: "p: a =\<^sub>A a"
+      fix p assume 1: "p: a =\<^sub>A a"
       show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A z \<rightarrow> a =\<^sub>A z"
       proof (rule Equal_elim[where ?x=a and ?y=a])
         fix u assume 2: "u: A"
@@ -152,11 +152,11 @@ proof compute
             by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3)
           qed (routine lems: assms 2 3)
         qed fact
-      qed (routine lems: assms 1) }
+      qed (routine lems: assms 1)
       
-      show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \<equiv> refl(a)"
+      next show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \<equiv> refl a"
       proof compute
-        { fix u assume 1: "u: A"
+        fix u assume 1: "u: A"
         show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z"
         proof
           fix z assume 2: "z: A"
@@ -165,22 +165,22 @@ proof compute
             show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z"
             by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2)
           qed (routine lems: assms 1 2)
-        qed fact }
+        qed fact
         
-        show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`refl(a) \<equiv> refl(a)"
+        next show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`(refl a) \<equiv> refl a"
         proof compute
-          { fix a assume 1: "a: A"
+          fix a assume 1: "a: A"
           show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a"
           proof
             show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a"
             by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1)
-          qed (routine lems: assms 1) }
+          qed (routine lems: assms 1)
           
-          show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`refl(a) \<equiv> refl(a)"
+          next show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`(refl a) \<equiv> refl a"
           proof compute
             show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a"
             by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms)
-            show "ind\<^sub>= refl (refl(a)) \<equiv> refl(a)"
+            show "ind\<^sub>= refl (refl a) \<equiv> refl a"
             proof compute
               show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" ..
             qed (routine lems: assms)
@@ -196,23 +196,23 @@ text "The raw object lambda term is cumbersome to use, so we define a simpler co
 
 axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 120) where
   pathcomp_def: "\<lbrakk>
-    A: U(i);
+    A: U i;
     x: A; y: A; z: A;
     p: x =\<^sub>A y; q: y =\<^sub>A z
   \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q"
 
 
 lemma pathcomp_type:
-  assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
+  assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
   shows "p \<bullet> q: x =\<^sub>A z"
 
 proof (subst pathcomp_def)
-  show "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+
+  show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+
 qed (routine lems: assms rpathcomp_type)
 
 
 lemma pathcomp_comp:
-  assumes "A : U(i)" and "a : A" shows "refl(a) \<bullet> refl(a) \<equiv> refl(a)"
+  assumes "A : U i" and "a : A" shows "(refl a) \<bullet> (refl a) \<equiv> refl a"
 by (subst pathcomp_def) (routine lems: assms rpathcomp_comp)
 
 
@@ -223,44 +223,45 @@ lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp
 section \<open>Higher groupoid structure of types\<close>
 
 lemma
-  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
   shows
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> refl(y)" and
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] refl(x) \<bullet> p"
+    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> (refl y)" and
+    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \<bullet> p"
 
 proof -
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> refl(y)"
+  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> (refl y)"
   by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
 
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] refl x \<bullet> p"
+  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] (refl x) \<bullet> p"
   by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
 qed
 
 
 lemma
-  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
   shows
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] refl(y)" and
-    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] refl(x)"
+    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" and
+    "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)"
 
 proof -
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] refl(y)"
+  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)"
   by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
 
-  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] refl(x)"
+  show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)"
   by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+
 qed
 
 
 lemma
-  assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y"
+  assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y"
   shows "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse>\<inverse> =[x =\<^sub>A y] p"
 by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)
 
+text "Next we construct a proof term of associativity of path composition."
 
 schematic_goal
   assumes
-    "A: U(i)"
+    "A: U i"
     "x: A" "y: A" "z: A" "w: A"
     "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w"
   shows
@@ -268,8 +269,8 @@ schematic_goal
 
 apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y])
 apply (rule assms)+
-apply (subst pathcomp_comp)
-
+\<comment> \<open>Continue by substituting \<open>refl x \<bullet> q = q\<close> etc.\<close>
+sorry
 
 
 end
-- 
cgit v1.2.3

