So, I have a Rodin event-b project and would like to define a known static relation. For examples sake, lets say I have a set {a,b,c} and would like to specify the relation constant which is equal to {(a,1),(a,2),(b,3)} in an context axiom. (May be multilined, but preferably single if feasable)
How would I go about this?
CONTEXT
example
SETS
list
CONSTANTS
a
b
c
relation
AXIOMS
axm1 : partition(list, {a}, {b}, {c})
axm2 : relation ∈ list↔1‥5
axm3 : ???
END
axm3: relation = {a↦1, a↦2, b↦3}