pre-system upgrade commit

3 files changed, 108 insertions, 93 deletions

diff --git a/HoTT.thy b/HoTT.thy
index 682319d..a13b1d4 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -1,63 +1,66 @@
 theory HoTT
-imports Pure
+  imports Pure
 begin
 
 section \<open>Setup\<close>
-text \<open>
-For ML files, routines and setup.
-\<close>
+
+text "For ML files, routines and setup."
 
 section \<open>Basic definitions\<close>
-text \<open>
-A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
-For now we do not implement universes, but simply follow the informal notation in the HoTT book.
-\<close> (* Actually unsure if a single meta-type suffices... *)
+
+text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
+We do not implement universes, but simply follow the informal notation in the HoTT book."
 
 typedecl Term
 
-subsection \<open>Judgements\<close>
+subsection \<open>Judgments\<close>
+
 consts
   is_a_type :: "Term \<Rightarrow> prop"           ("(_ : U)" [0] 1000)
-  is_of_type :: "Term \<Rightarrow> Term \<Rightarrow> prop"  ("(3_ :/ _)" [0, 0] 1000)
+  is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_ :/ _)" [0, 0] 1000)
 
 subsection \<open>Basic axioms\<close>
+
 subsubsection \<open>Definitional equality\<close>
-text\<open>
-We take the meta-equality \<equiv>, 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.
 
-Note that the Pure framework already provides axioms and results for the various properties of \<equiv>,
-which we make use of and extend where necessary.
-\<close>
+text "We take the meta-equality \<equiv>, 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.
+
+Note that the Pure framework already provides axioms and results for various properties of \<equiv>, which we make use of and extend where necessary."
 
 subsubsection \<open>Type-related properties\<close>
 
 axiomatization where
-  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"
+  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>
 
-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.
+subsubsection \<open>Dependent product type\<close>
 
-Note that the syntax \<^bold>\<lambda> (bold lambda) clashes with the proof term syntax!
-(See \<section>2.5.2, The Isabelle/Isar Implementation.)
-*)
+consts
+  Prod :: "[Term, (Term \<Rightarrow> Term)] \<Rightarrow> Term"
+syntax
+  "_Prod" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<Prod>_:_./ _)" 10)
+translations
+  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
+(* The above syntax translation binds the x in B *)
 
 axiomatization
-  Function :: "Term \<Rightarrow> Term \<Rightarrow> Term"  (infixr "\<rightarrow>" 10) and
-  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)
+  lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"  (binder "\<^bold>\<lambda>" 10) and
+  appl :: "[Term, Term] \<Rightarrow> Term"      ("(3_`/_)" [10, 10] 60)
 where
-  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 *)
+  Prod_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; \<And>(x::Term). x : A \<Longrightarrow> B(x) : U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U" and
+  Prod_intro: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term). \<lbrakk>A : U; \<And>(x::Term). x : A \<Longrightarrow> b(x) : B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x) : \<Prod>x:A. B(x)" and
+  Prod_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: "\<And>(b::Term \<Rightarrow> Term) (a::Term). (\<^bold>\<lambda>x. b(x))`a \<equiv> b(a)" and
+  Prod_uniq: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (f::Term). \<lbrakk>f : \<Prod>x:A. B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f"
+
+text "Observe that the metatype \<open>Term \<Rightarrow> Term\<close> is used to represent type families, for example \<open>Prod\<close> takes a type \<open>A\<close> and a type family \<open>B\<close> and constructs a dependent function type from them."
+
+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)."
+
+abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 30)
+where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
 
 subsubsection \<open>Nondependent product type\<close>
 
@@ -72,8 +75,10 @@ where
   Product_comp: "\<And>A B C g a b. \<lbrakk>C : U; g : A\<rightarrow>B\<rightarrow>C; a : A; b : B\<rbrakk> \<Longrightarrow> rec_Product(A,B,C,g)`(a,b) \<equiv> (g`a)`b"
 
 \<comment> \<open>Projection onto first component\<close>
