Email Gateway (May 18 2026 at 07:16): Email Gateway (May 18 2026 at 07:16):From: Tobias Nipkow <nipkow@in.tum.de>
Hi,
We have the list update notation xs[i := x]. It is frequently used with this
pattern: xs[i := f(xs!i)], which is awkward to read. I would like a shorthand
for this pattern, eg xs[i ::= f]. Examples:
xs[i ::= Suc]
xs[i ::= (%x. 2*x+5)]
There may well be better alternatives! Comments?
Tobias
PS Function update notation should be generalized analogously.
Email Gateway (May 18 2026 at 08:59):From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
I would even argue that this should not only be syntax but the actual definition of list update and function update, just like it is already the case for record field updates. These “map” like updates compose nicely to nested structures.
Regards,
Norbert
--
Norbert Schirmer (nschirmer@apple.com)
SEG Formal Verification
On 17. May 2026, at 11:36, Tobias Nipkow <nipkow@in.tum.de> wrote:
Hi,
We have the list update notation xs[i := x]. It is frequently used with this pattern: xs[i := f(xs!i)], which is awkward to read. I would like a shorthand for this pattern, eg xs[i ::= f]. Examples:
xs[i ::= Suc]
xs[i ::= (%x. 2*x+5)]There may well be better alternatives! Comments?
Tobias
PS Function update notation should be generalized analogously.
Email Gateway (May 18 2026 at 09:44):From: Manuel Eberl <manuel@pruvisto.org>
Seems reasonable. A possible alternative: xs[i, x := 2 * x + 5]
On 5/17/26 11:36, Tobias Nipkow wrote:
Hi,
We have the list update notation xs[i := x]. It is frequently used
with this pattern: xs[i := f(xs!i)], which is awkward to read. I would
like a shorthand for this pattern, eg xs[i ::= f]. Examples:xs[i ::= Suc]
xs[i ::= (%x. 2*x+5)]There may well be better alternatives! Comments?
Tobias
PS Function update notation should be generalized analogously.
Email Gateway (May 18 2026 at 11:10):From: Tjark Weber <tjark.weber@it.uu.se>
On Sun, 2026-05-17 at 11:36 +0200, Tobias Nipkow wrote:
We have the list update notation xs[i := x]. It is frequently used with this
pattern: xs[i := f(xs!i)], which is awkward to read. I would like a shorthand
for this pattern, eg xs[i ::= f]. Examples:
xs[i ::= Suc]
xs[i ::= (%x. 2*x+5)]
There may well be better alternatives! Comments?
This is a good idea, but the proposed syntax is suggestive of an update to a list of functions.
Maybe "xs[i := f _]" or "xs[i |-> f]"?
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (May 18 2026 at 11:24):From: Tobias Nipkow <nipkow@in.tum.de>
Norbert,
You are saying that the update I proposed should be primitive? That could be
done. If it is defined in terms of the current update, there is no problem (even
less so if it is an abbreviation). But deriving the current one from the new one
would entail a lot of proof maintenance, I suspect.
Tobias
On 18/05/2026 10:58, Norbert Schirmer (via cl-isabelle-users Mailing List) wrote:
I would even argue that this should not only be syntax but the actual definition
of list update and function update, just like it is already the case for record
field updates. These “map” like updates compose nicely to nested structures.Regards,
Norbert--
Norbert Schirmer (nschirmer@apple.com)
SEG Formal VerificationOn 17. May 2026, at 11:36, Tobias Nipkow <nipkow@in.tum.de> wrote:
Hi,
We have the list update notation xs[i := x]. It is frequently used with this
pattern: xs[i := f(xs!i)], which is awkward to read. I would like a shorthand
for this pattern, eg xs[i ::= f]. Examples:xs[i ::= Suc]
xs[i ::= (%x. 2*x+5)]There may well be better alternatives! Comments?
Tobias
PS Function update notation should be generalized analogously.
Email Gateway (May 18 2026 at 11:45):From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
When doing the theory from scratch I would really prefer the new one (map-like) to be the primitive notion and the current one to be a syntactic abbreviation (just as with records).
With the current ones as primitives it gets really messy when you do nested updates. In the first place you always have to deal with both “lookup”, e.g. nth and “update”, e.g. list_update, instead of just composing update functions. Nesting both such lookup and updates instead of just nesting map-like updates is not nice. I understand that it might be too much of an effort to change the definition -- it seams feasible for an AI to refactor the library and the AFP though. But I would rather prefer a new constant (with the obvious simp lemmas) for the map-like update instead of just syntax.
Regards,
Norbert
--
Norbert Schirmer (nschirmer@apple.com)
SEG Formal Verification
On 18. May 2026, at 13:23, Tobias Nipkow <nipkow@in.tum.de> wrote:
Norbert,
You are saying that the update I proposed should be primitive? That could be done. If it is defined in terms of the current update, there is no problem (even less so if it is an abbreviation). But deriving the current one from the new one would entail a lot of proof maintenance, I suspect.
Tobias
On 18/05/2026 10:58, Norbert Schirmer (via cl-isabelle-users Mailing List) wrote:
I would even argue that this should not only be syntax but the actual definition of list update and function update, just like it is already the case for record field updates. These “map” like updates compose nicely to nested structures.
Regards,
Norbert
--
Norbert Schirmer (nschirmer@apple.com)
SEG Formal VerificationOn 17. May 2026, at 11:36, Tobias Nipkow <nipkow@in.tum.de> wrote:
Hi,
We have the list update notation xs[i := x]. It is frequently used with this pattern: xs[i := f(xs!i)], which is awkward to read. I would like a shorthand for this pattern, eg xs[i ::= f]. Examples:
xs[i ::= Suc]
xs[i ::= (%x. 2*x+5)]There may well be better alternatives! Comments?
Tobias
PS Function update notation should be generalized analogously.
Email Gateway (May 18 2026 at 12:09):From: Tobias Nipkow <nipkow@in.tum.de>
On 18/05/2026 11:43, Manuel Eberl wrote:
Seems reasonable. A possible alternative: xs[i, x := 2 * x + 5]
I like that, in principle. Not sure about the exact syntax.
Maybe "=>" instead of ":=" ?
"," seems a bit arbitrary. Maybe ":"?
I had hoped the whole device could be extended to multiple dimensions, eg
xs[i,j: x => ...]
But there may be some established convention in the "lenses" community that I
am unaware of.
Tobias
On 5/17/26 11:36, Tobias Nipkow wrote:
Hi,
We have the list update notation xs[i := x]. It is frequently used with this
pattern: xs[i := f(xs!i)], which is awkward to read. I would like a shorthand
for this pattern, eg xs[i ::= f]. Examples:xs[i ::= Suc]
xs[i ::= (%x. 2*x+5)]There may well be better alternatives! Comments?
Tobias
PS Function update notation should be generalized analogously.
Last updated: May 23 2026 at 03:31 UTC