Dependent sum done, I think.

1 files changed, 40 insertions, 28 deletions

diff --git a/HoTT.thy b/HoTT.thy
index cf8b157..68de364 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -3,11 +3,9 @@ theory HoTT
 begin
 
 section \<open>Setup\<close>
-
 text "For ML files, routines and setup."
 
 section \<open>Basic definitions\<close>
-
 text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
 We do not implement universes, but simply follow the informal notation in the HoTT book."
 
@@ -20,14 +18,12 @@ consts
   is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_ :/ _)" [0, 0] 1000)
 
 subsection \<open>Type families\<close>
-
 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)"
 
 subsection \<open>Definitional equality\<close>
-
 text "We take the meta-equality \<open>\<equiv>\<close>, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory.
 
 Note that the Pure framework already provides axioms and results for various properties of \<open>\<equiv>\<close>, which we make use of and extend where necessary."
@@ -71,15 +67,12 @@ 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: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and
+  Prod_comp [simp]: "\<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: "\<And>(A::Term) (f::Term). \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq [simp]: "\<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>
@@ -106,30 +99,56 @@ where
   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: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). (* ADD CONSTRAINTS HERE *)
-    (indSum C)`f`(a,b) \<equiv> f`a`b"
+  Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). (indSum C)`f`(a,b) \<equiv> f`a`b"
 
 lemmas Sum_formation = Sum_form Sum_form[rotated]
 
 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>
+text "Projection functions"
 
-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)"
+consts
+  fst :: "[Term, 'a] \<Rightarrow> Term"  ("(1fst[/_,/ _])")
+  snd :: "[Term, 'a] \<Rightarrow> Term"  ("(1snd[/_,/ _])")
+overloading
+  fst_dep \<equiv> fst
+  snd_dep \<equiv> snd
+  fst_nondep \<equiv> fst
+  snd_nondep \<equiv> snd
+begin
+definition fst_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
+  "fst_dep 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)"
+definition snd_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
+  "snd_dep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)"
 
-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)
+definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where
+  "fst_nondep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)"
+
+definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
+  "snd_nondep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)"
+end
+
+lemma fst_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by simp
+lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp
+
+lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp
+lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp
 
 \<comment> \<open>Simplification rules for Sum\<close>
-lemmas Sum_simp [simp] = Sum_comp fst_comp snd_comp
+lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
 
-lemma "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) : A" by simp
+subsubsection \<open>Equality type\<close>
+
+axiomatization
+  Equal :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"  ("(_ =_ _)") and
+  refl :: "Term \<Rightarrow> Term"                   ("(refl'(_'))")
+where
+  Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =A b : U" and
+  Equal_intro: "\<And>A x. x : A \<Longrightarrow> refl x : x =A x"
 
+(*
 subsubsection \<open>Empty type\<close>
 
 axiomatization
@@ -152,13 +171,6 @@ where
   Nat_intro2: "\<And>n. n : Nat \<Longrightarrow> succ n : Nat"
   (* computation rules *)
 
-subsubsection \<open>Equality type\<close>
-
-axiomatization
-  Equal :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"  ("(_ =_ _)") and
-  refl :: "Term \<Rightarrow> Term"                   ("(refl'(_'))")
-where
-  Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =A b : U" and
-  Equal_intro: "\<And>A x. x : A \<Longrightarrow> refl x : x =A x"
+*)
 
 end
\ No newline at end of file