diff options
author | Josh Chen | 2018-06-01 03:39:51 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-01 03:39:51 +0200 |
commit | a7303e36651ea1f8ec50958415fa0db7295ad957 (patch) | |
tree | 8df911435e07db5875c86c6ed05a00f822d4c4cc /HoTT_Theorems.thy | |
parent | 095bc4a60ab2c38a56c34b4b99d363c4c0f14e3d (diff) |
Should be final version of Prod. Theorems proving stuff about currying. Rules for Sum, going to change them to use object-level arguments more.
Diffstat (limited to 'HoTT_Theorems.thy')
-rw-r--r-- | HoTT_Theorems.thy | 69 |
1 files changed, 50 insertions, 19 deletions
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! |