SSL linear_dependence.pvs   Sprache: unbekannt

linear_dependence  % [ parameters ]
  : THEORY

  BEGIN

IMPORTING matrices, matrix_props

 A,M,N: VAR PosFullMatrix
 
 m,i: VAR nat
 p: VAR posnat
 v: VAR Vector
 f,g: VAR [nat->real]
 zerow(p): PosFullMatrix = (: zero(p) :)
 zecolumn(p): PosFullMatrix = transpose(zerow(p))

 zerow_dim: LEMMA rows(zerow(p)) = 1 AND columns(zerow(p)) = p

 zecolumn_dim: LEMMA rows(zecolumn(p)) = p AND columns(zecolumn(p))=1
 

 row2mat(A, (j:below(rows(A)))): PosFullMatrix = (:row(A)(j):)
 
 row2mat_dim: LEMMA FORALL (j:below(rows(A))): rows(row2mat(A,j)) = 1 AND columns(row2mat(A,j)) = columns(A)

 sum_rows(A,f,(j:below(rows(A))), M): RECURSIVE PosFullMatrix = 
   IF j=0 THEN M+f(j)*row2mat(A,j)
   ELSE sum_rows(A,f,j-1, M+f(j)*row2mat(A,j))
   ENDIF
   MEASURE j

 sum_rows(A,f): PosFullMatrix = sum_rows(A,f, rows(A)-1, zerow(columns(A))) 

 sum_rows_eq: LEMMA FORALL (j:below(rows(A))): 
                 (FORALL (k:subrange(0,j)): f(k) = g(k)) IMPLIES 
      sum_rows(A,f,j,M) = sum_rows(A,g,j,M)

 sum_rows_add_start: LEMMA FORALL (j:below(rows(A))):
           sum_rows(A, f, j, M+N) = sum_rows(A, f, j, M) + N

 subtract_same_scal: LEMMA FORALL (j:below(rows(A))):  (f(j) * row2mat(A, j) - f(j) * row2mat(A, j)) = 0 * row2mat(A, j)

 
 sum_lem_prep: LEMMA FORALL(j:below(rows(A)), k:below(j+1)):
         sum_rows(A,f WITH [k:=0], j, M) = sum_rows(A, f, j, M) - f(k)*row2mat(A,k)  

 sum_lem: LEMMA FORALL(j:below(rows(A))): sum_rows(A,f WITH [j:=0]) = sum_rows(A,f) -f(j)*row2mat(A,j) 

 
 row_dependent(A,(j:below(rows(A))),f): bool = 
     (sum_rows(A,f) = zerow(columns(A)))

 row_dependence_lem: LEMMA FORALL (j:below(rows(A)), (f|f(j)=-1)):
       row_dependent(A,j,f) IMPLIES
       %FORALL ((M|rows(M) = columns(A) AND columns(M) =1)):
       row2mat(A,j)*M = sum_rows(A, f WITH [j:=0])*M
  
 row_dep(A, (j:below(rows(A))), f): bool = ((f(j)=-1 AND row_dependent(A,j,f)) OR (f = LAMBDA(i:nat): 0))
 
 row_dep_fun(A, (j:below(rows(A))), (f: {g:[nat->real]| row_dep(A,j,g)})): [nat->real] = 
       f WITH [j:= f(j)+1] 

  

  END linear_dependence

quality66%

[ Verzeichnis aufwärts0.11unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]