Quelle set_dichotomous.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
%  There is an injective (surjective) map between any pair of sets.
%  We have to special case empty sets because, if the range is empty,
%  there is NO function from nonempty D to R.
%
%  For PVS version 3.2.  January 18, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: sets_lemmas[D]
%  orders: set_dichotomous[D, R]
%
%-------------------------------------------------------------------------
set_dichotomous[D: TYPE, R: TYPE]: THEORY

% Hide uninteresting intermediate results
EXPORTING injective_or_surjective, injective_dichotomous,
           surjective_dichotomous WITH sets_lemmas[D]

BEGIN

  IMPORTING sets_lemmas[D], function_inverse_def[D, R]

  % ==========================================================================
  % Declarations used for the proofs only
  % ==========================================================================

  subset_injection: TYPE = [S: set[D], (injective?[(S), R])]

  d: VAR D
  r: VAR R
  i, j: VAR subset_injection

  injection_order(i, j): bool =
      subset?(i`1, j`1) AND (FORALL (d: (i`1)): i`2(d) = j`2(d))

  partial_injection_order: JUDGEMENT
    injection_order HAS_TYPE (partial_order?[subset_injection])

  IMPORTING zorn[subset_injection, injection_order]

  % ==========================================================================
  % The theorems
  % ==========================================================================

  injective_or_surjective: THEOREM
    (EXISTS (f: [D -> R]): injective?(f)) OR
    (EXISTS (f: [D -> R]): surjective?(f)) OR
    ((EXISTS d: TRUE) AND (FORALL r: FALSE))

  injective_dichotomous: COROLLARY
    (EXISTS (f: [D -> R]): injective?(f)) OR
    (EXISTS (f: [R -> D]): injective?(f))

  surjective_dichotomous: COROLLARY
    (EXISTS (f: [D -> R]): surjective?(f)) OR
    (EXISTS (f: [R -> D]): surjective?(f)) OR
    ((EXISTS d: TRUE) AND (FORALL r: FALSE)) OR
    ((FORALL d: FALSE) AND (EXISTS r: TRUE))

END set_dichotomous

quality83%

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