SSL mod_lems.pvs Sprache: PVS

mod_lems: THEORY
%------------------------------------------------------------------------
% Develops useful lemmas about mod
%
%
% 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 mod    %% in prelude NOW

  i,j,k: VAR int
  m: VAR posnat
  n,a,b,c,x: VAR nat
  jj: VAR nzint

% The following rule characterizes the property that incrementing
% modulo m wraps around the zero point.

  mod_0           : LEMMA mod(0,jj) = 0

  mod_1           : LEMMA j > 1 IMPLIES mod(1,j) = 1

  mod_by1         : LEMMA mod(i,1) = 0

  mod_to_rem      : LEMMA mod(i,m) = rem(m)(i)

  mod_0_divides   : LEMMA mod(i,jj) = 0 IFF divides(jj,i)

  mod_wrap_around : LEMMA n < m & (c <= m & c >= m-n) =>
                              mod(n+c, m) = n - (m-c)

  mod_wrap2       : LEMMA c < m IMPLIES mod(m+c, m) = c

% Injection-like properties for mod for limited ranges

  mod_inj1        : LEMMA x < m AND n < m AND c < m AND
                       mod(x + n, m) = mod(x + c, m) IMPLIES n = c

  mod_inj2        : LEMMA x < m AND n < m AND c < m AND
                        mod(x - n, m) = mod(x - c, m) IMPLIES n = c

  mod_wrap_inj    : LEMMA
      x < m AND a < m AND b < m AND a > 0
        IMPLIES (mod(x + a, m) = mod(x - b, m)) = (a + b = m)

  kk, vv: VAR nat
  mod_neg_limited : LEMMA 0 <= kk AND  kk < m AND vv < m AND
                      vv - kk < 0 IMPLIES mod(vv - kk,m) = m + vv - kk

  mod_int_quot: LEMMA FORALL (k:nat, n:posnat):
               integer_pred((k-mod(k,n))/n) AND (k-mod(k,n))/n>=0

  floor_div_prod: LEMMA FORALL (n,m:posnat,i:nat):
floor(i / (n*m)) = floor(floor(i / m) / n)

  mod_mult_quot: LEMMA FORALL (n,m:posnat,i:nat):
    mod(i, n * m) = mod(i, m) + m * mod((i - mod(i, m)) / m, n)

  AUTO_REWRITE+ mod_0
  AUTO_REWRITE+ mod_1
  AUTO_REWRITE+ mod_by1
  AUTO_REWRITE+ mod_eq_arg           %% mod(j,j) = 0
  AUTO_REWRITE+ mod_sum              %% mod(i+k*j,j) = mod(i,j)
  AUTO_REWRITE+ mod_of_mod           %% mod(i + mod(k,m), m) = mod(i+k, m)

END mod_lems

quality87%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.