|
%------------------------------------------------------------------------------
% Generalised constant functions
%
% Generalises real constant functions.
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 8/10/04 Initial Version
% Version 1.0 8/10/04 Generalised (inverse-)image
%------------------------------------------------------------------------------
const_fun_def[S,T:TYPE]: THEORY
BEGIN
x: VAR S
a: VAR T
X: VAR set[S]
Y: VAR set[T]
const_fun(a): [S->T] = LAMBDA x : a
constant?(f:[S->T]):bool = EXISTS a: f = const_fun(a)
image_const: LEMMA
image(const_fun(a),X)
= IF empty?(X) THEN emptyset[T] ELSE singleton(a) ENDIF
inverse_image_const: LEMMA
inverse_image(const_fun(a),Y)
= IF Y(a) THEN fullset[S] ELSE emptyset[S] ENDIF
END const_fun_def
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
