%------------------------------------------------------------------------------
% 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