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
permutations.
If anybody wants to push that work further, the agenda is roughly as
follows:
* Consolidate scattered material on permutations (functions) into
Library/Perm.thy (see my post
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-June/msg00091.html
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.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
