*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Permutations*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Thu, 23 Jun 2016 11:01:30 +0200*In-reply-to*: <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de>*Organization*: TU München*References*: <576B942B.7090900@informatik.tu-muenchen.de> <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de>

There is also a special type of sort-respecting permutations in Nominal2: Â $AFP/Nominal2/Nominal2_Base.thy definition Â "perm \<equiv> {f. bij f \<and> finite {a. f a \<noteq> a} \<and> Â Â Â(<forall>a. sort_of (f a) = sort_of a)}" typedef perm = "perm" The type "'a bij" would be nice. Â- Johannes Am Donnerstag, den 23.06.2016, 10:02 +0200 schrieb Manuel Eberl: > You are right, this is pretty dispersed. To make matters worse, IÂ > recently committed something called "Set_Permutations" for the set > ofÂ > all distinct lists consisting of elements of a set. > > Additionally, I still have some old material lying around about the > setÂ > of all permutations of a multilist (and, as a direct consequence ofÂ > that, of a list). That should probably also be added at some point. > > > 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? > > After dabbling with permutations a bit, I think that one may even > wantÂ > to have a type of permutations, implemented with Mappings by default. > > 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.) > >

**Follow-Ups**:**Re: [isabelle] Permutations***From:*Christian Urban

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

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

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