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
bigger ones).
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?
cheers
chris
Andrei
--- On *Thu, 2/28/13, Lawrence Paulson /<l...@cam.ac.uk>/* wrote:
From: Lawrence Paulson <l...@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.sterna...@gmail.com>
Cc: "isabelle-dev"
<isabelle-dev@mailbroy.informatik.tu-muenchen.de>, "Andrei Popescu"
<uuo...@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.
Larry
On 27 Feb 2013, at 12:14, Christian Sternagel <c.sterna...@gmail.com
</mc/compose?to=c.sterna...@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.sterna...@gmail.com </mc/compose?to=c.sterna...@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
>>>
>>>
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
>>> isabelle-...@in.tum.de </mc/compose?to=isabelle-...@in.tum.de>
>>>
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
