Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: new_mucalculus_prop.prf Sprache: PVS

Original von: PVS^©

finite_bags_aux[T: TYPE]: THEORY
%-------------------------------------------------------------------------
%
% Additional properties of finite bags.
%
%    Author: David Griffioen   (CWI Amsterdam and KUN)
%
%-------------------------------------------------------------------------
BEGIN

  IMPORTING finite_bags[T], bags_aux[T]

  x,e:  VAR T
  b:    VAR finite_bag
  p:    VAR pred[T]
  n,xn: VAR nat

  finite_bag_rest: LEMMA is_finite(rest[T](b))

  JUDGEMENT rest(b) HAS_TYPE finite_bag

  card_bag_rest      : LEMMA nonempty_bag?(b) IMPLIES
     card(b) = card(rest(b)) + 1

  %% ===== on finite bags and filters =====

  finite_filter      : THEOREM is_finite(filter(b,p))

  JUDGEMENT filter(b,p) HAS_TYPE finite_bag

  card_filter_insert: LEMMA card(filter(insert(x,b),p)) =
                               card(filter(b,p)) + IF p(x) THEN 1 ELSE 0 ENDIF

  card_filter_delete: LEMMA card(filter(delete(x,b,n),p)) =
                               card(filter(b,p)) - IF p(x) THEN min(b(x),n)
                                                    ELSE 0 ENDIF

END finite_bags_aux

¤ Dauer der Verarbeitung: 0.1 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.