+(*
 definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1\<langle>_,_\<rangle>)") where
-  "proj1\<langle>A,B\<rangle> \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)"
+  "\<And>A B x y. proj1\<langle>A,B\<rangle> \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. (\<lambda>x. x))"
+*)
 
 subsubsection \<open>Empty type\<close>
 
diff --git a/HoTT_Test.thy b/HoTT_Test.thy
deleted file mode 100644
index b37ac76..0000000
--- a/HoTT_Test.thy
+++ /dev/null
@@ -1,58 +0,0 @@
-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>
-
-\<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 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"
-proof -
-  have "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. x : B \<rightarrow> A" by (rule Function_intro)
-  thus "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" by (rule Function_intro)
-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)
-  from this have "(succ 0) : Nat" by (rule Nat_intro2)
-  thus "succ(succ 0) : Nat" by (rule Nat_intro2)
-qed
-
-text \<open>
-We can of course iterate the above for as many applications of \<open>succ\<close> as we like.
-The next thing to do is to implement some kind of induction tactic to automate such proofs.
-
-When we get more stuff working, I'd like to aim for formalizing the encode-decode method.
-\<close>
-
-end
\ No newline at end of file
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
new file mode 100644
index 0000000..bea3dfe
--- /dev/null
+++ b/HoTT_Theorems.thy
@@ -0,0 +1,68 @@
+theory HoTT_Theorems
+  imports HoTT
+begin
+
+text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified."
+
+section \<open>Foundational stuff\<close>
+
+theorem "\<lbrakk>A : U; A \<equiv> B\<rbrakk> \<Longrightarrow> B : U" by simp
+
+section \<open>Functions\<close>
+
+lemma "A : U \<Longrightarrow> \<^bold>\<lambda>x. x : A\<rightarrow>A"
+  by (rule Prod_intro)
+
+text "Note that there is no provision for declaring the type of bound variables outside of the scope of a lambda expression.
+Hence a statement like \<open>x : A\<close> is not needed (nor possible!) in the premises of the following lemma."
+
+lemma "\<lbrakk>A : U; A \<equiv> B\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. x : B\<rightarrow>A"
+proof -
+  assume
+    0: "A : U" and
+    1: "A \<equiv> B"
+  from 0 have 2: "\<^bold>\<lambda>x. x : A\<rightarrow>A" by (rule Prod_intro)
+  from 1 have 3: "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
+  from 3 and 2 show "\<^bold>\<lambda>x. x : B\<rightarrow>A" by (rule equal_types)
+  qed
+
+lemma "\<lbrakk>A : U; B : U; x : A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y. x : B\<rightarrow>A"
+proof -
+assume 
+  1: "A : U" and 
+  2: "B : U" and 
+  3: "x : A"
+then show "\<^bold>\<lambda>y. x : B\<rightarrow>A"
+proof -
+from 3 have "\<^bold>\<lambda>y. x : B\<rightarrow>A" by (rule Prod_intro)
+qed
+qed
+
+lemma "\<lbrakk>A : U;  B : U\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A"
+proof -
+  fix x
+  assume
+    "A : U" and
+    "B : U" and
+    "x : A"
+  then have "\<^bold>\<lambda>y. x : B\<rightarrow>A" by (rule Prod_intro)
+    
+qed
+
+section \<open>Nats\<close>
+
+text "Here's a dumb proof that 2 is a natural number."
+
+lemma "succ(succ 0) : Nat"
+proof -
+  have "0 : Nat" by (rule Nat_intro1)
+  from this have "(succ 0) : Nat" by (rule Nat_intro2)
+  thus "succ(succ 0) : Nat" by (rule Nat_intro2)
+qed
+
+text "We can of course iterate the above for as many applications of \<open>succ\<close> as we like.
+The next thing to do is to implement induction to automate such proofs.
+
+When we get more stuff working, I'd like to aim for formalizing the encode-decode method to be able to prove the only naturals are 0 and those obtained from it by \<open>succ\<close>."
+
+end
\ No newline at end of file