diff options
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Methods.thy | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 9a101e5..c314ed4 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -32,7 +32,7 @@ text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<ope Can also perform typechecking, and search for elements of a type." -method simple uses lems = (assumption | standard | rule lems)+ +method simple uses lems = (assumption | rule lems | standard)+ subsection \<open>Wellformedness checker\<close> @@ -62,13 +62,12 @@ method derive uses lems unfolds = ( subsection \<open>Simplification\<close> -text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> attempt to solve definitional equations by simplifying lambda applications. +text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> search for lambda applications to simplify and are suitable for solving definitional equalities, as well as harder proofs where \<open>derive\<close> fails. -\<open>simplify\<close> is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules. -In this case use \<open>rsimplify\<close> instead. +It is however not true that these methods are strictly stronger; if they fail to find a suitable substitution they will fail where \<open>derive\<close> may succeed. -Since these methods use \<open>derive\<close>, it is often (but not always) the case that theorems provable with \<open>derive\<close> are also provable with them. -(Whether this is the case depends on whether the call to \<open>subst (0) comp\<close> fails.)" +\<open>simplify\<close> is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules. +In this case use \<open>rsimplify\<close> instead." method rsimplify uses lems = (subst (0) comp, derive lems: lems)+ \<comment> \<open>\<open>subst\<close> performs an equational rewrite according to some computation rule declared as [comp], after which \<open>derive\<close> attempts to solve any new assumptions that arise.\<close> |