Quelle number_fields_bis.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Properties of (non-real) number fields
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            5/27/04   Initial version (DRL)
%
%             Narkawicz 12/2013
%------------------------------------------------------------------------------

number_fields_bis: THEORY

  BEGIN

  w, x, y, z:              VAR number_field
  n0x, n0y, n0z, nzx, nzy: VAR nznum

% We have (from the prelude) the following properties of number_fields:
%
%  commutative_add : POSTULATE x + y = y + x
%  associative_add : POSTULATE x + (y + z) = (x + y) + z
%  identity_add    : POSTULATE x + 0 = x
%  inverse_add     : AXIOM x + -x = 0
%  minus_add       : AXIOM x - y = x + -y
%  commutative_mult: AXIOM x * y = y * x
%  associative_mult: AXIOM x * (y * z) =  (x * y) * z
%  identity_mult   : AXIOM 1 * x = x
%  inverse_mult    : AXIOM n0x * (1/n0x) = 1
%  div_def         : AXIOM y/n0x = y * (1/n0x)
%  distributive    : POSTULATE x * (y + z) = (x * y) + (x * z)

% Because the built-in decision procedures only work for reals, we'll restate
% some of the above in order to define AUTO-REWRITEs. Because we don't expect
% users to have to type the names, we'll make the names long so as to avoid
% overloading and potential conflicts.

  number_fields_left_identity_add      : LEMMA 0 + x = x
  number_fields_right_identity_add     : LEMMA x + 0 = x
  number_fields_left_identity_mult     : LEMMA 1 * x = x
  number_fields_right_identity_mult    : LEMMA x * 1 = x
  number_fields_negate_is_left_inverse : LEMMA -x + x = 0
  number_fields_negate_is_right_inverse: LEMMA x + -x = 0

% However, the following are not available unless the field is a subtype
% of real. So we have to add them, proving from the AXIOMs above.

  % Cancellation Laws for equality

  both_sides_plus1:  LEMMA (x + z = y + z) IFF x = y
  both_sides_plus2:  LEMMA (z + x = z + y) IFF x = y
  both_sides_minus1: LEMMA (x - z = y - z) IFF x = y
  both_sides_minus2: LEMMA (z - x = z - y) IFF x = y

  number_fields_negate_negate          : LEMMA -(-x) = x

  zero_times1: LEMMA 0 * x = 0
  zero_times2: LEMMA x * 0 = 0
  nznum_times_nznum_is_nznum: JUDGEMENT *(nzx, nzy) HAS_TYPE nznum
  minus_nznum_is_nznum:       JUDGEMENT -(nzx)      HAS_TYPE nznum
  zero_times3: LEMMA x * y = 0 IFF x = 0 OR y = 0
  neg_times_neg: LEMMA (-x) * (-y) = x * y
  zero_is_neg_zero: LEMMA -0 = 0

  both_sides_times1: LEMMA (x * n0z = y * n0z) IFF x = y
  both_sides_times2: LEMMA (n0z * x = n0z * y) IFF x = y

  inv_ne_0: LEMMA 1/n0x /= 0
  nznum_div_nznum_is_nznum:   JUDGEMENT /(nzx, nzy) HAS_TYPE nznum
  both_sides_div1: LEMMA (x/n0z = y/n0z) IFF x = y
  both_sides_div2: LEMMA (n0z/n0x = n0z/n0y) IFF n0x = n0y

  times_plus: LEMMA (x + y) * (z + w) = x*z + x*w + y*z + y*w
  times_div1: LEMMA x * (y/n0z) = (x * y)/n0z
  times_div2: LEMMA (x/n0z) * y = (x * y)/n0z
  div_eq_zero: LEMMA x/n0z = 0 IFF x = 0

  div_simp:    LEMMA n0x/n0x = 1
  div_cancel1: LEMMA n0z * (x/n0z) = x
  div_cancel2: LEMMA (x/n0z) * n0z = x
  div_cancel3: LEMMA x/n0z = y IFF x = y * n0z
  div_cancel4: LEMMA y = x/n0z IFF y * n0z = x

  cross_mult: LEMMA (x/n0x = y/n0y) IFF (x * n0y = y * n0x)
  div_times:  LEMMA (x/n0x) * (y/n0y) = (x*y)/(n0x*n0y)
  add_div:    LEMMA (x/n0x) + (y/n0y) = (x * n0y + y * n0x)/(n0x * n0y)
  minus_div1: LEMMA (x/n0x) - (y/n0y) = (x * n0y - y * n0x)/(n0x * n0y)
  minus_div2: LEMMA (x/n0x - y/n0x) = (x - y)/n0x
  div_distributes: LEMMA (x/n0z) + (y/n0z) =  (x + y)/n0z
  div_distributes_minus: LEMMA (x/n0z) - (y/n0z) =  (x - y)/n0z
  div_div1:   LEMMA (x / (n0y / n0z)) = ((x * n0z) / n0y)
  div_div2:   LEMMA ((x / n0y) / n0z) = (x / (n0y * n0z))
  idem_add_is_zero: LEMMA x + x = x IMPLIES x = 0

  nonzero_times1: LEMMA n0x * y = 0 IFF y = 0
  nonzero_times2: LEMMA x * n0y = 0 IFF x = 0
  nonzero_times3: LEMMA n0x * n0y = 0 IFF FALSE

  idem_mult: LEMMA x * x = x IFF x = 0 OR x = 1

  number_fields_negative_times         : LEMMA (-x) * y = -(x * y)
  number_fields_times_negative         : LEMMA x * (-y) = -(x * y)

  number_fields_neg1_times        : LEMMA -1*x = -x

%  AUTO_REWRITE+  number_fields_left_identity_add
%  AUTO_REWRITE+  number_fields_right_identity_add
%  AUTO_REWRITE+  number_fields_left_identity_mult
%  AUTO_REWRITE+  number_fields_right_identity_mult
%  AUTO_REWRITE+  number_fields_negate_is_left_inverse
%  AUTO_REWRITE+  number_fields_negate_is_right_inverse
%  AUTO_REWRITE+  number_fields_negate_negate

%  AUTO_REWRITE+  number_fields_bis.zero_times1
%  AUTO_REWRITE+  number_fields_bis.zero_times2
%  AUTO_REWRITE+  number_fields_bis.zero_is_neg_zero

%  AUTO_REWRITE+  number_fields_bis.neg_times_neg
%  AUTO_REWRITE+  number_fields_bis.times_div1
%  AUTO_REWRITE+  number_fields_bis.times_div2

  END number_fields_bis

quality100%

¤ Dauer der Verarbeitung: 0.12 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.