Quelle  set_of_functions.pvs

set_of_functions [ T1, T2: TYPE ]: THEORY
%------------------------------------------------------------------------
%  number of functions from finite set A to finite set B
%
%        by Bruno Dutertre    Royal Holloway & Bedford New College
% 
%    defines:
% 
%      funset(A, B): finite_set[[(A)->(B)]] = fullset[[(A)->(B)]]
%
%------------------------------------------------------------------------
BEGIN

  IMPORTING fun_below_props, 
            finite_sets@func_composition

  n, m: VAR nat

  A: VAR finite_set[T1]
  B: VAR finite_set[T2]

  empty_finite_domain1    : LEMMA card(A) = 0 IMPLIES 
                                        (EXISTS (f: [(A) -> (B)]): TRUE)

  empty_finite_domain2    : LEMMA card(A) = 0 IMPLIES 
                                        (FORALL (f1, f2: [(A) -> (B)]): f1 = f2)

  empty_finite_range      : LEMMA card(B) = 0 AND card(A) /= 0 IMPLIES 
                                        (FORALL (f: [(A) -> (B)]): FALSE)

  finite_funset_bijection1: THEOREM card(A) = n AND card(B) = m IMPLIES
         (EXISTS (f: [[(A) -> (B)] -> [below[n] -> below[m]]]): bijective?(f))

  finite_funset_bijection2: THEOREM card(A) = n AND card(B) = m IMPLIES
         (EXISTS (f: [[(A) -> (B)] -> below[m ^ n]]): bijective?(f))

  finite_funset           : THEOREM is_finite_type[[(A) -> (B)]]

  funset(A, B): finite_set[[(A)->(B)]] = fullset[[(A)->(B)]]

  card_funset             : THEOREM card(funset(A, B)) = card(B) ^ card(A)

END set_of_functions