Quelle  commutative_ring_with_one.pvs

%------------------------------------------------------------------------------
% Commutative rings with one
%
%     Author: Rick Butler
%             David Lester, Manchester University & NIA
%
%     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
%------------------------------------------------------------------------------

commutative_ring_with_one[T:Type+,+,*:[T,T->T],zero,one:T]: THEORY

BEGIN

   ASSUMING IMPORTING ring_with_one_def[T,+,*,zero,one]

      fullset_is_commutative_ring_with_one: ASSUMPTION
                                         commutative_ring_with_one?(fullset[T])

   ENDASSUMING

   IMPORTING operator_defs_more[T], ring_with_one[T,+,*,zero,one],
             commutative_ring[T,+,*,zero]

   commutative_ring_with_one: TYPE+ = (commutative_ring_with_one?)
                                                          CONTAINING fullset[T]

   R: VAR commutative_ring_with_one

   commutative_ring_with_one_is: LEMMA commutative_ring_with_one?(R)

   commutative_ring_with_one_is_commutative_ring: JUDGEMENT
                     commutative_ring_with_one SUBTYPE_OF commutative_ring

   commutative_ring_with_one_is_ring_with_one: JUDGEMENT
                     commutative_ring_with_one SUBTYPE_OF ring_with_one

   commutative_ring_with_one_is_commutative_monoid: JUDGEMENT
               commutative_ring_with_one SUBTYPE_OF commutative_monoid[T,*,one]

END commutative_ring_with_one