# Re: [isabelle] Permutations

```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.)
>  > > >
>  >
>

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.