|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
