|
%------------------------------------------------------------------------------
% Rings with one
%
% 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_with_one[T:Type+,+,*:[T,T->T],zero,one:T]: THEORY
BEGIN
ASSUMING IMPORTING ring_def[T,+,*,zero],
ring_with_one_def[T,+,*,zero,one]
fullset_is_ring_with_one: ASSUMPTION ring_with_one?(fullset[T])
ENDASSUMING
IMPORTING ring_with_one_def[T,+,*,zero,one],
ring[T,+,*,zero], monoid[T,*,one], operator_defs_more[T]
ring_with_one: NONEMPTY_TYPE = (ring_with_one?) CONTAINING fullset[T]
R: VAR ring_with_one
x,y: VAR T
one_times : LEMMA one * x = x
times_one : LEMMA x * one = x
unique_left_identity : LEMMA (FORALL x: y*x = x) IFF y = one
unique_right_identity : LEMMA (FORALL x: x*y = x) IFF y = one
minus_one_times : LEMMA (-one)*x = -x
times_minus_one : LEMMA x*(-one) = -x
minus_one_sq_is_one : LEMMA (-one)*(-one) = one
ring_with_one_is_ring : JUDGEMENT ring_with_one SUBTYPE_OF ring
ring_with_one_is_monoid: JUDGEMENT ring_with_one SUBTYPE_OF monoid[T,*,one]
AUTO_REWRITE+ one_times % one * x = x
AUTO_REWRITE+ times_one % x * one = x
AUTO_REWRITE+ minus_one_times % (-one)*x = -x
AUTO_REWRITE+ times_minus_one % x*(-one) = -x
AUTO_REWRITE+ minus_one_sq_is_one % (-one)*(-one) = one
END ring_with_one
[ Seitenstruktur0.1Drucken
etwas mehr zur Ethik
]
|
