Quelle  set_dichotomous.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