[isabelle-dev] Extending well-founded relations to (total) well-orders

[Christian Sternagel]

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>