| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/algebra/ (NIST Fortran ©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quellcode-Bibliothek 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 ¤ 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.0.15Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
