Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 629 B

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): TRUE) AND NOT (EXISTS (f: [T1 -> T2]): surjective?(f))

  card_ge_surj: LEMMA
    card_ge[T1, T2] IFF
     ((EXISTS (t: T1): TRUE) AND (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

quality98%

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

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.