Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!

1 files changed, 15 insertions, 14 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 7453883..2ad0ac5 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -7,7 +7,7 @@ Basic setup of a homotopy type theory object logic with a cumulative Russell-sty
 *)
 
 theory HoTT_Base
-imports Pure "HOL-Eisbach.Eisbach"
+imports Pure
 
 begin
 
@@ -18,17 +18,14 @@ typedecl t  \<comment> \<open>Type of object types and terms\<close>
 typedecl ord  \<comment> \<open>Type of meta-level numerals\<close>
 
 axiomatization
-  O :: ord and
+  O   :: ord and
   Suc :: "ord \<Rightarrow> ord" and
-  lt :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999)
+  lt  :: "[ord, ord] \<Rightarrow> prop"  (infix "<" 999) and
+  leq :: "[ord, ord] \<Rightarrow> prop"  (infix "\<le>" 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 \<open>Method @{method proveSuc} proves statements of the form \<open>n < (Suc (... (Suc n) ...))\<close>.\<close>
+  leq_min [intro]: "O \<le> n"
 
 
 section \<open>Judgment\<close>
@@ -42,15 +39,15 @@ axiomatization
   U :: "ord \<Rightarrow> t"
 where
   U_hierarchy: "i < j \<Longrightarrow> U i: U j" and                               
-  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j"
+  U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and
+  U_cumulative': "\<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>
 
-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>
+@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}.
+\<close>
 
 
 section \<open>Type families\<close>
@@ -68,11 +65,15 @@ type_synonym tf = "t \<Rightarrow> t"  \<comment> \<open>Type of type families\<
 section \<open>Named theorems\<close>
 
 named_theorems comp
+named_theorems form
 
 text \<open>
 Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}.
-@{attribute comp} declares computation rules.
-These are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting.
+
+@{attribute form} declares type formation rules.
+These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes.
 \<close>
 
 (* Todo: Set up the Simplifier! *)