Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 10:54):

From: Leo Freitas <leo.freitas@newcastle.ac.uk>
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

Email Gateway (Aug 19 2022 at 10:54):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
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

Last updated: Apr 26 2024 at 12:28 UTC