[isabelle-dev] Zorn's lemma, the well-ordering-theorem, and extending well-founded relations to (total) well-orders

[Christian Sternagel]

On 02/28/2013 11:46 PM, Andrei Popescu wrote:
> Hi Christian,
>
> I am back from a 3-day trip which prevented me from answering sooner.
>
> Many thanks for your contribution! I'll go ahead and integrate your new
> Isar proofs of existing theorems and your new theorems.  But, same as
> Larry, I do now quite understand why do you want to split Zorn and avoid
> certain dependencies.

Maybe I confused myself ;). If I remember correctly, I can only build 
the bitbucket repo, if I have the separate Ordinal_Sum, since 
Constructions_on_Wellorders contains a reference to well_order_on from 
the old Zorn. Thus it seems that for this case the dependencies have to 
change (such that we can use the ordinal sum in Well_Order_Embedding).

Ah, but I just see that you only wondered about the split of Zorn ...
Well, never mind. Let's just forget about the split ;) (I guess it is 
just personal taste that I prefer more smaller theories over fewer 
bigger ones).

Btw: The new name order-extension principle was nonsense, sorry (I 
backed this change out again). This is usually used to extend partial 
orders to total orders but says nothing about well-foundedness... does 
anybody have a better name, or should we stick to Well_Order_Extension?

cheers

chris

