2.7 Library Algebra_II

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

from

Basic/Algebra_I version 0.3 get

DefineCommutativeGroup, Monoid,DefineGroup,Group, CommutativeGroup

from

Basic/Numbers version 0.3 get Nat, Int, Rat

from

Basic/StructuredDatatypes version 0.3 get FiniteSet

spec

DefineRing =

DefineCommutativeGroup with sort Elem, ops 0, __ + __

then

closed

{

Monoid with

0 |-> 1,

__+__ |-> __*__

}

then

%prec

__ + __ < __ * __

vars

x,y,z:Elem

.

%[Ring_distr1] (x+y)*z = (x * z) + (y * z)

.

%[Ring_distr2] z * ( x + y ) = (z * x) + (z * y)

end

spec

Ring  [DefineRing with sort Elem, ops 0, 1, __+__, __ * __ ] =

%def

CommutativeGroup [DefineCommutativeGroup]

with ops inv, __ - __

then

%def

%prec

__ - __ < __ * __

sort

RUnit = { x: Elem . exists x': Elem . x * x' = 1 /\ x' * x = 1 }

end

spec

DefineIntegralDomain =

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

then

axiom

%[zeroNotEqualOne] ¬ (1 = 0)

op

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

vars

x, y :Elem

.

%[withoutZeroDivisors] x=0 \/ y=0 if x * y = 0

end

spec

IntegralDomain 

[DefineIntegralDomain with sort Elem, ops 0, 1, __+__, __ * __ ] =

%def

Ring [DefineRing] with sort RUnit, ops inv, __ - __

then

%def

sort

Irred=	{ x: Elem .
	¬ (x e RUnit) /\
	( forall y, z: Elem . x = y * z => (y e RUnit \/ z e RUnit ) ) }

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

spec

DefineEuclidianRing =

DefineIntegralDomain with

sort Elem,

ops 0, 1, __+__, __ * __

and

{Nat reveal pred __ < __ }

then

op

delta: Elem -> Nat

vars

a,b: Elem

.

%[degree_function_def]

exists q,r : Elem .	a = q * b + r /\
	(r = 0 \/ delta(r) < delta(b) ) if (¬ b=0 )

end

spec

EuclidianRing 

[DefineEuclidianRing with

sorts Elem, Nat,

pred __ < __,

ops 0, 1, __+__, __ * __

]

=

IntegralDomain [DefineIntegralDomain]

with

sorts RUnit, Irred,

ops inv, __ - __

end

spec

ConstructField =

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

then

axiom

¬ 0 = 1

sort

NonZeroElement = { x: Elem . x =/= 0 }

then

closed

{

DefineGroup with

Elem |-> NonZeroElement,

0 |-> 1,

__+__ |-> __*__

}

end

%% an obvious view which helps to write the specification Field:

view

MultiplicativeGroup_in_Field:
DefineGroup to ConstructField

=

sort

Elem ^_|-> NonZeroElement,

ops

0 |-> 1,

__+__ |-> __*__

end

spec

DefineField =

ConstructField

hide sort NonZeroElement

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

end

spec

Field  [DefineField with sort Elem, ops 0, 1, __+__, __ * __ ] =

%def

Ring [DefineRing] with sort RUnit, ops inv, __ - __

then

%def

Group [view MultiplicativeGroup_in_Field]

with

sort	NonZeroElement,
ops	__ - __ |-> __ / __,
	inv |-> multInv

then

sort

Elem

%%

Dummy-Def of Elem, as %prec is

%%

only allowed after a BASIC-ITEM

%prec

{__+ __, __ - __ } < __ / __

then

%def

op

__ / __: Elem × Elem ->? Elem;

__ / __: Elem × NonZeroElement -> Elem

vars

x:Elem; n: NonZeroElement

.

%[Field_div_def1] 0/n=0

.

%[Field_div_def2] ¬ def x/0

then

%implies

vars

x,y:Elem

.

%[Field_div_dom] def x/y <=> ¬ y=0

end

spec

DefineCommutativeField =

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

then

op

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

end

spec

CommutativeField 

[DefineCommutativeField with

sort Elem,

ops 0, 1, __+__, __ * __

] =

%def

Field [DefineField]

end

view

EuclidianRing_in_Int:

DefineEuclidianRing to Int

=

%%

Signature of DefineIntegralDomain:

sort

Elem ^_|-> Int,

ops

0 |-> 0,

1 |-> 1,

__ + __ |-> __ + __ ,

__ * __ |-> __ * __,

delta |-> abs

end

view

CommutativeField_in_Rat:

DefineCommutativeField to Rat

=

sort

Elem |-> Rat,

ops

0 |-> 0,

1 |-> 1,

__+__ |-> __+__,

__*__ |-> __*__

end