Re: [isabelle] VDM maps and map comprehension in Isabelle

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.
This example is well-defined only if P(x, y) is single-valued on S and T. Otherwise, there might be multiple possible y's for some x, so which one should be taken? Option 2 avoids this issue by allowing arbitrary relations, and you have to prove single-valuedness yourself when needed.

In general, you should not convert sets to lists. As you have experienced, this complicates proofs severely. But you can build map comprehensions from lambda abstractions. The following encodes your example more easily:

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

Note that you cannot avoid the THE operator if you don't have a function to obtain the y for any given x. If you already have a map f to specify S and T as dom f and ran f, this simplifies to:

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.,
[(1, 'a'), (2, 'b')] maps 1 to 'a' and 2 to 'b', but I would not recommend that. This way, you clutter your proofs with the representation details and you lose unique representations: [(2, 'b'), (1, 'a')] is the same map as above.

If code generation is of interest, you might want to look at the type ('a, 'b) mapping from HOL/Library, but this is just isomorphic to 'a ~=> 'b.

Hope this helps

On 15/04/13 17:47, Leo Freitas wrote:

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


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