%------------------------------------------------------------------------------ % Groups definition file % % 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 %------------------------------------------------------------------------------
group_def[T:Type+,*:[T,T->T],one:T]: THEORY
BEGIN
IMPORTING monoid_def[T,*,one]
S: VAR set[T]
inv_exists?(S): bool
= FORALL (x:(S)): EXISTS (y:(S)): x*y = one AND y*x = one
group?(S): bool = monoid?(S) AND inv_exists?(S)
finite_group?(S): bool = group?(S) AND is_finite(S)
abelian_group?(S): bool = group?(S) AND commutative?[(S)](*)
finite_abelian_group?(S): bool = finite_group?(S) AND commutative?[(S)](*)
subgroup?(S:set[T],G:(group?)): bool = subset?(S,G) AND group?(S)
