div_nt: THEORY %------------------------------------------------------------------------ % Defines natural and integer division (Number Theory 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 away from zero (i.e. div(-7,3) = -3). This is 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. The % alternate approach (i.e. truncation towards zero: div(-7,3) = -2) is % simpler to compute because div(-i,m) = -div(i,m) under that % definition. It is the method defined in tha Ada reference manual. % %% 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_props -- now in prelude i,k: VAR int n: VAR nat m: VAR posnat j: VAR nonzero_integer x: VAR real negi,ngi2: VAR negint div(i,j): integer = floor(i/j) sgn(x): int = IF x >= 0 THEN 1 ELSE -1 ENDIF JUDGEMENT div(n,m) HAS_TYPE nat JUDGEMENT div(negi,m) HAS_TYPE negint JUDGEMENT div(negi,ngi2) HAS_TYPE nonneg_int JUDGEMENT div(m,negi) HAS_TYPE negint div_nat: LEMMA div(n,m) = IF n>=m THEN 1 + div(n-m, m) ELSE 0 ENDIF div_neg_d: LEMMA div(i,-j) = IF integer_pred(i/j) THEN -div(i,j) ELSE -div(i,j)-1 ENDIF div_neg: LEMMA div(-i,j) = IF integer_pred(i/j) THEN -div(i,j) ELSE -div(i,j)-1 ENDIF div_def: THEOREM div(i,m) = IF i >= m THEN 1 + div(i-m, m) ELSIF i >= 0 THEN 0 ELSIF integer_pred(i/m) THEN -div(-i,m) ELSE -1 - div(-i,m) ENDIF div_sgn: LEMMA div(i,-j) = div(-i,j) div_value: LEMMA i >= k*j AND i < (k+1)*j IMPLIES div(i,j) = k % ================== div for special values ============================= div_zero: LEMMA div(0,j) = 0 div_one: LEMMA abs(j) > 1 IMPLIES div(1,j) = IF j >= 0 THEN 0 ELSE -1 ENDIF 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 i = 0 OR (sgn(i) = sgn(j) AND abs(i) < abs(j)) div_lt: LEMMA abs(i) < abs(j) IMPLIES div(i,j) = IF i = 0 OR sgn(i) = sgn(j) THEN 0 ELSE -1 ENDIF div_parity: LEMMA sgn(i) = sgn(j) IMPLIES div(i,j) >= 0 div_parity_neg: LEMMA sgn(i) /= sgn(j) IMPLIES div(i,j) <= 0 div_smaller: LEMMA m * div(n,m) <= n div_abs: LEMMA abs(div(i,j)) = IF integer_pred(i/j) OR sgn(i) = sgn(j) THEN div(abs(i),abs(j)) ELSE div(abs(i),abs(j)) + 1 ENDIF div_max: LEMMA abs(j) * abs(div(i,j)) <= abs(i) + abs(j) % ================== div over addition ================================= div_multiple: LEMMA div(k*j,j) = k div_sum: LEMMA div(i+k*j,j) = div(i,j) + k END div_nt