library Basic/LinearAlgebra version 0.7 %% authors: L.Schröder, M.Roggenbach, T.Mossakowski %% date: 23.3.01 from Basic/Algebra_I version 0.7 get AbelianGroup, ExtAbelianGroup, Monoid, ExtMonoid, Group, ExtGroup, MonoidAction, RichMonoidAction, RichField, GroupAction, ExtGroupAction, Ring, AbelianGroup_in_Ring_add, ExtRing, CommutativeRing, ExtCommutativeRing, Field, EuclidianRing_in_Int from Basic/Numbers version 0.7 get Nat, Int from Basic/Algebra_II version 0.7 get Polynomial from Basic/StructuredDatatypes version 0.7 get Array, FiniteMap spec VectorSpace [Field]= MonoidAction [Monoid with ops e,__*__] with sort Space, op __*__ then closed{AbelianGroup with sort Elem |-> Space, ops e |-> 0, __ * __ |-> __ + __} then forall x,y: Space; a,b: Elem . (a + b) * x = a * x + b * x %(VS_distr1)% . a * (x + y) = a * x + a * y %(VS_distr2)% end view AbelianGroup_in_VectorSpace [Field]: AbelianGroup to VectorSpace [Field] = sort Elem |-> Space, ops e |-> 0, __ * __ |-> __ + __ end view GroupAction_in_VectorSpace [Field]: GroupAction [Group] to { VectorSpace [RichField reveal sorts Elem, NonZero[Elem], ops __ + __, __ * __, 0, e] then %def op __ * __: NonZero[Elem] * Space -> Space} = sort Elem |-> NonZero[Elem] end view VectorSpace_in_Field [Field]: VectorSpace [Field] to Field = sort Space |-> Elem, op __ * __: Elem * Space -> Space |-> __ * __: Elem * Elem -> Elem end spec ExtVectorSpace [VectorSpace [Field]] given Int = %def RichField and ExtAbelianGroup [view AbelianGroup_in_VectorSpace [Field]] with ops inv |-> -__, __ ^ __ |-> __ times __, __ / __ |-> __ - __ and RichMonoidAction [Monoid] and {FiniteMap[sort Space fit sort S |-> Space] [sort Elem fit sort T |-> Elem] with sort FiniteMap[Space,Elem] |-> LC[Space,Elem]} hide sorts FinSet[Space], FinSet[Elem], NonEmptySet[Space], NonEmptySet[Elem] then ExtGroupAction [view GroupAction_in_VectorSpace [Field]] then op eval: LC[Space,Elem] -> Space pred isZero: LC[Space,Elem] forall x: Space; r: Elem; l:LC[Space,Elem] . eval([])=0 %(eval_empty)% . [r/x]eps l => eval(l)=r*x+eval(l-[r/x]) %(eval_add)% . isZero(l) <=> forall y: Space. (def eval(y,l) => eval(y,l)=0) %(isZero_def)% end spec ConstructVSWithBase [Field][sort Base] given Int= ExtVectorSpace [VectorSpace [Field]] then %cons { sort Base < Space then %def FiniteMap [sort Base fit sort S|-> Base] [sort Elem fit sort T |-> Elem] with sort FiniteMap[Base,Elem] |-> LC[Base,Elem] then sort LC[Base,Elem] isZero(l) %(independent)% } end spec VSWithBase [Field][sort Base]= { ConstructVSWithBase [Field][sort Base]} reveal sort Space, ops __ + __: Space * Space -> Space, __ * __: Elem * Space -> Space, 0 : Space end spec ExtVSWithBase [VSWithBase [Field][sort Base]] given Int = %def ExtVectorSpace [VSWithBase [Field][sort Base]] and ConstructVSWithBase [Field][sort Base] with sort LC[Base,Elem] then %implies forall l,k: LC[Base,Elem] . eval(l)=eval(k) => l=k %(unique_representation)% then %def op coefficients: Space -> LC[Base,Elem] forall x:Space . eval(coefficients(x))=x %(coefficients_def)% then %implies forall l:LC[Base,Elem] . coefficients(eval(l))=l %(recover_coefficients)% end view VSWithBase_in_Field [Field]: VSWithBase [Field][sort Base] to {Field then sort One = {x: Elem. x = e} } = sorts Space |-> Elem, Base |-> One, op __ * __: Elem * Space -> Space |-> __ * __: Elem * Elem -> Elem end view VSWithBase_in_VectorSpace [Field] given Int: {VSWithBase [Field][sort Base] hide sort Base} to VectorSpace [Field] end spec Algebra [Field]= VectorSpace [Field] and closed {Ring with sort Elem |-> Space, ops __ + __, __ * __, 0, e} then sort Elem < Space forall r: Elem; x, y: Space . (r * x) * y = r * (x * y) %(Algebra_left_linear)% . x * (r * y) = r * (x * y) %(Algebra_right_linear)% end spec ExtAlgebra [Algebra [Field]] given Int = %def RichField and ExtVectorSpace [VectorSpace [Field]] and ExtRing [Algebra [Field] fit sort Elem |-> Space] and Polynomial [Field] then op eval: Poly[Elem] * Space -> Space forall a: Elem; p: Poly[Elem]; x: Space . eval(0,x) = 0 %(eval_poly_0)% . eval(a:::p, x) = a + eval(p,x) * x %(eval_poly_cons)% end spec FreeVectorSpace [Field][sort Base]= free {VectorSpace [Field] then op inject: Base -> Space } end spec ExtFreeVectorSpace [FreeVectorSpace[Field][sort Base]] given Int = ExtVectorSpace [FreeVectorSpace [Field][sort Base]] end view FreeVectorSpace_in_VSWithBase [Field] given Int: FreeVectorSpace [Field][sort Base] to { VSWithBase [Field][sort Base] then op inject: Base -> Space forall x:Base . inject(x) = x %(VSWB_inject_def)% } end view VSWithBase_in_FreeVectorSpace [Field][sort Base] given Int: VSWithBase [Field][sort Base] to {FreeVectorSpace [Field][sort Base] then %def sort Base < Space forall x: Base . x = inject(x) %(FVS_embed_def)% } end spec VectorTuple [VectorSpace[Field]][op n: Pos] given Int = %def { {{Array [ops 1,n: Int fit ops min: Int |-> 1, max: Int |-> n] [sort Space fit sort Elem|-> Space] with sorts Index |-> Nat[n], Array[Space]} hide sorts FinSet[Space], FinSet[Nat[n]], NonEmptySet[Space], NonEmptySet[Nat[n]]} then %implies sort Nat[n] < Nat then sort Tuple[Space,n]={ x: Array[Space]. forall i: Nat[n]. def x ! i } ops __ ! __: Tuple[Space,n] * Nat[n] -> Space; 0: Tuple[Space,n]; __*__: Elem * Tuple[Space,n] -> Tuple[Space,n]; __+__: Tuple[Space,n] * Tuple[Space,n] -> Tuple[Space,n]; auxsum: Tuple[Space,n] * Nat[n] -> Space; sum: Tuple[Space,n] -> Space forall r: Elem; x,y: Tuple[Space,n]; i: Nat[n] . 0 ! i = 0 %(Tuple_zero_def)% . (r * x) ! i = r * (x ! i) %(Elem_times_Tuple_def)% . (x + y) ! i = (x ! i) + (y ! i) %(Tuple_plus_def)% . auxsum(x, 1 as Nat[n]) = x ! (1 as Nat[n]) %(Tuple_auxsum_1)% . auxsum(x, suc(i) as Nat[n])= auxsum(x,i) + (x ! (suc(i) as Nat[n])) %(Tuple_auxsum_suc)% . sum(x) = auxsum(x, n as Nat[n]) %(Tuple_sum_def)% } hide op auxsum end view VectorSpace_in_VectorTuple [VectorSpace [Field]] [op n:Pos] given Int: VectorSpace [Field] to VectorTuple [VectorSpace [Field]][op n:Pos]= sort Space |-> Tuple[Space,n] end spec ConstructVector [Field][op n: Pos] given Int = %def {VectorTuple [view VectorSpace_in_Field [Field]][op n: Pos] with sort Tuple[Elem,n] |-> Vector[Elem,n], Nat[n], ops 0, __ * __, __ + __, sum} with op __ ! __: Vector[Elem,n] * Nat[n] -> Elem then { ops <__ || __> : Vector[Elem,n] * Vector[Elem,n] -> Elem; prod: Vector[Elem,n] -> Elem; unitVector: Nat[n] -> Vector[Elem,n]; auxmult: Vector[Elem,n] * Vector[Elem,n] -> Vector[Elem,n]; auxprod: Vector[Elem,n] * Nat[n] -> Elem pred perp: Vector[Elem,n] * Vector[Elem,n] forall x, y: Vector[Elem,n]; i, j: Nat[n] . auxmult(x,y) ! i = (x ! i) * (y ! i) %(Vector_auxmult_def)% . =sum(auxmult(x,y)) %(Vector_times_def)% . auxprod(x, 1 as Nat[n])=x ! (1 as Nat[n]) %(Vector_auxprod_1)% . auxprod(x, suc(i) as Nat[n]) = auxprod(x,i) * (x ! (suc(i) as Nat[n])) %(Vector_auxprod_suc)% . prod(x) = auxprod(x, n as Nat[n]) %(Vector_prod_def)% . perp(x,y) <=> ( =0) %(perp_def)% . unitVector(i) ! j = e when i = j else 0 %(unitVector_def)% sort UnitVector[Elem,n]= {x: Vector[Elem,n] . exists i: Nat[n]. x = unitVector(i)} } hide ops auxmult,auxprod then %implies forall x,y: Vector[Elem,n] . = %(scalar_prod_comm)% . = 0 => x = 0 %(scalar_prod_pos)% end spec Vector [Field]= ConstructVector [Field][op n: Pos] reveal sorts Vector[Elem,n], UnitVector[Elem,n], ops __ + __: Vector[Elem,n] * Vector[Elem,n] -> Vector[Elem,n], __ * __: Elem * Vector[Elem,n] -> Vector[Elem,n], 0 : Vector[Elem,n] end view VectorSpace_in_Vector [Field] given Nat: VectorSpace [Field] to Vector [Field] = sort Space |-> Vector[Elem,n] end view VSWithBase_in_Vector [Field] given Nat: VSWithBase [Field][sort Base] to Vector [Field] = sorts Space |-> Vector[Elem,n], Base |-> UnitVector[Elem,n] end spec SymmetricGroup [op n: Pos] given Int = %def sort Nat[n] = {i: Pos . i <= n} then %def Array [ops 1, n: Int fit ops min: Int |-> 1, max: Int |-> n] [sort Nat[n] fit sort Elem|-> Nat[n]] with sorts Array[Nat[n]], Index |-> Nat[n] then %def sort Perm[n]={p: Array[Nat[n]] . forall i: Nat[n] . exists j: Nat[n] . p ! j = i} ops id: Perm[n]; __ comp __: Perm[n] * Perm[n] -> Perm[n]; sign: Perm[n] -> Int; nFac: Nat = n! forall p,q: Perm[n]; i: Nat[n] . id ! i = i %(Perm_id_def)% . (p comp q) ! i = p ! (q ! i) %(Perm_comp_def)% . sign(p comp q) = sign(p) * sign(q) %(Perm_sign_homomorphic)% . abs(sign(p)) = 1 %(Perm_sign_range)% . exists r: Perm[n]. sign(r)= - 1 %(Perm_sign_surjective)% then %%cons sort PNat[n] = {i: Pos. i <= nFac} op perm: PNat[n] -> Perm[n] axiom forall p: Perm[n]. exists i: PNat[n]. perm(i) = p %(Perm_num_sur)% end view Group_in_SymmetricGroup [op n: Pos] given Nat: Group to SymmetricGroup [op n: Pos]= sort Elem |-> Perm[n], op __ * __ |-> __ comp __, e |-> id end spec Matrix [Field][op n: Pos] given Int= %def VectorTuple [view VectorSpace_in_Vector [Field]] [op n: Pos] with sort Nat[n], Tuple[Vector[Elem,n],n] |-> Matrix[Elem,n] and ConstructVector [Field][op n: Pos] and ExtRing [Field] then ops transpose: Matrix[Elem,n] -> Matrix[Elem,n]; 1: Matrix[Elem,n]; elementary: Nat[n] * Nat[n] -> Matrix[Elem,n]; __ * __: Matrix[Elem,n] * Vector[Elem,n] -> Vector[Elem,n]; __ * __: Matrix[Elem,n] * Matrix[Elem,n] -> Matrix[Elem,n]; det: Matrix[Elem,n] -> Elem forall a,b: Matrix[Elem,n]; x: Vector[Elem,n]; i,j,k: Nat[n] . (transpose(a) ! i) ! j = (a ! j) ! i %(transpose_def)% . (1 ! i) ! j = e when i = j else 0 %(Matrix_1_def)% . elementary(i,j) ! k = unitVector(j) when i = k else 0 %(elementary_def)% . (a * x) ! i = %(Matrix_times_Vector_def)% . ((a * b) ! i) = a * (b ! i) %(Matrix_mult_def)% sort ElemMatrix[Elem,n]= {x: Matrix[Elem,n]. exists i,j: Nat[n]. x = elementary(i,j)} then local { SymmetricGroup [op n: Pos] with sorts Perm[n], PNat[n], ops sign, perm, nFac then closed{ConstructVector [Field] [op nFac: Pos fit op n|-> nFac]} with sort Vector[Elem,nFac] then sorts Nat[nFac]=PNat[n] ops summands: Matrix[Elem,n] -> Vector[Elem,nFac]; factors: Matrix[Elem,n] * PNat[n] -> Vector[Elem,n] } within { forall a: Matrix[Elem,n]; i: Nat[n]; j: PNat[n] . factors(a,j) ! i = (a ! i) ! (perm(j) ! i) %(Matrix_factors_def)% . summands(a) ! j= prod(factors(a,j)) times sign(perm(j)) %(Matrix_summands_def)% . det(a)=sum(summands(a)) %(Leibnitz)% } then %implies forall a,b: Matrix[Elem,n] . det(0) = 0 %(det_0)% . not det(a) = 0 <=> forall x: Vector[Elem,n]. (a * x = 0 => x = 0) %(det_vanishes)% . det(1) = e %(det_1)% . det(a * b) = det(a) * det(b) %(det_mult)% end view Algebra_in_Matrix [Field][op n: Pos] given Nat: Algebra [Field] to Matrix [Field][op n: Pos]= sort Space |-> Matrix[Elem,n], op e |-> 1 end view VSWithBase_in_Matrix [Field][op n: Pos] given Nat: VSWithBase [Field][sort Base] to Matrix [Field][op n: Pos]= sorts Space |-> Matrix[Elem,n], Base |-> ElemMatrix[Elem,n] end spec FreeAlgebra [Field] = free{Algebra [Field] then op X:Space} end spec ExtFreeAlgebra [FreeAlgebra[Field]] given Int= ExtAlgebra [FreeAlgebra[Field]] end view FreeAlgebra_in_Polynomial [Field] given Int: FreeAlgebra[Field] to Polynomial [Field]= sort Space |-> Poly[Elem] end view Polynomial_in_ExtFreeAlgebra [FreeAlgebra [Field]] given Int: {Polynomial [Field] reveal sorts Elem, Poly[Elem], ops X, __ + __, __ * __} to ExtFreeAlgebra [FreeAlgebra [Field]]= sort Poly[Elem] |-> Space end spec RichVectorSpace = ExtVectorSpace [VectorSpace [Field]] end spec RichVSWithBase [Field][sort Base] = ExtVSWithBase [VSWithBase [Field][sort Base]] end spec RichAlgebra [Field]= ExtAlgebra [Algebra [Field]] end spec RichFreeVectorSpace [Field][sort Base] = ExtFreeVectorSpace [FreeVectorSpace [Field][sort Base]] end spec RichFreeAlgebra [Field] = ExtFreeAlgebra [FreeAlgebra[Field]] end view Polynomial_in_RichFreeAlgebra [Field] given Int: {Polynomial [Field] reveal sorts Elem, Poly[Elem], ops X, __ + __, __ * __} to RichFreeAlgebra [Field]= sort Poly[Elem] |-> Space end