Re: [isabelle] Permutations

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.



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.


(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.