[isabelle] Permutations



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

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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