[isabelle-dev] Permutations

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Jul 4 21:25:43 CEST 2016

Hi all,
see 59803048b0e8 for some basic facts about almost everywhere bijections
aka permutations. Maybe this will become a convenient coagulation point
for various scattered material in the future.
It turned out quite ambitious to formulate basic properties, e.g.
circularity. I did not search for any literature because I thought that
things covered in introductory courses should be straightforward to
formalize ;-).
My original interest had been cycles, but I realized that this needs
more work than I am willing to spend here, even more since I further
realized that the combinatorial interpretation of first Stirling numbers
can work just on cycles without need of their interpretation as
If anybody wants to push that work further, the agenda is roughly as
* Consolidate scattered material on permutations (functions) into
Library/Perm.thy (see my post
for further details).
* Gradually abandon Library/Permutation with its equivalence relation
‹perm› – it is much easier to reason about equality on multisets ‹mset
xs = mset ys›. There is also no equivalence relation ‹same_elems :: 'a
list ⇒ 'a list ⇒ bool›, but we write just ‹set xs = set ys›, for the
same and good reason.

I still have some work regarding cycles and combinatorial functions in
the drawer which I hope to finish gradually over time.


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20160704/0d7b20ac/attachment.asc>

More information about the isabelle-dev mailing list