diff options
| -rw-r--r-- | HoTT.thy | 37 | ||||
| -rw-r--r-- | HoTT_Theorems.thy | 69 |
2 files changed, 65 insertions, 41 deletions
@@ -23,20 +23,9 @@ 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." -abbreviation is_type_family :: "[(Term \<Rightarrow> Term), Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)") +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)" -\<comment> \<open> -I originally wrote the following, but I'm not sure it's useful. -\<open>theorem constant_type_family': "B : U \<Longrightarrow> \<lambda>_. B: A \<rightarrow> U" - proof - - assume "B : U" - then show "\<lambda>_. B: A \<rightarrow> U" . - qed - -lemmas constant_type_family = constant_type_family' constant_type_family'[rotated]\<close> -\<close> - 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. @@ -58,8 +47,8 @@ subsection \<open>Basic types\<close> subsubsection \<open>Dependent function/product\<close> consts - Prod :: "[Term, (Term \<Rightarrow> Term)] \<Rightarrow> Term" - lambda :: "[Term, (Term \<Rightarrow> Term)] \<Rightarrow> Term" + Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" + 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) @@ -76,13 +65,13 @@ axiomatization where Prod_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U" and - Prod_intro [intro]: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (B::Term \<Rightarrow> Term). + Prod_intro [intro]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term). (\<And>x::Term. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)" and - Prod_elim [elim]: "\<And>(f::Term) (A::Term) (B::Term \<Rightarrow> Term) (a::Term). + 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) (A::Term) (b::Term \<Rightarrow> 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). (\<^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" @@ -104,21 +93,25 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) axiomatization pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and - indSum :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term" + indSum :: "[Term \<Rightarrow> Term, [Term, Term] \<Rightarrow> Term, 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 \<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, 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_comp [simp]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::Term \<Rightarrow> Term) (a::Term) (b::Term). - (indSum C f (a,b)) \<equiv> f((a,b))" + 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" 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)" + +lemma "fst[A, B](a,b) \<equiv> a" unfolding fst_def by simp + 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." diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 0aefe94..5922b51 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -21,34 +21,65 @@ 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> proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by simp -text "Two arguments:" +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 "(\<^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 + +proposition wellformed_currying: + fixes + A::Term and + B::"Term \<Rightarrow> Term" and + C::"Term \<Rightarrow> Term \<Rightarrow> Term" + assumes + "A : U" and + "B: A \<rightarrow> U" and + "\<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" + 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)) lemma - assumes "a : A" and "b : B" - shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a`b \<equiv> a" -proof - - have "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a \<equiv> \<^bold>\<lambda>y:B. a" using assms(1) by (rule Prod_comp[of a A "\<lambda>x. \<^bold>\<lambda>y:B. x"]) - then have "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a`b \<equiv> (\<^bold>\<lambda>y:B. a)`b" by simp - also have "(\<^bold>\<lambda>y:B. a)`b \<equiv> a" using assms by simp - finally show "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)`a`b \<equiv> a" . + 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" + 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 * **]) + 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! |