products/sources/formale Sprachen/VDM/VDMSL/STVSL image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: monad.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% 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

[ Verzeichnis aufwärts0.1unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]