rcompose done

1 files changed, 60 insertions, 18 deletions

diff --git a/EqualProps.thy b/EqualProps.thy
index 9d23a99..d645fb6 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -15,20 +15,20 @@ begin
 
 section \<open>Symmetry / Path inverse\<close>
 
-definition inv :: "[Term, Term] \<Rightarrow> (Term \<Rightarrow> Term)"  ("(1inv[_,/ _])")
-  where "inv[x,y] \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) x y p"
+axiomatization inv :: "Term \<Rightarrow> Term"  ("_\<inverse>" [1000] 1000)
+  where inv_def: "inv \<equiv> \<lambda>p. ind\<^sub>= (\<lambda>x. refl(x)) p"
 
 
 lemma inv_type:
-  assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "inv[x,y](p): 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
-proof
+proof (rule Equal_elim[where ?x=x and ?y=y])  \<comment> \<open>Path induction\<close>
   show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> y =\<^sub>A x: U(i)" using assms(1) ..
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
 qed (fact assms)+
 
 
-lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) \<equiv> refl(a)"
+lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\<inverse> \<equiv> refl(a)"
 unfolding inv_def
 proof
   show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
@@ -38,24 +38,66 @@ qed (fact assms)
 
 section \<open>Transitivity / Path composition\<close>
 
-text "``Raw'' composition function, of type \<open>\<Prod>x,y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close>."
+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>.
+"
+
+axiomatization rcompose :: Term where
+  rcompose_def: "rcompose \<equiv> \<^bold>\<lambda>x y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= (\<lambda>x. refl(x)) q) p"
+
 
-definition rcompose :: "Term \<Rightarrow> Term"  ("(1rcompose[_])")
-  where "rcompose[A] \<equiv> \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:A. \<^bold>\<lambda>p:(x =\<^sub>A y). indEqual[A]
-    (\<lambda>x y _. \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)
-    (\<lambda>x. \<^bold>\<lambda>z:A. \<^bold>\<lambda>p:(x =\<^sub>A z). indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<lambda>x. refl(x)) x z p)
-    x y p"
+lemma rcompose_type:
+  assumes "A: U(i)"
+  shows "rcompose: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+unfolding rcompose_def
+proof
+  show "\<And>x. x: A \<Longrightarrow>
+    \<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+  proof
+    show "\<And>x y. \<lbrakk>x: A ; y: A\<rbrakk> \<Longrightarrow>
+       \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
+    proof
+      { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y"
+      show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z p. ind\<^sub>= refl p) p: \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z"
+      proof (rule Equal_elim[where ?x=x and ?y=y])
+        show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)"
+        proof
+          show "\<And>x y z. \<lbrakk>x: A; y: A; z: A\<rbrakk> \<Longrightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z: U(i)"
+            by (rule Prod_form Equal_form assms | assumption)+
+        qed (rule assms)
+
+        show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>z p. ind\<^sub>= refl p: \<Prod>z:A. x =\<^sub>A z \<rightarrow> x =\<^sub>A z"
+        proof
+          show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>p. ind\<^sub>= refl p: x =\<^sub>A z \<rightarrow> x =\<^sub>A z"
+          proof
+            { fix x z p assume asm: "x: A" "z: A" "p: x =\<^sub>A z"
+            show "ind\<^sub>= refl p: x =[A] z"
+            proof (rule Equal_elim[where ?x=x and ?y=z])
+              show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms)
+              show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" ..
+            qed (fact asm)+ }
+            show "\<And>x z. \<lbrakk>x: A; z: A\<rbrakk> \<Longrightarrow> x =\<^sub>A z: U(i)" by standard (rule assms)
+          qed
+        qed (rule assms)
+      qed (rule asm)+ }
+      show "\<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> x =\<^sub>A y: U(i)" by standard (rule assms)
+    qed
+  qed (rule assms)
+qed (fact assms)
 
+corollary
+  assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z"
+  shows "rcompose`x`y`p`z`q: x =\<^sub>A z"
+  by standard+ (rule rcompose_type assms)+
 
-definition compose :: "[Term, Term, Term] \<Rightarrow> [Term, Term] \<Rightarrow> Term"  ("(1compose[ _,/ _,/ _])")
-  where "compose[x,y,z] \<equiv> \<lambda>p."
 
+axiomatization compose :: "[Term, Term] \<Rightarrow> Term"  (infixl "\<bullet>" 60) where
+  compose_comp: "\<lbrakk>
+    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> rcompose`x`y`p`z`q"
 
-lemma compose_type:
-  assumes "A : U(i)" and "x : A" and "y : A" and "z : A"
-  shows "compose[A,x,y,z] : x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z"
-  unfolding rcompose_def
-  by (derive lems: assms)
 
 lemma compose_comp:
   assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"