Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Reconciling FinFuns in Distro and AFP


view this post on Zulip Email Gateway (Aug 22 2022 at 14:03):

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

back in 2012 theory FinFun has been placed in HOL/Library and the
corresponding AFP been left »as it is«. (I remember me also being
involved into that decision).

Despite the initial enthusiasm, uses of that theory remained rare.
Taking that into account and further the increase of reuse in the AFP,
it seems time to reconcile the distro version back into the AFP.

Are there any comments on this?

This measure is part of a bigger plan to
a) introduce a type of finite mappings;
b) let Mapping.thy base on that (as far as appropriate);
c) maybe also go for a general cleanup of Map.thy in the long run.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 14:03):

From: Lars Hupel <hupel@in.tum.de>
Minor clarification:

This measure is part of a bigger plan to
a) introduce a type of finite mappings;

This is already ongoing. Johannes and Fabian agreed to replacing the
finite maps in HOL-Probability with a new representation (cf
a4acecf4dc21), which will shortly appear in HOL-Library (it's not high
priority though).

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 14:04):

From: Tobias Nipkow <nipkow@in.tum.de>
Yes, that would be nice. Although, when I just went through it, only the
following concept seems too specilized and should be moved somewhere else:

map_upds

In fact, I suspect it is only used in Jinja* in the AFP and could be moved there.

Potentially also restrict_map, although that is a natural operation. [It's math
syntax would ideally use the symbol \upharpponright, but that does not exist yet.]

And map_le should be renamed to le_map.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 22 2022 at 14:04):

From: Makarius <makarius@sketis.net>
That symbol is called \<restriction> in $ISABELLE_HOME/etc/symbols. It
is used in theory Map for restrict_map latex syntax only.

Makarius

view this post on Zulip Email Gateway (Aug 22 2022 at 14:06):

From: Lars Hupel <hupel@in.tum.de>
See now Isabelle/2359e9952641. This contains some initial code setup
which should be enough for most purposes; it uses "AList" underneath.

There is a prime candidate for consolidation in the AFP (see
"Finite_Map2" theory), which I attempted to port, but then "back"ed out
(literally – there is a proof with over 10 "back" statements which I
would've had to fix). In case anyone is particularly adventurous, feel
free to go ahead ...

Cheers
Lars


Last updated: Mar 29 2024 at 08:18 UTC