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



I played with a slightly different approach, and completed your "sorry", but there are two more further down :-(

But who knows, perhaps you can use this.

Larry Paulson

Attachment: Well_Order_Extension.thy
Description: Binary data


On 19 Feb 2013, at 04:50, Christian Sternagel <c.sternagel at gmail.com> wrote:

> After giving up on the alternative recipe for the moment, I went back to Larry's suggestion. And indeed, the existing proof could be modified in a straight-forward way (see the attached theory).
> 
> (Note that well-foundedness of the given partial order is irrelevant. So the actual lemma is: every partial order can be extended to a total well-order.)
> 
> Now, I'll check whether this is also applicable in my setting (with explicit domains).
> 
> Thanks for all your hints and suggestions! (I'm still interested in the alternative proof ;))
> 
> cheers
> 
> chris
> 
> On 02/19/2013 12:22 AM, Lawrence Paulson wrote:
>> I see, it is a little more subtle than I thought, but I would guess that the proof of the well-ordering theorem itself can be modified to exhibit a well-ordering that is consistent with a given well-founded relation. As I recall, the well-ordering theorem is proved by Zorn's lemma and considers the set of all well orderings of subsets of a given set; one would need to modify the argument to restrict attention to well orderings that were consistent with W.
>> 
>> Surely this theorem has a name and a proof can be found somewhere.
>> 
>> Larry
>> 
>> On 18 Feb 2013, at 14:55, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:
>> 
>>> Hi Larry,
>>> 
>>> As far as I understand your suggestion, it does not even yield a ordering. For example, suppose that there are three elements a, b, c such that the well ordering <R obtained by the well-ordering theorems orders them as a <R b <R c. Now, consider the well-founded relation <W which orders c <W a and nothing else. Then, c <TO a as c<W a, and a <TO b and b <TO c as neither a <W b, b <W a, b <W c, nor c <W b. Hence,
>>> 
>>> c <TO a <TO b <TO c
>>> 
>>> which violates the ordering properties. Or am I misunderstanding something?
>>> 
>>> Andreas
>>> 
>>> On 02/18/2013 03:18 PM, Lawrence Paulson wrote:
>>>> I still don't see what's wrong with the following approach:
>>>> 
>>>> 1. Prove the well ordering theorem (maybe it has been proved already).
>>>> 
>>>> 2. Obtain the desired total ordering as a lexicographic combination of the partial order with the total well ordering of your type
>>>> 
>>>> [More specifically: given W a well founded relation and R a well ordering obtained by the well ordering theorem, define TO x y == W x y | (~ W x y & ~W y x & R x y)]
>>>> 
>>>> Larry Paulson
>>>> 
>>>> 
>>>> On 18 Feb 2013, at 06:32, Christian Sternagel <c.sternagel at gmail.com> wrote:
>>>> 
>>>>> Dear Andrei,
>>>>> 
>>>>> finally deadlines are over for the time being and I found your email again ;)
>>>>> 
>>>>> On 01/19/2013 12:22 AM, Andrei Popescu wrote:
>>>>>> My AFP formalization ordinals
>>>>>> 
>>>>>> http://afp.sourceforge.net/entries/Ordinals_and_Cardinals.shtml
>>>>> 
>>>>> I guess since Isabelle2013 this is now "~~/src/HOL/Cardinals/", right?
>>>>> 
>>>>>> (hopefully) provides the necessary ingredients: Initial segments in
>>>>>> Wellorder_Embedding, ordinal sum in theory Constructions_on_Wellorders,
>>>>>> and a transfinite recursion combinator (a small adaptation of the
>>>>>> wellfounded combinator) in theory Wellorder_Relation.
>>>>> 
>>>>> Could you elaborate on the mentioned finite recursion combinator and how it is used?
>>>>> 
>>>>> thanks in advance,
>>>>> 
>>>>> chris
>>>>> 
>>>>> 
>>>>> 
>>>> 
>>>> 
>> 
> 
> <Well_Order_Extension.thy>



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