*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Permutations*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Thu, 23 Jun 2016 10:02:03 +0200*In-reply-to*: <576B942B.7090900@informatik.tu-muenchen.de>*References*: <576B942B.7090900@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

Cheers, Manuel On 23/06/16 09:47, Florian Haftmann wrote:

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.thyIn 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.)

**Follow-Ups**:**Re: [isabelle] Permutations***From:*Johannes Hölzl

**Re: [isabelle] Permutations***From:*Florian Haftmann

**References**:**[isabelle] Permutations***From:*Florian Haftmann

- Previous by Date: [isabelle] Permutations
- Next by Date: Re: [isabelle] Permutations
- Previous by Thread: [isabelle] Permutations
- 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