*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] extending well-founded partial orders to total well-founded orders*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Tue, 19 Feb 2013 16:43:53 +1100*In-reply-to*: <512304A3.8020609@gmail.com>*References*: <1358522523.56111.YahooMailClassic@web120604.mail.ne1.yahoo.com> <5121CAFB.3040205@gmail.com> <B44BA006-9FA9-45BA-8664-7D8FD10EAD90@cam.ac.uk> <512240D9.7030003@inf.ethz.ch> <5A47F103-8F19-47FF-8BA5-04F6DBF18F16@cam.ac.uk> <512304A3.8020609@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

I suspect the sorry in this proof is important.

Yours, Thomas. On 19/02/13 15:50, Christian Sternagel wrote:

After giving up on the alternative recipe for the moment, I went backto Larry's suggestion. And indeed, the existing proof could bemodified 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 totalwell-order.)Now, I'll check whether this is also applicable in my setting (withexplicit domains).Thanks for all your hints and suggestions! (I'm still interested inthe 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 guessthat the proof of the well-ordering theorem itself can be modified toexhibit a well-ordering that is consistent with a given well-foundedrelation. As I recall, the well-ordering theorem is proved by Zorn'slemma and considers the set of all well orderings of subsets of agiven set; one would need to modify the argument to restrictattention to well orderings that were consistent with W.Surely this theorem has a name and a proof can be found somewhere. LarryOn 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 aordering. For example, suppose that there are three elements a, b, csuch that the well ordering <R obtained by the well-orderingtheorems orders them as a <R b <R c. Now, consider the well-foundedrelation <W which orders c <W a and nothing else. Then, c <TO a asc<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 cwhich violates the ordering properties. Or am I misunderstandingsomething?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 combinationof the partial order with the total well ordering of your type[More specifically: given W a well founded relation and R a wellordering obtained by the well ordering theorem, define TO x y == Wx y | (~ W x y & ~W y x & R x y)]Larry PaulsonOn 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 youremail 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 inWellorder_Embedding, ordinal sum in theoryConstructions_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 combinatorand how it is used?thanks in advance, 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 (simp add: partial_order_on_def preorder_on_def) apply (safe, simp_all add: int_less_def) apply (rule ccontr) apply (subgoal_tac "b < a") apply (erule notE, erule(1) antisymD) apply auto[1] apply simp apply auto[1] 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 add: int_less_def) apply simp done lemma False: "False" using well_ordering_extension[OF Partial_order_int_less] apply clarsimp apply (drule int_less_subset) apply (simp add: well_order_on_def linear_order_on_def) apply (simp add: well_order_on_def not_wf_int_less) done end

**Follow-Ups**:**Re: [isabelle] extending well-founded partial orders to total well-founded orders***From:*Christian Sternagel

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

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

**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:*Christian Sternagel

- 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