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