diff options
Diffstat (limited to '')
-rw-r--r-- | HoTT_Methods.thy | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 1f11230..9a101e5 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -13,11 +13,6 @@ theory HoTT_Methods begin -text "The methods \<open>simple\<close>, \<open>wellformed\<close>, \<open>derive\<close>, and \<open>simplify\<close> should together should suffice to automatically prove most HoTT theorems. -We also provide a method -" - - section \<open>Setup\<close> text "Import the \<open>subst\<close> method, used by \<open>simplify\<close>." @@ -67,9 +62,10 @@ method derive uses lems unfolds = ( subsection \<open>Simplification\<close> -text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> simplify lambda applications and attempt to solve definitional equations. +text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> attempt to solve definitional equations by simplifying lambda applications. -\<open>rsimplify\<close> can also be used to search for lambda expressions inhabiting given types. +\<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. 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.)" |