Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: find2.thy Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.