Re: [isabelle] Permutations



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.