Merge branch 'develop', ready for release 0.1.0

1 files changed, 20 insertions, 39 deletions

diff --git a/Proj.thy b/Proj.thy
index 74c561c..e76e8d3 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -1,62 +1,43 @@
-(*  Title:  HoTT/Proj.thy
-    Author: Josh Chen
+(*
+Title:  Proj.thy
+Author: Joshua Chen
+Date:   2018
 
 Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type.
 *)
 
 theory Proj
-  imports
-    HoTT_Methods
-    Prod
-    Sum
-begin
+imports HoTT_Methods Prod Sum
 
+begin
 
-definition fst :: "Term \<Rightarrow> Term" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p"
-definition snd :: "Term \<Rightarrow> Term" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p"
 
-text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
+definition fst :: "t \<Rightarrow> t" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p"
+definition snd :: "t \<Rightarrow> t" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p"
 
 lemma fst_type:
-  assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "fst p: A"
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "fst p: A"
 unfolding fst_def by (derive lems: assms)
 
 lemma fst_comp:
   assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "fst <a,b> \<equiv> a"
-unfolding fst_def
-proof compute
-  show "a: A" and "b: B a" by fact+
-qed (routine lems: assms)+
+unfolding fst_def by compute (derive lems: assms)
 
 lemma snd_type:
-  assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)"
-unfolding snd_def
-proof
-  show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> B (fst p): U i" by (derive lems: assms fst_type)
-  
-  fix x y
-  assume asm: "x: A" "y: B x"
-  show "y: B (fst <x,y>)"
-  proof (subst fst_comp)
-    show "A: U i" by (wellformed lems: assms(1))
-    show "\<And>x. x: A \<Longrightarrow> B x: U i" by (wellformed lems: assms(1))
-  qed fact+
-qed fact
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)"
+unfolding snd_def proof (derive lems: assms)
+  show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> fst p: A" using assms(1-2) by (rule fst_type)
+
+  fix x y assume asm: "x: A" "y: B x"
+  show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp)
+qed
 
 lemma snd_comp:
   assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "snd <a,b> \<equiv> b"
-unfolding snd_def
-proof compute
-  show "\<And>x y. y: B x \<Longrightarrow> y: B x" .
-  show "a: A" by fact
-  show "b: B a" by fact
-qed (routine lems: assms)
-
-
-text "Rule attribute declarations:"
+unfolding snd_def by (derive lems: assms)
 
-lemmas Proj_type [intro] = fst_type snd_type
-lemmas Proj_comp [comp] = fst_comp snd_comp
+lemmas Proj_types [intro] = fst_type snd_type
+lemmas Proj_comps [comp] = fst_comp snd_comp
 
 
 end