.Open Enumeration Types
. Why
Enumerations where introduced into Pascal.  They are
really to trivial to have a formal mathematical theory and
so were not "discovered" until this time.

They proved to be very useful for making programs
more readable, less error prone, and easier to maintain,
as a result they appeared in C, Ada, and C++.

. What
An enumeration type has a finite set of values in a fixed
sequence:
.As_is 		enum(bad, indifferent, good)
.As_is 		enum(green, amber, red)
.As_is 		enum(off, on)
.As_is 		enum(Yes, No)
Thes are best used by giving them names and using the name as a type in
later definitions:
.As_is 		weekday::=enum(mon,tue,wed,thur,fri,sat,sun).
.As_is 		month::=enum(jan,feb,mar,apr,may,jun,jul,aug,sep,oct,nov,dec).
The term "enum" is borrowed from C++.  In what follows the terms "pred",
"succ" and "ord" come from Pascal and Ada:

ENUMERATION::=following,
.Net
	Set::Finite(Sets),
	succ::gloss="Successor",
	succ::Set<->Set, partial one-to-one mapping/funtion/operator.
	pred::= /succ.
	pred::gloss="predescessor".
	()|-(e1): $PARTIAL_UNARY_ALGEBRA(Set, op=>succ, finite=>true, terminal).
	<=::@(Set,Set),
	|- For s,s':Set, s<=s' = for some n:0..*(s' = s.succ^n)
	|- (e2):(<=) in $Complete(Set),
	()|- (e3):For all s,s', s<=s' or s'<=s.
	()|- (e4):$linear_order(Set).
	first::=min(Set).
	last::=max(Set).
	(Set,last)|- (e5):last in terminal.
	(succ,e5)|- (e6):terminal = {last}.
	(e3)|- (e7):for all s:Set, some n:0..* ( s = first.pred^n ).
	(e7,succ)|- (e8):for all s:Set, one n:0..* ( s = first.succ^n ).
	ord::=gloss="order".
	For s:Set, ord(s) ::=the n:0..* ( s = first.succ^n ).
	()|- (e9):ord(last) = |Set| - 1.
.Close.Net ENUMERATION
. Exercise 1
Sketch out proofs of the theorems in $ENUMERATION above.
.Hole

. Example
.Net
 weekday:$ $ENUMERATION where following,
.Box
 weekday.Set={mon,tue,wed,thur,fri,sat,sun},
 mon:weekday.Set,
 tue:weekday.Set,
 ...
 sun:weekday.Set,
 weekday.succ= mon+>tue|tue+>wed|wed+>thu|thu+>fri|fri+>sat|sat+>sun,
 weekday.first=mon,
 weekday.last=sun,
 weekday.ord= /(mon,tue,wed,thur,fri,sat,sun) -1.
	= mon+>0 | tue+>1 | wed+>2 |thu+>3 | fri+>4 | sat+>5 | sun+>6.
.Close.Box
.Close.Net Example
. Notation
When we have a list of unique identifiers v then we can create
a new type T=enum v.
(enum):
For n:Nat, v:1..n-->identifier, T:identifier, (T=enum v) ::=following,
.Net
	|- $ENUMERATION(Set=img(v), succ=map[a:Set~v(length(v))](v(/v(a)+1)) ).
	|- T=Set.
	v(1) : T.
	v(2) : T.
 ... -- informal here
.Hole
	v(length(v)) : T.
.Close.Net
Notice that this allows you to refer to an identifier i in v as T.v
but not generate a new type by substituting a new identifier for T.
Using 'i' without T may also be ambiguous.  However, we can write
definitions because they imply a declaration and a equality:
. Example 2
	Answer::=enum(no, yes).
.Box
	Answer.no:Answer,
	Answer.yes:Answer,
	Answer.no=Answer.first,
	Answer.yes=Answer.last,
 ...
.Close.Box
However, `Bad=enum(no,no)` and `Bad2=enum(12, 42)` are not correct
and do not define Bad and Bad2.  Notice also that if `Answer(yes=>no)` was
allowed then this would generate `Bad`.

. Exercise 2
Prove that there is no complete UNARY_ALGEBRA that is finite
and is a linearly order set.

. Cyclic Enumerations
These would be useful if only they were implemented.
The key difference is that the values form a ring
rather than a line.  Each value has a successor.  Repeated
successors lead back to the initial one again.  All elements
have a unique predesessor.

CYCLIC_ENUMERATION::=following,
.Net
	|- $UNARY_ALGEBRA(Set, f=>succ, finite=true).
	|- succ in Set --- Set.
	pred ::= /succ.
	|- For s,s':Set, some n:0..*, s' = s.succ^n.
	cycle ::= |Set|.
	()|- for all s, s = s.succ^cycle.
	()|- succ^cycle=Id.
	()|- for all c, if succ^c = Id then for some n:0..*( c = n*cycle ).
	initialed::@.
	if initialed then initial::Set.

.Close.Net CYCLIC_ENUMERATION
. Example 3
.Net
 week = cycle(mon,tue,wed,thur,fri,sat,sun).
.Box
	week.set={mon,tue,wed,thur,fri,sat,sun},
	week.succ= mon+>tue|tue+>wed|...|sat+>sun|sun+>mon.
	week.cycle = 7.
 ...
.Close.Box
.Close.Net Example 3
. See Also
PARTIAL_UNARY_ALGEBRA::=http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#PARTIAL_UNARY_ALGEBRA
UNARY_ALGEBRA::=http://www.csci.csusb.edu/dick/maths/math_15_Unary_Algebra.html#UNARY_ALGEBRA
Linearly_ordered_sets::=http://www.csci.csusb.edu/dick/maths/math_21_Order.html#Linearly_ordered_sets

Complete::=http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html#Complete.
.Close Enumeration Types