Impressum mucalculus_prop.pvs Sprache: PVS

mucalculus_prop [ T:TYPE ] : THEORY
%-------------------------------------------------------------------
%  Fixed points of monotonic functions of type [set[T] -> set[T]]
%  (predicate transformers)
%
%  Shows that operators mu and nu defined in theory mucalculus
%  of the prelude defines the least and greatest fixpoints of
%  a monotonic function
%
%  Defines dual(H) = complement o H o complement
%
%  Shows that mu o dual = complement o nu and
%             nu o dual = complement o mu
%-------------------------------------------------------------------

  BEGIN

  F: VAR (monotonic?[T])

  p, q: VAR pred[T]

  A: VAR set[pred[T]]

  % Auxiliary functions defined in the prelude (theory mucalculus):
  % - relation <= is the same as the subset? relation
  % - glb(A) = { x:T | EXISTS (p: (A)): p(x) }
  % - lub(A) = { x:T | FORALL (p: (A)): p(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_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_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

  closure_mu: PROPOSITION F(mu(F)) <= mu(F)

  smallest_closed: PROPOSITION F(p) <= p IMPLIES mu(F) <= p

  fixpoint_mu1: PROPOSITION F(mu(F)) = mu(F)

  fixpoint_mu2: PROPOSITION fixpoint?(F)(mu(F))

  least_fixpoint1: PROPOSITION F(p) = p IMPLIES mu(F) <= p

  least_fixpoint2: PROPOSITION fixpoint?(F)(p) IMPLIES mu(F) <= p

  mu_lfp: JUDGEMENT mu(F) HAS_TYPE (lfp?(F))

  %--- 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))

  %--- dual of a predicate transformer

  H: VAR [pred[T] -> pred[T]]

  dual(H): [pred[T] -> pred[T]] = complement o H o complement

  dual_dual : LEMMA dual(dual(H)) = H

  dual_inclusion1 : LEMMA
H(complement(p)) <= complement(p) IFF p <= dual(H)(p)

  dual_inclusion2 : LEMMA
complement(p) <= H(complement(p)) IFF dual(H)(p) <= p

  dual_inclusion3 : LEMMA
H(p) <= p IFF complement(p) <= dual(H)(complement(p))

  dual_inclusion4 : LEMMA
p <= H(p) IFF dual(H)(complement(p)) <= complement(p)

  %--- fixed points and dual

  monotonic_dual_monotonic: JUDGEMENT dual(F) HAS_TYPE (monotonic?[T])

  least_fixpoint_dual: PROPOSITION mu(dual(F)) = complement(nu(F))

  greatest_fixpoint_dual: PROPOSITION nu(dual(F)) = complement(mu(F))

  END mucalculus_prop

quality86%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.