Re: [isabelle] Permutations



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