[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.