Email Gateway (Aug 22 2022 at 13:27): Email Gateway (Aug 22 2022 at 13:27):From: Christian Sternagel <c.sternagel@gmail.com>
On 06/23/2016 12:24 PM, Florian Haftmann wrote:
Hi all,
Am 23.06.2016 um 10:02 schrieb Manuel Eberl:
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?what I have in mind is a clarification of terminology here: permutations
as functions and list permutations should be introduced in separate
theories, where I guess that multisets as quotient type of permutated
lists can absorb a lot of the latter.If an application needs this relation, it can still formalize it. I did
not see any example for that in the theories.Am 23.06.2016 um 10:02 schrieb Manuel Eberl:
After dabbling with permutations a bit, I think that one may even want
to have a type of permutations, implemented with Mappings by default.Am 23.06.2016 um 11:01 schrieb Johannes Hölzl:
The type "'a bij" would be nice.
Note that a bijection is not necessarily a permutation: in a
permutation, each element a has a finite order, ie. some n > 0 such that
(f ^^ n) a = a.Am 23.06.2016 um 12:01 schrieb Christian Sternagel:
And in IsaFoR in
definition perms :: "('a \<Rightarrow> 'a) set"
where
"perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
by standard (auto simp: perms_def)where permutations have a type parameter and thus we have local-based
application of permutations instead of type-class-based (but otherwise I
got everything from the Nominal2 development, thanks).I don't quite understand the last paragraph. Which type-class are you
referring to?
I was referring to Nominal(2) and the type-class of "permutation-types"
(i.e., types whose inhabitants allow application of permutations). So
this is not strictly about permutations but just about a specific
application of them.
cheers
chris
Cheers,
FlorianIn 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.thyIn 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.)
Email Gateway (Aug 22 2022 at 13:27):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Am 23.06.2016 um 10:02 schrieb Manuel Eberl:
After dabbling with permutations a bit, I think that one may even want
to have a type of permutations, implemented with Mappings by default.Am 23.06.2016 um 11:01 schrieb Johannes Hölzl:
The type "'a bij" would be nice.
Note that a bijection is not necessarily a permutation: in a
permutation, each element a has a finite order, ie. some n > 0 such that
(f ^^ n) a = a.Am 23.06.2016 um 12:01 schrieb Christian Sternagel:
And in IsaFoR in
definition perms :: "('a \<Rightarrow> 'a) set"
where
"perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
by standard (auto simp: perms_def)where permutations have a type parameter and thus we have local-based
application of permutations instead of type-class-based (but otherwise I
got everything from the Nominal2 development, thanks).I don't quite understand the last paragraph. Which type-class are you
referring to?I was referring to Nominal(2) and the type-class of "permutation-types"
(i.e., types whose inhabitants allow application of permutations). So
this is not strictly about permutations but just about a specific
application of them.
I see.
My conclusion is that an abstract type of permutations
Abs_perm :: ('a => 'a) => 'a perm
apply :: 'a perm => 'a => 'a
affected :: 'a perm => 'a set
where "a in affected p <--> apply p a != a"
makes really sense. E.g. it is easy to define the order of an element:
order :: 'a perm => 'a => nat
order p a =
Min {0 < n <= Suc (card (affected p)). (f ^^ n) a = a}
Cheers,
Florian
cheers
chris
Cheers,
FlorianIn 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.thyIn 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.)
Email Gateway (Aug 22 2022 at 13:39):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
recently I did a full text search concerning permutations and I found
that the existing material is quite dispersed.
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.)
signature.asc
Email Gateway (Aug 22 2022 at 13:39):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:39):From: Johannes Hölzl <hoelzl@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:39):From: Christian Urban <christian.urban@kcl.ac.uk>
...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.)
Email Gateway (Aug 22 2022 at 13:39):From: Christian Sternagel <c.sternagel@gmail.com>
And in IsaFoR in
http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/968059663689/thys/Auxiliaries/Renaming.thy
definition perms :: "('a \<Rightarrow> 'a) set"
where
"perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
by standard (auto simp: perms_def)
where permutations have a type parameter and thus we have local-based
application of permutations instead of type-class-based (but otherwise I
got everything from the Nominal2 development, thanks).
cheers
chris
Email Gateway (Aug 22 2022 at 13:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
Am 23.06.2016 um 10:02 schrieb Manuel Eberl:
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?
what I have in mind is a clarification of terminology here: permutations
as functions and list permutations should be introduced in separate
theories, where I guess that multisets as quotient type of permutated
lists can absorb a lot of the latter.
If an application needs this relation, it can still formalize it. I did
not see any example for that in the theories.
Am 23.06.2016 um 10:02 schrieb Manuel Eberl:
After dabbling with permutations a bit, I think that one may even want
to have a type of permutations, implemented with Mappings by default.
Am 23.06.2016 um 11:01 schrieb Johannes Hölzl:
The type "'a bij" would be nice.
Note that a bijection is not necessarily a permutation: in a
permutation, each element a has a finite order, ie. some n > 0 such that
(f ^^ n) a = a.
Am 23.06.2016 um 12:01 schrieb Christian Sternagel:
And in IsaFoR in
definition perms :: "('a \<Rightarrow> 'a) set"
where
"perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
by standard (auto simp: perms_def)where permutations have a type parameter and thus we have local-based
application of permutations instead of type-class-based (but otherwise I
got everything from the Nominal2 development, thanks).
I don't quite understand the last paragraph. Which type-class are you
referring to?
Cheers,
Florian
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.thyIn 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.)
Last updated: Nov 21 2024 at 12:39 UTC