[isabelle] Nice representation for access to maps



Hi,

I have a map which maps type X to type Y option
type_synonym MAP = "X ⇒ Y option"

Given i is my index into the map:
i::X

I want to evaluate a proposition P about the map elements:
Proposition P :: Y -> bool

I only care about the map elements which exist, e.g. are not None:
ALL (y::Y). (mymap :: MAP) i = Some y ⟶ P y

Is there a way to get a nicer and more intuitive notation like:
P mymap[i]


Regards
  Cornelius





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