CBS-beta / Funcons-beta
Sets 
### Sets

[
  Type   sets
  Funcon set
  Funcon set-elements
  Funcon is-in-set
  Funcon is-subset
  Funcon set-insert
  Funcon set-unite
  Funcon set-intersect
  Funcon set-difference
  Funcon set-size
  Funcon some-element
  Funcon element-not-in
]


Meta-variables
  GT <: ground-values


Built-in Type
  sets(GT)

/*
  `sets(GT)` is the type of possibly-empty finite sets `{V1, ..., Vn}` 
  where `V1:GT`, ..., `Vn:GT`.

*/


Built-in Funcon
  set(_:(GT)*) : =>sets(GT)

/*
  The notation `{V1, ..., Vn}` for `set(V1, ..., Vn)` is built-in.

*/

Assert
  {V*:(GT)*} == set(V*)
/*
  Note that `set(...)` is not a constructor operation. The order and duplicates
  of argument values are ignored (e.g., `{1,2,1}` denotes the same set as `{1,2}` 
  and `{2,1}`).

*/


Built-in Funcon
  set-elements(_:sets(GT)) : =>(GT)*

/*
  For each set `S`, the sequence of values `V*` returned by `set-elements(S)`
  contains each element of `S` just once. The order of the values in `V*` is
  unspecified, and may vary between sets (e.g., `set-elements{1,2}` could be
  `(1,2)` and `set-elements{1,2,3}` could be `(3,2,1)`). 

*/

Assert
  set(set-elements(S)) == S


Built-in Funcon
  is-in-set(_:GT, _:sets(GT)) : =>booleans

/*
  `is-in-set(GV,S)` tests whether `GV` is in the set `S`.

*/

Assert
  is-in-set(GV:GT, { }) == false
Assert
  is-in-set(GV:GT, {GV}:sets(GT)) == true


Built-in Funcon
  is-subset(_:sets(GT), _:sets(GT)) : =>booleans

/*
  `is-subset(S1,S2)` tests whether `S1` is a subset of `S2`.

*/

Assert
  is-subset({ }, S:sets(GT)) == true
Assert
  is-subset(S:sets(GT), S) == true


Built-in Funcon
  set-insert(_:GT, _:sets(GT)) : =>sets(GT)

/*
  `set-insert(GV, S)` returns the set union of `{GV}` and `S`.

*/

Assert
  is-in-set(GV:GT, set-insert(GV:GT, S:sets(GT))) == true


Built-in Funcon
  set-unite(_:(sets(GT))*) : =>sets(GT)

/*
  `set-unite(...)` unites a sequence of sets.

*/

Assert
  set-unite(S:sets(GT), S) == S
Assert
  set-unite(S1:sets(GT), S2:sets(GT)) == set-unite(S2, S1)
Assert
  set-unite(S1:sets(GT), set-unite(S2:sets(GT), S3:sets(GT))) ==
    set-unite(set-unite(S1, S2), S3)
Assert
  set-unite(S1:sets(GT), S2:sets(GT), S3:sets(GT)) == 
    set-unite(S1, set-unite(S2, S3))
Assert
  set-unite(S:sets(GT)) == S
Assert
  set-unite( ) == { }


Built-in Funcon
  set-intersect(_:(sets(GT))+) : =>sets(GT)

/*
  `set-intersect(GT,...)` intersects a non-empty sequence of sets.

*/

Assert
  set-intersect(S:sets(GT), S) == S
Assert
  set-intersect(S1:sets(GT), S2:sets(GT)) == set-intersect(S2, S1)
Assert
  set-intersect(S1:sets(GT), set-intersect(S2:sets(GT), S3:sets(GT))) == 
    set-intersect(set-intersect(S1, S2), S3)
Assert
  set-intersect(S1:sets(GT), S2:sets(GT), S3:sets(GT)) == 
    set-intersect(S1, set-intersect(S2, S3))
Assert
  set-intersect(S:sets(GT)) == S


Built-in Funcon
  set-difference(_:sets(GT), _:sets(GT)) : =>sets(GT)

/*
  `set-difference(S1, S2)` returns the set containing those elements of `S1`
  that are not in `S2`.

*/

Built-in Funcon
  set-size(_:sets(GT)) : =>natural-numbers

Assert
  set-size(S:sets(GT)) == length(set-elements(S))


Funcon
  some-element(_:sets(GT)) : =>GT?

Assert
  some-element(S:sets(GT)) == index(1, set-elements(S))
Assert
  some-element{ } == ( )


Built-in Funcon
  element-not-in(GT:types, _:set(GT)) : =>GT?

/*
  `element-not-in(GT, S)` gives an element of the type `GT` not in the set 
  `S`, or `( )` when `S` is empty. When the set of elements of `GT` is infinite,
  `element-not-in(GT, S)` never gives `( )`.

*/