*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 18 Feb 2013 15:55:21 +0100*Cc*: Andrei Popescu <uuomul at yahoo.com>, Christian Sternagel <c.sternagel at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <B44BA006-9FA9-45BA-8664-7D8FD10EAD90@cam.ac.uk>*References*: <1358522523.56111.YahooMailClassic@web120604.mail.ne1.yahoo.com> <5121CAFB.3040205@gmail.com> <B44BA006-9FA9-45BA-8664-7D8FD10EAD90@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130106 Thunderbird/17.0.2

Hi Larry,

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.shtmlI 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

**Follow-Ups**:**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:*Andrei Popescu

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

- 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