Quelle  finite_cyclic_groups.pvs

finite_cyclic_groups[T:Type+,*:[T,T->T],one:T]: THEORY
%-----------------------------------------------------------------------------
% Cyclic Groups
%
%     Author: Rick Butler
%
% 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 finite_groups[T,*,one], cyclic_group[T,*,one],
             ints@primes


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

   prime_order_cycle: THEOREM prime?(order(G)) IMPLIES
                              cyclic?(G)


END finite_cyclic_groups