Quelle  lagrange.pvs

%------------------------------------------------------------------------------
% Lagrange
%
%     Author: Rick Butler
%             David Lester, Manchester University & NIA
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%------------------------------------------------------------------------------

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

BEGIN

   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING group[T,*,one], cosets[T,*,one]
             

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

   IMPORTING lagrange_scaf


% Herstein Lemma 2.4.5 (Corollary)

   right_coset_finite: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
                               is_finite(right_coset(G,H)(a))

   finite_right_coset_correspondence: LEMMA
               subgroup?(H,G) AND member(a,G) AND member(b,G) IMPLIES
               card(right_coset(G,H)(a)) = card(right_coset(G,H)(b))

% Herstein Theorem 2.4.1

  set_right_cosets_full: LEMMA FORALL (G: group, H: subgroup(G)):
                              Union(fullset[right_cosets(G,H)]) = G


  right_cosets_disjoint: LEMMA FORALL (G: group, H: subgroup(G), A,B: right_cosets(G, H)):
                                     A = B OR disjoint?(A,B)


  right_cosets_partition: LEMMA FORALL (G: finite_group, H: subgroup(G)):
                                    finite_partition?[T](fullset[right_cosets(G, H)])



  Lagrange: THEOREM subgroup?(H,G) IMPLIES divides(order(H),order(G))  %% NEW rwb


END lagrange