Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nice representation for access to maps


view this post on Zulip Email Gateway (Aug 19 2022 at 08:10):

From: "C. Diekmann" <diekmann@in.tum.de>
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


Last updated: Mar 29 2024 at 01:04 UTC