diff options
| -rw-r--r-- | HoTT.thy | 53 | ||||
| -rw-r--r-- | HoTT_Theorems.thy | 52 |
2 files changed, 69 insertions, 36 deletions
@@ -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> diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 5922b51..aeddf9f 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -16,7 +16,7 @@ section \<open>Functions\<close> subsection \<open>Typing functions\<close> -text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following." +text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following." lemma "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. @@ -41,9 +41,9 @@ proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by text "Currying:" -lemma "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. f x y)`a \<equiv> \<^bold>\<lambda>y:B. f a y" by simp +lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f x y)`a \<equiv> \<^bold>\<lambda>y:B(a). f a y" by simp -lemma "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. \<^bold>\<lambda>z:C. f x y z)`a`b`c \<equiv> f a b c" by simp +lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). \<^bold>\<lambda>z:C(x)(y). f x y z)`a`b`c \<equiv> f a b c" by simp proposition wellformed_currying: fixes @@ -56,29 +56,53 @@ proposition wellformed_currying: "\<And>x::Term. C(x): B(x) \<rightarrow> U" shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U" proof (rule Prod_formation) - show "\<And>x::Term. x : A \<Longrightarrow> \<Prod>y:B(x). C x y : U" + fix x::Term + assume *: "x : A" + show "\<Prod>y:B(x). C x y : U" proof (rule Prod_formation) - fix x y::Term - assume "x : A" - show "y : B x \<Longrightarrow> C x y : U" by (rule assms(3)) - qed (rule assms(2)) -qed (rule assms(1)) + show "B(x) : U" using * by (rule assms) + qed (rule assms) +qed (rule assms) + +proposition triply_curried: + fixes + A::Term and + B::"Term \<Rightarrow> Term" and + C::"[Term, Term] \<Rightarrow> Term" and + D::"[Term, Term, Term] \<Rightarrow> Term" + assumes + "A : U" and + "B: A \<rightarrow> U" and + "\<And>x y::Term. y : B(x) \<Longrightarrow> C(x)(y) : U" and + "\<And>x y z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" + shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U" +proof (rule Prod_formation) + fix x::Term assume 1: "x : A" + show "\<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U" + proof (rule Prod_formation) + show "B(x) : U" using 1 by (rule assms) + + fix y::Term assume 2: "y : B(x)" + show "\<Prod>z:C(x)(y). D(x)(y)(z) : U" + proof (rule Prod_formation) + show "C x y : U" using 2 by (rule assms) + show "\<And>z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" by (rule assms) + qed + qed +qed (rule assms) lemma fixes a b A::Term and B::"Term \<Rightarrow> Term" and f C::"[Term, Term] \<Rightarrow> Term" - assumes "\<And>x y::Term. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y" + assumes "\<And>x y::Term. f x y : C x y" shows "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f x y : \<Prod>x:A. \<Prod>y:B(x). C x y" proof fix x::Term - assume *: "x : A" show "\<^bold>\<lambda>y:B(x). f x y : \<Prod>y:B(x). C x y" proof - fix y::Term - assume **: "y : B(x)" - show "f x y : C x y" by (rule assms[OF * **]) + show "\<And>y. f x y : C x y" by (rule assms) qed qed |