NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • Top File of PVS algebra Library

     
    
    %------------------------------------------------------------------------------
    % 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
    
    
    

    The tag [*] identifies links that are outside the NASA domain