[isabelle-dev] Permutations

[Johannes Hölzl]

Ah sorry, my previous email should have been a response here.

Very nice!

One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?

 - Johannes

Am Montag, den 04.07.2016, 21:25 +0200 schrieb Florian Haftmann:
> 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/msg0009
> 1.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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev