[isabelle-dev] Extending well-founded relations to (total) well-orders
Christian Sternagel
c.sternagel at gmail.com
Thu Feb 21 05:58:38 CET 2013
Dear all,
how about adding Andrei's proof (discussed on isbelle-users) to
HOL/Library (or somewhere else)? I polished the latest version (see
attachment).
cheers
chris
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...
Name: Well_Order_Extension.thy
Type: application/x-example
Size: 9644 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130221/8e040ae0/attachment.bin>
More information about the isabelle-dev
mailing list