SSL cyclic_group.pvs

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

BEGIN
%------------------------------------------------------------------------
%  The imported type T with * and one must be a group.
%  From this foundation other groups are created.  These are just subgroups of the
%  underlying imported type.
%------------------------------------------------------------------------
   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING group[T,*,one]

   a: VAR T
   S: VAR set[T]
   H,G: VAR group
   i: VAR int

%  generated_by(a): group = {t: T | EXISTS (i: int): t = a^i}
%  cyclic?(G): boolean = EXISTS (a:(G)): G = generated_by(a)

   generated_by_lem     : LEMMA generated_by(a)(a^i)

   generated_is_subgroup: LEMMA member(a,G) IMPLIES
                                              subgroup?(generated_by(a),G)

   generated_by_is_finite: LEMMA S = generated_by(a) AND 
                                 (EXISTS (k: posnat): a^k = one)
                              IMPLIES finite_group?(S)


   cyclic_abelian: THEOREM cyclic?(G) IMPLIES abelian_group?(G)


   %% TRICKY %%
   cyclic_subgroup: LEMMA subgroup?(H,G) AND cyclic?(G) IMPLIES cyclic?(H)

   
   is_cyclic   : LEMMA (EXISTS (a:(G)): FORALL (x: (G)): 
                          EXISTS (n: nat): x = a^n) IMPLIES
                                 cyclic?(G)


           
END cyclic_group