factor_groups[T:Type+,*:[T,T->T],one:T]: THEORY
%-----------------------------------------------------------------------------
%  Experimental theory working towards factor groups
%
%     Author: Rick Butler
%
%-----------------------------------------------------------------------------
BEGIN
  
   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING normal_subgroups[T,*,one]

   AUTO_REWRITE+ member


   H,G: VAR group[T,*,one]
   a,b,h:   VAR T


   p0: LEMMA FORALL (G: group, H: normal_subgroup(G), A,B: left_cosets(G, H)):
                    nonempty?[set[T]]({S: set[T] | EXISTS (a, b: (G)):
                                  A = a*H AND B = b*H AND S = (a * b)*H })

 
   prep: LEMMA FORALL (a1,a2,b1,b2: (G)): FORALL (H: normal_subgroup(G)):
       a1*H = a2*H AND b1*H = b2*H IMPLIES (a1*b1)*H = (a2*b2)*H

   mult_prep: LEMMA FORALL (G: group, H: normal_subgroup(G), A,B: left_cosets(G, H)):
                    singleton?[set[T]] ({S: set[T] | EXISTS (a, b: (G)):
                                                  A = a*H AND B = b*H AND S = (a * b)*H })

   AUTO_REWRITE+ left_coset

   mult(G:group,H:normal_subgroup(G))(A,B: left_cosets(G,H)): left_cosets(G,H)  = 
            lc_gen(G,H,A)*lc_gen(G,H,B)*H


   mult_lem  : LEMMA FORALL (G: group, H: normal_subgroup(G), a,b: (G)): 
                        mult(G,H)(a*H,b*H) = (a*b)*H

   mult_in   : LEMMA FORALL (G: group, H: normal_subgroup(G)),(A,B: left_cosets(G,H)):
                             mult(G, H)(A,B)(a) IMPLIES G(a)     

   mult_is_coset: LEMMA FORALL (G: group, H: normal_subgroup(G)),(A,B: left_cosets(G,H)):
                           EXISTS (a: (G)): mult(G, H)(A,B) = a*H                    



   N_is_identity: LEMMA FORALL (G: group, N: normal_subgroup(G)), (A: left_cosets(G,N)):
                               mult(G,N)(N,A) = A AND mult(G,N)(A,N) = A


   IMPORTING group               

   left_cosets_group: THEOREM FORALL (G: group, N: normal_subgroup(G)):
              group?[left_cosets(G, N), mult(G, N), N](fullset[left_cosets(G, N)])


   ; %% ----- define G/N as set of all left_cosets

   /(G: group[T,*,one], N: normal_subgroup(G)): group[left_cosets(G,N),mult(G,N),N] 
                 = fullset[left_cosets(G, N)]


   over(G: group[T,*,one], N: normal_subgroup(G)): group[left_cosets(G,N),mult(G,N),N] 
                 = fullset[left_cosets(G, N)]

  factor_type(G:group,N:normal_subgroup(G)): TYPE+ = left_cosets(G,N)
 
END factor_groups