*To*: Isabelle-Users Mailinglist <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Permutations*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 23 Jun 2016 09:47:55 +0200*Organization*: TU Munich*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Hi all, recently I did a full text search concerning permutations and I found that the existing material is quite dispersed. > * Predicates for permutations (functions) > * Library/Permutations.thy > * Permutations.permutation :: "('a â 'a) â bool" > * Permutations.permutes :: "('a â 'a) â 'a set â bool" > * Representation as swaps > * Library/Permutations.thy > * Permutations.swapidseq :: "nat â ('a â 'a) â bool" > * Permutations.evenperm :: "('a â 'a) â bool" > * Permutations.sign :: "('a â 'a) â int" > * Planarity_Certificates/Planarity/Permutations_2.thy > * Permutations_2.funswapid :: "'a â 'a â 'a â 'a" > * Permutations_2.perm_swap :: "'a â 'a â ('a â 'a) â 'a â 'a" > * Permutations_2.perm_rem :: "'a â ('a â 'a) â 'a â 'a" > * Jordan_Normal_Form/Missing_Permutations.thy > * Missing_Permutations.signof :: "(nat â nat) â 'a" > * Representation as cycles > * Planarity_Certificates/Planarity/Executable_Permutations.thy > * Permuting lists > * Library/Permutations.thy > * Permutations.permute_list :: "(nat â nat) â 'a list â 'a list" > * Library/Permutation.thy > * Permutation.perm :: "'a list â 'a list â bool" > * btw that equivalence relation would be expressed better as Âmset xs = mset ysÂ anyway > * Derangements > * Derangements/Derangements.thy > * Derangements.derangements :: "nat set â (nat â nat) set" > * Derangements.count_derangements :: "nat â nat" > * Representation as association lists > * Library/Permutations.thy > * Permutations.list_permutes :: "('a Ã 'a) list â 'a set â bool" > * Permutations.permutation_of_list :: "('a Ã 'a) list â 'a â 'a" > * Permutations.inverse_permutation_of_list :: "('a Ã 'a) list â 'a â 'a" > * Various theorems > * Jordan_Normal_Form/Missing_Permutations.thy > * Completeness/PermutationLemmas.thy In the mid-run there is clearly room for improvement here. I would suggest one theory Library/Permutation.thy which introduces the basics (predicates, swaps, cycles) consistently with all available corresponding theorems. The more specialized things (association lists etc) could go to separate theories. But this rough sketch has still time for consideration. Cheers, Florian (For the curious, I stumbled over that issue as follows: first, I inspected the sources for occurrences of Âno_notationÂ since these are possible candidates to user syntax bundles; one of these has been the infix syntax Â_ choose _Â for binomial coefficients, which lead me to reconsider other combinatorial coefficients (Stirling numbers) as well; hence the interest in permutations.) -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Permutations***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Specification.definition: Getting theorem for Const, not Free?
- Next by Date: Re: [isabelle] Permutations
- Previous by Thread: [isabelle] CfP: F-IDE2016, 3rd Workshop on Formal Integrated Development Environment
- Next by Thread: Re: [isabelle] Permutations
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list