diff options
| -rw-r--r-- | HoTT.thy | 25 | ||||
| -rw-r--r-- | HoTT_Test.thy (renamed from test.thy) | 26 |
2 files changed, 33 insertions, 18 deletions
@@ -17,8 +17,8 @@ typedecl Term subsection \<open>Judgements\<close> consts - is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)") (* Add precedences when I figure them out! *) - is_of_type :: "Term \<Rightarrow> Term \<Rightarrow> prop" ("(_ : _)") + is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)" [0] 1000) + is_of_type :: "Term \<Rightarrow> Term \<Rightarrow> prop" ("(3_ :/ _)" [0, 0] 1000) subsection \<open>Basic axioms\<close> subsubsection \<open>Definitional equality\<close> @@ -30,15 +30,12 @@ Note that the Pure framework already provides axioms and results for the various which we make use of and extend where necessary. \<close> - -theorem DefEq_symmetry: "\<And>A B. A \<equiv> B \<Longrightarrow> B \<equiv> A" - by (rule Pure.symmetric) - subsubsection \<open>Type-related properties\<close> axiomatization where - equal_types: "\<And>A B x. \<lbrakk>A \<equiv> B; x : A\<rbrakk> \<Longrightarrow> x : B" and - inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U" + term_substitution: "\<And>(A::Term) (x::Term) y::Term. x \<equiv> y \<Longrightarrow> A(x) \<equiv> A(y)" and + equal_types: "\<And>(A::Term) (B::Term) x::Term. \<lbrakk>A \<equiv> B; x : A\<rbrakk> \<Longrightarrow> x : B" and + inhabited_implies_type: "\<And>(x::Term) A::Term. x : A \<Longrightarrow> A : U" subsection \<open>Basic types\<close> @@ -47,16 +44,18 @@ subsubsection \<open>Nondependent function type\<close> Write this for now to test stuff, later I should make this an instance of the dependent function. Same for the nondependent product below. + +Note that the syntax \<^bold>\<lambda> (bold lambda) clashes with the proof term syntax! +(See \<section>2.5.2, The Isabelle/Isar Implementation.) *) axiomatization Function :: "Term \<Rightarrow> Term \<Rightarrow> Term" (infixr "\<rightarrow>" 10) and - lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 10) and - (* Is bold lambda already used by something else? Proof transformers in Pure maybe?... *) - appl :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(_`_)") + lambda :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" [1000, 0, 0] 10) and + appl :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(3_`/_)" [10, 10] 10) where - Function_form: "\<And>A B. \<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> A\<rightarrow>B : U" and - Function_intro: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b(x) : B) \<Longrightarrow> \<^bold>\<lambda>x. b(x) : A\<rightarrow>B" and + Function_form: "\<And>(A::Term) B::Term. \<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> A\<rightarrow>B : U" and + Function_intro: "\<And>(A::Term) (B::Term) b::Term. (\<And>x. x : A \<Longrightarrow> b(x) : B) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : A\<rightarrow>B" and Function_elim: "\<And>A B f a. \<lbrakk>f : A\<rightarrow>B; a : A\<rbrakk> \<Longrightarrow> f`a : B" (* beta and eta reductions should go here *) @@ -1,21 +1,36 @@ -theory test +theory HoTT_Test imports HoTT begin text \<open>Check trivial stuff:\<close> + lemma "Null : U" by (rule Null_form) +lemma "\<lbrakk>A \<equiv> B; x : B\<rbrakk> \<Longrightarrow> x : A" +proof - + assume "A \<equiv> B" + then have "B \<equiv> A" by (rule Pure.symmetric) + then have "x : B \<Longrightarrow> x :A" by (rule equal_types) + oops +(* qed---figure out how to discharge assumptions *) + text \<open> Do functions behave like we expect them to? (Or, is my implementation at least somewhat correct?... \<close> -lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" +\<comment> {* NOTE!!! The issues with substitution here. +We need the HoTT term \<open>b\<close> and the type family \<open>B\<close> to indeed be a Pure \<lambda>-term! +This seems to mean that I have to implement the HoTT types in more than one Pure type. +See CTT.thy for examples. +*} + +lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x:A. x) : B\<rightarrow>A" proof - - have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule DefEq_symmetry) - then have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types) - thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" by (rule Function_intro) + have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule Pure.symmetric) + then have "\<And>x::Term. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types) + thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x:A. x) : B\<rightarrow>A" by (rule Function_intro) qed lemma "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" @@ -25,6 +40,7 @@ proof - qed text \<open>Here's a dumb proof that 2 is a natural number:\<close> + lemma "succ(succ 0) : Nat" proof - have "0 : Nat" by (rule Nat_intro1) |