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 monad.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Monads
%
%     Author: Rick Butler
%             David Lester, Manchester University & NIA
%
%     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
%------------------------------------------------------------------------------

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

BEGIN

   ASSUMING IMPORTING monad_def[T,*,one]

       fullset_is_monad: ASSUMPTION monad?(fullset[T])

   ENDASSUMING

   IMPORTING monad_def[T,*,one], groupoid[T,*]

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

   M:   VAR monad
   x,y: VAR T

   one_member:            LEMMA member(one,M)
   one_in    :            LEMMA M(one)
   left_identity:         LEMMA one * x = x
   right_identity:        LEMMA x * one = x
   unique_left_identity:  LEMMA (FORALL (x:(M)): y*x = x) IFF y = one
   unique_right_identity: LEMMA (FORALL (x:(M)): x*y = x) IFF y = one

   one_is_monad:          LEMMA monad?(singleton[T](one))

   trivial_monad: monad = singleton(one)

   monad_is_groupoid: JUDGEMENT monad SUBTYPE_OF groupoid

   AUTO_REWRITE+ one_member
   AUTO_REWRITE+ one_in
   AUTO_REWRITE+ left_identity
   AUTO_REWRITE+ right_identity
   AUTO_REWRITE+  member
   AUTO_REWRITE+  one_is_monad

   sing_one_finite_monad: LEMMA finite_monad?(singleton[T](one))

   finite_monad: TYPE+ = (finite_monad?)
   commutative_monad: TYPE+ = (commutative_monad?)
   finite_commutative_monad: TYPE+ = (finite_commutative_monad?)

   F: VAR finite_monad

   order(F):posnat  = card(F)

   order_is_1: LEMMA order(F) = 1 IMPLIES F = singleton[T](one)

   finite_monad_is_monad: JUDGEMENT finite_monad SUBTYPE_OF monad

   commutative_monad_is_monad:    JUDGEMENT commutative_monad SUBTYPE_OF monad

   finite_commutative_monad_is_commutative_monad:
      JUDGEMENT finite_commutative_monad SUBTYPE_OF commutative_monad

   finite_commutative_monad_is_finite_monad:
      JUDGEMENT finite_commutative_monad SUBTYPE_OF finite_monad

END monad

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.