Quelle  top.pvs

%------------------------------------------------------------------------------
% Mathematical Structures (algebra)
%
% Group-, Ring-, and Field-like Mathematical Structures.
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler,  NASA Langley
%             
%
%     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
%     Version 1.3          10/18/04   Added a bunch of AUTO-REWRITE+s
%     Version 1.4           8/27/07   Added theory cyclic_groups
%     Version 1.5          12/14/07   Lagrange proof improved, cosets
%                                     factor_groups
%     Version 1.6          12/20/07   Consolidated finite_* theories into
%                                     main theories -- no need for parent type
%                                     to be finite. Can construct finite
%                                     groups from infinite domains, renamed 
%                                     inverse -> inv for slow typers
%
%------------------------------------------------------------------------------

top: THEORY

BEGIN

   IMPORTING top_group,
             %---------------------
             groupoid,              
             commutative_groupoid,  
             semigroup,             
             commutative_semigroup, 
             monad,                 
             monoid,                
             cyclic_monoid,
             cyclic_group,
             group,   
             subgroups,          
             lagrange,
             abelian_group,      
             symmetric_groups,
             group_test,

             finite_cyclic_groups,
             infinite_cyclic_groups,
             factor_groups,          %% RWB experimental
             A_group,       
             homomorphisms, 
             cayleys,       
             zn,                   

             top_field,
             %---------------------------
             ring,                      % semigroup[T,*]
             commutative_ring,          % commutative_semigroup[T,*]
             ring_nz_closed,            % semigroup[T,*], semigroup[nz_T,*]
             ring_with_one,             % monoid[T,*,one]
             commutative_ring_with_one, % commutative_monoid[T,*,one]
             integral_domain,           % commutative_semigroup[T,*]
                                        % commutative_semigroup[nz_T,*]
             division_ring,             % monoid[T,*,one], group[nz_T,*,one]
             field                      % commutative_monoid[T,*,one]
                                        % abelian_group[nz_T,*,one]
END top