Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Request for feedback: dedicated session or AFP...


view this post on Zulip Email Gateway (Mar 11 2021 at 11:04):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear all,

combinatorics has been a repeating topic in private discussions over the
last years.

Currently I am working on a few additions to the distribution (e.g. more
connections between related concepts like »_ <~~> _«, »mset _= mset _«,
»permute_list«).

There are already quite well-developed theories on combinatorics,
covering binomial coefficients, stirling numbers, (finite) permutations,
counting principles etc., but they are scattered over different parts of
the distribution and AFP.

While some material has to reside where it is now due to dependencies,
there is clearly a set of theories which could be grouped in its own
session, with the option to turn it into an AFP entry later. This
session could also include a small document (similar in spirit to
Guide.thy in Word_Lib) to explain the existing material.

Any comments?

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Mar 11 2021 at 11:19):

From: Lawrence Paulson <lp15@cam.ac.uk>
A session consisting of material related to combinatorics certainly makes sense. It’s a very diverse topic however. For example, Ramsey theory belongs there. It will take some thought to organise properly.

Larry

view this post on Zulip Email Gateway (Mar 11 2021 at 11:41):

From: Manuel Eberl <eberlm@in.tum.de>
Florian already knows this, but just as a reminder: I am also working on
a major overhaul of permutations in HOL that is nicer to work with and
also contains some material that was missing so far (such as the
definition of a cycle, and the fact that every permutation is a
composition of disjoing cycles).

Or rather I was working on this – it's maybe 80–90% finished, but even
after it is finished 100%, there will be a large amount of work to be
done to integrate all of this with the existing material that uses
permutations.

Cheers,

Manuel
smime.p7s

view this post on Zulip Email Gateway (Mar 11 2021 at 19:06):

From: Tobias Nipkow <nipkow@in.tum.de>
I would welcome any move of material from the distribution to the AFP.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Mar 13 2021 at 07:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

I would welcome any move of material from the distribution to the AFP.

I would prefer that also – in the long run.

But there is a bootstrap problem: the material has to be identified and
accumulated first, and for organizational reasons this is easier in the
distribution. I don't know of a procedure to submit and empty AFP entry
which gets populated only over time.

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Mar 13 2021 at 13:46):

From: Tobias Nipkow <nipkow@in.tum.de>
On 13/03/2021 08:30, Florian Haftmann wrote:

I would welcome any move of material from the distribution to the AFP.

I would prefer that also – in the long run.

But there is a bootstrap problem: the material has to be identified and
accumulated first, and for organizational reasons this is easier in the
distribution. I don't know of a procedure to submit and empty AFP entry
which gets populated only over time.

That is indeed a bit tricky. If you find some coherent material that nothing
else in the distribution depends on, I recommend to turn it into an AFP entry.
That entry can of course grow over time (or spawn further entries), but you
don't want to start with an empty entry. Then there is the question of the title
if it is meant to grow over time...

Tobias

Cheers,
Florian

smime.p7s


Last updated: Dec 05 2021 at 22:18 UTC