Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] List update pattern xs[i := f(xs!i)

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.

smime.p7s

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

smime.p7s

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

smime.p7s

Email Gateway (May 27 2026 at 07:13):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>

The notation like
xs[i: x => 2*x]
is essentially
xs[i: f]
where f is written in a "Lean-like lambda notation". Such an ad-hoc
deviation from the Isabelle lambda notation may be too casual. And it
will force the explicit formulation even for functions with names.
Which leads (back) to the idea:
xs[i => f]
where =>
becomes exactly the abbreviation for the pattern
i := f(xs!i)
This happens to be the very first of Tobias' suggestions, just =>
instead of ::=. I like it.

Stepan

On 18-May-26 2:09 PM, Tobias Nipkow wrote:

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.

Email Gateway (May 27 2026 at 08:01):

From: Tobias Nipkow <nipkow@in.tum.de>

Good point. I now think that something like xs[i ?? f] is the right notation but
would not use => for ?? because it does look like a function with argument i.

Tobias

On 27/05/2026 09:12, Stepan Holub (via cl-isabelle-users Mailing List) wrote:

The notation like
xs[i: x => 2*x]
is essentially
xs[i: f]
where f is written in a "Lean-like lambda notation". Such an ad-hoc deviation
from the Isabelle lambda notation may be too casual. And it will force the
explicit formulation even for functions with names.
Which leads (back) to the idea:
xs[i => f]
where =>
becomes exactly the abbreviation for the pattern
i := f(xs!i)
This happens to be the very first of Tobias' suggestions, just => instead
of ::=. I like it.

Stepan

On 18-May-26 2:09 PM, Tobias Nipkow wrote:

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.

smime.p7s

Email Gateway (May 27 2026 at 08:14):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>

True. Perhaps  ?? could feature \circ, since f(xs!i) is essentially (f
\circ xs) i.

Stepan

On 27-May-26 10:01 AM, Tobias Nipkow wrote:

Good point. I now think that something like xs[i ?? f] is the right
notation but would not use => for ?? because it does look like a
function with argument i.

Tobias

On 27/05/2026 09:12, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:

The notation like
xs[i: x => 2*x]
is essentially
xs[i: f]
where f is written in a "Lean-like lambda notation". Such an ad-hoc
deviation from the Isabelle lambda notation may be too casual. And it
will force the explicit formulation even for functions with names.
Which leads (back) to the idea:
xs[i => f]
where =>
becomes exactly the abbreviation for the pattern
i := f(xs!i)
This happens to be the very first of Tobias' suggestions, just =>
instead of ::=. I like it.

Stepan

On 18-May-26 2:09 PM, Tobias Nipkow wrote:

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: Jun 12 2026 at 04:13 UTC