>
> Andrei
>
> --- On *Thu, 2/28/13, Lawrence Paulson /<lp15 at cam.ac.uk>/* wrote:
>
>
>     From: Lawrence Paulson <lp15 at cam.ac.uk>
>     Subject: Re: [isabelle-dev] Zorn's lemma, the well-ordering-theorem,
>     and extending well-founded relations to (total) well-orders
>     To: "Christian Sternagel" <c.sternagel at gmail.com>
>     Cc: "isabelle-dev"
>     <isabelle-dev at mailbroy.informatik.tu-muenchen.de>, "Andrei Popescu"
>     <uuomul at yahoo.com>
>     Date: Thursday, February 28, 2013, 4:04 PM
>
>     I'm all in favour of refactoring the proofs. That might occasion
>     moving material from one file to another. But I would keep that to a
>     minimum. It isn't unusual to go deep into the past when
>     investigating the origins of some issue.
>
>     Larry
>
>     On 27 Feb 2013, at 12:14, Christian Sternagel <c.sternagel at gmail.com
>     </mc/compose?to=c.sternagel at gmail.com>> wrote:
>
>      > Dear Larry
>      >
>      > please note that my proposal is not just about a split of the
>     existing theory Zorn.thy, but also about a modernization of part of
>     it (which I think makes it easier to understand, but I might be
>     wrong... could be that the main purpose of this experiment was just
>     to make me understand the formalized proofs ;)) as well as adding
>     new facts (the order-extension principle). So please consider it,
>     even if no split is done.
>      >
>      > Nevertheless. Separating facts that are about the subset relation
>     from the more general version of Zorn's lemma would make sense for
>     at least one purpose: reusing the former in developments that use a
>     different definition of partial order (and that are "incompatible"
>     with the latter).
>      >
>      > As to the point that a split would make examination of past
>     versions more difficult. How do you mean? True, it would be hard to
>     compare a version that comes somewhere after the split with one
>     somewhere before the split (via plain diff), but how often does that
>     happen? Isn't the typical use-case comparison of successive changesets?
>      >
>      > cheers
>      >
>      > chris
>      >
>      > On 02/27/2013 08:49 PM, Lawrence Paulson wrote:
>      >> I don't see the point of splitting Zorn into multiple files. It
>     isn't especially large. Such a change really has nothing to do with
>     the question of locating proved results, and it would make it harder
>     to examine past versions.
>      >> Larry
>      >>
>      >> On 27 Feb 2013, at 05:57, Christian Sternagel
>     <c.sternagel at gmail.com </mc/compose?to=c.sternagel at gmail.com>> wrote:
>      >>
>      >>> Dear all,
>      >>>
>      >>> in the meanwhile I had a close look at the existing Zorn.thy
>     (mostly to understand the proof myself) and came up with the
>     following proposal:
>      >>>
>      >>> see
>      >>>
>      >>>
>     https://bitbucket.org/csternagel/zorns-lemma-and-the-well-ordering-theorem/
>      >>>
>      >>> for the related hg repository (from which you will hopefully
>     merge into the Isabelle repo ;)).
>      >>>
>      >>> I propose the following changes to ~~/src/HOL/Cardinals and
>     ~~/src/HOL/Library.
>      >>>
>      >>> 1) Make facts about the ordinal sum available in a separate
>     theory, to avoid too early dependency on the old
>     ~~/src/HOL/Library/Zorn. This is a prerequisite to make the
>     remainder of my proposal work. (see Ordinal_Sum.thy)
>      >>>
>      >>> 2) Split the current Zorn.thy into three separate parts.
>      >>>
>      >>>  - Zorn_Subset.thy
>      >>>    Here we are only concerned with the special case of Zorn's
>     lemma for the subset relation. This constitutes a modernized version
>     of the old Zorn.thy, employing locales for structuring (cf. Andrei's
>     rel locale in ~~/src/HOL/Cardinals; I find this kind of structuring
>     very convenient) and only Isar proofs (some of the old apply scripts
>     were very brittle, e.g., using auto or simp as initial proof steps).
>     Hopefully it is also easier to understand than the old scripts (or
>     maybe it is just because I spend so much time with the proofs ;)).
>      >>>
>      >>>  - Zorn.thy
>      >>>    The general version of Zorn's lemma for arbitrary partial
>     orders.
>      >>>
>      >>>  - Well_Ordering_Theorem.thy
>      >>>    The well-ordering-theorem. It seems important enough to give
>     it it's own theory. Moreover, in the previous setup it seemed to be
>     easily overlooked (not even some Isabelle veterans knew whether it
>     was already formalized).
>      >>>
>      >>> 3) Add a formalization of the well-order extension theorem to
>     ~~/src/HOL/Library. (see Well_Order_Extension.thy)
>      >>>
>      >>> In My_Zorn.thy it is illustrated that the new structure is more
>     versatile than the old one. It is, e.g,. very easy to combine it
>     with my alternative definitions of partial orders (po_on from
>     AFP/Well_Quasi_Orders/Restricted_Predicates).
>      >>>
>      >>> cheers
>      >>>
>      >>> chris
>      >>>
>      >>> On 02/21/2013 01:58 PM, Christian Sternagel wrote:
>      >>>> Dear all,
>      >>>>
>      >>>> how about adding Andrei's proof (discussed on isbelle-users) to
>      >>>> HOL/Library (or somewhere else)? I polished the latest version
>     (see
>      >>>> attachment).
>      >>>>
>      >>>> cheers
>      >>>>
>      >>>> chris
>      >>>>
>      >>>> PS: In case you are wondering: "Why is he interested in these
>     results?"
>      >>>> Here is my original motivation: In term rewriting, termination
>     tools
>      >>>> employ simplification orders (like the Knuth-Bendix order, the
>      >>>> lexicographic path order, ...) whose definition is often based
>     on a
>      >>>> given well-partial-order as precedence. However, termination tools
>      >>>> typically use well-founded partial orders as precedences. Thus
>     we need
>      >>>> to be able to extend a given well-founded (partial order)
>     relation to a
>      >>>> well-partial-order when we want to apply the theoretical
>     results about
>      >>>> simplification orders to proofs that are generated by
>     termination tools.
>      >>>> (Since every total well-order is also a well-partial-order,
>     this is
>      >>>> possible by the above mentioned results.)
>      >>>>
>      >>>
>      >>> _______________________________________________
>      >>> isabelle-dev mailing list
>      >>> isabelle-dev at in.tum.de </mc/compose?to=isabelle-dev at in.tum.de>
>      >>>
>     https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>      >>
>      >
>