Discussion:
[isabelle] Reconciling FinFuns in Distro and AFP
(too old to reply)
Lars Hupel
2016-09-05 09:00:50 UTC
Permalink
Raw Message
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
Makarius
2016-09-09 13:43:40 UTC
Permalink
Raw Message
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.]
That symbol is called \<restriction> in $ISABELLE_HOME/etc/symbols. It
is used in theory Map for restrict_map latex syntax only.


Makarius
Lars Hupel
2016-09-16 20:36:01 UTC
Permalink
Raw Message
Post by Lars Hupel
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).
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

Loading...