diff options
| -rw-r--r-- | HoTT.thy | 48 | ||||
| -rw-r--r-- | HoTT_Theorems.thy | 77 |
2 files changed, 81 insertions, 44 deletions
@@ -46,14 +46,14 @@ 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>_:_./ _)" 30) + "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" 30) translations "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)" "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)" (* The above syntax translations bind the x in the expressions B, b. *) -abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 30) +abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 10) where "A\<rightarrow>B \<equiv> \<Prod>_:A. B" axiomatization @@ -69,7 +69,7 @@ where 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 [simp]: "\<And>(A::Term) (f::Term). \<^bold>\<lambda>x:A. (f`x) \<equiv> f" + Prod_uniq [simp]: "\<And>A f::Term. \<^bold>\<lambda>x:A. (f`x) \<equiv> f" lemmas Prod_formation = Prod_form Prod_form[rotated] @@ -80,7 +80,7 @@ subsubsection \<open>Dependent pair/sum\<close> axiomatization Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" syntax - "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 10) + "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) translations "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" @@ -89,7 +89,7 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) axiomatization pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and - indSum :: "[Term \<Rightarrow> 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 @@ -97,9 +97,9 @@ where \<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) (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 + \<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) (a::Term) (b::Term). (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] @@ -118,16 +118,16 @@ overloading 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)" + "fst_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)" 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)" + "snd_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)" 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)" + "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)" + "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 @@ -136,18 +136,32 @@ lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B 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> +\<comment> \<open>Simplification rules for projections\<close> lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp subsubsection \<open>Equality type\<close> axiomatization - Equal :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term" ("(_ =_ _)") and - refl :: "Term \<Rightarrow> Term" ("(refl'(_'))") + Equal :: "[Term, Term, Term] \<Rightarrow> Term" +syntax + "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)") +translations + "a =\<^sub>A b" \<rightleftharpoons> "CONST Equal A a b" + +axiomatization + refl :: "Term \<Rightarrow> Term" and + indEqual :: "([Term, Term, Term] \<Rightarrow> Term) \<Rightarrow> Term" 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" + Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U" and + + Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x" + +(* and + + Equal_elim [elim]: "\<And>(C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (x::Term) (y::Term) (p::Term). + \<lbrakk>\<rbrakk> \<Longrightarrow> (indEqual C)`f`x`y`p : C(x)(y)(p)" +*) (* subsubsection \<open>Empty type\<close> diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index a44c8f9..1ac4484 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -21,19 +21,19 @@ text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribut lemma "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. proposition "A \<equiv> B \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A" - proof - - assume assm: "A \<equiv> B" - have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. - from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp - with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" .. - qed +proof - + assume assm: "A \<equiv> B" + have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. + from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp + with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" .. +qed proposition "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A" - proof - fix a - assume "a : A" - then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. - qed +proof + fix a + assume "a : A" + then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" .. +qed subsection \<open>Function application\<close> @@ -61,9 +61,9 @@ proof (rule Prod_formation) fix x::Term assume *: "x : A" show "\<Prod>y:B(x). C x y : U" - proof (rule Prod_formation) - show "B(x) : U" using * by (rule assms) - qed (rule assms) + proof (rule Prod_formation) + show "B(x) : U" using * by (rule assms) + qed (rule assms) qed (rule assms) proposition triply_curried: @@ -81,36 +81,59 @@ proposition triply_curried: 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 "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 + 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 +lemma curried_type: fixes a b A::Term and B::"Term \<Rightarrow> Term" and f C::"[Term, Term] \<Rightarrow> Term" - assumes "\<And>x y::Term. f x y : C x y" + assumes "\<And>x y::Term. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> 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 - show "\<And>y. f x y : C x y" by (rule assms) - qed + proof + fix y::Term + assume **: "y : B(x)" + show "f x y : C x y" using * ** by (rule assms) + qed qed text "Note that the propositions and proofs above often say nothing about the well-formedness of the types, or the well-typedness of the lambdas involved; one has to be very explicit and prove such things separately! This is the result of the choices made regarding the premises of the type rules." +text "The following shows that the dependent sum inductor has the type we expect it to have:" + +lemma + assumes "C: \<Sum>x:A. B(x) \<rightarrow> U" + shows "indSum(C) : \<Prod>f:(\<Prod>x:A. \<Prod>y:B(x). C((x,y))). \<Prod>p:(\<Sum>x:A. B(x)). C(p)" +proof - + define F and P where + "F \<equiv> \<Prod>x:A. \<Prod>y:B(x). C((x,y))" and + "P \<equiv> \<Sum>x:A. B(x)" + + have "\<^bold>\<lambda>f:F. \<^bold>\<lambda>p:P. indSum(C)`f`p : \<Prod>f:F. \<Prod>p:P. C(p)" + proof (rule curried_type) + fix f p::Term + assume "f : F" and "p : P" + with assms show "indSum(C)`f`p : C(p)" unfolding F_def P_def .. + qed + + then show "indSum(C) : \<Prod>f:F. \<Prod>p:P. C(p)" by simp +qed + text "Polymorphic identity function." consts Ui::Term |