library Basic/Algebra_I
version 0.7
%% authors: M.Roggenbach, T.Mossakowski, L.Schröder
%% date: 23.3.01

%prec {__*__} < {__^ __}
%prec {__ + __, __ - __, -__} < {__ / __, __ * __}

from Basic/RelationsAndOrders version 0.7 get TotalOrder, ExtTotalOrder,
RichTotalOrder, PreOrder, EquivalenceRelation

from Basic/Numbers version 0.7 get Nat, Int, Rat

spec 
     BinAlg =
     sort
          Elem
     op
          __ * __: Elem * Elem -> Elem
end

spec
     SemiGroup =
     BinAlg
then
     op
          __ * __: Elem * Elem -> Elem, assoc
end

spec
     SigPowerBinAlg [sort Exponent] =
     BinAlg
then	
     op __ ^ __: Elem * Exponent -> Elem
end

spec 
     PowerTheorems [sort Exponent;
		    ops __ + __, __ * __: Exponent * Exponent -> Exponent] =
     SigPowerBinAlg [sort Exponent]
then
     forall x: Elem; n,m: Exponent
     . x ^ (n + m)=x ^ n * x ^ m		%(Power_add)%
     . x ^ (n * m)=(x ^ n) ^ m             	%(Power_mult)%
end

	

spec 
     CommutativeSemiGroup =
     SemiGroup
then
     op __*__: Elem * Elem -> Elem, comm
end

spec
     PowerTheoremsComm [sort Exponent;
		ops __ + __, __ * __: Exponent * Exponent -> Exponent] =
     SigPowerBinAlg [sort Exponent]
then
     forall x,y: Elem; n: Exponent
     . x^ n * y^ n=(x*y)^ n             	%(Power_basemult)%
end

view
     CommutativeSemiGroup_in_ExtTotalOrder_max [TotalOrder] :
     CommutativeSemiGroup to ExtTotalOrder [TotalOrder] =
op
     __ * __ |-> max
end



view
     CommutativeSemiGroup_in_ExtTotalorder_min [TotalOrder] :
     CommutativeSemiGroup to ExtTotalOrder [TotalOrder] =
op
     __*__ |-> min
end


spec
     Monoid =
     SemiGroup
then
     ops
           e:      Elem;
           __ * __:Elem * Elem -> Elem, unit e
end

spec
     CommutativeMonoid =
     Monoid
and
     CommutativeSemiGroup
end

view
     CommutativeMonoid_in_Nat_Add:
     CommutativeMonoid to Nat
=
     sort
          Elem |-> Nat,
     ops
           e |-> 0,
           __ * __ |-> __ + __
end

view
     CommutativeMonoid_in_Nat_Mult:
     CommutativeMonoid to Nat
=
     sort
          Elem |-> Nat,
     ops
	  e |-> 1,
	  __ * __ |-> __ * __
end

view
     CommutativeMonoid_in_Int_Mult:
     CommutativeMonoid to Int
=
     sort
          Elem |-> Int,
     ops
	  e |-> 1,
	  __ * __ |-> __ * __
end


spec
     Group =
     Monoid
then
     forall x: Elem
     . exists x': Elem . x' * x = e
end




spec
     AbelianGroup =
	Group 
and
	CommutativeMonoid
end

view
     AbelianGroup_in_Int_Add:
     AbelianGroup to Int
=
     sort
          Elem |-> Int,
     ops
	  __ * __ |-> __ + __,
	  e	  |-> 0
end

spec
     MonoidAction [Monoid] =
     sort
          Space
     op
          __*__: Elem * Space -> Space
     forall x: Space; a,b: Elem
     . e * x = x	             		%(MAction_unit)%
     . (a * b) * x = a * (b * x)             	%(MAction_assoc)%
end

spec
     GroupAction [Group] =
     MonoidAction [Group]
end


spec
     Ring =
     AbelianGroup with sort Elem, 
		       ops __ * __ |-> __ + __,
			   e	   |-> 0
and
     Monoid with ops e, __*__
then
     forall x,y,z:Elem
     . (x + y) * z = (x * z) + (y * z)       	%(Ring_distr1)%
     . z * ( x + y ) = (z * x) + (z * y)     	%(Ring_distr2)%
end

view AbelianGroup_in_Ring_add:
     AbelianGroup to Ring =	
     ops e |-> 0,
	 __ * __ |-> __ + __
end

spec
     CommutativeRing =
     Ring
and
     CommutativeMonoid with ops e, __ * __     
end

spec
     IntegralDomain =
     CommutativeRing
then
     forall x,y: Elem 
     . ( x * y = 0 => ( x = 0 \/ y = 0 ) ) 	%(noZeroDiv)%
     . not (e = 0)             			%(zeroNeqOne)%
end

spec
     EuclidianRing =
     IntegralDomain and {Nat reveal pred  __<__ }
then
     op
          delta: Elem ->? Nat
     forall a,b: Elem
     . def delta(a) if not a = 0 		%(ER_delta_dom)%
     . (exists q,r : Elem . a = q * b + r /\
                               (r = 0 \/ delta(r) < delta(b) )) 
		if not b = 0             	%(ER_div)% 
