:: Logical Correctness of Vector Calculation Programs
:: by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004 Association of Mizar Users


begin

registration
let D be non empty set ;
cluster non empty set ;
existence
not for b1 being XFinSequence of D holds b1 is empty
proof end;
end;

theorem :: PRGCOR_2:1
canceled;

theorem Th2: :: PRGCOR_2:2
for D being non empty set
for f being non empty XFinSequence of D holds len f > 0 by AFINSQ_1:18;

definition
let D be set ;
let q be FinSequence of D;
func FS2XFS q -> XFinSequence of D means :Def1: :: PRGCOR_2:def 1
( len it = len q & ( for i being Nat st i < len q holds
q . (i + 1) = it . i ) );
existence
ex b1 being XFinSequence of D st
( len b1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b1 . i ) )
proof end;
uniqueness
for b1, b2 being XFinSequence of D st len b1 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b1 . i ) & len b2 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b2 . i ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines FS2XFS PRGCOR_2:def 1 :
for D being set
for q being FinSequence of D
for b3 being XFinSequence of D holds
( b3 = FS2XFS q iff ( len b3 = len q & ( for i being Nat st i < len q holds
q . (i + 1) = b3 . i ) ) );

definition
let D be set ;
let q be XFinSequence of D;
func XFS2FS q -> FinSequence of D means :: PRGCOR_2:def 2
( len it = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = it . i ) );
existence
ex b1 being FinSequence of D st
( len b1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b1 . i ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st len b1 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b1 . i ) & len b2 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b2 . i ) holds
b1 = b2
proof end;
end;

