From ce2f78d04b78f7179729a1f5c792b1dc2ff3e1a8 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 23 Feb 2019 01:42:18 +0100
Subject: rewrite associativity proof

---
 Eq.thy | 33 ++++++++++++++++-----------------
 1 file changed, 16 insertions(+), 17 deletions(-)

(limited to 'Eq.thy')

diff --git a/Eq.thy b/Eq.thy
index 7783682..e89aeea 100644
--- a/Eq.thy
+++ b/Eq.thy
@@ -18,7 +18,7 @@ axiomatization
   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)
+  "_Eq" :: "[t, t, t] \<Rightarrow> t"  ("(2_ =[_]/ _)" [101, 0, 101] 100)
 translations
   "a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b"
 
@@ -191,14 +191,13 @@ In particular, changing the order causes unification to fail in the path inducti
 It seems to be good practice to order the variables in the order over which we will path-induct.
 \<close>
 
-declare[[pretty_pathcomp=false]]
-
 schematic_goal pathcomp_assoc:
   assumes "A: U i"
   shows 
     "?a: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>q: y =[A] z. \<Prod>w: A. \<Prod>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"
+
   apply (quantify 3)
   apply (path_ind' "{x, y, p}
     \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(r: z =[A] w).
@@ -213,20 +212,20 @@ schematic_goal pathcomp_assoc:
   apply (path_ind' "{xb, w, r}
     Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w]
       Eq.pathcomp A xb xb w (Eq.pathcomp A xb xb xb (refl xb) (refl xb)) r")
-  
-  text \<open>And now the rest is routine.\<close>
-  
-  apply (derive; (rule assms|assumption)?)
-  apply (compute, rule assms, assumption)+
-  apply (elim Eq_intro, rule Eq_intro, assumption)
-  apply (compute, rule assms, assumption)+
-  apply (elim Eq_intro)
-  apply (compute, rule assms, assumption)+
-  apply (rule Eq_intro, elim Eq_intro)
-  apply (compute, rule assms, assumption)+
-  apply (rule Eq_intro, elim Eq_intro)
-  apply (derive lems: assms)
-done
+
+text \<open>The rest is now routine.\<close>
+
+proof
+  fix x assume *: "x: A"
+  show "pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)): x =[A] x"
+   and "pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x): x =[A] x"
+   and "pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x): x =[A] x"
+   and "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)"
+   and "refl(refl x): pathcomp A x x x (pathcomp A x x x (refl 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 (derive lems: assms)
 
 (* Possible todo:
    implement a custom version of schematic_goal/theorem that exports the derived proof term.
-- 
cgit v1.2.3