SSL finite_groups.pvs

finite_groups[T:Type+,*:[T,T->T],one:T]: THEORY
%-----------------------------------------------------------------------------
% Cyclic Groups
%
%     Author: Rick Butler and David Lester
%
% This are groups generated by an element and repeated multiplication
% using the following defined in theory group.
%
%      generated_by(a): group = {t: T | EXISTS (i: int): t = a^i}
%
%      cyclic?(G): boolean = EXISTS (a:(G)): G = generated_by(a)
%
%-----------------------------------------------------------------------------
BEGIN

   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING


   IMPORTING group[T,*,one],
             ints@primes


   G,H: VAR finite_group
   S:   VAR (nonempty?[T])
   a,b: VAR T
   n:   VAR nat


   finite_generated_by: LEMMA member(a,G) IMPLIES 
                                  is_finite(generated_by(a))   %% RWB

   finite_generated_by_def: LEMMA member(a,G) AND S = generated_by(a) 
                                  IMPLIES S = {t:T | EXISTS (n:posnat): n <= card(S) AND t = a^n}

   finite_generated_by_one: LEMMA member(a,G) AND S = generated_by(a) 
                                  IMPLIES a^card(S) = one


   generated_by_card_1: LEMMA member(a,G) AND 
                              card(generated_by(a)) = 1
                                 IMPLIES a = one AND
                                         generated_by(a) = singleton[T](one)

   
   finite_group_elements: LEMMA member(a,G) IMPLIES finite_order?(a)

   period(G:finite_group,a:(G)):posnat = min({n:posnat | a^n = one})

   a_hat_period:     LEMMA member(a,G) IMPLIES a^(period(G,a)) = one


   finite_subgroup_def: LEMMA
                     subgroup?(S,G) IFF (subset?(S,G) AND star_closed?(S))

   orders_equal: LEMMA order(H) = order(G) AND subgroup?(H,G)
                       IMPLIES G = H


   IMPORTING lagrange[T,*,one]

   period_is_generated_order: LEMMA member(a,G) IMPLIES 
                                         period(G,a) = order(generated_by(a))

   period_element_divides_group: COROLLARY member(a,G) IMPLIES
                                                  divides(period(G,a),order(G))


END finite_groups