Quelle matrix_inv.pvs Sprache: PVS

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

quality95%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.