diff options
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 29 |
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! *) |