[isabelle-dev] Extending well-founded relations to (total) well-orders
c.sternagel at gmail.com
Thu Feb 21 05:58:38 CET 2013
how about adding Andrei's proof (discussed on isbelle-users) to
HOL/Library (or somewhere else)? I polished the latest version (see
PS: In case you are wondering: "Why is he interested in these results?"
Here is my original motivation: In term rewriting, termination tools
employ simplification orders (like the Knuth-Bendix order, the
lexicographic path order, ...) whose definition is often based on a
given well-partial-order as precedence. However, termination tools
typically use well-founded partial orders as precedences. Thus we need
to be able to extend a given well-founded (partial order) relation to a
well-partial-order when we want to apply the theoretical results about
simplification orders to proofs that are generated by termination tools.
(Since every total well-order is also a well-partial-order, this is
possible by the above mentioned results.)
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 9644 bytes
Desc: not available
More information about the isabelle-dev