Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 5 kB

Quelle group_action.pvs Sprache: PVS

%%-------------------** Group Action and Class Equation **-------------------
%%
%% Author          : André Luiz Galdino
%%                   Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: November 28, 2011
%%
%%---------------------------------------------------------------------------

group_action[T: TYPE, *: [T,T -> T], one: T, T1: TYPE]: THEORY

BEGIN

     ASSUMING IMPORTING algebra@group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING algebra@group[T,*,one],
             algebra@factor_groups[T,*,one],
             lagrange_index[T,*,one],
             class_equation_scaf[set[T1],T1],
             groups_scaf

    G, H, K: VAR group[T,*,one]
       X, Y: VAR set[T1]
          p: VAR posnat
          n: VAR nat
     F(G,X): TYPE = [(G), (X) -> (X)]

%%%%% Definitions %%%%

   group_action?(G, X)(f:F(G,X)): bool = FORALL (g1, g2:(G), x: (X)):
                             f(one, x) = x AND f(g1 * g2, x) = f(g1, f(g2, x))

   stabilizer(G,X)(f: F(G,X), x: (X)): {S: set[T] | subset?(S,G)} = {g:(G) | f(g,x) = x}

   orbit(G,X)(f: F(G,X), x: (X)): {Y: set[T1] | subset?(Y,X)} = {y:(X) | EXISTS (g:(G)): y = f(g, x)}

   orbits(G,X)(f: F(G,X)): setofsets[T1] = {Y: set[T1] | EXISTS (x:(X)): Y = orbit(G,X)(f,x)}


   Fix(G,X)(f: F(G,X)): {Y: set[T1] | subset?(Y,X)} = {x:(X) | FORALL (g:(G)): f(g, x) = x}

   orbits_nFix(G,X)(f: F(G,X)): setofsets[T1] = {Y: (orbits(G,X)(f)) |
                                     EXISTS (x: {x:(X) | NOT member(x, Fix(G,X)(f))}): Y = orbit(G,X)(f,x)}

%%%%% Properties and results %%%%

   stabilizer_is_subgroup: LEMMA FORALL (x:(X), f:F(G,X)):
                              group_action?(G, X)(f) IMPLIES subgroup?(stabilizer(G,X)(f, x), G)

   singleton_iff_Fix: LEMMA FORALL (x:(X), f:F(G,X)):
                         group_action?(G, X)(f)
                            IMPLIES
                              (orbit(G,X)(f,x) = singleton(x) IFF member(x, Fix(G,X)(f)))

   empty_iff_eq_Fix: LEMMA FORALL (f:F(G,X)):
                              group_action?(G, X)(f)
                                 IMPLIES
                                    (empty?(orbits_nFix(G,X)(f)) IFF X = Fix(G,X)(f))

   orbits_nFix_disj_Fix: LEMMA FORALL (f:F(G,X)):
                            group_action?(G, X)(f)
                               IMPLIES disjoint?(Fix(G,X)(f),Union(orbits_nFix(G,X)(f)))

   orbits_is_union: LEMMA FORALL (f:F(G,X)):
                       group_action?(G, X)(f)
                          IMPLIES Union(orbits(G,X)(f)) = union(Fix(G,X)(f), Union(orbits_nFix(G,X)(f)))

   orbit_nonempty: LEMMA FORALL (x:(X), f:F(G,X)):
                      group_action?(G, X)(f) IMPLIES nonempty?(orbit(G,X)(f,x))

   orbits_nonempty: LEMMA FORALL (f:F(G,X)): nonempty?(X) AND group_action?(G, X)(f)
                             IMPLIES nonempty?(orbits(G,X)(f))

   set_orbits_is: LEMMA FORALL (f:F(G,X)): group_action?(G, X)(f)
                          IMPLIES Union(orbits(G,X)(f)) = X

   orbit_is_finite: LEMMA FORALL (x:(X), f:F(G,X)):
                            is_finite(X) AND group_action?(G, X)(f)
                               IMPLIES
                                  is_finite(orbit(G,X)(f,x))

   orbits_disjoint: LEMMA FORALL (f:F(G,X), A,B: (orbits(G,X)(f))):
                             group_action?(G, X)(f)
                                IMPLIES
                                   A = B OR disjoint?(A,B)

   orbits_partition: LEMMA  FORALL (f:F(G,X)):
                              is_finite(X) AND group_action?(G, X)(f)
                                IMPLIES
                                   finite_partition?(orbits(G,X)(f))

   orbits_nFix_partition: LEMMA FORALL (f:F(G,X)):
                                   is_finite(X) AND group_action?(G, X)(f)
                                      IMPLIES
                                         finite_partition?(orbits_nFix(G,X)(f))

   orbits_eq_index_aux: LEMMA
      FORALL (x:(X), f:F(G,X)): group_action?(G, X)(f)
        IMPLIES
          EXISTS (f:[(left_cosets(G,stabilizer(G,X)(f, x))) -> (orbit(G,X)(f,x))]): bijective?(f)

   orbits_eq_index: LEMMA FORALL (G:finite_group, x:(X), f:F(G,X)):
                         is_finite(X) AND group_action?(G, X)(f)
                            IMPLIES
                              index(G, stabilizer(G,X)(f, x)) = card(orbit(G,X)(f,x))

%%%%% Class Equation %%%%%%%%%%%%%%%%%%%%%%%%

%                 ----
%  sigma(X, f) =  \     f(x)
%                 /
%                 ----
%              member(x,X)

   counting_formula: LEMMA FORALL (f:F(G,X)):
                             finite_group?(G) AND is_finite(X) AND
                             nonempty?(X)     AND group_action?(G, X)(f)
                                IMPLIES
                                  card(X) = sigma_set.sigma(orbits(G,X)(f), card)

   class_equation: LEMMA FORALL (f:F(G,X)):
                            finite_group?(G) AND is_finite(X) AND
                            nonempty?(X)     AND group_action?(G, X)(f)
                               IMPLIES
                                  card(X) = card(Fix(G,X)(f)) + sigma_set.sigma(orbits_nFix(G,X)(f), card)

   Fix_congruence: LEMMA FORALL (f:F(G,X)):
                            finite_group?(G) AND order(G) = p^n AND
                            is_finite(X)     AND nonempty?(X)   AND
                            prime?(p)        AND group_action?(G, X)(f)
                              IMPLIES
                                 divides(p, card(X) - card(Fix(G,X)(f)))

END group_action

quality62%

¤ Dauer der Verarbeitung: 0.1 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.