Quelle  div.pvs

div: THEORY

%------------------------------------------------------------------------
% Defines natural and integer division  (Ada Style)
%
% There is no universally agreed semantics for integer division for a
% negative argument.  For a negative argument, division can be defined
% with truncation towards or away from zero.  The definition in this
% theory truncates toward zero (i.e. div(-7,3) = -2).  This is 
% simpler to compute because div(-i,m) = -div(i,m) and is the
% method defined in tha Ada reference manual. The alternate method
% (i.e. truncation away from zero: div(-7,3) = -3) is the approach
% used in most number theory books.  This approach has the
% advantage that div(i,m) = the greatest integer less than i/m.
%
% AUTHOR
% ------
% 
%   Ricky W. Butler       email: r.w.butler@larc.nasa.gov
%   Mail Stop 130      fax: (804) 864-4234
%   NASA Langley Research Center    phone: (804) 864-6198
%   Hampton, Virginia 23681-0001
%------------------------------------------------------------------------


  BEGIN

  IMPORTING floor_div_lems, abs_rews


  i,k: VAR int
  n: VAR nat
  m: VAR posnat
  j: VAR nonzero_integer
  x: VAR real

  div(i,j): integer = sgn(i)*sgn(j)*floor(abs(i)/abs(j))

  div_nat:     LEMMA div(n,m) = floor(n/m)

  div_rew:     LEMMA div(n,m) = IF n < m THEN 0 ELSE 1 + div(n-m,m) ENDIF

  div_def:     LEMMA div(i,j) = IF i/j >= 0 THEN floor(i/j)
    ELSE ceiling(i/j)
    ENDIF    


  div_value:    LEMMA IF sgn(i) = sgn(j) THEN
                         i >= k*j AND i < (k+1)*j IMPLIES div(i,j) = k 
                      ELSE
                         i > (k-1)*j AND i <= k*j IMPLIES div(i,j) = k
                      ENDIF 


  div_neg: LEMMA div(-i,j) = -div(i,j)

  div_neg_d: LEMMA div(i,-j) = -div(i,j)
 
% ================== div for special values =============================

  div_zero:   LEMMA div(0,j) = 0
  
  div_one:   LEMMA abs(j) > 1 IMPLIES div(1,j) = 0
  
  div_minus1:   LEMMA abs(j) > 1 IMPLIES div(-1, j) = 0
  
  div_eq_arg:   LEMMA div(j,j) = 1
  
  div_by_one:   LEMMA div(i,1) = i
  
  div_eq_0:   LEMMA div(i,j) = 0 IMPLIES abs(i) < abs(j)
  
  div_lt:   LEMMA abs(i) < abs(j) IMPLIES div(i,j) = 0

  div_lt_nat:   LEMMA n < m IMPLIES div(n,m) = 0

  div_is_0:       LEMMA div(i,j) = 0 IFF abs(i) < abs(j)
  
  div_parity:   LEMMA (sgn(i) = sgn(j) AND abs(i) >= abs(j)) IMPLIES
     div(i,j) > 0
      
  div_parity_neg: LEMMA (sgn(i) /= sgn(j) AND abs(i) >= abs(j)) IMPLIES
                          div(i,j) < 0

  div_ge_0:       LEMMA (sgn(i) = sgn(j) IMPLIES div(i,j) >= 0) AND
                          (div(i,j) >= 0 IMPLIES 
                             abs(i) < abs(j) OR sgn(i) = sgn(j))

  div_le_0:       LEMMA (sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0) AND
     (div(i,j) <= 0 IMPLIES 
                             abs(i) < abs(j) OR sgn(i) /= sgn(j))

  div_smaller:    LEMMA m * div(n,m) <= n 
 
  div_abs:        LEMMA abs(div(i,j)) = div(abs(i),abs(j))

  div_max:        LEMMA abs(j)*abs(div(i,j)) <= abs(i)

% ================== div over addition =================================

  div_multiple:   LEMMA div(k*j,j) = k   
  
  div_even:   LEMMA integer_pred(i/j) IMPLIES i - j*div(i,j) = 0
  
  div_sum:   LEMMA IF integer_pred(i/j) OR sgn(i+k*j) = sgn(i) THEN
      div(i+k*j,j) = div(i,j) + k
   ELSE 
      div(i+k*j,j) = div(i,j) + k + sgn(i)*sgn(j)
   ENDIF

  b: VAR nat
  div_sum_nat:   LEMMA div(n+b*m,m) = div(n,m) + b

  nonposint: TYPE = {i: int | i <= 0} CONTAINING -1
  negint: TYPE = {i: int | i < 0} CONTAINING -1

  npi: VAR nonposint
  negi: VAR negint

  JUDGEMENT div(n,m) HAS_TYPE nat
  JUDGEMENT div(npi,m) HAS_TYPE  nonposint
  JUDGEMENT div(npi,negi) HAS_TYPE nat
  JUDGEMENT div(m,negi) HAS_TYPE nonposint

  div_0: LEMMA div(0,j) = 0

  AUTO_REWRITE+ div_0
  AUTO_REWRITE+ div_eq_arg              % LEMMA div(j,j) = 1
  AUTO_REWRITE+ div_by_one              % LEMMA div(i,1) = i
  AUTO_REWRITE+ div_multiple            % LEMMA div(k*j,j) = k   
  AUTO_REWRITE+ div_lt_nat              % LEMMA n < m IMPLIES div(n,m) = 0
  AUTO_REWRITE+ div_nat                 % LEMMA div(n,m) = floor(n/m)

  END div