products/sources/formale sprachen/Coq/toplevel/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: matrix_inv.pvs   Sprache: Unknown

matrix_inv: THEORY


BEGIN

  IMPORTING matrix_diag


  SM,SM1,SM2: VAR FullMatrix

  r: VAR real

  nzr: VAR nzreal

  M,N,A,B: VAR Matrix

  v,v1,v2: VAR Vector

  i,j,k,p : VAR nat

  m,n : VAR nat

  pn,pm : VAR posnat

  F,G: VAR [[nat,nat]->real]

  Mp,Np: VAR (nonempty?)

  PFM,D1,D2,D: VAR PosFullMatrix

  SQ,IQ,GQ,
  SQ2,IQ2,GQ2,DQ,DQ2,
  Q,R,S,T,
  Q2,R2,S2,T2: VAR Square


  left_inv(S|det(S)/=0): {Q:SquareMatrix(rows(S))|Q*S=Id(rows(S))} =
    LET dg = diag(true,false,S), R=dg`multip,
     newT = form_matrix(LAMBDA (i,j): IF i/=j OR entry(R*S)(i,i)=0 THEN 0
               ELSE 1/entry(R*S)(i,i) ENDIF,rows(S),rows(S))
    IN newT*R


  mult_left_inv_right: LEMMA det(S)/=0 IMPLIES
    S*left_inv(S)=Id(rows(S))

  invertible?(SQ): bool =
    EXISTS (IQ): rows(IQ) = rows(SQ) AND
      IQ*SQ = Id(rows(SQ)) AND SQ*IQ = Id(rows(SQ))

  invertible_rew: LEMMA
    invertible?(SQ) IFF
    (det(SQ)/=0 OR
     (EXISTS (IQ): rows(IQ) = rows(SQ) AND IQ*SQ=Id(rows(SQ))) OR
     (EXISTS (IQ): rows(IQ) = rows(SQ) AND SQ*IQ=Id(rows(SQ))))

  inverse(SQ|det(SQ)/=0 OR invertible?(SQ)): {IQ |
    rows(IQ) = rows(SQ) AND
      IQ*SQ = Id(rows(SQ)) AND SQ*IQ = Id(rows(SQ))} = left_inv(SQ)

   mult_inverse_left: LEMMA invertible?(SQ) IMPLIES
     inverse(SQ)*SQ = Id(rows(SQ))

   mult_inverse_right: LEMMA invertible?(SQ) IMPLIES
     SQ*inverse(SQ) = Id(rows(SQ))

   inverse_unique: LEMMA rows(IQ)=rows(SQ) AND (IQ*SQ = Id(rows(SQ)) OR 
     SQ*IQ = Id(rows(SQ)))
     IMPLIES (invertible?(SQ) AND det(SQ)/=0 AND IQ=inverse(SQ) AND
     IQ*SQ=Id(rows(SQ)) AND SQ*IQ=Id(rows(SQ)))

   invertible_det: LEMMA invertible?(SQ) IFF det(SQ)/=0

   invertible_mult: LEMMA rows(S)=rows(R) AND (det(S)/=0 OR invertible?(S)) AND
            (det(R)/=0 OR invertible?(R)) IMPLIES
     (det(S*R)/=0 AND invertible?(S*R))

   inverse_mult: LEMMA rows(S)=rows(R) AND (det(S)/=0 OR invertible?(S)) AND
            (det(R)/=0 OR invertible?(R)) IMPLIES
     inverse(S*R) = inverse(R)*inverse(S)

   det_inverse: LEMMA det(S)/=0 OR invertible?(S) IMPLIES
     det(inverse(S)) = 1/det(S)

   inverse_invertible: LEMMA det(S)/=0 OR invertible?(S) IMPLIES invertible?(inverse(S))

   inverse_inverse: LEMMA det(S)/=0 OR invertible?(S) IMPLIES
    inverse(inverse(S)) = S

   GH(pn:posnat): Square = form_matrix(LAMBDA (i,j): IF i<j THEN i^2+j^3+3 ELSE i*j-2+i^3+0.1^i ENDIF,pn,pn)

   det_nonzero_simple_prod: LEMMA det(S)/=0 IMPLIES
     is_simple_prod?(rows(S),true,false)(S)

   mult_induction: LEMMA FORALL (P:[SquareMatrix(rows(S))->bool]):
     (FORALL (i,j,r): i<rows(S) AND j<rows(S) AND i/=j IMPLIES 
       P(Easr(rows(S))(i,j,r))) AND
     (FORALL (i,r): i<rows(S) AND r/=0 IMPLIES 
       P(Esr(rows(S))(i,r))) AND
     P(Id(rows(S))) AND
     (FORALL (Q,R:SquareMatrix(rows(S))): P(Q) AND P(R) 
       IMPLIES P(Q*R)) AND
     det(S)/=0
     IMPLIES
     P(S)

   det_transpose: LEMMA FORALL (SM:PosFullMatrix):
     det(transpose(SM)) = det(SM)


END matrix_inv

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]