Generics|Basics|Specifics
1. Generics
Introduces: nonmap-range .
open.
2. Basics
Introduces: map , range , map of _ to _ , empty-map , disjoint-union _ , mapped-set _ .
Needs: Tuples/Basics . map <= component .
- map = disjoint-union (map of element to range)* .
- range = nonmap-range | map (disjoint) .
- map of _ to _ :: element, range -> map (total, injective) .
- empty-map : map .
- disjoint-union _ :: map* -> map (partial, associative, commutative, unit is empty-map) .
- mapped-set _ :: map -> set (total) .
(1) disjoint-union ( ) = empty-map ;
disjoint-union (map of e:element to r:range) = map of e:element to
r:range .
intersection (mapped-set m1, mapped-set m2) is empty-set = true
=> disjoint-union (m1:map, m2:map) : map .
intersection (mapped-set m1, mapped-set m2) is empty-set = false
=> disjoint-union (m1:map, m2:map) = nothing .
(2) mapped-set empty-map = empty-set ;
mapped-set map of e:element to r:range = set of e ;
mapped-set disjoint-union (m1:map, m2:map)
= disjoint-union (mapped-set m1, mapped-set m2) .
closed except Generics.
3. Specifics
Introduces: _ [ _to_ ] , _at_ , overlay_ , _restricted to_ , _omitting_ .
Includes: Instant/Distinction ( map
for s , _ is _ ) .
Needs: Tuples/Basics .
- _ [ _to_ ] :: map, element, range -> map .
- _at_ :: map, element -> range (partial) .
- overlay _ :: map* -> map (total, associative, idempotent, unit is empty-map).
- _restricted to_ :: map, set -> map (total).
- _omitting_ :: map, set -> map (total) .
(1) (m <= map) [e <= element to r <= range] = m & disjoint-union (map of
e to r)*.
(2) empty-map at e:element = nothing ;
map of e':element to r:range at e:element
= when e is e' then r
disjoint-union (m:map, m':map) at e:element
= when there is disjoint-union (m, m')
then ((m at e)|(m' at e)) .
(3) overlay (m:map, m':map) = disjoint-union (m, m' omitting mapped-set
m) .
(4) empty-map restricted to s:set = empty-map ;
map of e:element to r:range restricted to s:set
= if e is in s then map of e to r else empty-map ;
disjoint-union (m:map, m':map) restricted to s:set
= when there is disjoint-union (m, m')
then disjoint-union (m restricted to s, m' restricted to s) .
(5) empty-map omitting s:set = empty-map ;
map of e:element to r:range omitting s:set =
if e is in s then empty-map else map of e to r ;
disjoint-union (m:map, m':map) omitting s:set
= when there is disjoint-union (m, m')
then disjoint-union (m omitting s, m' omitting s) .
(6) empty-map is m:disjoint-union (map of element to range)+ = false ;
map of e1:element to r1:range is map of
e2:element to r2:range
= if e1 is e2 then
r1 is r2 else false ;
disjoint-union (map of e:element to r:range, m:map) is
m':map
= when not (e is in mapped-set m) then if not (e is in mapped set
m')
then false else both ((r is (m' at e)), (m is (m' omitting set of
e))) .
|