Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: monad.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.