Sets

Generics| Basics| Specifics
1. Generics
Introduces: nonset-element .
Includes: Instant/Distinction ( nonset-element for s , _is_ ) . nonset-element = ž. _is_ :: nonset-element, nonset-element -> truth-value (total) .
open.

2. Basics
Introduces: set , element , set of _ .
Needs: Tuples/Basics . element <= component .
  • set = set of element* .
  • element = nonset-element | set (disjoint) .
  • set of _ :: element* -> set (total) .
(1) set of (e:element*, e1:element, e2:element, e':element*) = set of (e, e2, e1, e') .
(2) e1 is e2 = true => set of (e:element*, e1:element, e2:element, e':element*) = set of (e, e1, e') . closed except Generics .

3. Specifics
Introduces: _ [ _ ] , elements _ , empty-set , disjoint-union _ , union _ , difference _ , intersection _ , _ restricted to _ , _ omitting _ , _ [in _ ] , _ [not in _] , _ is in _ , _ is included in _ .
Includes: Instant/Partial Order ( set for s , _is_ , _ is included in _ for _ is less than _ ) .
Needs: Tuples, Lists .
  • _ [ _ ] :: set, element -> set .
  • elements _ :: ( set -> element* (strict, linear) .
  • empty-set : set .
  • disjoint-union _ :: set* -> set (partial, associative, commutative, unit is empty-set) .
  • union _ :: set* -> set (total, associative, commutative, idempotent, unit is empty-set) .
  • difference _ :: set, set -> set (total) .
  • intersection _ :: set+ -> set (total, associative, commutative, idempotent).
  • _ restricted to _ :: list [element], set -> list [element] (total) .
  • _ omitting _ :: list [element], set -> list [element] (total) .
  • _ [in _ ] :: element, set -> element (partial) .
  • _ [not in _ ] :: element, set -> element (partial) .
  • _ is in _ :: element, set -> truth-value (total) .
  • _ is included in _ :: set, set -> truth-value (total) .
  • _is_ :: set, set -> truth-value (total) .
(1) (s <= set) [ e <= element ] = s & set of e* .
(2) s = set of e:element* ; distinct e = true => elements (s:set) = shuffle e .
(3) empty-set = set of ( ) .
(4) disjoint-union (s:set, t:set) = when intersection (s, t) is empty-set then union (s, t) .
(5) union (set of e1:element*, set of e2:element*) = set of (e1, e2) .
(6) difference (empty-set, s:set) = empty-set ; difference (s:set, empty-set) = s ; difference (set of e:element, s:set) = if e is in s then empty-set else set of e ; difference (union (s:set, t:set), u':set) = union (difference (s, u'), difference (t, u')) .
(7) intersection (empty-set, s:set) = empty-set ; intersection (set of e:element, s:set) = if e is in s then set of e else empty-set ; intersection (union (s:set, t:set), u':set) = union (intersection (s, u'), intersection (t, u')) .
(8) empty-list restricted to s:set = empty-list ; empty-list omitting s:set = empty-list .
(9) concatenation (list of e:element, l:list) restricted to s:set = if e is in s then concatenation (list of e, l restricted to s) else l restricted to s ; concatenation (list of e:element, l:list) omitting s:set = if not (e is in s) then concatenation (list of e, l omitting s) else l omitting s .
(10)(e:element) [in s:set] = when e is in s then e ; (e:element) [not in s:set] e:element = when not (e is in s) then e .
(11)e:element is in empty-set = false ; e:element is in union (s:set, t:set) = either ((e is in s), (e is in t)) .
(12)s:set is included in t:set = union (s, t) is t .
(13)empty-set is set of e:element+ = false ; union (set of e:element, s:set) is t:set = both ((e is in t), (difference (s, set of e) is difference (t, set of e))) .


   
Data Notation Summary| Instant| Truth-Values| Numbers| Lists| Strings | Tuples| Maps