3.7 Finite Sets

spec

Elem =

sort

Elem

end

spec

GenerateFiniteSet [Elem with sort Elem] =

free

{

type

FinSet[Elem]::=	{} | set(Elem) |
	__ u __ (FinSet[Elem];FinSet[Elem])

op

__ u __:	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem],
	assoc, comm, idem, unit {}

}

%%

intended system of representatives:

%%

{} and

%%

set(x₁) u ... u set(x_n),

%%

where n > 1, x_i e Elem, x_i =/= x_j for i =/= j, and

%%

x₁ < x₂ < ...< x_n (< is an arbitrary order on Elem)

end

spec

FiniteSet [Elem with sort Elem] =

GenerateFiniteSet [Elem]

and

Nat

then

preds

__  elemOf __:	Elem ×FinSet[Elem];
__ c __:	FinSet[Elem] ×FinSet[Elem]

ops

__ + __ :	Elem ×FinSet[Elem] -> FinSet[Elem];
__ + __,
__ - __ :	FinSet[Elem] ×Elem -> FinSet[Elem];
__ n __,
__ - __,
__ symmDiff __:	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem];
#__:	FinSet[Elem] -> Nat;

vars

x,y : Elem; S,T,U,V:FinSet[Elem]

.

%[elemOf_empty] ¬ x  elemOf {}

.

%[elemOf_set] x  elemOf set(y) <=> (x=y)

.

%[elemOf_union] x  elemOf (S u T) <=> (x  elemOf S) \/ (x  elemOf T)

.

%[subset_empty] {} c S

.

%[subset_set] set(x) c S <=> x  elemOf S

.

%[subset_union] (S u T) c U <=> S c U /\ T c U

.

%[FinSet_add_def1] x + S = set(x) u S

.

%[FinSet_add_def2] S + x = x + S

.

%[FinSet_sub_empty] {} - x = {}

.

%[FinSet_sub_set1] set(y) - x = set(y) if ¬ x = y

.

%[FinSet_sub_set2] set(y) - x = {} if x = y

.

%[FinSet_sub_union] (S u T) - x = (S - x) u (T - x)

.

%[intersect_empty] {} n S = {}

.

%[intersect_set1] set(x) n S = {} if ¬ x  elemOf S

.

%[intersect_set2] set(x) n S = set(x) if x  elemOf S

.

%[intersect_union] (S u T) n U = ( S n U ) u (T n U)

.

%[diff_empty] {} - S = {}

.

%[diff_set1] set(x) - S = set(x) if ¬ x  elemOf S

.

%[diff_set2] set(x) - S = {} if x  elemOf S

.

%[diff_union] (S u T) - U = (S - U ) u (T - U)

.

%[symmDiff_def] S symmDiff T = (S - T) u (T - S)

.

%[FinSet_numberOf_empty] #{} = 0

.

%[numberOf_FinSet_set] #set(x) = 1

.

%[numberOf_FinSet_union] #S u T = #S + #T

then

%cons

ops

__ n __:	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem],
	assoc, comm, idem;
__ symmDiff __ :	FinSet[Elem] ×FinSet[Elem] -> FinSet[Elem],
	comm;

vars

x: Elem; S,T: FinSet[Elem]

.

%[subset_characterization]

S c T <=> ( forall x: Elem . x  elemOf S => x  elemOf T )

end

view

PartialOrder_in_FiniteSet [Elem]:

PartialOrder to FiniteSet [Elem]

=

sort

Elem ^_|-> FinSet[Elem] ,

pred

__ < __ ^_|-> __ c __

end

spec

FinitePowerSet

[FiniteSet [Elem with sort Elem] then op X: FinSet[Elem]]

=

sorts

FinitePowerSet[X]=	{ Y: FinSet[Elem] . Y c X };
Elem[X] =	{x : Elem . x  elemOf X }

preds

__  elemOf __ :	Elem[X] ×FinitePowerSet[X];
__ c __:	FinitePowerSet[X] ×FinitePowerSet[X]

ops

{}:	FinitePowerSet[X];
set :	Elem[X] -> FinitePowerSet[X];
add:	Elem[X] × FinitePowerSet[X] -> FinitePowerSet[X];
__ u __,
__ n __,
__ - __,
__ symmDiff __:	FinitePowerSet[X] ×FinitePowerSet[X]
	-> FinitePowerSet[X]

%%

These predicates and operations

%%

are determined by overloading.

end

view

DefineBooleanAlgebra_in_FinitePowerSet

[Elem with sort Elem] then op X: FinSet[Elem]]

:

DefineBooleanAlgebra to

FinitePowerSet [FiniteSet [Elem with sort Elem] then op X: FinSet[Elem]]

=

sort

Elem ^_|-> FinitePowerSet[X],

ops

0 |-> {},

1 |-> X,

__ |¯| __ |-> __ n __,

__ |_| __ |-> __ u __

end

%% the definition of a factorial ring depends on the sorts
%% Unit and Irred, which both have to be interpreted
%% in a structure that shall be seen as a factorial ring
%% therefore we do not split the specification into two parts
%% as we did for the above algebraic structures

spec

FactorialRing

[DefineIntegralDomain with

sort	Elem,
ops	0, 1, __+__, __ * __

]

=

IntegralDomain [DefineIntegralDomain]

with

sorts	RUnit, Irred,
ops	inv, __ - __

and

FiniteSet [sort Irred]

then

preds

equiv: Irred ×Irred;

equiv: FinSet[Irred] ×FinSet[Irred]

op

prod: FinSet[Irred] -> Elem

vars

x: Elem; u,v: RUnit; i,j: Irred; S,T :FinSet[Irred]

.

%[product_FinSet_empty] prod({}) = 1

.

%[product_FinSet_set] prod(set(i)) = i

.

%[product_FinSet_union] prod(S u T) = prod(S) * prod(T)

.

%[equiv_Irred_def]

equiv(i,j) <=> exists u: RUnit . i= u * j

.

%[equiv_FinSet_def]

equiv(S,T) <=>	( S={} /\ T={} ) \/
	(exists s,t: Irred . s  elemOf S /\ t  elemOf T /\
	equiv(s,t) /\ equiv(S - s, T - t) )

%%

any element of the ring is the product of irreducible elements:

.

%[representation_by_irred_elems]

exists S:FinSet[Irred] . exists u:RUnit . x = u * prod(S)

%%

the product is "unique":

.

%[unique_product]

equiv(S,T) if

x=u * prod(S) /\ x=v * prod(T)

end