Re: [isabelle] Nice representation for access to maps



Hi

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

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

--
  Peter


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.