Re: [isabelle] Nice representation for access to maps



There is also the function Option.set :: 'a option => 'a set, which
may be useful:

ALL y\<in>Option.set (mymap i). P y

- Brian

On Wed, Jul 11, 2012 at 1:49 PM, Peter Lammich <lammich at in.tum.de> wrote:
> 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.