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

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

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

From: Tobias Nipkow <nipkow@in.tum.de>

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

Tobias

smime.p7s

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

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

Last updated: Dec 05 2021 at 22:18 UTC