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
