*To*: Lawrence Paulson <lp15 at cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Mon, 18 Feb 2013 07:27:46 -0800 (PST)*Cc*: Christian Sternagel <c.sternagel at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <512240D9.7030003@inf.ethz.ch>

Hi Larry, To prevent Andreas's counterexample, there is no way but to choose the well-ordering in a manner that respects W, namely, as follows: The minimal elements of W, say, forming the set M0, should come first. Then should come the minimal elements of what is left in W after removing M0, say, M1, and so on. My transfinite construction does just that: it well-orders each M_i and puts the M_i's together as M0 < M1 < M2 < ... Andrei --- On Mon, 2/18/13, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> Subject: Re: [isabelle] extending well-founded partial orders to total well-founded orders To: "Lawrence Paulson" <lp15 at cam.ac.uk> Cc: "Christian Sternagel" <c.sternagel at gmail.com>, "Andrei Popescu" <uuomul at yahoo.com>, cl-isabelle-users at lists.cam.ac.uk Date: Monday, February 18, 2013, 4:55 PM 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 >> >> >> > >

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

- Previous by Date: Re: [isabelle] extending well-founded partial orders to total well-founded orders
- Next by Date: [isabelle] Conf. Intelligent Computer Mathematics (CICM 2013), July 8-12, 2013, Bath, UK
- 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