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



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






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