diff options
| -rw-r--r-- | HoTT_Base.thy | 2 | ||||
| -rw-r--r-- | Prod.thy | 31 | ||||
| -rw-r--r-- | Sum.thy | 49 |
3 files changed, 51 insertions, 31 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9b7c3e2..7794601 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -34,7 +34,7 @@ consts is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) axiomatization where - inhabited_implies_type: "\<And>a A. a : A \<Longrightarrow> A : U" + inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U" section \<open>Type families\<close> @@ -16,40 +16,47 @@ axiomatization \<comment> \<open>Application binds tighter than abstraction.\<close> appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60) + +section \<open>Syntax\<close> + syntax "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30) "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" 30) "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3PROD _:_./ _)" 30) "_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3%%_:_./ _)" 30) -\<comment> \<open>The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>.\<close> +text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>." + translations "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)" "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)" "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)" "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)" -\<comment> \<open>Type rules\<close> + +section \<open>Type rules\<close> + axiomatization where - Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U" + Prod_form: "\<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. \<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" + Prod_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" + Prod_elim: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a" and - Prod_comp [simp]: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" + Prod_comp: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" and - Prod_uniq [simp]: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f" + Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f" + +text "The type rules should be able to be used as introduction rules by the standard reasoner:" -\<comment> \<open>The funny thing about the first premises of the computation and uniqueness rules is that they introduce a variable B that doesn't actually explicitly appear in the statement of the conclusion. -In a sense, they say something like "if this condition holds for some type family B... (then we can apply the rule)". -This forces the theorem prover to search for a suitable B. Is this additional overhead necessary? -It *is* a safety check for well-formedness...\<close> +lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim 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)." -\<comment> \<open>Nondependent functions are a special case.\<close> +text "Nondependent functions are a special case." + abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_:A. B" + end
\ No newline at end of file @@ -15,6 +15,9 @@ axiomatization pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1indSum[_,/ _])") + +section \<open>Syntax\<close> + syntax "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3SUM _:_./ _)" 20) @@ -23,30 +26,35 @@ translations "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)" + +section \<open>Type rules\<close> + axiomatization where - Sum_form [intro]: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U" + Sum_form: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U" and - Sum_intro [intro]: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x" + Sum_intro: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x" and - Sum_elim [elim]: "\<And>A B C f p. \<lbrakk> + Sum_elim: "\<And>A B C f p. \<lbrakk> C: \<Sum>x:A. B x \<rightarrow> U; \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y); p : \<Sum>x:A. B x \<rbrakk> \<Longrightarrow> indSum[A,B] C f p : C p" and - Sum_comp [simp]: "\<And>A B C f a b. \<lbrakk> + Sum_comp: "\<And>A B C f a b. \<lbrakk> C: \<Sum>x:A. B x \<rightarrow> U; \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y); a : A; b : B a \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b" +lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp + \<comment> \<open>Nondependent pair\<close> abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" -section \<open>Projections\<close> +section \<open>Projection functions\<close> consts fst :: "[Term, 'a] \<Rightarrow> Term" ("(1fst[/_,/ _])") @@ -74,23 +82,28 @@ begin "snd_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p" end -text "Properties of projections:" +text "Simplifying projections:" -lemma fst_dep_comp: +lemma fst_dep_comp: (* Potential for automation *) assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \<equiv> a" -proof (unfold fst_dep_def) (* GOOD AUTOMATION EXAMPLE *) - have "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A, B] (\<lambda>_. A) (\<lambda>x y. x) p : A" .. - moreover have "(a, b) : \<Sum>x:A. B x" using assms .. - then have "fst[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" unfolding fst_dep_def by (simp add: Prod_comp) - have "A : U" using assms(2) .. - then have "\<lambda>_. A: \<Sum>x:A. B x \<rightarrow> U" . - moreover have "\<And>x y. x : A \<Longrightarrow> (\<lambda>x y. x) x y : A" . - moreover - ultimately show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by simp -qed +proof (unfold fst_dep_def) + \<comment> "Write about this proof: unfolding, how we set up the introduction rules (explain \<open>..\<close>), do a trace of the proof, explain the meaning of keywords, etc." -thm Sum_comp + have *: "A : U" using assms(2) .. (* I keep thinking this should not have to be done explicitly, but rather automated. *) + + then have "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A" .. + + moreover have "(a,b) : \<Sum>x:A. B x" using assms .. + + ultimately have "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv> + indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" .. + + also have "indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a" + by (rule Sum_comp) (rule *, assumption, (rule assms)+) + + finally show "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv> a" . +qed lemma snd_dep_comp: assumes "a : A" and "b : B a" |