%------------------------------------------------------------------------------
% Extras for PartialFunctionDefinitions
%
% Author: David Lester <[email protected]> Manchester University
%
% Version 1.0 03/30/06
%------------------------------------------------------------------------------
partial_function_props[X,Y:TYPE]: THEORY
BEGIN
IMPORTING PartialFunctionDefinitions[X,Y],
orders@lift_props[Y]
f,f1,f2: VAR LiftPartialFunction
dom(f): set[X] = dom(LPartFun_to_SPartFun(f))
range(f):set[Y] = image(fun(LPartFun_to_SPartFun(f)),
dom(LPartFun_to_SPartFun(f)))
graph(f):set[[X,Y]] = graph(fun(LPartFun_to_SPartFun(f)))
x: VAR X
y,y1,y2: VAR Y
Z: VAR set[Y]
z: VAR lift[Y]
h: VAR [X->Y]
member_dom: LEMMA dom(f)(x) IFF f(x) /= bottom
member_graph: LEMMA (EXISTS y: graph(f)(x,y)) IFF f(x) /= bottom
graph_eq: LEMMA graph(f1) = graph(f2) IFF f1 = f2
graph?(G:set[[X,Y]]):bool
= FORALL x,y1,y2: G(x,y1) AND G(x,y2) IMPLIES y1 = y2
g: VAR (graph?)
from_graph(g):LiftPartialFunction
= LAMBDA x: LET Z = {y | g(x,y)} IN
IF nonempty?(Z) THEN up(choose(Z)) ELSE bottom ENDIF
graph_is_graph?: LEMMA graph?(graph(f))
graph_from_graph: LEMMA graph(from_graph(g)) = g
from_graph_graph: LEMMA from_graph(graph(f)) = f
lifted(h):LiftPartialFunction = LAMBDA x: up(h(x))
END partial_function_props
¤ Dauer der Verarbeitung: 0.0 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.
|
