# [isabelle] VDM maps and map comprehension in Isabelle

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

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