|
%------------------------------------------------------------------------------
% Rings
%
% Author: David Lester, Manchester University & NIA
% Rick Butler
%
% Version 1.0 3/1/02
% Version 1.1 12/3/03 New library structure
% Version 1.2 5/5/04 Reworked for definition files DRL
%------------------------------------------------------------------------------
ring[T:Type+,+:[T,T->T],*:[T,T->T],zero:T]: THEORY
BEGIN
ASSUMING IMPORTING ring_def[T,+,*,zero]
fullset_is_ring: ASSUMPTION ring?(fullset[T])
ENDASSUMING
IMPORTING abelian_group[T,+,zero],
operator_defs_more[T]
ring: NONEMPTY_TYPE = (ring?) CONTAINING fullset[T]
% To bring elegance into this theory we define unary and binary minus.
;
-: MACRO [T->T] = inv;
-: MACRO [T,T->T] = (LAMBDA (x,y:T): x + inv[T,+,zero](y))
w,x,y,z: VAR T
R: VAR ring
S: VAR set[T]
plus_associative : LEMMA (x + y) + z = x + (y + z)
plus_commutative : LEMMA x + y = y + x
times_associative : LEMMA (x * y) * z = x * (y * z)
right_distributive : LEMMA x * (y + z) = (x * y) + (x * z)
left_distributive : LEMMA (x + y) * z = (x * z) + (y * z)
zero_plus : LEMMA zero + x = x
plus_zero : LEMMA x + zero = x
negate_is_left_inv : LEMMA -x + x = zero
negate_is_right_inv : LEMMA x + -x = zero
cancel_right_plus : LEMMA x + z = y + z IFF x = y
cancel_left_plus : LEMMA z + x = z + y IFF x = y
negate_negate : LEMMA -(-x) = x
cancel_right_minus : LEMMA x - z = y - z IFF x = y
cancel_left_minus : LEMMA z - x = z - y IFF x = y
negate_zero : LEMMA -zero = zero
negate_plus : LEMMA -(x + y) = -y - x
times_plus : LEMMA (x + y) * (z + w) = x*z + x*w + y*z + y*w
idempotent_add_is_zero : LEMMA x + x = x IMPLIES x = zero
zero_times : LEMMA zero * x = zero
times_zero : LEMMA x * zero = zero
negative_times : LEMMA (-x) * y = - (x * y)
times_negative : LEMMA x * (-y) = - (x * y)
negative_times_negative: LEMMA (-x) * (-y) = x * y
ring_is_abelian_group : JUDGEMENT ring SUBTYPE_OF abelian_group
subring_is_ring : LEMMA subring?(S,R) IMPLIES ring?(S)
sq(x):T = x*x
sq_rew : LEMMA x*x = sq(x)
sq_neg : LEMMA sq(-x) = sq(x)
sq_plus : LEMMA sq(x+y) = sq(x) + x*y + y*x + sq(y)
sq_minus : LEMMA sq(x-y) = sq(x) - x*y - y*x + sq(y)
sq_neg_minus: LEMMA sq(x-y) = sq(y-x)
sq_zero : LEMMA sq(zero) = zero
AUTO_REWRITE+ zero_plus % zero + x = x
AUTO_REWRITE+ plus_zero % x + zero = x
AUTO_REWRITE+ negate_is_left_inv % -x + x = zero
AUTO_REWRITE+ negate_is_right_inv % x + -x = zero
AUTO_REWRITE+ negate_negate % -(-x) = x
AUTO_REWRITE+ negate_zero % -zero = zero
AUTO_REWRITE+ zero_times % zero * x = zero
AUTO_REWRITE+ times_zero % x * zero = zero
END ring
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
