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. Andrei --- On Thu, 2/28/13, Lawrence Paulson <[email protected]> wrote: From: Lawrence Paulson <[email protected]> Subject: Re: [isabelle-dev] Zorn's lemma, the well-ordering-theorem, and extending well-founded relations to (total) well-orders To: "Christian Sternagel" <[email protected]> Cc: "isabelle-dev" <[email protected]>, "Andrei Popescu" <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 >>> [email protected] >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
