*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Permutations*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Thu, 23 Jun 2016 12:56:46 +0200*In-reply-to*: <576BB8F9.2040402@informatik.tu-muenchen.de>*References*: <576B942B.7090900@informatik.tu-muenchen.de> <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de> <576BB8F9.2040402@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

On 06/23/2016 12:24 PM, Florian Haftmann wrote: > 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? I was referring to Nominal(2) and the type-class of "permutation-types" (i.e., types whose inhabitants allow application of permutations). So this is not strictly about permutations but just about a specific application of them. cheers chris > > 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.) >>> >> >

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Permutations***From:*Florian Haftmann

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

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

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

- 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