:: by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura

::

:: Received July 13, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

:: deftheorem defines is_an_xrep_of PRGCOR_2:def 1 :

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 ) ) );

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:1

for D being non empty set

for p being XFinSequence of D st NAT c= D & p . 0 is Nat & p . 0 in dom p holds

p is_an_xrep_of XFS2FS* p

for p being XFinSequence of D st NAT c= D & p . 0 is Nat & p . 0 in dom p holds

p is_an_xrep_of XFS2FS* p

proof end;

definition

let x be object ;

let y be set ;

let a, b, c be object ;

correctness

coherence

( ( x in y implies a is object ) & ( x = y implies b is object ) & ( not x in y & not x = y implies c is object ) );

consistency

for b_{1} being object st x in y & x = y holds

( b_{1} = a iff b_{1} = b );

end;
let y be set ;

let a, b, c be object ;

correctness

coherence

( ( x in y implies a is object ) & ( x = y implies b is object ) & ( not x in y & not x = y implies c is object ) );

consistency

for b

( b

proof end;

:: deftheorem Def2 defines IFLGT PRGCOR_2:def 2 :

for x being object

for y being set

for a, b, c being object 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 ) );

for x being object

for y being set

for a, b, c being object 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 Th2: :: PRGCOR_2:2

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 )

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 ;

ex b_{1} 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))) ) & b_{1} = s . n )

for b_{1}, b_{2} 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))) ) & b_{1} = 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))) ) & b_{2} = s . n ) holds

b_{1} = b_{2}

end;
assume that

A1: b . 0 is Nat and

A2: b . 0 < len a ;

func inner_prd_prg (a,b) -> Real means :Def3: :: PRGCOR_2:def 3

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 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 );

ex b

( 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))) ) & b

proof end;

uniqueness for b

( 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))) ) & b

( 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))) ) & b

b

proof end;

:: deftheorem Def3 defines inner_prd_prg PRGCOR_2:def 3 :

for a, b being XFinSequence of REAL st b . 0 is Nat & b . 0 < len a holds

for b_{3} being Real holds

( b_{3} = 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))) ) & b_{3} = s . n ) );

for a, b being XFinSequence of REAL st b . 0 is Nat & b . 0 < len a holds

for b

( b

( 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))) ) & b

theorem Th3: :: PRGCOR_2:3

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)

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:4

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) )

( 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:5

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)))

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;

:: Vector Calculation Program: Scalar Product of Vector

::

:: The following C program is correct if it is used under some limited

::conditions, which are shown in the theorem following the definition

::after this program.

:: But it still remains a possibility of overflow.

:: The following program does not take an explicit function form.

::It means the value of the function does not have a sense.

::The result of the calculation is

::given in a variable c. Precisely speaking, the result is not unique,

::because of the difference of initial value of c.

:: For a model of such a program, we propose the logical predicate form

::(we call such a model, Logical-Model of a program) in the following

::definition.

::

::#define V_SIZE 1024

::void scalar_prd_prg(float c[V_SIZE], float a, float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]=a*b[i];

:: }

:: return;

::}

::The following definition is Logical-Model of the above program.

::

:: The following C program is correct if it is used under some limited

::conditions, which are shown in the theorem following the definition

::after this program.

:: But it still remains a possibility of overflow.

:: The following program does not take an explicit function form.

::It means the value of the function does not have a sense.

::The result of the calculation is

::given in a variable c. Precisely speaking, the result is not unique,

::because of the difference of initial value of c.

:: For a model of such a program, we propose the logical predicate form

::(we call such a model, Logical-Model of a program) in the following

::definition.

::

::#define V_SIZE 1024

::void scalar_prd_prg(float c[V_SIZE], float a, float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]=a*b[i];

:: }

:: return;

::}

::The following definition is Logical-Model of the above program.

:: deftheorem defines scalar_prd_prg PRGCOR_2:def 4 :

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) ) ) ) );

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:6

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) ) )

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;

:: Vector Calculation Program: Minus Vector

::#define V_SIZE 1024

::void vector_minus_prg(float c[V_SIZE], float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]= -b[i];

:: }

:: return;

::}

::The following definition is Logical-Model of the above program.

::#define V_SIZE 1024

::void vector_minus_prg(float c[V_SIZE], float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]= -b[i];

:: }

:: return;

::}

::The following definition is Logical-Model of the above program.

:: deftheorem defines vector_minus_prg PRGCOR_2:def 5 :

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) ) ) ) );

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

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) ) )

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;

:: Vector Calculation Program: Sum of Vectors

::

:: The following program is the same type of scalar_prd_prg, but gives a result

:: a+b in a variable c.

::

::#define V_SIZE 1024

::void vector_add_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]=a[i]+b[i];

:: }

:: return;

::}

::

:: The following program is the same type of scalar_prd_prg, but gives a result

:: a+b in a variable c.

::

::#define V_SIZE 1024

::void vector_add_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]=a[i]+b[i];

:: }

:: return;

::}

:: deftheorem defines vector_add_prg PRGCOR_2:def 6 :

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) ) ) ) );

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:8

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) ) )

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;

:: Vector Calculation Program: Subtraction of Vectors

::

:: The following program is the same type of scalar_prd_prg, but gives a result

:: a-b in a variable c.

::

::#define V_SIZE 1024

::void vector_sub_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]=a[i]-b[i];

:: }

:: return;

::}

::

:: The following program is the same type of scalar_prd_prg, but gives a result

:: a-b in a variable c.

::

::#define V_SIZE 1024

::void vector_sub_prg(float c[V_SIZE], float a[V_SIZE], float b[V_SIZE])

::{ int n,i;

:: c[0]=b[0];

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=1;i<=n;i++)c[i]=a[i]-b[i];

:: }

:: return;

::}

:: deftheorem defines vector_sub_prg PRGCOR_2:def 7 :

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) ) ) ) );

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:9

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) ) )

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;

::#define V_SIZE 1024

:: float inner_prd_prg(float a[V_SIZE],float b[V_SIZE]){

:: int n,i; float s[V_SIZE];

:: s[0]=0;

:: n=(int)(b[0]);

:: if (n != 0)

:: { for(i=0;i<n;i++)s[i+1]=s[i]+a[i+1]*b[i+1];

:: }

:: return s[n];

:: }