diff options
| -rw-r--r-- | HoTT_Base.thy | 10 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 5 |
2 files changed, 13 insertions, 2 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index ee36af4..e36b237 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -51,11 +51,18 @@ where 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" +lemma U_hierarchy': "U i: U (Suc i)" by (fact U_hierarchy[OF lt_Suc]) + +declare U_hierarchy' [intro!] + text \<open> Using method @{method rule} with @{thm U_cumulative} and @{thm U_cumulative'} is unsafe: if applied blindly it will very easily lead to non-termination. Instead use @{method elim}, or instantiate the rules suitably. @{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}. + +@{thm U_hierarchy'} is declared with safe @{attribute intro} to be used by the method @{theory_text derive} to handle the universe hierarchy. +Note that @{thm U_hierarchy} is unsafe. \<close> @@ -69,6 +76,9 @@ text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" ("&_" [0] 3) where "&A \<equiv> \<lambda>_. A" +abbreviation (input) Id :: "t \<Rightarrow> t" where "Id \<equiv> \<lambda>x. x" +\<comment> \<open>NOTE: removing the input attribute causes term evaluations and even theorem attribute declarations to loop! Possible bug?\<close> + section \<open>Named theorems\<close> diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 27f252b..e45608e 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -64,11 +64,12 @@ section \<open>Derivation search\<close> text \<open> The method @{theory_text derive} combines @{method routine} and @{method compute} to search for derivations of judgments. -It also handles universes using @{method hierarchy} and @{method cumulativity}. +It also handles universes using @{method cumulativity}. +The method @{method hierarchy} has been observed to cause looping in previous versions, and is hence no longer part of @{theory_text derive}. \<close> method derive uses lems declares comp = - (routine add: lems | compute add: lems comp: comp | cumulativity form: lems | hierarchy)+ + (routine add: lems | compute add: lems comp: comp | cumulativity form: lems)+ section \<open>Additional method combinators\<close> |