From 6389f18fd17e4333aba3fcdcc9ed2810d4cb1da5 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 9 Jul 2018 11:17:50 +0200
Subject: Pre-universe implementation commit

---
 EqualProps.thy | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

(limited to 'EqualProps.thy')

diff --git a/EqualProps.thy b/EqualProps.thy
index cb267c6..43b4eb5 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -19,16 +19,14 @@ definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
   where "inv[A,x,y] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) x y p"
 
 
-lemma inv_type:
-  assumes "p : x =\<^sub>A y"
-  shows "inv[A,x,y]`p : y =\<^sub>A x"
+lemma inv_type: assumes "x : A" and "y : A" shows "inv[A,x,y] : x =\<^sub>A y \<rightarrow> y =\<^sub>A x"
   unfolding inv_def
   by (derive lems: assms)
-      
 
-lemma inv_comp:
-  assumes "a : A"
-  shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
+corollary assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x"
+  by (derive lems: inv_type assms)
+
+lemma inv_comp: assumes "a : A" shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
   unfolding inv_def by (simplify lems: assms)
 
 
@@ -43,27 +41,24 @@ definition rcompose :: "Term \<Rightarrow> Term"  ("(1rcompose[_])")
     x y p"
 
 
-text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>."
+text "``Natural'' composition function, of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>."
 
 abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
   where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:(x =\<^sub>A y). \<^bold>\<lambda>q:(y =\<^sub>A z). rcompose[A]`x`y`p`z`q"
 
 
 lemma compose_type:
-  assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z"
-  shows "compose[A,x,y,z]`p`q : x =\<^sub>A z"
+assumes "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 : A"
-  shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
+lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)"
   unfolding rcompose_def
   by (simplify lems: assms)
 
 
-lemmas Equal_simps [intro] = inv_comp compose_comp
+lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp
+lemmas EqualProps_comps [comp] = inv_comp compose_comp
 
 
 end
\ No newline at end of file
-- 
cgit v1.2.3