Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: new_mucalculus_prop.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.