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
