2.3 Library Algebra_I

library Basic/Algebra_I 
version 0.3
%% authors: M.Roggenbach, T.Mossakowski
%% date: 1.11.99

spec

SemiGroup =

sort

Elem

op

__ + __:	Elem ×Elem -> Elem,
	assoc

end

spec

Monoid =

SemiGroup with sort Elem, op __ + __

then

op

0:Elem;
__ + __:	Elem ×Elem -> Elem,
	unit 0

end

spec

CommutativeMonoid =

Monoid with sort Elem, op 0, __ + __

then

op

__ + __:	Elem ×Elem -> Elem,
	comm

end

spec

DefineGroup =

Monoid with sort Elem, op 0, __ + __

then

var

x:Elem

.

%[Group_ExInverse_Def]

exists x': Elem . x + x' = 0 /\ x' + x = 0

end

spec

Group  [DefineGroup with sort Elem, op 0, __ + __ ] =

%def

ops

inv: Elem -> Elem;

__ - __: Elem ×Elem -> Elem;

vars

x,y: Elem

.

%[Group_inverse1] x + inv(x) = 0

.

%[Group_inverse2] inv(x) + x = 0

.

%[Group_minus_def] x - y = x + inv(y)

end

spec

DefineCommutativeGroup =

DefineGroup with sort Elem, op 0, __ + __

then

op

__ + __:	Elem ×Elem -> Elem,
	comm

end

spec

CommutativeGroup 

[DefineCommutativeGroup with sort Elem, op 0, __ + __ ] =

%def

Group [DefineGroup] with ops inv, __ - __

end