*To*: Johannes Hölzl <hoelzl at in.tum.de>*Subject*: Re: [isabelle] Permutations*From*: Christian Urban <christian.urban at kcl.ac.uk>*Date*: Thu, 23 Jun 2016 10:27:36 +0100*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=christian.urban@kcl.ac.uk;*Cc*: cl-isabelle-users at lists.cam.ac.uk*References*: <576B942B.7090900@informatik.tu-muenchen.de> <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de> <1466672490.4846.4.camel@in.tum.de>*Reply-to*: christian.urban at kcl.ac.uk*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99

...and by transitivity also of course in Nominal1 in $src/HOL/Nominal/Nominal.thy type_synonym 'x prm = "('x \<times> 'x) list" ;o) Christian On Thursday, June 23, 2016 at 11:01:30 (+0200), Johannes HÃlzl wrote: > 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 Sternagel

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

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

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

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