From decb363a30a30c1875bf4b93bc544c28edf3149e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 7 Jul 2018 23:03:33 +0200
Subject: Library snapshot. Methods written, everything nicely organized.

---
 EqualProps.thy | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

(limited to 'EqualProps.thy')

diff --git a/EqualProps.thy b/EqualProps.thy
index 2807587..cb267c6 100644
--- a/EqualProps.thy
+++ b/EqualProps.thy
@@ -22,22 +22,14 @@ definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
 lemma inv_type:
   assumes "p : x =\<^sub>A y"
   shows "inv[A,x,y]`p : y =\<^sub>A x"
-  by (derive lems: assms unfolds: inv_def)
+  unfolding inv_def
+  by (derive lems: assms)
       
 
 lemma inv_comp:
   assumes "a : A"
   shows "inv[A,a,a]`refl(a) \<equiv> refl(a)"
-
-proof -
-  have "inv[A,a,a]`refl(a) \<equiv> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a)"
-    by (derive lems: assms unfolds: inv_def)
-
-  also have "indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)"
-    by (simple lems: assms)
-
-  finally show "inv[A,a,a]`refl(a) \<equiv> refl(a)" .
-qed
+  unfolding inv_def by (simplify lems: assms)
 
 
 section \<open>Transitivity / Path composition\<close>
@@ -50,6 +42,7 @@ definition rcompose :: "Term \<Rightarrow> Term"  ("(1rcompose[_])")
     (\<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"
 
+
 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>."
 
 abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
@@ -59,14 +52,15 @@ abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compo
 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"
-  by (derive lems: assms unfolds: rcompose_def)
+  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)"
-
-sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close>
+  unfolding rcompose_def
+  by (simplify lems: assms)
 
 
 lemmas Equal_simps [intro] = inv_comp compose_comp
-- 
cgit v1.2.3