Re: [isabelle] Nice representation for access to maps


On maps, you have "dom" and "ran", that are the domain and range of the

In your case, you could write: "ALL y\<in>ran mymap. P y"


On Mi, 2012-07-11 at 13:29 +0200, C. Diekmann wrote:
> 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.