Re: [isabelle] extending well-founded partial orders to total well-founded orders

Hi Andrei,

now it was verbose enough for me ;)

On 02/20/2013 07:50 PM, Andrei Popescu wrote:
"dclosed (Field R0) W" holds since R0 is in K.  You probably were
referring to the extension of R0 with a0---let us call it R1. See below.

yes, sorry for that.

I forgot to mention: a0 should be taken to be W-minimal in Field W -
Field R0.  This is where well-foundedness of W is used.
Now, with this proviso, we have "dclosed (Field R1) W".

That was the crucial point, thanks!

As for further extending R0 to have the field UNIV, you can use the
well-ordering theorem to obtain a well-order R on UNIV - Field R0, and
then perform R0 + R (the ordinal sum:all elements of R0 are smaller than
all those of R).

Also this easily worked out (thanks to your Cardinals library).

Thus we have:

Every well-founded relation can be extended to a well-order.

And as corollary, every well-founded relation can be extended to a total well-order.

Find the (not yet polished) proofs attached (I gather that calls to the smt method are nothing we want in finished proofs, right?).



Attachment: Well_Order_Extension.thy
Description: application/example

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