Quellcode-Bibliothek normal_subgroups.pvs

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

   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

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

   AUTO_REWRITE+ member


   inv(a:T): MACRO T = inv[T,*,one](a)

   H,G,N: VAR group[T,*,one]

   normal_prep: LEMMA (FORALL (a: (G)): subset?(inv(a)*N*a,N) ) AND subgroup?(N,G) 
                      IMPLIES FORALL (a: (G)): a*N*inv(a) = N


   normal_subgroup?(N: group[T,*,one], G: group[T,*,one]): boolean = subgroup?(N,G) AND
                                          FORALL (a: (G)): subset?(inv(a)*N*a,N) ;

   normal_left_is_right: THEOREM normal_subgroup?(N,G) IFF 
                                  (subgroup?(N,G) AND 
                                  (FORALL (a:(G)): a*N = N*a))

   normal_subgroup(G): TYPE = {N: group | normal_subgroup?(N,G)}

   normal_subgroup_is_subgroup: JUDGEMENT normal_subgroup(G) SUBTYPE_OF subgroup(G)


   a,h: VAR T
   nsg_prop      : LEMMA FORALL (G: group, H: normal_subgroup(G)): 
                         G(a) and H(h) IMPLIES H(a*h*inv(a))


   nsg_prop2     : LEMMA FORALL (G: group, H: normal_subgroup(G)): 
                         G(a) and H(h) IMPLIES H(inv(a)*h*a)


   lc_gen_normal : LEMMA normal_subgroup?(H,G) AND G(a) IMPLIES
                         (EXISTS (h: (H)): lc_gen(G,H,a*H) = h*a)



   abelian_normal: LEMMA abelian_group?(G) and subgroup?(H,G)
                         IMPLIES normal_subgroup?(H,G)


END normal_subgroups