[isabelle-dev] Zorn's lemma, the well-ordering-theorem, and extending well-founded relations to (total) well-orders
c.sternagel at gmail.com
Fri Mar 1 06:49:07 CET 2013
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
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?
> --- 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.
> 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
> >>> 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
> >>> 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
> >>> - 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
> >>> 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
> >>>> attachment).
> >>>> cheers
> >>>> chris
> >>>> PS: In case you are wondering: "Why is he interested in these
> >>>> Here is my original motivation: In term rewriting, termination
> >>>> 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>
More information about the isabelle-dev