diff options
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Theorems.thy | 43 | ||||
| -rw-r--r-- | Prod.thy | 2 | ||||
| -rw-r--r-- | scratch.thy | 24 |
3 files changed, 45 insertions, 24 deletions
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index ab5374d..871c553 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -16,42 +16,39 @@ section \<open>\<Prod> type\<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" .. +proposition assumes "A : U" shows "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" using assms .. -proposition "A \<equiv> B \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A" +proposition + assumes "A : U" and "A \<equiv> B" + shows "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" proof - - assume "A \<equiv> B" - then have *: "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp - - have "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" .. - with * show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" by simp + have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp + moreover have "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" using assms(1) .. + ultimately show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" by simp qed -proposition "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A" +proposition + assumes "A : U" and "B : U" + shows "\<^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" .. - - ML_val \<open>@{context} |> Variable.names_of\<close> - -qed + fix x + assume "x : A" + with assms(2) show "\<^bold>\<lambda>y:B. x : B\<rightarrow>A" .. +qed (rule assms) subsection \<open>Function application\<close> -proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by simp +proposition assumes "a : A" shows "(\<^bold>\<lambda>x:A. x)`a \<equiv> a" using assms by simp text "Currying:" -term "lambda A (\<lambda>x. \<^bold>\<lambda>y:B(x). y)" - -thm Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"] - -lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a \<equiv> \<^bold>\<lambda>y:B(a). y" -proof (rule Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"]) +lemma + assumes "a : A" + shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a \<equiv> \<^bold>\<lambda>y:B(a). y" +proof show "\<And>x. a : A \<Longrightarrow> x : A \<Longrightarrow> \<^bold>\<lambda>y:B x. y : B x \<rightarrow> B x" lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a`b \<equiv> b" by simp @@ -33,7 +33,7 @@ translations axiomatization where Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U" and - Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" + Prod_intro [intro]: "\<And>A B b. \<lbrakk>A : U; \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" and Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a" and diff --git a/scratch.thy b/scratch.thy new file mode 100644 index 0000000..331b607 --- /dev/null +++ b/scratch.thy @@ -0,0 +1,24 @@ +theory scratch + imports IFOL + +begin + +lemma disj_swap: "P \<or> Q \<Longrightarrow> Q \<or> P" +apply (erule disjE) (* Compare with the less useful \<open>rule disjE\<close> *) + apply (rule disjI2) + apply assumption +apply (rule disjI1) +apply assumption +done + +lemma imp_uncurry: "P \<longrightarrow> (Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R" +apply (rule impI) +apply (erule conjE) +apply (drule mp) +apply assumption +apply (drule mp) +apply assumption +apply assumption +done + +end
\ No newline at end of file |