1 files changed, 41 insertions, 58 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 916f6aa..07fbfc4 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,94 +1,77 @@
 (*  Title:  HoTT/HoTT_Base.thy
-    Author: Josh Chen
+    Author: Joshua Chen
 
-Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell.
+Basic setup of a homotopy type theory object logic with a Russell-style cumulative universe hierarchy.
 *)
 
 theory HoTT_Base
-  imports Pure
+imports
+  Pure
+  "HOL-Eisbach.Eisbach"
+
 begin
 
 
-section \<open>Foundational definitions\<close>
+section \<open>Basic setup\<close>
 
-text "Meta syntactic type for object-logic types and terms."
+typedecl t  \<comment> \<open>Type of object types and terms\<close>
+typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
 
-typedecl Term
+axiomatization
+  O :: ord and
+  Suc :: "ord \<Rightarrow> ord" and
+  lt :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999)
+where
+  lt_Suc [intro]: "n < (Suc n)" and
+  lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and
+  Suc_monotone [simp]: "m < n \<Longrightarrow> (Suc m) < (Suc n)"
 
+method proveSuc = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+)
 
-text "
-  Formalize the typing judgment \<open>a: A\<close>.
-  For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it.
-"
+text \<open>Method @{method proveSuc} proves statements of the form \<open>n < (Suc (... (Suc n) ...))\<close>.\<close>
 
-judgment has_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_:/ _)" [0, 0] 1000)
 
+section \<open>Judgment\<close>
 
-section \<open>Universe hierarchy\<close>
+judgment hastype :: "[t, t] \<Rightarrow> prop"  ("(3_:/ _)")
 
-text "Finite meta-ordinals to index the universes."
 
-typedecl Ord
+section \<open>Universes\<close>
 
 axiomatization
-  O :: Ord and
-  S :: "Ord \<Rightarrow> Ord"  ("S _" [0] 1000) and
-  lt :: "[Ord, Ord] \<Rightarrow> prop"  (infix "<" 999) and
-  leq :: "[Ord, Ord] \<Rightarrow> prop"  (infix "\<le>" 999)
+  U :: "ord \<Rightarrow> t"
 where
-  lt_min: "\<And>n. O < S n"
-and
-  lt_monotone1: "\<And>n. n < S n"
-and
-  lt_monotone2: "\<And>m n. m < n \<Longrightarrow> S m < S n"
-and
-  leq_min: "\<And>n. O \<le> n"
-and
-  leq_monotone1: "\<And>n. n \<le> S n"
-and
-  leq_monotone2: "\<And>m n. m \<le> n \<Longrightarrow> S m \<le> S n"
-
-lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2
-  \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close>
-
-text "Define the universe types."
+  U_hierarchy: "i < j \<Longrightarrow> U i: U j" and                               
+  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j"
 
-axiomatization
-  U :: "Ord \<Rightarrow> Term"
-where
-  U_hierarchy: "\<And>i j. i < j \<Longrightarrow> U i: U j"
-and
-  U_cumulative: "\<And>A i j. \<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j"
+text \<open>
+Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination.
+One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably.
+\<close>
 
-text "
-  The rule \<open>U_cumulative\<close> is very unsafe: if used as-is it will usually lead to an infinite rewrite loop!
-  To avoid this, it should be instantiated before being applied.
-"
+method cumulativity = (elim U_cumulative, proveSuc)  \<comment> \<open>Proves \<open>A: U i \<Longrightarrow> A: U (Suc (... (Suc i) ...))\<close>.\<close>
+method hierarchy = (rule U_hierarchy, proveSuc)  \<comment> \<open>Proves \<open>U i: U (Suc (... (Suc i) ...)).\<close>\<close>
 
 
 section \<open>Type families\<close>
 
-text "
-  The following abbreviation constrains the output type of a meta lambda expression when given input of certain type.
-"
-
-abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop"  ("(1_: _ \<longrightarrow> _)")
+abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop"  ("(1_:/ _ \<longrightarrow> _)")
   where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)"
 
-text "
-  The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types.
-"
+text \<open>
+The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"} where @{term "A::t"} and @{term "B::t"} are small types.
+\<close>
 
-type_synonym Typefam = "Term \<Rightarrow> Term"
+type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families.\<close>
 
 
 section \<open>Named theorems\<close>
 
-text "
-  Named theorems to be used by proof methods later (see HoTT_Methods.thy).
-  
-  \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
-"
+text \<open>
+Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
+\<open>wellform\<close> declares necessary well-formedness conditions for type and inhabitation judgments.
+\<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+\<close>
 
 named_theorems wellform
 named_theorems comp