hoelzl at in.tum.de
Tue Jul 5 10:19:41 CEST 2016
Ah sorry, my previous email should have been a response here.
One question: why did you only set it up for monoid_mult and inverse,
and not as a ab_group_mult?
Am Montag, den 04.07.2016, 21:25 +0200 schrieb Florian Haftmann:
> Hi all,
> see 59803048b0e8 for some basic facts about almost everywhere
> aka permutations. Maybe this will become a convenient coagulation
> 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
> 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
> 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
> xs = mset ys›. There is also no equivalence relation ‹same_elems ::
> 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
> the drawer which I hope to finish gradually over time.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev