%%-------------------** p-Groups and Burside Theorem **-------------------
%%                                                                          
%% Author          : André Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%                    
%% Last Modified On: November 28, 2011
%%                                                                          
%%------------------------------------------------------------------------


p_groups[T:Type, *:[T,T->T], one:T]: THEORY

BEGIN
  
     ASSUMING IMPORTING algebra@group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING


   IMPORTING algebra@finite_cyclic_groups,
             algebra@finite_groups[T,*,one],
             normalizer_centralizer[T,*,one],
             cauchy[T, *, one]

    G, H, K: VAR group[T,*,one]
          p: VAR posnat
          n: VAR nat


%%%%% Definitions %%%%%

   p_group?(G:finite_group, p: {p:posnat | prime?(p)} ): bool = FORALL (a:(G)): 
                                                              (EXISTS (n: nat): period(G,a) = p^n)


   alt(G:group,H: subgroup(G),K: subgroup(G))(h:(H), A: (left_cosets(G,K))): set[T] = h*A


; %%%%% Properties and results %%%%%


   alt_is_action: LEMMA FORALL (H, K: subgroup(G)):
                           group_action?(H, left_cosets(G,K))(alt(G,H,K))


   Fix_iff_subset: LEMMA FORALL (H, K: subgroup(G), g: (G)): 
                            member(g*K,  Fix(H,left_cosets(G,K))(alt(G,H,K))) IFF subset?(H, g*K*inv(g))

 
   Fix_iff_subset_cor: LEMMA FORALL (G:finite_group, H, K: subgroup(G), g: (G)): 
                                member(g*H,  Fix(H,left_cosets(G,H))(alt(G,H,H))) IFF H = g*H*inv(g)

   subgroup_is_p_group: LEMMA FORALL (G:finite_group,H: subgroup(G)): 
                                 prime?(p) AND p_group?(G,p) IMPLIES p_group?(H,p)

   p_group_iff_power: LEMMA FORALL (G:finite_group): 
                                  prime?(p) IMPLIES (p_group?(G,p) IFF (EXISTS (m:nat): order(G) = p^m))

   p_divides_index: LEMMA FORALL (G:finite_group, H:subgroup(G)): 
                            prime?(p) AND p_group?(G,p) AND H /= G IMPLIES divides(p, index(G,H))

   factor_cyclic: LEMMA cyclic?(G/center(G)) IMPLIES abelian_group?(G)

   normalizer_index: LEMMA FORALL (G:finite_group, H:subgroup(G)): 
                                 prime?(p) AND p_group?(H,p) AND divides(p, index(G,H))
                                   IMPLIES divides(p, index(normalizer(G,H), H))
 
   subgroup_proper: LEMMA  FORALL (G:finite_group, H:subgroup(G)): 
                                 prime?(p) AND p_group?(G,p) AND H /= G
                                   IMPLIES H /= normalizer(G,H)

%%%%% Burside Theorem %%%%%

  burside_theorem: THEOREM FORALL (G:finite_group): 
                                  order(G) > 1 AND prime?(p) AND p_group?(G,p)
                                     IMPLIES order(center(G)) >= p
   
  p_square_is_abelian: LEMMA FORALL (G:finite_group): prime?(p) AND order(G) = p^2 
                               IMPLIES abelian_group?(G)

 

END p_groups