Quelle cosets.pvs Sprache: 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

quality98%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.