From e6473c383b479610cee4c0119e5811a12a938cf9 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 14 Aug 2018 17:43:03 +0200
Subject: Well-formation rules are back in the methods; new theory synthesizing
 the natural number predecessor function.

---
 Proj.thy | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'Proj.thy')

diff --git a/Proj.thy b/Proj.thy
index aa7e8ec..5c05eb2 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -18,12 +18,10 @@ axiomatization snd :: "Term \<Rightarrow> Term" where snd_def: "snd \<equiv> \<l
 
 text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
 
-
 lemma fst_type:
   assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
 unfolding fst_def by (derive lem: 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
@@ -31,7 +29,6 @@ proof
   show "a: A" and "b: B(a)" by fact+
 qed (rule 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
@@ -47,7 +44,6 @@ proof
   qed fact+
 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
@@ -58,6 +54,8 @@ proof
 qed (simple lem: assms)
 
 
+text "Rule declarations:"
+
 lemmas Proj_types [intro] = fst_type snd_type
 lemmas Proj_comps [intro] = fst_comp snd_comp
 
-- 
cgit v1.2.3