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/algebra/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

Quelle monoid.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Monoids
%
%     Author: David Lester, Manchester University & NIA
%             Rick Butler
%
%     Version 1.0            3/1/02
%     Version 1.1           12/3/03   New library structure
%     Version 1.2            5/5/04   Reworked for definition files DRL
%------------------------------------------------------------------------------

monoid[T:Type+,*:[T,T->T],one:T]: THEORY

BEGIN

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

       fullset_is_monoid: ASSUMPTION monoid?(fullset[T])

   ENDASSUMING

   IMPORTING monoid_def[T,*,one], monad[T,*,one], semigroup[T,*]

   monoid: TYPE+ = (monoid?) CONTAINING fullset[T]

   S:   VAR set[T]
   M:   VAR monoid
   a:   VAR T
   n,m: VAR nat

   monoid_is_monad:     JUDGEMENT monoid SUBTYPE_OF monad
   monoid_is_semigroup: JUDGEMENT monoid SUBTYPE_OF semigroup

   submonoid?(S,M): bool = subset?(S,M) AND monoid?(S)

   power_0:             LEMMA power(a,0)            = one
   power_1:             LEMMA power(a,1)            = a
   one_power:           LEMMA power(one,n)          = one
   power_def:           LEMMA power(a,n+1)          = power(a,n)*a
   power_mult:          LEMMA power(a,n)*power(a,m) = power(a,n+m)
   power_power:         LEMMA power(power(a,n),m)   = power(a,n*m)
   power_commutes:      LEMMA power(a,n)*power(a,m) = power(a,m)*power(a,n)
   power_member:        LEMMA member(a,M) IMPLIES member(power(a,n),M)

   one_is_monoid:       LEMMA monoid?(singleton[T](one))

   AUTO_REWRITE+ power_0
   AUTO_REWRITE+ power_1
   AUTO_REWRITE+ one_power
   AUTO_REWRITE+ one_is_monoid

   generated_is_submonoid: LEMMA member(a,M) IMPLIES
                                                submonoid?(generated_set(a),M)

   generated_set_card_1: LEMMA member(a,M) AND
                               is_finite(generated_set(a)) AND
                               card(generated_set(a)) = 1
                                 IMPLIES a = one AND
                                      generated_set(a) = singleton[T](one)

   finite_monoid: TYPE+ = (finite_monoid?)

   F: VAR finite_monoid

   finite_monoid_is_monoid: JUDGEMENT finite_monoid SUBTYPE_OF monoid
   finite_monoid_is_finite_monad:
                          JUDGEMENT finite_monoid SUBTYPE_OF finite_monad

   finite_submonoids: LEMMA submonoid?(S,M) IMPLIES finite_monoid?(F)

   commutative_monoid: TYPE+ = (commutative_monoid?)

   commutative_monoid_is_monoid: JUDGEMENT commutative_monoid SUBTYPE_OF monoid
   commutative_monoid_is_commutative_monad:
                  JUDGEMENT commutative_monoid SUBTYPE_OF commutative_monad

   H: VAR commutative_monoid
   commutative_submonoids: LEMMA submonoid?(S,H) IMPLIES commutative_monoid?(S)

END monoid

quality100%

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