:: deftheorem defines XFS2FS PRGCOR_2:def 2 :
for D being set
for q being XFinSequence of D
for b3 being FinSequence of D holds
( b3 = XFS2FS q iff ( len b3 = len q & ( for i being Nat st 1 <= i & i <= len q holds
q . (i -' 1) = b3 . i ) ) );

theorem Th3: :: PRGCOR_2:3
for k being Nat
for a being set holds k --> a is XFinSequence
proof end;

theorem Th4: :: PRGCOR_2:4
for D being set
for n being Nat
for r being set st r in D holds
n --> r is XFinSequence of D
proof end;

definition
let D be non empty set ;
let q be FinSequence of D;
let n be Nat;
assume that
A1: n > len q and
A2: NAT c= D ;
func FS2XFS* q,n -> non empty XFinSequence of D means :Def3: :: PRGCOR_2:def 3
( len q = it . 0 & len it = n & ( for i being Nat st 1 <= i & i <= len q holds
it . i = q . i ) & ( for j being Nat st len q < j & j < n holds
it . j = 0 ) );
existence
ex b1 being non empty XFinSequence of D st
( len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds
b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b1 . j = 0 ) )
proof end;
uniqueness
for b1, b2 being non empty XFinSequence of D st len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds
b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b1 . j = 0 ) & len q = b2 . 0 & len b2 = n & ( for i being Nat st 1 <= i & i <= len q holds
b2 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b2 . j = 0 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines FS2XFS* PRGCOR_2:def 3 :
for D being non empty set
for q being FinSequence of D
for n being Nat st n > len q & NAT c= D holds
for b4 being non empty XFinSequence of D holds
( b4 = FS2XFS* q,n iff ( len q = b4 . 0 & len b4 = n & ( for i being Nat st 1 <= i & i <= len q holds
b4 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b4 . j = 0 ) ) );

definition
let D be non empty set ;
let p be non empty XFinSequence of D;
assume that
A1: p . 0 is Nat and
A2: p . 0 in len p ;
func XFS2FS* p -> FinSequence of D means :Def4: :: PRGCOR_2:def 4
for m being Nat st m = p . 0 holds
( len it = m & ( for i being Nat st 1 <= i & i <= m holds
it . i = p . i ) );
existence
ex b1 being FinSequence of D st
for m being Nat st m = p . 0 holds
( len b1 = m & ( for i being Nat st 1 <= i & i <= m holds
b1 . i = p . i ) )
proof end;
uniqueness
for b1, b2 being FinSequence of D st ( for m being Nat st m = p . 0 holds
( len b1 = m & ( for i being Nat st 1 <= i & i <= m holds
b1 . i = p . i ) ) ) & ( for m being Nat st m = p . 0 holds
( len b2 = m & ( for i being Nat st 1 <= i & i <= m holds
b2 . i = p . i ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines XFS2FS* PRGCOR_2:def 4 :
for D being non empty set
for p being non empty XFinSequence of D st p . 0 is Nat & p . 0 in len p holds
for b3 being FinSequence of D holds
( b3 = XFS2FS* p iff for m being Nat st m = p . 0 holds
( len b3 = m & ( for i being Nat st 1 <= i & i <= m holds
b3 . i = p . i ) ) );

theorem Th5: :: PRGCOR_2:5
for D being non empty set
for p being non empty XFinSequence of D st p . 0 = 0 & 0 < len p holds
XFS2FS* p = {}
proof end;

definition
let D be non empty set ;
let p be XFinSequence of D;
let q be FinSequence of D;
pred p is_an_xrep_of q means :Def5: :: PRGCOR_2:def 5
( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) );
end;

:: deftheorem Def5 defines is_an_xrep_of PRGCOR_2:def 5 :
for D being non empty set
for p being XFinSequence of D
for q being FinSequence of D holds
( p is_an_xrep_of q iff ( NAT c= D & p . 0 = len q & len q < len p & ( for i being Nat st 1 <= i & i <= len q holds
p . i = q . i ) ) );

theorem :: PRGCOR_2:6
for D being non empty set
for p being non empty XFinSequence of D st NAT c= D & p . 0 is Nat & p . 0 in len p holds
p is_an_xrep_of XFS2FS* p
proof end;

definition
let x, y, a, b, c be set ;
func IFLGT x,y,a,b,c -> set equals :Def6: :: PRGCOR_2:def 6
a if x in y
b if x = y
otherwise c;
correctness
coherence
( ( x in y implies a is set ) & ( x = y implies b is set ) & ( not x in y & not x = y implies c is set ) );
consistency
for b1 being set st x in y & x = y holds
( b1 = a iff b1 = b );
;
end;

:: deftheorem Def6 defines IFLGT PRGCOR_2:def 6 :
for x, y, a, b, c being set holds
( ( x in y implies IFLGT x,y,a,b,c = a ) & ( x = y implies IFLGT x,y,a,b,c = b ) & ( not x in y & not x = y implies IFLGT x,y,a,b,c = c ) );

theorem Th7: :: PRGCOR_2:7
for D being non empty set
for q being FinSequence of D
for n being Nat st NAT c= D & n > len q holds
ex p being XFinSequence of D st
( len p = n & p is_an_xrep_of q )
proof end;

definition
let a, b be XFinSequence of REAL ;
assume that
A1: b . 0 is Nat and
A2: b . 0 < len a ;
func inner_prd_prg a,b -> Real means :Def7: :: PRGCOR_2:def 7
 ex s being XFinSequence of REAL ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & it = s . n );
existence
ex b1 being Real ex s being XFinSequence of REAL ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n )
proof end;
uniqueness
for b1, b2 being Real st ex s being XFinSequence of REAL ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b1 = s . n ) & ex s being XFinSequence of REAL ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b2 = s . n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines inner_prd_prg PRGCOR_2:def 7 :
for a, b being XFinSequence of REAL st b . 0 is Nat & b . 0 < len a holds
for b3 being Real holds
( b3 = inner_prd_prg a,b iff ex s being XFinSequence of REAL ex n being Integer st
( len s = len a & s . 0 = 0 & n = b . 0 & ( n <> 0 implies for i being Nat st i < n holds
s . (i + 1) = (s . i) + ((a . (i + 1)) * (b . (i + 1))) ) & b3 = s . n ) );

theorem Th8: :: PRGCOR_2:8
for a being FinSequence of REAL
for s being XFinSequence of REAL st s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) holds
Sum a = s . (len a)
proof end;

theorem :: PRGCOR_2:9
for a being FinSequence of REAL ex s being XFinSequence of REAL st
( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) )
proof end;

