Quellcode-Bibliothek block_matrices.pvs Sprache: PVS

% Linear Algebra library
% Heber Herencia-Zapana NIA
% Gilberto Pérez        University of Coruña Spain
% Pablo Ascariz         University of Coruña Spain
% Felicidad Aguado      University of Coruña Spain
% Date: December, 2013

% This file gives the construction and properties of block vectors and block matrices

block_matrices: THEORY

BEGIN

IMPORTING matrices,sigma_lemmas

m,n,p,q: VAR posnat

%------------------------------------------------------------
% Definition of Block Matrices
%------------------------------------------------------------
% We define matrices of 2x2 blocks.

Block_Matrix: TYPE = [# rows1: posnat,rows2: posnat,cols1: posnat,cols2: posnat,matrix: [below(rows1 + rows2), below(cols1 + cols2) -> real] #]

M,N: VAR Block_Matrix

%------------------------------------------------------------
% Matrix Conversions
%------------------------------------------------------------

%Given a Block Matrix, we obtain the Matrix given by it
Block2M(M): Matrix = (# rows := M`rows1 + M`rows2, cols := M`cols1 + M`cols2,matrix := LAMBDA (i: below(M`rows1 + M`rows2), j: below(M`cols1 + M`cols2)): M`matrix(i,j) #)

conversion Block2M

%Given a Block Matrix, we obtain the four Matrices given by its blocks
Block2M1(M): Matrix = (# rows := M`rows1, cols := M`cols1,matrix := LAMBDA (i: below(M`rows1), j: below(M`cols1)): M`matrix(i,j) #) %upper left block

Block2M2(M): Matrix = (# rows := M`rows2, cols := M`cols1,matrix := LAMBDA (i: below(M`rows2), j: below(M`cols1)): M`matrix(i + M`rows1,j) #) %lower left block

Block2M3(M): Matrix = (# rows := M`rows1, cols := M`cols2,matrix := LAMBDA (i: below(M`rows1), j: below(M`cols2)): M`matrix(i,j + M`cols1) #) %upper right block

Block2M4(M): Matrix = (# rows := M`rows2, cols := M`cols2,matrix := LAMBDA (i: below(M`rows2), j: below(M`cols2)): M`matrix(i + M`rows1,j + M`cols1) #) %lower right block

% Given four Matrices and its Dimensions we obtain the Block Matrix composed by them, which has the following form:
% (A C)
% (B D)
M2Block(m,n,p,q)(A: Mat(m,p),B: Mat(n,p),C: Mat(m,q),D: Mat(n,q)): Block_Matrix =  (# rows1 := A`rows,rows2 := B`rows,cols1 := A`cols,cols2 := C`cols,matrix :=
      LAMBDA (i: below(A`rows + B`rows), j: below(A`cols + C`cols)):
     IF i < A`rows THEN
          IF j < A`cols THEN A`matrix(i,j)
             ELSE C`matrix(i,j - A`cols)
   ENDIF

          ELSE IF j < A`cols THEN B`matrix (i - A`rows,j)
      ELSE D`matrix(i - A`rows,j - A`cols)
   ENDIF
     ENDIF
     #)

%------------------------------------------------------------
% Definition of Block Vectors
%------------------------------------------------------------

Block_Vector: TYPE = [# comp1: posnat,comp2: posnat,vector: [below(comp1 + comp2) -> real] #]

Block_Vector2: TYPE = [# comp1: posnat,comp2: posnat,vector1: [below(comp1) -> real],vector2: [below(comp2) -> real] #]

Block_Vect(m,n): TYPE = {V: Block_Vector | V`comp1 = m AND V`comp2 = n}

V: Var Block_Vector

%------------------------------------------------------------
% Vector Conversions
%------------------------------------------------------------

BV1toBV2(V): Block_Vector2 = (# comp1 := V`comp1, comp2 := V`comp2, vector1 := LAMBDA (i: below(V`comp1)): V`vector(i),vector2 := LAMBDA (i: below(V`comp2)): V`vector(i + V`comp1)#)

BV2toBV1(V: Block_Vector2): Block_Vector = (# comp1 := V`comp1, comp2 := V`comp2, vector := LAMBDA (i: below(V`comp1 + V`comp2)): IF i < V`comp1 THEN V`vector1(i) ELSE V`vector2(i - V`comp1) ENDIF #)

Block2V(V): Vector[V`comp1 + V`comp2] = LAMBDA (i: below[V`comp1 + V`comp2]): V`vector(i)

Block2V1(V): Vector[V`comp1] = LAMBDA (i: below[V`comp1]): V`vector(i)

Block2V2(V): Vector[V`comp2] = LAMBDA (i: below[V`comp2]): V`vector(i + V`comp1)

V2Block(m,n: posnat)(x: Vector[m],y: Vector[n]): Block_Vector = (# comp1 := m,comp2 := n,vector :=
      LAMBDA (i: below(m + n)):
     IF i < m THEN x(i)
     ELSE y(i - m) ENDIF
     #);

Vec2Block(m,n: posnat)(x: Vector[m + n]): Block_Vector = (# comp1 := m,comp2 := n,vector := LAMBDA (i: below(m + n)): x(i) #);

conversion BV1toBV2,BV2toBV1

%------------------------------------------------------------
% Definitions involving Block Matrices
%------------------------------------------------------------

Btranspose(M): Block_Matrix =  (# rows1 := M`cols1,rows2 := M`cols2,cols1 := M`rows1,cols2 := M`rows2,matrix := LAMBDA (i: below(M`cols1 + M`cols2), j: below(M`rows1 + M`rows2)): M`matrix(j,i) #)

Bsquare?(M): bool = square?(M)

Bdiag_square?(M): bool = square?(Block2M1(M)) AND square?(Block2M4(M))

Bsymmetric?(M): bool = symmetric?(M)

same_Bdim?(M)(N): bool = M`rows1 = N`rows1 AND M`rows2 = N`rows2 AND M`cols1 = N`cols1 AND M`cols2 = N`cols2;

%------------------------------------------------------------
% Block Operations
%------------------------------------------------------------

*(V, (W: Block_Vect(V`comp1,V`comp2))): real = Block2V1(V)*Block2V1(W) + Block2V2(V)*Block2V2(W);

*(M: (Bdiag_square?),V: Block_Vect(M`cols1,M`cols2)): Block_Vector2 = (# comp1 := M`rows1, comp2 := M`rows2,vector1 := Block2M1(M)*Block2V1(V) + Block2M3(M)*Block2V2(V), vector2 := Block2M2(M)*Block2V1(V) + Block2M4(M)*Block2V2(V)#);

+(M: Block_Matrix,N: (same_Bdim?(M))): Block_Matrix = (# rows1 := M`rows1,rows2 := M`rows2,cols1 := M`cols1 ,cols2 := M`cols2,matrix := LAMBDA (i: below(M`rows1 + M`rows2),j: below(M`cols1 + M`cols2)): M`matrix(i,j) + N`matrix(i,j) #);

*(r: real, M: Block_Matrix): Block_Matrix = M WITH [`matrix := LAMBDA (i: below(M`rows1 + M`rows2), j: below(M`cols1 + M`cols2)): r * M`matrix(i, j)];

%------------------------------------------------------------
% Generic Lemmas about Blocks
%------------------------------------------------------------

conv_transp: LEMMA FORALL (M: Block_Matrix): Btranspose(M) = M2Block(M`cols1,M`cols2,M`rows1,M`rows2)(transpose(Block2M1(M)),transpose(Block2M3(M)),transpose(Block2M2(M)),transpose(Block2M4(M)))

block_square: LEMMA FORALL (M: Block_Matrix): Bdiag_square?(M) IMPLIES Bsquare?(M)

block_symmetric: LEMMA FORALL (M: Block_Matrix): symmetric?(Block2M1(M)) AND symmetric?(Block2M4(M)) AND transpose(Block2M2(M)) = Block2M3(M) IMPLIES Bsymmetric?(M);

block_symmetric2: LEMMA FORALL (M: Block_Matrix): Bsymmetric?(M) AND square?(Block2M1(M)) AND square?(Block2M4(M)) IMPLIES symmetric?(Block2M1(M)) AND symmetric?(Block2M4(M)) AND transpose(Block2M2(M)) = Block2M3(M)

%------------------------------------------------------------
% Lemmas about Equalities and Operations withs Blocks
%------------------------------------------------------------

blockV_equal: LEMMA FORALL (W: Block_Vect(V`comp1,V`comp2)): V = W IFF Block2V(V) = Block2V(W)

VtoBlocktoV1: LEMMA FORALL (x: Vector[m],y: Vector[n]): Block2V1(V2Block(m,n)(x,y)) = x

VtoBlocktoV2: LEMMA FORALL (x: Vector[m],y: Vector[n]): Block2V2(V2Block(m,n)(x,y)) = y

VtoBlocktoV: LEMMA FORALL (x: Vector[m],y: Vector[n],i: below[m + n]): Block2V(V2Block(m,n)(x,y))(i) = IF i < m THEN x(i) ELSE y(i - m) ENDIF

Vec_block_Vec: LEMMA FORALL (m,n: posnat, V: Vector[m + n]): Block2V(Vec2Block(m, n)(V)) = V

block_Vec_block: LEMMA FORALL (V: Block_Vector): Vec2Block(V`comp1, V`comp2)(Block2V(V)) = V

block_product: LEMMA FORALL (M: (Bdiag_square?),V: Block_Vect(M`cols1,M`cols2)): Block2V(M*V) = Block2M(M)*Block2V(V)

Block2V_product: LEMMA FORALL (W: Block_Vect(V`comp1,V`comp2)): V*W = Block2V(V)*Block2V(W)

END block_matrices

quality39%

¤ 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.0.0Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.