Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Added type formation rules expressing necessity of the conditions.

1 files changed, 81 insertions, 16 deletions

diff --git a/Sum.thy b/Sum.thy
index 8e7ccd6..0a062cf 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -7,7 +7,6 @@ Dependent sum type.
 
 theory Sum
   imports Prod
-
 begin
 
 axiomatization
@@ -32,6 +31,10 @@ section \<open>Type rules\<close>
 axiomatization where
   Sum_form: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U"
 and
+  Sum_form_cond1: "\<And>A B. (\<Sum>x:A. B x : U) \<Longrightarrow> A : U"
+and
+  Sum_form_cond2: "\<And>A B. (\<Sum>x:A. B x : U) \<Longrightarrow> B: A \<rightarrow> U"
+and
   Sum_intro: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
 and
   Sum_elim: "\<And>A B C f p. \<lbrakk>
@@ -48,6 +51,7 @@ and
     \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b"
 
 lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
+lemmas Sum_form_conds [elim] = Sum_form_cond1 Sum_form_cond2
 
 \<comment> \<open>Nondependent pair\<close>
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
@@ -76,44 +80,104 @@ overloading
   snd_nondep \<equiv> snd
 begin
   definition snd_dep :: "[Term, Typefam] \<Rightarrow> Term" where
-    "snd_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>p. B fst[A,B]`p) (\<lambda>x y. y) p"
+    "snd_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p"
   
   definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
     "snd_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p"
 end
 
-text "Simplifying projections:"
+text "Results about projections:"
+
+lemma fst_dep_type:
+  assumes "p : \<Sum>x:A. B x"
+  shows "fst[A,B]`p : A"
+
+proof \<comment> \<open>The standard reasoner knows to backchain with the product elimination rule here...\<close>
+  \<comment> \<open>Also write about this proof: compare the effect of letting the standard reasoner do simplifications, as opposed to using the minus switch and writing everything out explicitly from first principles.\<close>
+
+  have *: "\<Sum>x:A. B x : U" using assms ..
+  
+  show "fst[A,B]: (\<Sum>x:A. B x) \<rightarrow> A"
+
+  proof (unfold fst_dep_def, standard) \<comment> \<open>...and with the product introduction rule here...\<close>
+    show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A"
+    
+    proof \<comment> \<open>...and with sum elimination here.\<close>
+      show "A : U" using * ..
+    qed
+  
+  qed (rule *)
+
+qed (rule assms)
+
 
 lemma fst_dep_comp:  (* Potential for automation *)
   assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
   shows "fst[A,B]`(a,b) \<equiv> a"
-proof (unfold fst_dep_def)
+
+proof -
   \<comment> "Write about this proof: unfolding, how we set up the introduction rules (explain \<open>..\<close>), do a trace of the proof, explain the meaning of keywords, etc."
 
   have *: "A : U" using assms(2) ..  (* I keep thinking this should not have to be done explicitly, but rather automated. *)
-  
-  then have "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A" ..
-  
-  moreover have "(a,b) : \<Sum>x:A. B x" using assms ..
-  
-  ultimately have "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv>
-    indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" ..
+
+  have "fst[A,B]`(a,b) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)"
+  proof (unfold fst_dep_def, standard)
+    show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A" using * ..
+    show "(a,b) : \<Sum>x:A. B x" using assms ..
+  qed
   
   also have "indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a"
     by (rule Sum_comp) (rule *, assumption, (rule assms)+)
   
-  finally show "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv> a" .
+  finally show "fst[A,B]`(a,b) \<equiv> a" .
 qed
 
+
+lemma snd_dep_type:
+  assumes "p : \<Sum>x:A. B x"
+  shows "snd[A,B]`p : B (fst[A,B]`p)"
+oops
+\<comment> \<open>Do we need this for the following lemma?\<close>
+
+
 lemma snd_dep_comp:
-  assumes "a : A" and "b : B a"
+  assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
   shows "snd[A,B]`(a,b) \<equiv> b"
 proof -
-  have "\<lambda>p. B fst[A,B]`p: \<Sum>x:A. B x \<rightarrow> U"
-    
-  show "snd[A,B]`(a,b) \<equiv> b" unfolding fst_dep_def
+  \<comment> \<open>We use the following two lemmas:\<close>
+
+  have lemma1: "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> B (fst[A,B]`p) : U"
+  proof -
+      fix p assume "p : \<Sum>x:A. B x"
+      then have "fst[A,B]`p : A" by (rule fst_dep_type)
+      then show "B (fst[A,B]`p) : U" by (rule assms(1))
+  qed
+
+  have lemma2: "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> y : B (fst[A,B]`(x, y))"
+  proof -
+    fix x y assume "x : A" and "y : B x"
+    moreover with assms(1) have "fst[A,B]`(x,y) \<equiv> x" by (rule fst_dep_comp)
+    ultimately show "y : B (fst[A,B]`(x,y))" by simp
+  qed
+
+  \<comment> \<open>And now the proof.\<close>
+
+  have "snd[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b)"
+  proof (unfold snd_dep_def, standard)
+    show "(a,b) : \<Sum>x:A. B x" using assms ..
+
+    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)"
+      by (standard, elim lemma1, elim lemma2) (assumption, rule *)
+  qed
+
+  also have "indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b) \<equiv> b"
+    by (standard, elim lemma1, elim lemma2) (assumption, (rule assms)+)
+
+  finally show "snd[A,B]`(a,b) \<equiv> b" .
 qed
 
+
 lemma fst_nondep_comp:
   assumes "a : A" and "b : B"
   shows "fst[A,B]`(a,b) \<equiv> a"
@@ -131,4 +195,5 @@ qed
 
 lemmas proj_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
 
+
 end
\ No newline at end of file