*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 28 Oct 2013 08:44:35 +0100*In-reply-to*: <526AC0F8.5080705@informatik.tu-muenchen.de>*References*: <5268E404.9050304@gmail.com> <5268EEED.1030502@inf.ethz.ch> <526AC0F8.5080705@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Florian,

Andreas On 25/10/13 21:05, Florian Haftmann wrote:

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? Florian

**Follow-Ups**:**Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping***From:*Dmitriy Traytel

**References**:**[isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping***From:*Christian Sternagel

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

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

- Previous by Date: [isabelle] WRLA 2014 Call for papers
- Next by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Previous by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Next by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list