*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:01:06 +0200*In-reply-to*: <m24m8kxnjr.fsf@kcl.ac.uk>*References*: <576B942B.7090900@informatik.tu-muenchen.de> <0f9a58ed-eeb9-7f36-360f-473a71fa2c25@in.tum.de> <1466672490.4846.4.camel@in.tum.de> <m24m8kxnjr.fsf@kcl.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

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). cheers chris On 06/23/2016 11:27 AM, Christian Urban wrote: > > ...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.) > > > > > > >

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

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

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

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

- 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