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

```I suspect the sorry in this proof is important.

```
Among other things, I can demonstrate a contradiction from your result, as shown in the attached theory. This is intuitive - if I begin with a partial order with an infinite descending chain, all containing orders must also contain said chain.
```
Yours,
Thomas.

On 19/02/13 15:50, Christian Sternagel 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?
```

chris

```
```

```
```
```
```
```
```theory False

imports "~/Well_Order_Extension"

begin

definition
"int_less = {(x, (y :: int)). x < y}"

text {* If the less-than relation on integers is a subset of a partial
relation, then it is the partial relation. *}
lemma int_less_subset:
"\<lbrakk> int_less <= r; Partial_order r \<rbrakk> \<Longrightarrow> (r - Id) = int_less"
apply (rule ccontr)
apply (subgoal_tac "b < a")
apply (erule notE, erule(1) antisymD)
apply auto
apply simp
apply auto
done

lemma field_id: "Field Id = UNIV"
by (auto simp: Field_def)

lemma Partial_order_int_less: "Partial_order (int_less Un Id)"
apply (simp add: partial_order_on_def preorder_on_def refl_on_def
field_id)
apply (auto simp: int_less_def intro!: transI antisymI)
done

lemma not_wf_int_less:
"\<not> wf int_less"
apply clarsimp
apply (drule_tac P="\<lambda>x. x > 0" and a=0 in wf_induct)
apply (drule_tac x="x - 1" in spec)
apply simp
done

lemma False: "False"
using well_ordering_extension[OF Partial_order_int_less]
apply clarsimp
apply (drule int_less_subset)