symmetric_groups.pvs

symmetric_groups[N: posnat]: THEORY
%
%  RWB: adapted from old algebra library
%
BEGIN

   S: set[posnat] = fullset[{n: posnat | n <= N}]

   perm: TYPE = (bijective?[(S),(S)])

   Sym: set[perm] = fullset[perm]

   IMPORTING group_def

   id: perm = identity[(S)]

   op: [perm,perm -> perm] = function_props[(S),(S),(S)].o

   Sym_is_group: LEMMA group?[perm,op,identity[(S)]](Sym)

%   Sym_finite: LEMMA is_finite[perm](Sym)   %% UNPROVED %%

%   IMPORTING factorial

%   order_Sym: LEMMA order[perm,op,id](Sym) = factorial(N)  %% UNPROVED %%

END symmetric_groups