products/sources/formale sprachen/PVS/algebra/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: tau_declaration.prf   Sprache: PVS

Original von: PVS©
cosets[T:Type+,*:[T,T->T],one:T]: THEORY
%------------------------------------------------------------------------------
% Left and Right Cosets
%
%     Author: Rick Butler, NASA Langley
%             Adapted from work done by David Lester, Manchester
%
%     Version 1.0           12/12/07  
%
% This theory defines convenient notation:
%
%     a*H  -- left coset
%     H*a  -- right coset   
%
%------------------------------------------------------------------------------


BEGIN
%------------------------------------------------------------------------
%  The imported type T with * and one must be a group.
%  From this foundation other groups are created.  These are just subgroups of the
%  underlying imported type.
%------------------------------------------------------------------------
   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING group[T,*,one]

   S,R:       VAR set[T]
   H,G:       VAR group
   a,b,x,y,z: VAR T
   m:         VAR nat


% Herstein Lemma 2.4.3

   congruent_mod(G:group,H:subgroup(G))(a,b:T):bool
                                                       = member(a*inv(b),H)
   congruence_is_equivalence: LEMMA 
        subgroup?(H,G) IMPLIES equivalence?[T](congruent_mod(G,H))


% ---------- Special Coset Notation ------------

   ;

   *(a: T, H: set[T]): set[T] = {t:T | EXISTS (h:(H)): t = a*h} ;  %% left

   *(H: set[T], a: T): set[T] = {t:T | EXISTS (h:(H)): t = h*a} ;  %% right

   left_coset_subset : LEMMA FORALL (H: subgroup(G)),(a:(G)): subset?(a*H,G)
   right_coset_subset: LEMMA FORALL (H: subgroup(G)),(a:(G)): subset?(H*a,G)

   left_coset_one    : LEMMA one*S = S
   right_coset_one   : LEMMA S*one = S

   left_coset_assoc  : LEMMA a*(b*S) = (a*b)*S
   right_coset_assoc : LEMMA (S*a)*b = S*(a*b)

   lr_coset_assoc    : LEMMA (a*S)*b = a*(S*b)

   subset_left_coset : LEMMA subset?(S, R) IMPLIES subset?(a*S, a*R)
   subset_right_coset: LEMMA subset?(S, R) IMPLIES subset?(S*a, R*a)

%  ------------- Cosets ------------------------

% Herstein Lemma 2.4.4

   right_coset(G:group,H:subgroup(G))(a:(G)): { s: set[T] | subset?(s,G)}  
                                                           %% was set[(G)]
                        = H*a
%                       = image((LAMBDA (h:(H)): h*a),(H))


   right_coset_image: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
                        right_coset(G,H)(a) = image((LAMBDA (h:(H)): h*a),(H))

   right_coset_is: LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
                        right_coset(G,H)(a) = {x: T | congruent_mod(G,H)(a,x)}

   right_coset_def   : LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
                        right_coset(G,H)(a) = H*a

% Herstein Lemma 2.4.5

   nonempty_right_coset: LEMMA  subgroup?(H,G) AND member(a,G) IMPLIES
                                                 nonempty?(right_coset(G,H)(a))

   right_coset_correspondence: LEMMA FORALL (A,B:set[T]):
     subgroup?(H,G) AND member(a,G) AND member(b,G) AND
         A = right_coset(G,H)(a) AND B = right_coset(G,H)(b) IMPLIES
       EXISTS (f:[(A)->(B)]): bijective?(f)

% left stuff

   left_coset(G:group,H:subgroup(G))(a:(G)): { s: set[T] | subset?(s,G)}   
                                                          %% was set[(G)]
                        = a*H
%                       = image((LAMBDA (h:(H)): a*h),(H))

   left_coset_image  : LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
                        left_coset(G,H)(a) = image((LAMBDA (h:(H)): a*h),(H))

   left_coset_def    : LEMMA subgroup?(H,G) AND member(a,G) IMPLIES
                        left_coset(G,H)(a) = a*H


%  ---- Define Types ----

   left_cosets(G:group,H:subgroup(G)): TYPE = {s: set[T] |
                      EXISTS (a: (G)): s = a*H}


   right_cosets(G:group,H:subgroup(G)): TYPE = {s: set[T] |
                      EXISTS (a: (G)): s = H*a}

%  --- retrieve a generator -- not unique

   lc_gen(G:group, H: subgroup(G),lc: left_cosets(G,H)): {a: T | G(a) AND lc = a*H} =
                choose({a: T | G(a) AND lc = a*H})

   lc_gen_def: LEMMA subgroup?(H,G) AND G(a) IMPLIES
                         lc_gen(G,H,a*H)*H = a*H



   rc_gen(G:group, H: subgroup(G), rc: right_cosets(G,H)): {a: T | G(a) AND rc = H*a} =
                choose({a: T | G(a) AND rc = H*a})

   rc_gen_def: LEMMA subgroup?(H,G) AND G(a) IMPLIES
                         H*rc_gen(G,H,H*a) = H*a



   lc_eq     : LEMMA subgroup?(H,G) AND a*H = b*H
                     IMPLIES (EXISTS (h: (H)): a = b*h) 


   lc_is_eq  : LEMMA subgroup?(H,G) AND (EXISTS (h: (H)): a = b*h) 
                        IMPLIES a*H = b*H



   rc_eq     : LEMMA subgroup?(H,G) AND H*a = H*b
                     IMPLIES (EXISTS (h: (H)): a = h*b) 


   rc_is_eq  : LEMMA subgroup?(H,G) AND (EXISTS (h: (H)): a = h*b) 
                        IMPLIES H*a = H*b


END cosets

¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff