Re: [isabelle] Question concerning HOAS
On 05/16/2011 02:34 PM, Andreas Lochbihler wrote:
Well-foundedness of the subterm relation will also help you a lot when
you try to prove termination for functions defined with the function
package. Alex might be able to tell you more about how to set it up such
that the function package can use wf_tree_subterm.
It won't use it automatically, since automated termination proving is
based on measure functions into natural numbers only. However, you can
use such a subterm relation in manual termination proofs, e.g., using
the "relation" method.
This archive was generated by a fusion of
Pipermail (Mailman edition) and