theorem :: PRGCOR_2:10
for a, b being FinSequence of REAL
for n being Nat st len a = len b & n > len a holds
|(a,b)| = inner_prd_prg (FS2XFS* a,n),(FS2XFS* b,n)
proof end;

definition
let b, c be XFinSequence of REAL ;
let a be Real;
let m be Integer;
pred m scalar_prd_prg c,a,b means :Def8: :: PRGCOR_2:def 8
( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = a * (b . i) ) ) );
end;

:: deftheorem Def8 defines scalar_prd_prg PRGCOR_2:def 8 :
for b, c being XFinSequence of REAL
for a being Real
for m being Integer holds
( m scalar_prd_prg c,a,b iff ( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = a * (b . i) ) ) ) );

theorem :: PRGCOR_2:11
for b being non empty XFinSequence of REAL
for a being Real
for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds
( ex c being XFinSequence of REAL st m scalar_prd_prg c,a,b & ( for c being non empty XFinSequence of REAL st m scalar_prd_prg c,a,b holds
XFS2FS* c = a * (XFS2FS* b) ) )
proof end;

definition
let b, c be XFinSequence of REAL ;
let m be Integer;
pred m vector_minus_prg c,b means :Def9: :: PRGCOR_2:def 9
( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = - (b . i) ) ) );
end;

:: deftheorem Def9 defines vector_minus_prg PRGCOR_2:def 9 :
for b, c being XFinSequence of REAL
for m being Integer holds
( m vector_minus_prg c,b iff ( len c = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = - (b . i) ) ) ) );

theorem :: PRGCOR_2:12
for b being non empty XFinSequence of REAL
for m being Nat st b . 0 is Nat & len b = m & b . 0 < m holds
( ex c being XFinSequence of REAL st m vector_minus_prg c,b & ( for c being non empty XFinSequence of REAL st m vector_minus_prg c,b holds
XFS2FS* c = - (XFS2FS* b) ) )
proof end;

definition
let a, b, c be XFinSequence of REAL ;
let m be Integer;
pred m vector_add_prg c,a,b means :Def10: :: PRGCOR_2:def 10
( len c = m & len a = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) ) );
end;

:: deftheorem Def10 defines vector_add_prg PRGCOR_2:def 10 :
for a, b, c being XFinSequence of REAL
for m being Integer holds
( m vector_add_prg c,a,b iff ( len c = m & len a = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) + (b . i) ) ) ) );

theorem :: PRGCOR_2:13
for a, b being non empty XFinSequence of REAL
for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds
( ex c being XFinSequence of REAL st m vector_add_prg c,a,b & ( for c being non empty XFinSequence of REAL st m vector_add_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) + (XFS2FS* b) ) )
proof end;

definition
let a, b, c be XFinSequence of REAL ;
let m be Integer;
pred m vector_sub_prg c,a,b means :Def11: :: PRGCOR_2:def 11
( len c = m & len a = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) - (b . i) ) ) );
end;

:: deftheorem Def11 defines vector_sub_prg PRGCOR_2:def 11 :
for a, b, c being XFinSequence of REAL
for m being Integer holds
( m vector_sub_prg c,a,b iff ( len c = m & len a = m & len b = m & ex n being Integer st
( c . 0 = b . 0 & n = b . 0 & ( n <> 0 implies for i being Nat st 1 <= i & i <= n holds
c . i = (a . i) - (b . i) ) ) ) );

theorem :: PRGCOR_2:14
for a, b being non empty XFinSequence of REAL
for m being Nat st b . 0 is Nat & len a = m & len b = m & a . 0 = b . 0 & b . 0 < m holds
( ex c being XFinSequence of REAL st m vector_sub_prg c,a,b & ( for c being non empty XFinSequence of REAL st m vector_sub_prg c,a,b holds
XFS2FS* c = (XFS2FS* a) - (XFS2FS* b) ) )
proof end;