Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping

Hi Andreas,

> Therefore, you have to switch to some other type. There are two options:
> 1. Use ('a, 'b) mapping. I recommend that you only use it for code
> generation, the mapping type in its current state is not suitable for
> proving lots of stuff.

once there has been the rough idea to reformulate Map.thy using a
dedicated type like in Mapping.thy.  The user-visible difference would
be that element lookups need a dedicated function

  lookup :: ('a, 'b) mapping => 'a => 'b option

But this could be inserted implicitly by coercions also whenever a ('a,
'b) mapping it used in place of a function.

I did not pursue this further, since my impression was that (unlike
sets) the syntax in Map.thy is not so pervasively common, so
specification requiring executable data structures can just be based on
Mapping.thy.  Considering your statement about »easy going« of proofs in
Mapping.thy, maybe we have to rethink about it.  Or is it just that
lemmas / automation are missing?



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.