Library snapshot. Methods written, everything nicely organized.

7 files changed, 45 insertions, 20 deletions

diff --git a/Equal.thy b/Equal.thy
index 7732dd0..18a4207 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -9,6 +9,7 @@ theory Equal
   imports HoTT_Base
 begin
 
+
 axiomatization
   Equal :: "[Term, Term, Term] \<Rightarrow> Term" and
   refl :: "Term \<Rightarrow> Term"  ("(refl'(_'))" 1000) and
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
diff --git a/HoTT.thy b/HoTT.thy
index 42796c1..948dd14 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -5,7 +5,6 @@ Load all the component modules for the HoTT logic.
 *)
 
 theory HoTT
-
 imports
 
 (* Basic theories *)
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index cfced79..60e5167 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -15,7 +15,7 @@ section \<open>Setup\<close>
 text "Named theorems to be used by proof methods later (see HoTT_Methods.thy).
 
 \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while
-\<open>comp\<close> declares computation rules used when simplifying function application."
+\<open>comp\<close> declares computation rules, which are used by the simplification method as equational rewrite rules."
 
 named_theorems wellform
 named_theorems comp
diff --git a/Prod.thy b/Prod.thy
index 544a719..bf4e4e9 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -9,6 +9,7 @@ theory Prod
   imports HoTT_Base
 begin
 
+
 axiomatization
   Prod :: "[Term, Typefam] \<Rightarrow> Term" and
   lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
diff --git a/Proj.thy b/Proj.thy
index 7957669..805a624 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -12,6 +12,7 @@ theory Proj
     Sum
 begin
 
+
 consts
   fst :: "[Term, 'a] \<Rightarrow> Term"  ("(1fst[/_,/ _])")
   snd :: "[Term, 'a] \<Rightarrow> Term"  ("(1snd[/_,/ _])")
@@ -49,13 +50,17 @@ text "Typing judgments and computation rules for the dependent and non-dependent
 lemma fst_dep_type:
   assumes "p : \<Sum>x:A. B x"
   shows "fst[A,B]`p : A"
-  by (derive lems: assms unfolds: fst_dep_def)
+  unfolding fst_dep_def
+  by (derive lems: assms)
 
 
 lemma fst_dep_comp:
   assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
   shows "fst[A,B]`(a,b) \<equiv> a"
+  unfolding fst_dep_def
+  by (simplify lems: assms)
 
+\<comment> \<open> (* Old proof *)
 proof -
   have "fst[A,B]`(a,b) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)"
     by (derive lems: assms unfolds: fst_dep_def)
@@ -65,8 +70,9 @@ proof -
   
   finally show "fst[A,B]`(a,b) \<equiv> a" .
 qed
+\<close>
 
-
+\<comment> \<open> (* Old lemma *)
 text "In proving results about the second dependent projection function we often use the following lemma."
 
 lemma lem:
@@ -77,12 +83,16 @@ proof -
   have "fst[A,B]`(x,y) \<equiv> x" using assms by (rule fst_dep_comp)
   then show "y : B (fst[A,B]`(x,y))" using assms by simp
 qed
+\<close>
 
 
 lemma snd_dep_type:
   assumes "p : \<Sum>x:A. B x"
   shows "snd[A,B]`p : B (fst[A,B]`p)"
+  unfolding fst_dep_def snd_dep_def
+  by (simplify lems: assms)
 
+\<comment> \<open> (* Old proof *)
 proof (derive lems: assms unfolds: snd_dep_def)
   show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def)
   
@@ -90,12 +100,16 @@ proof (derive lems: assms unfolds: snd_dep_def)
   have "B: A \<rightarrow> U" by (wellformed jdgmt: assms)
   then show "y : B (fst[A, B]`(x,y))" using asm by (rule lem)
 qed (assumption | rule assms)+
+\<close>
 
 
 lemma snd_dep_comp:
   assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
   shows "snd[A,B]`(a,b) \<equiv> b"
+  unfolding snd_dep_def fst_dep_def
+  by (simplify lems: assms)
 
+\<comment> \<open> (* Old proof *)
 proof -
   have "snd[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b)"
   proof (derive lems: assms unfolds: snd_dep_def)
@@ -115,6 +129,7 @@ proof -
 
   finally show "snd[A,B]`(a,b) \<equiv> b" .
 qed
+\<close>
 
 
 text "For non-dependent projection functions:"
@@ -122,13 +137,17 @@ text "For non-dependent projection functions:"
 lemma fst_nondep_type:
   assumes "p : A \<times> B"
   shows "fst[A,B]`p : A"
-  by (derive lems: assms unfolds: fst_nondep_def)
+  unfolding fst_nondep_def 
+  by (derive lems: assms)
 
 
 lemma fst_nondep_comp:
   assumes "a : A" and "b : B"
   shows "fst[A,B]`(a,b) \<equiv> a"
+  unfolding fst_nondep_def
+  by (simplify lems: assms)
 
+\<comment> \<open> (* Old proof *)
 proof -
   have "fst[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)"
     by (derive lems: assms unfolds: fst_nondep_def)
@@ -138,12 +157,16 @@ proof -
 
   finally show "fst[A,B]`(a,b) \<equiv> a" .
 qed
+\<close>
 
 
 lemma snd_nondep_type:
   assumes "p : A \<times> B"
   shows "snd[A,B]`p : B"
+  unfolding snd_nondep_def
+  by (derive lems: assms)
 
+\<comment> \<open> (* Old proof *)
 proof
   show "snd[A,B] : A \<times> B \<rightarrow> B"
   proof (derive unfolds: snd_nondep_def)
@@ -151,11 +174,16 @@ proof
     show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B" by (derive lems: asm)
   qed (wellformed jdgmt: assms)+
 qed (rule assms)
+\<close>
 
 
 lemma snd_nondep_comp:
   assumes "a : A" and "b : B"
   shows "snd[A,B]`(a,b) \<equiv> b"
+  unfolding snd_nondep_def
+  by (simplify lems: assms)
+
+\<comment> \<open> (* Old proof *)
 proof -
   have "snd[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b)"
     by (derive lems: assms unfolds: snd_nondep_def)
@@ -165,6 +193,7 @@ proof -
 
   finally show "snd[A,B]`(a,b) \<equiv> b" .
 qed
+\<close>
 
 
 end
\ No newline at end of file
diff --git a/Sum.thy b/Sum.thy
index fe38960..46bb022 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -9,6 +9,7 @@ theory Sum
   imports HoTT_Base
 begin
 
+
 axiomatization
   Sum :: "[Term, Typefam] \<Rightarrow> Term" and
   pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
@@ -54,7 +55,7 @@ lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
 lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2
 lemmas Sum_comps [comp] = Sum_comp
 
-\<comment> \<open>Nondependent pair\<close>
+text "Nondependent pair."
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
   where "A \<times> B \<equiv> \<Sum>_:A. B"