From 76ac8ed82317f3f62f26ecc88f412c61004bcffa Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 13:13:55 +0200
Subject: Reorganizing theories

---
 Proj.thy | 56 ++++++++++++++++++++------------------------------------
 1 file changed, 20 insertions(+), 36 deletions(-)

(limited to 'Proj.thy')

diff --git a/Proj.thy b/Proj.thy
index 74c561c..f272224 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -1,62 +1,46 @@
-(*  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
+  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
   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+
+  fix x y assume asm: "x: A" "y: B x"
+  show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp)
 qed fact
 
 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
-- 
cgit v1.2.3


From 8e4ca285430c7bcdabbd4ea34da38e0770f4a832 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 17 Sep 2018 15:33:42 +0200
Subject: Tweak proof

---
 Proj.thy | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

(limited to 'Proj.thy')

diff --git a/Proj.thy b/Proj.thy
index f272224..e76e8d3 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -7,10 +7,7 @@ Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent
 *)
 
 theory Proj
-imports
-  HoTT_Methods
-  Prod
-  Sum
+imports HoTT_Methods Prod Sum
 
 begin
 
@@ -28,12 +25,12 @@ unfolding fst_def by compute (derive lems: assms)
 
 lemma snd_type:
   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
-  show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> B (fst p): U i" by (derive lems: assms fst_type)
-  
+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 fact
+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"
-- 
cgit v1.2.3