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:
recently I did a full text search concerning permutations and I found
that the existing material is quite dispersed.
* Predicates for permutations (functions)
* Permutations.permutation :: "('a â 'a) â bool"
* Permutations.permutes :: "('a â 'a) â 'a set â bool"
* Representation as swaps
* Permutations.swapidseq :: "nat â ('a â 'a) â bool"
* Permutations.evenperm :: "('a â 'a) â bool"
* Permutations.sign :: "('a â 'a) â int"
* 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"
* Missing_Permutations.signof :: "(nat â nat) â 'a"
* Representation as cycles
* Permuting lists
* Permutations.permute_list :: "(nat â nat) â 'a list â 'a list"
* Permutation.perm :: "'a list â 'a list â bool"
* btw that equivalence relation would be expressed better as Âmset xs = mset ysÂ anyway
* Derangements.derangements :: "nat set â (nat â nat) set"
* Derangements.count_derangements :: "nat â nat"
* Representation as association lists
* 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
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 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