Finished proofs of projections

2 files changed, 77 insertions, 21 deletions

diff --git a/Prod.thy b/Prod.thy
index 7facc27..5f0d272 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -64,7 +64,7 @@ lemmas Prod_form_conds [elim] = Prod_form_cond1 Prod_form_cond2
 text "Nondependent functions are a special case."
 
 abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 40)
-  where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"
+  where "A \<rightarrow> B \<equiv> \<Prod>_:A. B"  
 
 
 end
\ No newline at end of file
diff --git a/Proj.thy b/Proj.thy
index 22feecb..c4703d7 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -118,8 +118,7 @@ proof
       fix p assume *: "p : \<Sum>x:A. B x"
       have **: "B: A \<rightarrow> U" by (wellformed jdgmt: *)
       fix x y assume "x : A" and "y : B x"
-      note ** this
-      then show "y : B (fst[A,B]`(x,y))" by (rule lemma2)
+      with ** show "y : B (fst[A,B]`(x,y))" by (rule lemma2)
     qed
   qed (wellformed jdgmt: assms)
 qed (rule assms)
@@ -136,16 +135,16 @@ proof -
 
     fix p assume *: "p : \<Sum>x:A. B x"
     show "indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)"
-    proof (standard, elim snd_dep_welltyped)
-      show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> y : B (fst[A,B]`(x,y))" using assms
-        by (elim snd_dep_const_type)
+    proof (standard, elim lemma1)
+      fix x y assume "x : A" and "y : B x"
+      with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2)
     qed (rule *)
   qed
 
   also have "indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b) \<equiv> b"
-  proof (standard, elim snd_dep_welltyped)
-    show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> y : B (fst[A,B]`(x,y))" using assms
-      by (elim snd_dep_const_type)
+  proof (standard, elim lemma1)
+    fix x y assume "x : A" and "y : B x"
+    with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2)
   qed (rule assms)+
 
   finally show "snd[A,B]`(a,b) \<equiv> b" .
@@ -154,26 +153,83 @@ qed
 
 text "For non-dependent projection functions:"
 
-print_statement fst_dep_type
-print_statement fst_dep_type[where ?p = p and ?A = A and ?B = "\<lambda>_. B"]
+lemma fst_nondep_type:
+  assumes "p : A \<times> B"
+  shows "fst[A,B]`p : A"
 
+proof
+  show "fst[A,B] : A \<times> B \<rightarrow> A"
+  proof (unfold fst_nondep_def, standard)
+    fix q assume *: "q : A \<times> B"
+    show "indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) q : A"
+    proof
+      show "A : U" by (wellformed jdgmt: assms)
+    qed (assumption, rule *)
+  qed (wellformed jdgmt: assms)
+qed (rule assms)
 
-lemma fst_nondep_type: "p : A \<times> B \<Longrightarrow> fst[A,B]`p : A"
-by (rule fst_dep_type[where ?B = "\<lambda>_. B"])
-  
 
 lemma fst_nondep_comp:
   assumes "a : A" and "b : B"
   shows "fst[A,B]`(a,b) \<equiv> a"
-proof (unfold fst_nondep_def)
-  have "A : U" using assms(1) ..
-  then show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def 
+
+proof -
+  have "fst[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)"
+  proof (unfold fst_nondep_def, standard)
+    show "(a,b) : A \<times> B" using assms ..
+    show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) p : A"
+    proof
+      show "A : U" by (wellformed jdgmt: assms(1))
+    qed
+  qed
+
+  also have "indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a"
+  proof
+    show "A : U" by (wellformed jdgmt: assms(1))
+  qed (assumption, (rule assms)+)
+
+  finally show "fst[A,B]`(a,b) \<equiv> a" .
 qed
 
-lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b"
+
+lemma snd_nondep_type:
+  assumes "p : A \<times> B"
+  shows "snd[A,B]`p : B"
+
+proof
+  show "snd[A,B] : A \<times> B \<rightarrow> B"
+  proof (unfold snd_nondep_def, standard)
+    fix q assume *: "q : A \<times> B"
+    show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B"
+    proof
+      have **: "\<lambda>_. B: A \<rightarrow> U" by (wellformed jdgmt: assms)
+      have "fst[A,B]`p : A" using assms by (rule fst_nondep_type)
+      then show "B : U" by (rule **)
+    qed (assumption, rule *)
+  qed (wellformed jdgmt: assms)
+qed (rule assms)
+
+
+lemma snd_nondep_comp:
+  assumes "a : A" and "b : B"
+  shows "snd[A,B]`(a,b) \<equiv> b"
 proof -
-  assume "a : A" and "b : B"
-  then have "(a, b) : A \<times> B" ..
-  then show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp
+  have "snd[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b)"
+  proof (unfold snd_nondep_def, standard)
+    show "(a,b) : A \<times> B" using assms ..
+    show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p : B"
+    proof
+      show "B : U" by (wellformed jdgmt: assms(2))
+    qed
+  qed
+
+  also have "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b) \<equiv> b"
+  proof
+    show "B : U" by (wellformed jdgmt: assms(2))
+  qed (assumption, (rule assms)+)
+
+  finally show "snd[A,B]`(a,b) \<equiv> b" .
 qed
 
+
+end
\ No newline at end of file