|
%------------------------------------------------------------------------------
% Monoids
%
% Author: David Lester, Manchester University & NIA
% Rick Butler
%
% 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
%------------------------------------------------------------------------------
monoid[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN
ASSUMING IMPORTING monoid_def[T,*,one], semigroup_def
fullset_is_monoid: ASSUMPTION monoid?(fullset[T])
ENDASSUMING
IMPORTING monoid_def[T,*,one], monad[T,*,one], semigroup[T,*]
monoid: TYPE+ = (monoid?) CONTAINING fullset[T]
S: VAR set[T]
M: VAR monoid
a: VAR T
n,m: VAR nat
monoid_is_monad: JUDGEMENT monoid SUBTYPE_OF monad
monoid_is_semigroup: JUDGEMENT monoid SUBTYPE_OF semigroup
submonoid?(S,M): bool = subset?(S,M) AND monoid?(S)
power_0: LEMMA power(a,0) = one
power_1: LEMMA power(a,1) = a
one_power: LEMMA power(one,n) = one
power_def: LEMMA power(a,n+1) = power(a,n)*a
power_mult: LEMMA power(a,n)*power(a,m) = power(a,n+m)
power_power: LEMMA power(power(a,n),m) = power(a,n*m)
power_commutes: LEMMA power(a,n)*power(a,m) = power(a,m)*power(a,n)
power_member: LEMMA member(a,M) IMPLIES member(power(a,n),M)
one_is_monoid: LEMMA monoid?(singleton[T](one))
AUTO_REWRITE+ power_0
AUTO_REWRITE+ power_1
AUTO_REWRITE+ one_power
AUTO_REWRITE+ one_is_monoid
generated_is_submonoid: LEMMA member(a,M) IMPLIES
submonoid?(generated_set(a),M)
generated_set_card_1: LEMMA member(a,M) AND
is_finite(generated_set(a)) AND
card(generated_set(a)) = 1
IMPLIES a = one AND
generated_set(a) = singleton[T](one)
finite_monoid: TYPE+ = (finite_monoid?)
F: VAR finite_monoid
finite_monoid_is_monoid: JUDGEMENT finite_monoid SUBTYPE_OF monoid
finite_monoid_is_finite_monad:
JUDGEMENT finite_monoid SUBTYPE_OF finite_monad
finite_submonoids: LEMMA submonoid?(S,M) IMPLIES finite_monoid?(F)
commutative_monoid: TYPE+ = (commutative_monoid?)
commutative_monoid_is_monoid: JUDGEMENT commutative_monoid SUBTYPE_OF monoid
commutative_monoid_is_commutative_monad:
JUDGEMENT commutative_monoid SUBTYPE_OF commutative_monad
H: VAR commutative_monoid
commutative_submonoids: LEMMA submonoid?(S,H) IMPLIES commutative_monoid?(S)
END monoid
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
