*To*: Leo Freitas <leo.freitas at newcastle.ac.uk>*Subject*: Re: [isabelle] VDM maps and map comprehension in Isabelle*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 16 Apr 2013 13:46:44 +0200*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <24C73ADC-12A6-4685-9310-96307B9F2E2A@ncl.ac.uk>*References*: <24C73ADC-12A6-4685-9310-96307B9F2E2A@ncl.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130329 Thunderbird/17.0.5

Hi Leo, > In VDM map comprehension is given as > > { x |-> y | x <- S, y <- T, P(x, y) } , where x and y come from sets S and T and > property P(x,y) hold.

%x. if x : S & (EX y. y : T & P (x, y)) then Some (THE y. y : T & P (x, y)) else None

restrict_map f {x. P (x, the (f x))} If you only need finite maps, you can represent them directly as associative lists, e.g.,

Hope this helps Andreas On 15/04/13 17:47, Leo Freitas wrote:

Hi, I am encoding some VDM specifications using Isabelle and I am deciding on what to use to represent them. ---- option 1: the type (~=>) from Map.thy It works well up to the point where I needed to add expressions with map comprehension.

> In VDM map comprehension is given as > > { x |-> y | x <- S, y <- T, P(x, y) } , where x and y come from sets S and T and > property P(x,y) hold.

In Isabelle I used the following (convoluted?) construct, given a map f ∈ (Loc ⇀ nat) that is also finite f: map_of [ (x, the(f x)) . x ← sorted_list_of_set (dom f) , P x f ] This leads to complicated proofs I was hoping to avoid. Map.thy expects a list of pairs for building map comprehension through list comprehension, which needs to have its generated values through lists instead of the sets of VDM, hence the use of sorted_list_of_set. ---- option 2: maps as restricted set of pairs This doesn't have as much automation and has some extra lemmas about function application that I inherited from an encoding of Event-B in Isabelle by Mathias Schimaltz. Here map comprehension is just through set comprehension but function application uses THE operator. Any thoughts / suggestions / rationale-of-choice on what would be best to use as an adequate representation? Many thanks Best, Leo

**References**:**[isabelle] VDM maps and map comprehension in Isabelle***From:*Leo Freitas

- Previous by Date: Re: [isabelle] surprising behavior of schematic_lemma
- Next by Date: Re: [isabelle] defining nat1 in isabelle
- Previous by Thread: [isabelle] VDM maps and map comprehension in Isabelle
- Next by Thread: [isabelle] old methods
- Cl-isabelle-users April 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