*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 19 Feb 2013 22:59:51 +0000*Cc*: Andrei Popescu <uuomul at yahoo.com>, cl-isabelle-users at lists.cam.ac.uk, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <512304A3.8020609@gmail.com>*References*: <1358522523.56111.YahooMailClassic@web120604.mail.ne1.yahoo.com> <5121CAFB.3040205@gmail.com> <B44BA006-9FA9-45BA-8664-7D8FD10EAD90@cam.ac.uk> <512240D9.7030003@inf.ethz.ch> <5A47F103-8F19-47FF-8BA5-04F6DBF18F16@cam.ac.uk> <512304A3.8020609@gmail.com>

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**

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>

**References**:**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Lawrence Paulson

**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Andreas Lochbihler

**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Lawrence Paulson

**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Next by Date: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Previous by Thread: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Next by Thread: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list