Prod_comp should have a type constraint. This also fixes a false proof for the dependent sum projection functions.

1 files changed, 31 insertions, 22 deletions

diff --git a/HoTT.thy b/HoTT.thy
index 8c9fa20..cf8b157 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -21,7 +21,7 @@ consts
 
 subsection \<open>Type families\<close>
 
-text "Type families are implemented as meta-level lambda terms of type \<open>Term \<Rightarrow> Term\<close> that further satisfy the following property."
+text "Type families are implemented using meta-level lambda expressions \<open>P::Term \<Rightarrow> Term\<close> that further satisfy the following property."
 
 abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
   where "P: A \<rightarrow> U \<equiv> (\<And>x::Term. x : A \<Longrightarrow> P(x) : U)"
@@ -46,12 +46,12 @@ subsection \<open>Basic types\<close>
 
 subsubsection \<open>Dependent function/product\<close>
 
-consts
-  Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
+axiomatization
+  Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
   lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
 syntax
-  "_Prod" :: "[idt, Term, Term] \<Rightarrow> Term"     ("(3\<Prod>_:_./ _)" 10)
-  "__lambda" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<^bold>\<lambda>_:_./ _)" 10)
+  "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"     ("(3\<Prod>_:_./ _)" 10)
+  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<^bold>\<lambda>_:_./ _)" 10)
 translations
   "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
   "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
@@ -71,17 +71,20 @@ where
   Prod_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (f::Term) (a::Term).
     \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)" and
 
-  Prod_comp [simp]: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and
+  Prod_comp: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and
 
-  Prod_uniq [simp]: "\<And>(A::Term) (f::Term). \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq: "\<And>(A::Term) (f::Term). \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
 
 lemmas Prod_formation = Prod_form Prod_form[rotated]
 
+\<comment> \<open>Simplification rules for Prod\<close>
+lemmas Prod_simp [simp] = Prod_comp Prod_uniq
+
 text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
 
 subsubsection \<open>Dependent pair/sum\<close>
 
-consts
+axiomatization
   Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
 syntax
   "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<Sum>_:_./ _)" 10)
@@ -93,33 +96,39 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"   (infixr "\<times>" 50)
 
 axiomatization
   pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
-  indSum :: "[Term \<Rightarrow> Term, [Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term"
+  indSum :: "[Term \<Rightarrow> Term] \<Rightarrow> Term"
 where
   Sum_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U" and
 
   Sum_intro [intro]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (a::Term) (b::Term).
     \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)" and
 
-  Sum_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::[Term, Term] \<Rightarrow> Term) (p::Term).
-    \<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; \<And>x y::Term. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> (indSum C f p) : C(p)" and
+  Sum_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::Term) (p::Term).
+    \<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> (indSum C)`f`p : C(p)" and
 
-  Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::[Term, Term] \<Rightarrow> Term) (a::Term) (b::Term). (indSum C f (a,b)) \<equiv> f a b"
+  Sum_comp: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). (* ADD CONSTRAINTS HERE *)
+    (indSum C)`f`(a,b) \<equiv> f`a`b"
 
 lemmas Sum_formation = Sum_form Sum_form[rotated]
 
-definition fst :: "[Term, [Term, Term] \<Rightarrow> Term] \<Rightarrow> (Term \<Rightarrow> Term)"  ("(1fst[/_,/ _])")
-  where "fst[A, B] \<equiv> indSum (\<lambda>_. A) (\<lambda>a. \<lambda>b. a)"
+text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible.
+Hence only the type family \<open>C\<close> is left as a meta-level argument to the inductor indSum."
+
+\<comment> \<open>Projection functions\<close>
+
+definition fst :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"  ("(1fst[/_,/ _])")
+  where "fst[A, B] \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)"
+
+definition snd :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"  ("(1snd[/_,/ _])")
+  where "snd[A, B] \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)"
 
-lemma "fst[A, B](a,b) \<equiv> a" unfolding fst_def by simp
+lemma fst_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_def by (simp add: Sum_comp)
+lemma snd_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_def by (simp add: Sum_comp)
 
-text "A choice had to be made for the elimination rule: we formalize the function \<open>f\<close> taking \<open>a : A\<close> and \<open>b : B(x)\<close> and returning \<open>C((a,b))\<close> as a meta level \<open>f::Term \<Rightarrow> Term\<close> instead of an object logic dependent function \<open>f : \<Prod>x:A. B(x)\<close>.
-However we should be able to later show the equivalence of the formalizations."
+\<comment> \<open>Simplification rules for Sum\<close>
+lemmas Sum_simp [simp] = Sum_comp fst_comp snd_comp
 
-\<comment> \<open>Projection onto first component\<close>
-(*
-definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1\<langle>_,_\<rangle>)") where
-  "\<And>A B x y. proj1\<langle>A,B\<rangle> \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. (\<lambda>x. x))"
-*)
+lemma "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) : A" by simp
 
 subsubsection \<open>Empty type\<close>