div_nat: THEORY
%------------------------------------------------------------------------
% Defines natural division:
%
%    Author:   Rick Butler                NASA Langley Research Center
%
% NOTE.  See div library for division defined over the integers
% 
%------------------------------------------------------------------------

BEGIN

  IMPORTING floor_more

  n,k: VAR nat
  m: VAR posnat
  i: VAR int

  div(n,m): upto(n) = floor(n/m)

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

  div_value    : LEMMA n >= k*m AND n < (k+1)*m IMPLIES div(n,m) = k 

  div_sum_nat  : LEMMA n + i*m >= 0 IMPLIES div(n+i*m,m) = div(n,m) + i

  div_multiple : LEMMA div(k*m,m) = k   
  
  div_is_0     : LEMMA div(n,m) = 0 IFF n < m

% ------------ some order relationships -------------
  
  div_smaller  : LEMMA m * div(n,m) <= n 

  div_rem_small: LEMMA n - m * div(n,m) < m

  div_mult_lt  : LEMMA n < k*m IFF div(n,m) < k

% ------------ Special arguments ------------

  div_by_one   : LEMMA div(n,1) = n
              
  div_zero     : LEMMA div(0,m) = 0
              
  div_eq_arg   : LEMMA div(m,m) = 1

  div_one      : LEMMA m > 1 IMPLIES div(1,m) = 0
  
  div_even     : LEMMA integer_pred(n/m) IMPLIES n - m*div(n,m) = 0
  
END div_nat