From c73a924eb679dea0455414a91dcdeb66b3f827f9 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 5 Jun 2018 13:02:44 +0200 Subject: Dependent sum done, I think. --- HoTT.thy | 68 ++++++++++++++++++++++++++++++++++++++-------------------------- 1 file changed, 40 insertions(+), 28 deletions(-) (limited to 'HoTT.thy') 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 \Setup\ - text "For ML files, routines and setup." section \Basic definitions\ - text "A single meta-level type \Term\ 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] \ prop" ("(3_ :/ _)" [0, 0] 1000) subsection \Type families\ - text "Type families are implemented using meta-level lambda expressions \P::Term \ Term\ that further satisfy the following property." abbreviation is_type_family :: "[Term \ Term, Term] \ prop" ("(3_:/ _ \ U)") where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" subsection \Definitional equality\ - text "We take the meta-equality \\\, 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 \\\, which we make use of and extend where necessary." @@ -71,15 +67,12 @@ where Prod_elim [elim]: "\(A::Term) (B::Term \ Term) (f::Term) (a::Term). \f : \x:A. B(x); a : A\ \ f`a : B(a)" and - Prod_comp: "\(A::Term) (b::Term \ Term) (a::Term). a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" and + Prod_comp [simp]: "\(A::Term) (b::Term \ Term) (a::Term). a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" and - Prod_uniq: "\(A::Term) (f::Term). \<^bold>\x:A. (f`x) \ f" + Prod_uniq [simp]: "\(A::Term) (f::Term). \<^bold>\x:A. (f`x) \ f" lemmas Prod_formation = Prod_form Prod_form[rotated] -\ \Simplification rules for Prod\ -lemmas Prod_simp [simp] = Prod_comp Prod_uniq - text "Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation)." subsubsection \Dependent pair/sum\ @@ -106,30 +99,56 @@ where Sum_elim [elim]: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term) (p::Term). \C: \x:A. B(x) \ U; f : \x:A. \y:B(x). C((x,y)); p : \x:A. B(x)\ \ (indSum C)`f`p : C(p)" and - Sum_comp: "\(C::Term \ Term) (f::Term) (a::Term) (b::Term). (* ADD CONSTRAINTS HERE *) - (indSum C)`f`(a,b) \ f`a`b" + Sum_comp [simp]: "\(C::Term \ Term) (f::Term) (a::Term) (b::Term). (indSum C)`f`(a,b) \ 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 \C\ is left as a meta-level argument to the inductor indSum." -\ \Projection functions\ +text "Projection functions" -definition fst :: "[Term, Term \ Term] \ Term" ("(1fst[/_,/ _])") - where "fst[A, B] \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B(x). x)" +consts + fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") + snd :: "[Term, 'a] \ Term" ("(1snd[/_,/ _])") +overloading + fst_dep \ fst + snd_dep \ snd + fst_nondep \ fst + snd_nondep \ snd +begin +definition fst_dep :: "[Term, Term \ Term] \ Term" where + "fst_dep A B \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B(x). x)" -definition snd :: "[Term, Term \ Term] \ Term" ("(1snd[/_,/ _])") - where "snd[A, B] \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B(x). y)" +definition snd_dep :: "[Term, Term \ Term] \ Term" where + "snd_dep A B \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B(x). y)" -lemma fst_comp: "\a : A; b : B(a)\ \ fst[A,B]`(a,b) \ a" unfolding fst_def by (simp add: Sum_comp) -lemma snd_comp: "\a : A; b : B(a)\ \ snd[A,B]`(a,b) \ b" unfolding snd_def by (simp add: Sum_comp) +definition fst_nondep :: "[Term, Term] \ Term" where + "fst_nondep A B \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B. x)" + +definition snd_nondep :: "[Term, Term] \ Term" where + "snd_nondep A B \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B. y)" +end + +lemma fst_dep_comp: "\a : A; b : B(a)\ \ fst[A,B]`(a,b) \ a" unfolding fst_dep_def by simp +lemma snd_dep_comp: "\a : A; b : B(a)\ \ snd[A,B]`(a,b) \ b" unfolding snd_dep_def by simp + +lemma fst_nondep_comp: "\a : A; b : B\ \ fst[A,B]`(a,b) \ a" unfolding fst_nondep_def by simp +lemma snd_nondep_comp: "\a : A; b : B\ \ snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by simp \ \Simplification rules for Sum\ -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 "\a : A; b : B(a)\ \ fst[A,B]`(a,b) : A" by simp +subsubsection \Equality type\ + +axiomatization + Equal :: "Term \ Term \ Term \ Term" ("(_ =_ _)") and + refl :: "Term \ Term" ("(refl'(_'))") +where + Equal_form: "\A a b. \a : A; b : A\ \ a =A b : U" and + Equal_intro: "\A x. x : A \ refl x : x =A x" +(* subsubsection \Empty type\ axiomatization @@ -152,13 +171,6 @@ where Nat_intro2: "\n. n : Nat \ succ n : Nat" (* computation rules *) -subsubsection \Equality type\ - -axiomatization - Equal :: "Term \ Term \ Term \ Term" ("(_ =_ _)") and - refl :: "Term \ Term" ("(refl'(_'))") -where - Equal_form: "\A a b. \a : A; b : A\ \ a =A b : U" and - Equal_intro: "\A x. x : A \ refl x : x =A x" +*) end \ No newline at end of file -- cgit v1.2.3