Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Concerning Fun.swap


view this post on Zulip Email Gateway (Mar 28 2021 at 09:21):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

I stumbled over an ancient combinator dating back to 2005.

There is the »modifying swap«
‹Fun.swap a b f = f (a := f b, b:= f a)›

However most applications need the canonical swap
‹swap a b x = (if x = a then b else if x = b then a else x)›

and help themselves by writing
‹Fun.swap a b id›

hence avoiding the pain to introduce another combinator.

for that.

Given that the modifying swap can simply expressed as (*)
‹Fun.swap a b f = f o swap a b›

it is tempting to change Fun.swap to the canonical swap and replace
remaining occurrences of the modifying swap using (*).

Any suggestions?

Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Mar 28 2021 at 14:34):

From: Lawrence Paulson <lp15@cam.ac.uk>
Sounds good to me! It’s good to reduce the number of easily inter-definable primitives.
Larry

view this post on Zulip Email Gateway (May 22 2021 at 06:26):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
To conclude this thread: this will be part of the next Isabelle release.

Florian
OpenPGP_signature


Last updated: Jul 15 2022 at 23:21 UTC