Email Gateway (Aug 22 2022 at 14:03): 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
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
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
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
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: Nov 21 2024 at 12:39 UTC