*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Permutations*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 23 Jun 2016 12:24:57 +0200*In-reply-to*: <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de>*Organization*: TU Munich*References*: <576B942B.7090900@informatik.tu-muenchen.de> <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Hi all, Am 23.06.2016 um 10:02 schrieb Manuel Eberl: > It is not clear to me at all how these things can be unified. The > notions of permutations as âall lists with elements of a given > set/multiset/listâ and permutations as âa bijection from a finite sets > to itselfâ are clearly related, but how can this relation be formalised > in the best way? what I have in mind is a clarification of terminology here: permutations as functions and list permutations should be introduced in separate theories, where I guess that multisets as quotient type of permutated lists can absorb a lot of the latter. If an application needs this relation, it can still formalize it. I did not see any example for that in the theories. Am 23.06.2016 um 10:02 schrieb Manuel Eberl: > After dabbling with permutations a bit, I think that one may even want > to have a type of permutations, implemented with Mappings by default. Am 23.06.2016 um 11:01 schrieb Johannes HÃlzl: > The type "'a bij" would be nice. Note that a bijection is not necessarily a permutation: in a permutation, each element a has a finite order, ie. some n > 0 such that (f ^^ n) a = a. Am 23.06.2016 um 12:01 schrieb Christian Sternagel: > And in IsaFoR in > http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/968059663689/thys/Auxiliaries/Renaming.thy > > definition perms :: "('a \<Rightarrow> 'a) set" > where > "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}" > > typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set" > by standard (auto simp: perms_def) > > where permutations have a type parameter and thus we have local-based > application of permutations instead of type-class-based (but otherwise I > got everything from the Nominal2 development, thanks). I don't quite understand the last paragraph. Which type-class are you referring to? Cheers, Florian > In any case, any kind of change here will probably lead to a lot of > adjustments in every work that uses permutations. This reform will not > be an easy task. > > > 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.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:*Christian Sternagel

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

**Re: [isabelle] Permutations***From:*Manuel Eberl

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