end

view
     EuclidianRing_in_Int :
     EuclidianRing to Int
=
     sorts
          Elem |-> Int,
     ops
          delta |-> abs,
	  e |-> 1
end

spec
     ConstructField =
     CommutativeRing
then
     axiom
          not e = 0
     sort
          NonZeroElem = { x: Elem . not x = 0 }
then
     closed
     {
          Group with
           sort Elem |-> NonZeroElem,
           ops e, __*__
     }
end

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

view
     AbelianGroup_in_ConstructField :
     AbelianGroup to ConstructField 
=
     sort
          Elem |-> NonZeroElem
end

spec
     Field =
     ConstructField hide sort NonZeroElem
end

view
     Field_in_Rat: Field to Rat
=
     sort Elem |-> Rat,
     op e |-> 1
end

spec
     ExtSemiGroup[SemiGroup] given Nat =
%def
     SigPowerBinAlg [sort Pos]
then
     forall x: Elem; n: Pos
     . x ^ 1 = x             			%(SGroup_pow_1)%
     . x ^ suc(n) = x * (x ^ n)             	%(SGroup_pow_suc)%
then
     %implies
     PowerTheorems [Nat fit sort Exponent |-> Pos]
end


spec 
     ExtCommutativeSemiGroup [CommutativeSemiGroup] given Nat =
%def
     ExtSemiGroup [SemiGroup]
then
     %implies
     PowerTheoremsComm [Nat fit sort Exponent |-> Pos]
end


spec
     ExtMonoid  [Monoid] given Nat =
%def
     ExtSemiGroup [SemiGroup]
then 
     SigPowerBinAlg [sort Nat]
then
     forall x: Elem
     . x ^ 0 = e             			%(Monoid_pow_0)%
then %implies
     forall n: Nat
     . e ^ n = e             			%(Monoid_pow_unit)%
and
     PowerTheorems [Nat fit sort Exponent |-> Nat] 
end

spec
     ExtCommutativeMonoid  [CommutativeMonoid]
     given Nat =
%def
     ExtMonoid [Monoid]
and
     ExtCommutativeSemiGroup [CommutativeSemiGroup]
then
     %implies
     PowerTheoremsComm [Nat fit sort Exponent |-> Nat] 
end

spec
     ExtGroup [Group] given Int =
%def
     ExtMonoid [Monoid] 
then
     ops
           inv: Elem -> Elem;
           __ / __: Elem * Elem -> Elem;
     forall x,y: Elem
     . inv(x) * x = e             		%(Group_inverse_def)%
     . x / y = x * inv(y)             		%(Group_div_def)%
then
     SigPowerBinAlg [sort Int]
then
     forall x: Elem; p: Pos
     . x^ (- p)=inv(x ^ p)             		%(Group_pow_neg)%
then %implies
     forall x,y,z: Elem; n,m: Int
     . x * inv(x) = e             		%(Group_right_inv)%
     . x = y if z * x = z * y             	%(Group_left_canc)%
     . x = y if x * z = y * z             	%(Group_right_canc)%
     . inv(inv(x))=x             		%(Group_inv_inv)%
     . inv(e)=e             			%(Group_inv_e)%
     . inv(x*y)=inv(y)*inv(x)             	%(Group_inv_prod)%
and
     PowerTheorems [Int fit sort Exponent |-> Int]
end

spec ExtAbelianGroup  [AbelianGroup] given Int =
%def
     ExtGroup[AbelianGroup]
and
     ExtCommutativeMonoid[AbelianGroup]
end

spec
     ExtMonoidAction [MonoidAction [Monoid]] given Nat =
%def
     ExtMonoid [Monoid]
then 
     pred connected: Space * Space
     forall x,y: Space
     . connected(x,y) <=> exists a: Elem . a * x = y     
						%(Action_connected_def)%
end

view PreOrder_in_ExtMonoidAction [MonoidAction [Monoid]] given Nat:
     PreOrder to ExtMonoidAction [MonoidAction [Monoid]] =
     sort Elem |-> Space,
     pred __ <= __ |-> connected
end


spec
     ExtGroupAction [GroupAction [Group]] given Int =
%def
     ExtMonoidAction [GroupAction [Group]]
and
     ExtGroup [Group]
then
     %implies
     forall a,b:Elem; x,y: Space
     . x = y if a * x = a * y             	%(GroupAct_inj)%
     . exists z: Space . a * z = x             	%(GroupAct_surj)%

end

view EqRel_in_ExtGroupAction [GroupAction [Group]] given Int:
     EquivalenceRelation to ExtGroupAction [GroupAction [Group]] =
     sort Elem |-> Space,
     pred __ ~ __ |-> connected
end


spec
     ExtRing  [Ring ] given Int =
%def
     ExtAbelianGroup [view AbelianGroup_in_Ring_add]
     with ops   inv     |-> -__,
		__ / __ |-> __ - __,
		__ ^ __ |-> __ times __
and
     ExtMonoid[Monoid]
     with op  __ ^ __
