Quelle new_mucalculus_prop.pvs Sprache: PVS

% 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

quality96%

¤ 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.