*To*: Christian Sternagel <c.sternagel at gmail.com>, 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 17:13:53 +0200*In-reply-to*: <10dc4ec4-0d85-47bb-b3cd-21ae978ef39c@gmail.com>*Organization*: TU Munich*References*: <576B942B.7090900@informatik.tu-muenchen.de> <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de> <576BB8F9.2040402@informatik.tu-muenchen.de> <10dc4ec4-0d85-47bb-b3cd-21ae978ef39c@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

>> 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. I see. My conclusion is that an abstract type of permutations Abs_perm :: ('a => 'a) => 'a perm apply :: 'a perm => 'a => 'a affected :: 'a perm => 'a set where "a in affected p <--> apply p a != a" makes really sense. E.g. it is easy to define the order of an element: order :: 'a perm => 'a => nat order p a = Min {0 < n <= Suc (card (affected p)). (f ^^ n) a = a} Cheers, Florian > > 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.) >>>> >>> >> > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

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

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

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

**Re: [isabelle] Permutations***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] Permutations
- Next by Date: [isabelle] theory FSet exists twice
- Previous by Thread: Re: [isabelle] Permutations
- Next by Thread: [isabelle] Ordered Pair Definition
- 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