Quelle  groups_scaf.pvs

%%-------------------** Some properties of groups and subgroups  **-------------
%%                                                                          
%% Author          : André Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%                    
%% Last Modified On: November 28, 2011
%%                                                                          
%%------------------------------------------------------------------------------


groups_scaf[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@group,
            algebra@factor_groups,
            algebra@finite_groups[T,*,one],
            general_properties,
            right_left_cosets

      G, H, N, K: VAR group
         a, b, c: VAR T
            p, k: VAR posnat
               m: VAR int
               i: VAR nat

%%%%% Definitions %%%%%

  subgroup_contain(G: group, N: subgroup(G)): TYPE = {H: group | subgroup?(H,G) AND subset?(N, H)}



%%%%% Properties of groups and subgroups %%%%%

   divby_r: LEMMA a = b * c  IFF a * inv[T,*,one](c)  = b

   subgroup_transitive: LEMMA subgroup?(H,G) AND  subgroup?(K,H)
                                IMPLIES subgroup?(K,G)

   normal_subgroup_tran: LEMMA subgroup?(H,G) AND subgroup?(N,H) AND
                          normal_subgroup?(N,G)
                                IMPLIES normal_subgroup?(N,H)

   subgroup_intersection: LEMMA  subgroup?(H,G) AND subgroup?(K,G) 
                                IMPLIES subgroup?(intersection(H,K),G)

   conjugate_is_subgroup: LEMMA FORALL (a: (G), H:subgroup(G)): subgroup?(a*H*inv(a),G)

   center_is_normal: LEMMA  normal_subgroup?(center(G),G)

   abelian_eq_center: LEMMA abelian_group?(G) IFF G = center(G)


   order_gt_1: LEMMA FORALL (G:finite_group): 
                      prime?(p) AND divides(p, order(G)) IMPLIES order(G) > 1
  
   order_gt_p: LEMMA FORALL (G:finite_group): 
                      prime?(p) AND divides(p, order(G)) IMPLIES order(G) >= p

   exists_diff_one: LEMMA FORALL (G:finite_group):
                                 order(G) > 1 IMPLIES EXISTS (x: (G)): x /= one

   one_iff_divides: LEMMA FORALL (G:finite_group, a:(G)): 
                             a^m = one IFF divides(period(G,a), m)

   order_power: LEMMA FORALL (G:finite_group, a:(G)): 
                               LET n = period(G,a) IN
                               period(G,a^k) = n / gcd(k,n)


   coset_power_nat: LEMMA FORALL (x:(G), H:normal_subgroup(G)): 
                             ^[left_cosets(G,H),mult(G,H),H](x*H, i) = (x^i)*H

   coset_power_int: LEMMA FORALL (x:(G), H:normal_subgroup(G)): 
                             ^[left_cosets(G,H),mult(G,H),H](x*H, m) = (x^m)*H
END groups_scaf