|
% A simulation of Bruno Dutertre's fixedpoints/mucalculus_prop.
%
% Author: Alfons Geser, National Institute of Aerospace
% Date: Feb 2005
new_mucalculus_prop[T: TYPE]: THEORY
BEGIN
IMPORTING
fixed_points[set[T]],
sets_complete_lattices[T]
leq_equals_subset: LEMMA <= = subset?[T]
monotonic_is_monotone: JUDGEMENT
(monotonic?[T]) SUBTYPE_OF (monotone?(subset?))
leq_is_complete_lattice: JUDGEMENT
<= HAS_TYPE (complete_lattice?[set[T]])
IMPORTING complementary_lattices[set[T], <=]
C: VAR (complement?(<=))
F: VAR (monotonic?[T])
p, q: VAR pred[T]
x: VAR set[T]
A: VAR set[pred[T]]
fixpoint_equals_fixed_point: LEMMA
fixpoint?(F) = fixed_point?[set[T]](F)
fixpoint2_equals_fixed_point: LEMMA
fixpoint?(F, x) = fixed_point?[set[T]](F)(x)
antisymmetry: LEMMA p <= q AND q <= p IMPLIES p = q
reflexivity: LEMMA p <= p
%--- glb(A) is the greatest lower bound of A
glb_equals_glb: LEMMA glb[T] = glb[set[T]](subset?)
glb_lower_bound: LEMMA FORALL (q: (A)): glb(A) <= q
glb_greatest_lower_bound: LEMMA
p <= glb(A) IFF FORALL (q: (A)): p <= q
%--- lub(A) is the least upper bound of A
lub_equals_lub: LEMMA lub[T] = lub[set[T]](subset?)
lub_upper_bound: LEMMA FORALL (q: (A)): q <= lub(A)
lub_least_upper_bound: LEMMA
lub(A) <= p IFF FORALL (q: (A)): q <= p
%--- properties of mu operator
mu_equals_least_prefixed_point: LEMMA
mu(F) = glb[set[T]](<=)(prefixed_point?(<=)(F))
smallest_closed: PROPOSITION F(p) <= p IMPLIES mu(F) <= p
fixpoint_mu2: PROPOSITION fixpoint?(F)(mu(F))
fixpoint_mu1: PROPOSITION F(mu(F)) = mu(F)
closure_mu: PROPOSITION F(mu(F)) <= mu(F)
least_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES mu(F) <= p
least_fixpoint1: PROPOSITION F(p) = p IMPLIES mu(F) <= p
lfp_equals_lfp: LEMMA lfp?(F) = lfp?[set[T]](<=)(F)
mu_lfp: JUDGEMENT mu(F) HAS_TYPE (lfp?(F))
%--- fixed points and dual
monotonic_dual_monotonic: JUDGEMENT dual(C)(F) HAS_TYPE (monotonic?[T])
least_fixpoint_dual: PROPOSITION mu(dual(C)(F)) = C(nu(F))
greatest_fixpoint_dual: PROPOSITION nu(dual(C)(F)) = C(mu(F))
complement_is_complement: JUDGEMENT
complement[T] HAS_TYPE (complement?(<=))
%--- properties of nu operator
closure_nu: PROPOSITION nu(F) <= F(nu(F))
largest_closed: PROPOSITION p <= F(p) IMPLIES p <= nu(F)
fixpoint_nu1: PROPOSITION F(nu(F)) = nu(F)
fixpoint_nu2: PROPOSITION fixpoint?(F)(nu(F))
greatest_fixpoint1: PROPOSITION F(p) = p IMPLIES p <= nu(F)
greatest_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES p <= nu(F)
nu_gfp: JUDGEMENT nu(F) HAS_TYPE (gfp?(F))
END new_mucalculus_prop
¤ Dauer der Verarbeitung: 0.30 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.
|
