Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek card_comp_props.pvs   Sprache: PVS

 
%-------------------------------------------------------------------------
%
%  Basic properties of the type cardinality comparison functions
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: functions[T1,T2], functions[T2,T1]
%  sets_aux: card_comp[T1,T2], card_comp[T2,T1], card_comp_props[T1,T2]
%
%-------------------------------------------------------------------------
card_comp_props[T1: TYPE, T2: TYPE]: THEORY

 EXPORTING ALL WITH functions[T1, T2], functions[T2, T1],
                    card_comp[T1, T2], card_comp[T2, T1]

 BEGIN

  IMPORTING card_comp[T1, T2], card_comp[T2, T1]

  % The following imports are for the proofs only
  IMPORTING function_inverse_def[T1, T2]
  IMPORTING function_inverse_def[T2, T1]
  IMPORTING orders@set_dichotomous[T1, T2], 
            orders@set_antisymmetric[T1, T2]


  % ==========================================================================
  % We defined card_lt and card_ge as we did to avoid special casing empty
  % sets, which these results show would be necessary.
  % ==========================================================================

  card_lt_surj: LEMMA
    card_lt[T1, T2] IFF
     (EXISTS (t: T2): TRUEAND NOT (EXISTS (f: [T1 -> T2]): surjective?(f))

  card_ge_surj: LEMMA
    card_ge[T1, T2] IFF
     ((EXISTS (t: T1): TRUEAND (FORALL (t: T2): FALSE)) OR
      (EXISTS (f: [T1 -> T2]): surjective?(f))


  % ==========================================================================
  % The relationships of the functions
  % ==========================================================================

  card_lt_le: LEMMA card_lt[T1, T2] => card_le[T1, T2]
  card_gt_ge: LEMMA card_gt[T1, T2] => card_ge[T1, T2]

  card_lt_gt: LEMMA card_lt[T1, T2] = card_gt[T2, T1]
  card_le_ge: LEMMA card_le[T1, T2] = card_ge[T2, T1]
  card_gt_lt: LEMMA card_gt[T1, T2] = card_lt[T2, T1]
  card_ge_le: LEMMA card_ge[T1, T2] = card_le[T2, T1]

  card_lt_ge: LEMMA card_lt[T1, T2] XOR card_ge[T1, T2]
  card_le_gt: LEMMA card_le[T1, T2] XOR card_gt[T1, T2]

  card_eq_le_ge: LEMMA
    card_eq[T1, T2] IFF card_le[T1, T2] AND card_ge[T1, T2]
  card_le_lt_eq: LEMMA
    card_le[T1, T2] IFF card_lt[T1, T2] OR card_eq[T1, T2]
  card_ge_gt_eq: LEMMA
    card_ge[T1, T2] IFF card_gt[T1, T2] OR card_eq[T1, T2]

  card_lt_neq_ngt: LEMMA
    card_lt[T1, T2] => NOT card_eq[T1, T2] AND NOT card_gt[T1, T2]
  card_gt_neq_nlt: LEMMA
    card_gt[T1, T2] => NOT card_eq[T1, T2] AND NOT card_lt[T1, T2]


  % ==========================================================================
  % (anti)commutativity and (anti)symmetry of the functions
  % ==========================================================================

  card_lt_anticommutative: LEMMA card_lt[T1, T2] => NOT card_lt[T2, T1]

  card_le_antisymmetric: LEMMA
    card_le[T1, T2] AND card_le[T2, T1] => card_eq[T1, T2]

  card_eq_symmetric: LEMMA card_eq[T1, T2] = card_eq[T2, T1]

  card_ge_antisymmetric: LEMMA
    card_ge[T1, T2] AND card_ge[T2, T1] => card_eq[T1, T2]

  card_gt_anticommutative: LEMMA card_gt[T1, T2] => NOT card_gt[T2, T1]


  % ==========================================================================
  % dichotomy and trichotomy of the functions
  % ==========================================================================

  card_lt_trichotomous: LEMMA
    card_lt[T1, T2] OR card_lt[T2, T1] OR card_eq[T1, T2]

  card_le_dichotomous: LEMMA card_le[T1, T2] OR card_le[T2, T1]

  card_ge_dichotomous: LEMMA card_ge[T1, T2] OR card_ge[T2, T1]

  card_gt_trichotomous: LEMMA
    card_gt[T1, T2] OR card_gt[T2, T1] OR card_eq[T1, T2]

 END card_comp_props

98%


¤ 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.0.12Bemerkung:  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






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.






                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik

Monitoring

Montastic status badge