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
