Email Gateway (Jan 14 2025 at 19:16): Email Gateway (Jan 14 2025 at 19:16):From: Tobias Nipkow <nipkow@in.tum.de>
The expression "concat(replicate n xs)" occurs frequently in the area of formal
languages / combinatorics on words. That is why Stepan Holub and friends have
defined an infix operator
"xs \<^sup>@n = concat(replicate n xs)"
Because it has also cropped up in other places, I would like to define this
operator already in List (i.e. Main) and am wondering about the syntax:
^@ or ^^
The latter exists and is overloaded, which may require type annotations in a few
places but means it is more `standard'.
Any feedback on this proposal?
Tobias
Email Gateway (Jan 14 2025 at 19:43):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
In fact, I am myself rather neutral in this respect. I got used to the
notation ^@ we introduced to avoid conflicts, but I am still aware of
its being pretty non-standard.
Stepan
On 14-Jan-25 8:16 PM, Tobias Nipkow wrote:
The expression "concat(replicate n xs)" occurs frequently in the area
of formal languages / combinatorics on words. That is why Stepan Holub
and friends have defined an infix operator"xs \<^sup>@n = concat(replicate n xs)"
Because it has also cropped up in other places, I would like to define
this operator already in List (i.e. Main) and am wondering about the
syntax:^@ or ^^
The latter exists and is overloaded, which may require type
annotations in a few places but means it is more `standard'.Any feedback on this proposal?
Tobias
Email Gateway (Jan 14 2025 at 21:34):From: Tobias Nipkow <nipkow@in.tum.de>
On 14/01/2025 20:43, Stepan Holub (via cl-isabelle-users Mailing List) wrote:
In fact, I am myself rather neutral in this respect. I got used to the notation
^@ we introduced to avoid conflicts, but I am still aware of its being pretty
non-standard.
You already tried some other overloaded notation (maybe ^^?) and found there
were too many ambiguities that needed to be resolved?
Tobias
Stepan
On 14-Jan-25 8:16 PM, Tobias Nipkow wrote:
The expression "concat(replicate n xs)" occurs frequently in the area of
formal languages / combinatorics on words. That is why Stepan Holub and
friends have defined an infix operator"xs \<^sup>@n = concat(replicate n xs)"
Because it has also cropped up in other places, I would like to define this
operator already in List (i.e. Main) and am wondering about the syntax:^@ or ^^
The latter exists and is overloaded, which may require type annotations in a
few places but means it is more `standard'.Any feedback on this proposal?
Tobias
Email Gateway (Jan 15 2025 at 10:08):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
I tried it now, and annotations are needed only very exceptionally.
Stepan
On 14-Jan-25 10:33 PM, Tobias Nipkow wrote:
On 14/01/2025 20:43, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:In fact, I am myself rather neutral in this respect. I got used to
the notation ^@ we introduced to avoid conflicts, but I am still
aware of its being pretty non-standard.You already tried some other overloaded notation (maybe ^^?) and found
there were too many ambiguities that needed to be resolved?Tobias
Stepan
On 14-Jan-25 8:16 PM, Tobias Nipkow wrote:
The expression "concat(replicate n xs)" occurs frequently in the
area of formal languages / combinatorics on words. That is why
Stepan Holub and friends have defined an infix operator"xs \<^sup>@n = concat(replicate n xs)"
Because it has also cropped up in other places, I would like to
define this operator already in List (i.e. Main) and am wondering
about the syntax:^@ or ^^
The latter exists and is overloaded, which may require type
annotations in a few places but means it is more `standard'.Any feedback on this proposal?
Tobias
Email Gateway (Jan 26 2025 at 14:43):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
A propos: a more ambitious question, certainly considered before, is
whether lists with append and Nil deserve to be instantiated as
monoid_mult. After all, they are /the/ free monoid. Then we would simply
have ^.
Stepan
On 14-Jan-25 8:16 PM, Tobias Nipkow wrote:
The expression "concat(replicate n xs)" occurs frequently in the area
of formal languages / combinatorics on words. That is why Stepan Holub
and friends have defined an infix operator"xs \<^sup>@n = concat(replicate n xs)"
Because it has also cropped up in other places, I would like to define
this operator already in List (i.e. Main) and am wondering about the
syntax:^@ or ^^
The latter exists and is overloaded, which may require type
annotations in a few places but means it is more `standard'.Any feedback on this proposal?
Tobias
Email Gateway (Jan 26 2025 at 14:57):From: Florian Haftmann <florian.haftmann@cit.tum.de>
A propos: a more ambitious question, certainly considered before, is
whether lists with append and Nil deserve to be instantiated as
monoid_mult. After all, they are /the/ free monoid. Then we would simply
have ^.
The interpretation is already there:
https://isabelle.sketis.net/repos/isabelle/file/tip/src/HOL/List.thy#l945
I don’t recall whether there was once a deliberate decision not to make
it a full type class instance – but beware that this will preclude any
different instantiation users might want for specific applications.
But there is nothing wrong providing that instantiation in a separate
library theory.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jan 26 2025 at 15:13):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Yes, I fully understand that instantiation policy should be cautious and
conservative, although I wonder whether concatenation is not the only
reasonable instance of monoid multiplication for lists. My point was
that full instantiation would solve Tobias's question about concat
replicate in a simple and natural way.
Stepan
On 26-Jan-25 3:56 PM, Florian Haftmann wrote:
A propos: a more ambitious question, certainly considered before, is
whether lists with append and Nil deserve to be instantiated as
monoid_mult. After all, they are /the/ free monoid. Then we would
simply have ^.The interpretation is already there:
https://isabelle.sketis.net/repos/isabelle/file/tip/src/HOL/List.thy#l945I don’t recall whether there was once a deliberate decision not to
make it a full type class instance – but beware that this will
preclude any different instantiation users might want for specific
applications.But there is nothing wrong providing that instantiation in a separate
library theory.Cheers,
Florian
Email Gateway (Jan 26 2025 at 15:54):From: Tobias Nipkow <nipkow@in.tum.de>
Please note that I have very recently defined ^^ on lists and ported some of
Stepan's lemmas to List. However, this is not a final decision. I would be just
as happy with ^. In fact, I agree that this subtheory (with ^ or ^^) should go
into a separate theory. I would put it into the AFP for visibility (and because
List-Index is already there).
From the previous discussion it seems to me there should be a separate theory
List_Power that defines ^ on lists. Same as Stepan, I would argue it is the only
reasonable interpretation for ^ on lists. Moreover, there is still ^^ for other
interpretations.
Any objections?
Tobias
On 26/01/2025 16:13, Stepan Holub (via cl-isabelle-users Mailing List) wrote:
Yes, I fully understand that instantiation policy should be cautious and
conservative, although I wonder whether concatenation is not the only reasonable
instance of monoid multiplication for lists. My point was that full
instantiation would solve Tobias's question about concat replicate in a simple
and natural way.Stepan
On 26-Jan-25 3:56 PM, Florian Haftmann wrote:
A propos: a more ambitious question, certainly considered before, is whether
lists with append and Nil deserve to be instantiated as monoid_mult. After
all, they are /the/ free monoid. Then we would simply have ^.The interpretation is already there: https://isabelle.sketis.net/repos/
isabelle/file/tip/src/HOL/List.thy#l945I don’t recall whether there was once a deliberate decision not to make it a
full type class instance – but beware that this will preclude any different
instantiation users might want for specific applications.But there is nothing wrong providing that instantiation in a separate library
theory.Cheers,
Florian
Email Gateway (Jan 26 2025 at 15:55):From: Florian Haftmann <florian.haftmann@cit.tum.de>
From the previous discussion it seems to me there should be a separate
theory List_Power that defines ^ on lists. Same as Stepan, I would argue
it is the only reasonable interpretation for ^ on lists. Moreover, there
is still ^^ for other interpretations.
Sounds fine to me.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jan 26 2025 at 16:25):From: Makarius <makarius@sketis.net>
On 26/01/2025 16:52, Tobias Nipkow wrote:
Please note that I have very recently defined ^^ on lists and ported some of
Stepan's lemmas to List. However, this is not a final decision. I would be
just as happy with ^. In fact, I agree that this subtheory (with ^ or ^^)
should go into a separate theory. I would put it into the AFP for visibility
(and because List-Index is already there).
There is 1 week left to figure out the final form of that, for
Isabelle2025-RC1. See also
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025
Makarius
Email Gateway (Jan 28 2025 at 21:10):From: Tobias Nipkow <nipkow@in.tum.de>
After some more discussions I/we decided against the type class version of the
list power operator: although having (^) is attractive, it would also give us 1
and (*) on lists (defined as [] and (@)). Although mathemtically reasonable, it
is problematic because lists and their notation are so basic. Thus I have opted
for the overloaded ^^ operator that will be available as a separate theory.
Tobias
On 26/01/2025 16:52, Tobias Nipkow wrote:
Please note that I have very recently defined ^^ on lists and ported some of
Stepan's lemmas to List. However, this is not a final decision. I would be just
as happy with ^. In fact, I agree that this subtheory (with ^ or ^^) should go
into a separate theory. I would put it into the AFP for visibility (and because
List-Index is already there).From the previous discussion it seems to me there should be a separate theory
List_Power that defines ^ on lists. Same as Stepan, I would argue it is the only
reasonable interpretation for ^ on lists. Moreover, there is still ^^ for other
interpretations.Any objections?
Tobias
On 26/01/2025 16:13, Stepan Holub (via cl-isabelle-users Mailing List) wrote:
Yes, I fully understand that instantiation policy should be cautious and
conservative, although I wonder whether concatenation is not the only
reasonable instance of monoid multiplication for lists. My point was that full
instantiation would solve Tobias's question about concat replicate in a simple
and natural way.Stepan
On 26-Jan-25 3:56 PM, Florian Haftmann wrote:
A propos: a more ambitious question, certainly considered before, is whether
lists with append and Nil deserve to be instantiated as monoid_mult. After
all, they are /the/ free monoid. Then we would simply have ^.The interpretation is already there: https://isabelle.sketis.net/repos/
isabelle/file/tip/src/HOL/List.thy#l945I don’t recall whether there was once a deliberate decision not to make it a
full type class instance – but beware that this will preclude any different
instantiation users might want for specific applications.But there is nothing wrong providing that instantiation in a separate library
theory.Cheers,
Florian
Email Gateway (Jan 29 2025 at 14:03):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Makes sense. I support your decision by roughly 51:49.
Stepan
On 1/28/2025 10:09 PM, Tobias Nipkow wrote:
After some more discussions I/we decided against the type class
version of the list power operator: although having (^) is attractive,
it would also give us 1 and (*) on lists (defined as [] and (@)).
Although mathemtically reasonable, it is problematic because lists and
their notation are so basic. Thus I have opted for the overloaded ^^
operator that will be available as a separate theory.Tobias
On 26/01/2025 16:52, Tobias Nipkow wrote:
Please note that I have very recently defined ^^ on lists and ported
some of Stepan's lemmas to List. However, this is not a final
decision. I would be just as happy with ^. In fact, I agree that this
subtheory (with ^ or ^^) should go into a separate theory. I would
put it into the AFP for visibility (and because List-Index is already
there).From the previous discussion it seems to me there should be a
separate theory List_Power that defines ^ on lists. Same as Stepan, I
would argue it is the only reasonable interpretation for ^ on lists.
Moreover, there is still ^^ for other interpretations.Any objections?
Tobias
On 26/01/2025 16:13, Stepan Holub (via cl-isabelle-users Mailing
List) wrote:Yes, I fully understand that instantiation policy should be cautious
and conservative, although I wonder whether concatenation is not the
only reasonable instance of monoid multiplication for lists. My
point was that full instantiation would solve Tobias's question
about concat replicate in a simple and natural way.Stepan
On 26-Jan-25 3:56 PM, Florian Haftmann wrote:
A propos: a more ambitious question, certainly considered before,
is whether lists with append and Nil deserve to be instantiated as
monoid_mult. After all, they are /the/ free monoid. Then we would
simply have ^.The interpretation is already there:
https://isabelle.sketis.net/repos/
isabelle/file/tip/src/HOL/List.thy#l945I don’t recall whether there was once a deliberate decision not to
make it a full type class instance – but beware that this will
preclude any different instantiation users might want for specific
applications.But there is nothing wrong providing that instantiation in a
separate library theory.Cheers,
Florian
Last updated: Jan 30 2025 at 04:21 UTC