Quellcode-Bibliothek cayleys.pvs

cayleys[T: Type+, *:[T,T->T], one:T]: THEORY
%-----------------------------------------------------------------------------
%  Experimental theory 
%
%     Author: Rick Butler
%
%-----------------------------------------------------------------------------
BEGIN

   ASSUMING IMPORTING group_def[T,*,one], semigroup_def

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING


   IMPORTING homomorphisms

   IMPORTING A_group[T], group
   

   S: VAR semigroup[T,*]

   al(S: set[T], a:(S)):[(S) -> T] = (LAMBDA (s:(S)): a*s);

   ML(S): set[maps(S)] = {al: [(S) -> (S)] | EXISTS (x: (S)): al = al(S,x)}


   cayley_prep: LEMMA FORALL (G: group[T,*,one]): FORALL (a: (G)):
                      bijective?[(G), (G)](LAMBDA (s: (G)): a * s)

   trans_is_group: LEMMA FORALL (G: group[T,*,one]): 
                            group?[maps[T](G), op(G), id(G)](ML(G))

   Cayleys: THEOREM FORALL (G: group[T,*,one]): 
                           isomorphic?[T,*,one,maps(G),op(G),id(G)](G, ML(G))
 
 
END cayleys