and
     preds
          isIrred, isUnit: Elem
     sorts
           NonZero[Elem] = { x: Elem . not x = 0 };
           RUnit[Elem] = { x: Elem . isUnit(x) };
           Irred[Elem] = { x: Elem . isIrred(x) }
     forall x,y: Elem
     . isUnit(x) <=> exists y: Elem . x * y = e /\ y * x = e
						%(Ring_isUnit_def)%
     . isIrred(x) <=> (not isUnit(x) /\ 
	forall y, z: Elem . (x = y * z => (isUnit(y) \/ isUnit(z))))        
						%(Ring_isIrred_def)% 
then
%def
     ops 
	e: RUnit[Elem];
        -__: RUnit[Elem] -> RUnit[Elem];
	__ * __: RUnit[Elem] * RUnit[Elem] -> RUnit[Elem]
end

spec
     ExtCommutativeRing  [CommutativeRing] given Int =
%def
     ExtRing[Ring]
then
     preds
           hasNoZeroDivisors: ();
           __ divides __ :    Elem * Elem;
           associated:        Elem * Elem
     forall x,y: Elem
     . hasNoZeroDivisors <=> forall x,y: Elem. (x * y = 0 => x=0 \/ y=0) 
						%(hasNoZeroDivisors_def)%
     . x divides y <=> exists z: Elem. x * z = y
						%(divides_def)%
     . associated(x,y) <=> exists u:RUnit[Elem]. x=u*y             
						%(associated_def)%
then
     %implies
     forall x,y:Elem
     . associated(x,y) <=> (x divides y /\ y divides x)
end

view
     PreOrder_in_ExtCRing  [CommutativeRing] given Int:
     PreOrder to
     ExtCommutativeRing[CommutativeRing] =
     pred
          __ <= __ |-> __ divides __
end

view
     EqRel_in_ExtCRing  [CommutativeRing] given Int:
     EquivalenceRelation to
     ExtCommutativeRing[CommutativeRing]=
     pred
          __ ~ __ |-> associated
end

spec
     ExtIntegralDomain  [IntegralDomain] given Int =
%def
     ExtCommutativeRing [CommutativeRing]
then
     op __ * __:  NonZero[Elem] * NonZero[Elem] -> NonZero[Elem]
then
     %implies
     axiom hasNoZeroDivisors
end

spec
     ExtEuclidianRing  [EuclidianRing] given Int=
%def
     ExtIntegralDomain [IntegralDomain]
end

spec
     ExtField  [Field] given Int=
%def 
     ExtRing [Ring]
then
closed
     {
	ExtAbelianGroup[view AbelianGroup_in_ConstructField]
	with sort NonZeroElem|->NonZero[Elem],
	     ops inv, __ / __, __ ^ __}
then
     op
           __ / __: Elem * Elem ->? Elem;
     forall x:Elem; n: NonZero[Elem]
     . 0/n=0             			%(Field_div_def1)%
     . not def x/0				%(Field_div_def2)%
then
     %implies
     forall x,y:Elem
     . def x/y <=> not y=0             		%(Field_div_dom)%
end



spec RichSemiGroup =
     ExtSemiGroup [SemiGroup]
end

spec RichCommutativeSemiGroup =
     ExtCommutativeSemiGroup [CommutativeSemiGroup]
end

spec RichMonoid =
     ExtMonoid [Monoid]
end

spec RichCommutativeMonoid = 
     ExtCommutativeMonoid [CommutativeMonoid]
end

spec RichGroup =
     ExtGroup [Group]
end

spec RichAbelianGroup =
     ExtAbelianGroup [AbelianGroup]
end

spec RichMonoidAction [Monoid] =
     ExtMonoidAction [MonoidAction [Monoid]]
end

view PreOrder_in_RichMonoidAction [Monoid]:
     PreOrder to RichMonoidAction [Monoid]=
     sort Elem |-> Space,
     pred __ <= __ |-> connected
end

spec RichGroupAction [Group] =
     ExtGroupAction [GroupAction [Group]]
end

view EqRel_in_RichGroupAction [Group]:
     EquivalenceRelation to RichGroupAction [Group]=
     sort Elem |-> Space,
     pred __ ~ __ |-> connected
end

spec RichRing =
     ExtRing [Ring]
end

spec RichCommutativeRing =
     ExtCommutativeRing [CommutativeRing]
end

view
     PreOrder_in_RichCRing:
     PreOrder to RichCommutativeRing =
     pred
          __ <= __ |-> __ divides __
end

view
     EqRel_in_RichCRing:
     EquivalenceRelation to RichCommutativeRing =
     pred
          __ ~ __ |-> associated
end

spec RichIntegralDomain =
     ExtIntegralDomain [IntegralDomain]
end

spec RichEuclidianRing =
     ExtEuclidianRing [EuclidianRing]
end

spec RichField =
     ExtField [Field]
end


view
     CommutativeSemiGroup_in_RichTotalOrder:
     CommutativeSemiGroup to RichTotalOrder =
op
     __ * __ |-> max
end 

view
     CommutativeSemiGroup_in_RichTotalOrder :
     CommutativeSemiGroup to RichTotalOrder =
op
     __*__ |-> min
end