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.

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.