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

---
 Proj.thy | 41 ++++++++++++++++-------------------------
 1 file changed, 16 insertions(+), 25 deletions(-)

(limited to 'Proj.thy')

diff --git a/Proj.thy b/Proj.thy
index 805a624..31deaf9 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -47,16 +47,12 @@ section \<open>Properties\<close>
 
 text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
 
-lemma fst_dep_type:
-  assumes "p : \<Sum>x:A. B x"
-  shows "fst[A,B]`p : A"
+lemma fst_dep_type: assumes "p : \<Sum>x:A. B x" shows "fst[A,B]`p : A"
   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"
+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)
 
@@ -86,9 +82,7 @@ qed
 \<close>
 
 
-lemma snd_dep_type:
-  assumes "p : \<Sum>x:A. B x"
-  shows "snd[A,B]`p : B (fst[A,B]`p)"
+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)
 
@@ -103,9 +97,7 @@ 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"
+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)
 
@@ -132,18 +124,14 @@ qed
 \<close>
 
 
-text "For non-dependent projection functions:"
+text "Nondependent projections:"
 
-lemma fst_nondep_type:
-  assumes "p : A \<times> B"
-  shows "fst[A,B]`p : A"
+lemma fst_nondep_type: assumes "p : A \<times> B" shows "fst[A,B]`p : A"
   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"
+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)
 
@@ -160,9 +148,7 @@ qed
 \<close>
 
 
-lemma snd_nondep_type:
-  assumes "p : A \<times> B"
-  shows "snd[A,B]`p : B"
+lemma snd_nondep_type: assumes "p : A \<times> B" shows "snd[A,B]`p : B"
   unfolding snd_nondep_def
   by (derive lems: assms)
 
@@ -177,9 +163,7 @@ qed (rule assms)
 \<close>
 
 
-lemma snd_nondep_comp:
-  assumes "a : A" and "b : B"
-  shows "snd[A,B]`(a,b) \<equiv> b"
+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)
 
@@ -196,4 +180,11 @@ qed
 \<close>
 
 
+lemmas Proj_rules [intro] =
+  fst_dep_type snd_dep_type fst_nondep_type snd_nondep_type
+  fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
+
+lemmas Proj_comps [comp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
+
+
 end
\ No newline at end of file
-- 
cgit v1.2.3