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

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?


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

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,


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