sigma_bijection.pvs Interaktion und
PortierbarkeitPVS

%------------------------------------------------------------------------------
% Re-ordering of sums
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
sigma_bijection[T: TYPE FROM int]: THEORY

BEGIN

  ASSUMING

    connected_domain: ASSUMPTION (FORALL (x, y: T), (z: integer):
                                       x <= z AND z <= y IMPLIES T_pred(z))

  ENDASSUMING

  IMPORTING reals@sigma

  low,high,
  l,h,n,m,i : VAR T
  rng, nn   : VAR nat
  pn        : VAR posnat
  z         : VAR int
  a,x,B     : VAR real
  F         : VAR [T->real]

  subrange_T(n,m): TYPE = {k:T | n <= k AND k <= m}

% The following theorem shows that we can re-order the summation of
% any finite sum.

  sigma_bijection: LEMMA
     low <= high IMPLIES
     FORALL (phi:(bijective?[subrange_T(low,high),subrange_T(low,high)])):
       sigma[subrange_T(low,high)](low,high,F)
               = sigma[subrange_T(low,high)](low,high,F o phi)

END sigma_bijection

quality83%