Quellcode-Bibliothek cauchy.pvs

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


cauchy[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  ints@primes,
              algebra@finite_groups,
              algebra@finite_cyclic_groups[T,*,one],
              group_action,
              zp_group,
              cauchy_scaf[T]



              G: VAR finite_group
              p: VAR posnat
   fs, fs1, fs2: VAR finseq
              n: VAR nat
              a: VAR T

   fseq_product(fs): RECURSIVE T =  IF length(fs) = 0 THEN one
                                    ELSE fs`seq(0)*fseq_product(rest(fs))
                                    ENDIF
                                    MEASURE length(fs)

   S(G)(n): set[finseq] = {fs: finseq | length(fs) = n AND 
                                        (FORALL (i: below[n]): member(fs`seq(i), G)) AND 
                                        fseq_product(fs) = one}

   same_element(a, fs):bool = FORALL (i: below[length(fs)]): fs`seq(i) = a


   SE(G)(n): set[finseq] = {fs: (S(G)(n)) | EXISTS (a: (G)): same_element(a, fs)}
   


 %%%%% Properties %%%


   fseq_product_in: LEMMA (FORALL (i: below[length(fs)]): member(fs`seq(i), G))
                              IMPLIES member(fseq_product(fs), G)

   fseq_product_o: LEMMA (FORALL (i: below[length(fs1)]): member(fs1`seq(i), G)) AND
                              (FORALL (j: below[length(fs2)]): member(fs2`seq(j), G))
                                     IMPLIES
                                        fseq_product(fs1 o fs2) = fseq_product(fs1) * fseq_product(fs2)


   fseq_product_one: LEMMA (FORALL (i: below[length(fs)]): member(fs`seq(i), G))
                                  IMPLIES  inv(fseq_product(fs)) * fseq_product(fs) = one

   fseq_product_power: LEMMA FORALL (g: (G)): same_element(g, fs) IMPLIES fseq_product(fs) = g^length(fs)

   one_in_SE: LEMMA length(fs) = n AND same_element(one, fs) IMPLIES member(fs, SE(G)(n))

   order_SE: LEMMA FORALL (g: (G)): prime?(p) AND g /= one AND 
                                         same_element(g, fs) AND member(fs, SE(G)(p))
                                            IMPLIES period(G,g) = p

   S_bij_set_seq: LEMMA LET A = set_seq(G)(p - 1),
                                B = S(G)(p)         IN
                            EXISTS (g:[(A)->(B)]): bijective?(g)

   S_is_finite:LEMMA is_finite(S(G)(n))

   S_card: LEMMA card(S(G)(p)) = card(G)^(p - 1)



%%%%% Group action %%%


   F(p, G)(k: (Zn[p]), fs: (S(G)(p))): finseq = (# length := p,
                                                      seq := (LAMBDA (i: below[p]):fs`seq(rem(p)(i + k))) #)


   F_1(fs)(k: below[length(fs)]): finseq = (# length := length(fs) - k,
                                                 seq := (LAMBDA (i: below[length(fs) - k]): 
                                                            fs`seq(rem(length(fs))(i + k))) #)

   F_2(fs)(k: below[length(fs)]): finseq = (# length := k,
                                                seq := (LAMBDA (i: below[k]): fs`seq(i)) #)



   F_o_F12: LEMMA FORALL (k: (Zn[p]), fs: (S(G)(p))): F(p,G)(k, fs) = F_1(fs)(k) o F_2(fs)(k)

   
   fs_o_F21: LEMMA FORALL (k: (Zn[p]), fs: (S(G)(p))): fs = F_2(fs)(k) o F_1(fs)(k)


   F_in_S: LEMMA FORALL (k: (Zn[p]), fs: (S(G)(p))): member(F(p,G)(k, fs), S(G)(p))


   F_is_action: LEMMA group_action?[below(p),++,0,finseq](Zn[p],S(G)(p))(F(p,G))




%%%%% Fixed point subset %%%

   Fixed_subset: LEMMA  LET H = Zn[p],
                            X = S(G)(p),
                            f = F(p, G) IN
                        Fix[below(p),++,0,finseq](H,X)(f) = SE(G)(p)


%%%%% Cauchy Theorem %%%

   cauchy: THEOREM prime?(p) AND divides(p, order(G)) IMPLIES EXISTS (x: (G)):  period(G,x) = p

   cauchy_cor: COROLLARY prime?(p) AND divides(p, order(G)) IMPLIES EXISTS (H: subgroup(G)): order(H) = p


END cauchy