$$$everything.pvs
everything : THEORY

  BEGIN

  IMPORTING pigeon_hole, finite_set_props2, power_sets

  END everything

$$$below_props.pvs
below_props : THEORY

  BEGIN

  n, m : VAR nat

  p : VAR posnat


  %---------------------------------------------------
  %  Cartesian product of {0 ... n-1} and {0 ... m-1}
  %---------------------------------------------------

  cartesian_bijection : PROPOSITION
	EXISTS (f : [[below(n), below(m)] -> below(n * m)]) : bijective?(f)



  %---------------------------------------------
  %  Functions from {0 ... n-1} to {0 ... m-1}
  %---------------------------------------------

  empty_domain1 : LEMMA
	EXISTS (f : [below(0) -> below(m)]) : true

  empty_domain2 : LEMMA
	FORALL (f1, f2 : [below(0) -> below(m)]) : f1 = f2

  empty_range : LEMMA
	m = 0 IMPLIES FORALL (f : [below[p]-> below(m)]) : FALSE

  funset_bijection : PROPOSITION
	EXISTS (f : [[below(n) -> below(m)] -> below(m ^ n)]) : bijective?(f)

  END below_props


$$$below_props.prf
(|below_props|
 (|cartesian_bijection| "" (SKOLEM!)
  (("" (CASE "m!1 = 0")
    (("1" (ASSERT)
      (("1" (INST + "LAMBDA (x : [below(n!1), below(m!1)]) : 0")
        (("1" (GRIND :IF-MATCH NIL)
          (("1" (TYPEPRED "x1!1`2") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
         ("2" (SKOLEM!)
          (("2" (TYPEPRED "x!1`2") (("2" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL)
     ("2"
      (INST + "lambda (x: [below(n!1), below(m!1)]): m!1 * x`1 + x`2")
      (("1" (GRIND :IF-MATCH NIL)
        (("1" (LEMMA "euclid_nat" ("a" "y!1" "b" "m!1"))
          (("1" (SKOLEM!)
            (("1" (INST + "(q!1, r!1)")
              (("1" (ASSERT) NIL NIL)
               ("2"
                (USE "both_sides_times_pos_lt2"
                     ("x" "q!1" "y" "n!1" "pz" "m!1"))
                (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("2" (FORWARD-CHAIN "unique_division")
          (("2" (APPLY-EXTENSIONALITY 2) NIL NIL)) NIL))
        NIL)
       ("2" (SKOLEM!)
        (("2" (ASSERT)
          (("2"
            (USE "both_sides_times_pos_le1"
                 ("x" "x!1`1" "y" "n!1-1" "pz" "m!1"))
            (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|empty_domain1| "" (SKOSIMP)
  (("" (INST + "LAMBDA (x : below(0)) : 0") (("" (GRIND) NIL NIL))
    NIL))
  NIL)
 (|empty_domain2| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY) NIL NIL))
  NIL)
 (|empty_range| "" (SKOSIMP*)
  (("" (TYPEPRED "f!1(0)") (("" (ASSERT) NIL NIL)) NIL)) NIL)
 (|funset_bijection_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|funset_bijection| "" (SKOLEM + ("m!1" _))
  (("" (INDUCT "n")
    (("1" (INST + "LAMBDA (x : [below(0) -> below(m!1)]) : 0")
      (("1" (GRIND)
        (("1" (REWRITE "empty_domain1") NIL NIL)
         ("2" (REWRITE "empty_domain2") NIL NIL))
        NIL)
       ("2" (GRIND) NIL NIL))
      NIL)
     ("2" (SKOSIMP*)
      (("2" (CASE "m!1 = 0")
        (("1" (DELETE -2)
          (("1"
            (INST + "LAMBDA (h : [below(1 + j!1) -> below(m!1)]) : 0")
            (("1" (GRIND)
              (("1" (TYPEPRED "x1!1(0)") (("1" (ASSERT) NIL NIL)) NIL))
              NIL)
             ("2" (GRIND)
              (("2" (TYPEPRED "h!1(0)") (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL)
         ("2" (ASSERT)
          (("2"
            (INST + "LAMBDA (h : [below(1 + j!1)-> below(m!1)]) :
                                                                         m!1 * f!1(LAMBDA (x : below(j!1)) : h(x)) + h(j!1)")
            (("1" (GRIND :IF-MATCH NIL)
              (("1" (LEMMA "euclid_nat" ("a" "y!1" "b" "m!1"))
                (("1" (SKOLEM!)
                  (("1" (INST -4 "q!1")
                    (("1" (SKOLEM!)
                      (("1"
                        (INST +
                         "LAMBDA (x : below(j!1 + 1)) : IF x = j!1 THEN r!1 ELSE x!1(x) ENDIF")
                        (("1" (ASSERT)
                          (("1" (REWRITE "eta[below(j!1), below(m!1)]")
                            (("1" (ASSERT) NIL NIL)) NIL))
                          NIL)
                         ("2" (REDUCE) NIL NIL))
                        NIL))
                      NIL)
                     ("2"
                      (LEMMA "both_sides_times_pos_lt2"
                       ("x" "q!1" "y" "m!1 ^ j!1" "pz" "m!1"))
                      (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (LEMMA "unique_division")
                (("2"
                  (INST - "m!1" "f!1(LAMBDA (x: below(j!1)): x1!1(x))"
                   "f!1(LAMBDA (x: below(j!1)): x2!1(x))" "x1!1(j!1)"
                   "x2!1(j!1)")
                  (("2" (GROUND)
                    (("2" (INST? -3)
                      (("2" (ASSERT)
                        (("2" (APPLY-EXTENSIONALITY :FNUM 2 :HIDE? T)
                          (("2"
                            (CASE "(LAMBDA (x: below(j!1)): x1!1(x))(x!1) = x2!1(x!1)")
                            (("1" (ASSERT) NIL NIL)
                             ("2" (REPLACE*) (("2" (ASSERT) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (SKOLEM!)
              (("2" (AUTO-REWRITE "expt_plus" "expt_x1")
                (("2"
                  (LEMMA "both_sides_times_pos_le2"
                   ("x" "f!1(LAMBDA (x: below(j!1)): h!1(x))" "y"
                    "m!1 ^ j!1 - 1" "pz" "m!1"))
                  (("2"
                    (TYPEPRED "f!1(LAMBDA (x: below(j!1)): h!1(x))")
                    (("2" (ASSERT)
                      (("2" (NAME-REPLACE "v" "m!1 ^ j!1")
                        (("2" (ASSERT) (("2" (POSTPONE) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$set_of_functions.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  A and B two finite sets
%  - number of functions from A to B
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

set_of_functions [ T1, T2 : TYPE ] : THEORY

  BEGIN

  IMPORTING finite_sets@finite_sets, below_props, bijection_inverse,
	more_function_props

  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 : LEMMA
	card(A) = n AND card(B) = m IMPLIES
	    EXISTS (f : [[(A) -> (B)] -> [below(n) -> below(m)]]) : bijective?(f)

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

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


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

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

  END set_of_functions

$$$set_of_functions.prf
(|set_of_functions|
 (|empty_finite_domain1| "" (SKOSIMP)
  (("" (REWRITE "empty_card" :DIR RL)
    (("" (INST + "LAMBDA (x : (A!1)) : epsilon! (y : (B!1)) : true")
      (("" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|empty_finite_domain2| "" (SKOSIMP*)
  (("" (REWRITE "empty_card" :DIR RL)
    (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|empty_finite_range| "" (ASSERT)
  (("" (SKOSIMP*)
    (("" (REWRITE "empty_card" :DIR RL)
      (("" (REWRITE "empty_card" :DIR RL)
        (("" (GRIND :IF-MATCH NIL)
          (("" (INST - "f!1(x!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|finite_funset_bijection1| "" (SKOSIMP)
  (("" (REWRITE "card_bij")
    (("" (REWRITE "card_bij")
      (("" (SKOSIMP*)
        (("" (ASSERT)
          ((""
            (INST +
             "LAMBDA (h : [(A!1) -> (B!1)]) : f!2 o h o inv(f!1)")
            (("" (HIDE -1 -2)
              (("" (GRIND :IF-MATCH NIL :EXCLUDE ("inv"))
                (("1" (INST + "inv(f!2) o y!1 o f!1")
                  (("1" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("1" (USE "comp_inverse_right" ("f" "f!1"))
                      (("1" (USE "comp_inverse_right" ("f" "f!2"))
                        (("1" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL)
                 ("2" (REWRITE "composition_right_cancel2")
                  (("2" (REWRITE "composition_left_cancel2")
                    (("2" (REVEAL -2) (("2" (ASSERT) NIL NIL)) NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|finite_funset_bijection2_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|finite_funset_bijection2| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "finite_funset_bijection1")
    (("" (LEMMA "funset_bijection" ("n" "n!1" "m" "m!1"))
      (("" (SKOSIMP*)
        (("" (INST + "f!1 o f!2")
          (("" (REWRITE "composition_bijective") NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|finite_funset| "" (SKOLEM!)
  (("" (EXPAND "is_finite_type")
    (("" (NAME "n1" "card(A!1)")
      (("" (NAME "n2" "card(B!1)")
        (("" (FORWARD-CHAIN "finite_funset_bijection2")
          (("" (EXPAND "bijective?")
            (("" (SKOSIMP)
              (("" (INST + "n2 ^ n1" "f!1") (("" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|funset_TCC1| "" (SKOLEM!)
  (("" (REWRITE "finite_full" :DIR RL)
    (("" (REWRITE "finite_funset") NIL NIL)) NIL))
  NIL)
 (|card_funset_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|card_funset| "" (SKOSIMP)
  (("" (NAME-REPLACE "n1" "card(A!1)" :HIDE? NIL)
    (("" (NAME-REPLACE "n2" "card(B!1)" :HIDE? NIL)
      (("" (REWRITE "card_bij" +)
        (("" (FORWARD-CHAIN "finite_funset_bijection2")
          (("" (SKOLEM!)
            (("" (INST + "lambda (x: (funset(A!1, B!1))): f!1(x)")
              (("" (DELETE -2 -3) (("" (GRIND :EXCLUDE "^") NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$power_sets.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Power sets, finiteness and cardinality  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

power_sets [T : TYPE ] : THEORY

  BEGIN

  S, U : VAR setof[T]

  A : VAR finite_set[T]

  n : VAR nat


  powerset(S) : setof[setof[T]] = { U | subset?(U, S) }


  IMPORTING set_of_functions, finite_set_props

  B : finite_set[nat] = { n | n <= 1} 

  card_B : LEMMA  card(B) = 2


  powerset_bijection : LEMMA
	EXISTS (f : [(powerset(S)) -> [(S) -> (B)]]) : bijective?(f)

  finite_powerset_bijection : LEMMA
	EXISTS (f : [(powerset(A)) -> (funset(A, B))]) : bijective?(f)

  finite_powerset : JUDGEMENT powerset(A) HAS_TYPE finite_set[setof[T]]

  card_powerset : PROPOSITION  card(powerset(A)) = 2 ^ card(A)

  elem_finite_powerset : PROPOSITION
	FORALL (X : (powerset(A))) : is_finite(X)

  END power_sets

$$$power_sets.prf
(|power_sets|
 (B_TCC1 "" (EXPAND "is_finite")
  (("" (INST 1 "2" "LAMBDA (x : ({n: nat | n <= 1})) : x")
    (("" (GRIND) NIL NIL)) NIL))
  NIL)
 (|card_B| "" (REWRITE "card_bij")
  (("" (INST + "lambda (x: (B)): x")
    (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
  NIL)
 (|powerset_bijection| "" (SKOSIMP)
  ((""
    (INST +
     "lambda (U: (powerset(S!1))): lambda (x: (S!1)): IF U(x) THEN 1 ELSE 0 ENDIF")
    (("1" (GRIND)
      (("1" (INST + "{ z : T | S!1(z) AND y!1(z) = 1 }")
        (("1" (APPLY-EXTENSIONALITY :HIDE? T)
          (("1" (SMASH)
            (("1" (TYPEPRED "y!1(x!1)") (("1" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL)
         ("2" (SKOSIMP) NIL NIL))
        NIL)
       ("2" (APPLY-EXTENSIONALITY :HIDE? T)
        (("2" (IFF)
          (("2" (PROP)
            (("1" (INST?)
              (("1" (ASSERT)
                (("1"
                  (CASE "(LAMBDA (x: (S!1)): IF x1!1(x) THEN 1 ELSE 0 ENDIF)(x!1) = 1")
                  (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)
                   ("2" (ASSERT) NIL NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (INST? -3)
              (("2" (ASSERT)
                (("2"
                  (CASE "(LAMBDA (x: (S!1)): IF x1!1(x) THEN 1 ELSE 0 ENDIF)(x!1) = 1")
                  (("1" (ASSERT) NIL NIL)
                   ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (AUTO-REWRITE "B") (("2" (ASSERT) NIL NIL)) NIL)
     ("3" (AUTO-REWRITE "B") (("3" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|finite_powerset_bijection| "" (SKOLEM!)
  (("" (LEMMA "powerset_bijection" ("S" "A!1"))
    (("" (SKOLEM!)
      (("" (INST + "f!1")
        (("1" (GRIND) NIL NIL)
         ("2" (DELETE -) (("2" (GRIND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|finite_powerset| "" (SKOLEM!)
  (("" (LEMMA "finite_powerset_bijection" ("A" "A!1"))
    (("" (FORWARD-CHAIN "bijection_finite_set1") NIL NIL)) NIL))
  NIL)
 (|card_powerset| "" (SKOLEM!)
  (("" (LEMMA "finite_powerset_bijection" ("A" "A!1"))
    (("" (REWRITE "equipotent_finite_sets" :DIR RL)
      (("" (REWRITE "card_funset") (("" (REWRITE "card_B") NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|elem_finite_powerset| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "powerset")
    (("" (FORWARD-CHAIN "finite_subset") NIL NIL)) NIL))
  NIL))


$$$finite_set_props2.pvs
finite_set_props2 [ T: TYPE ] : THEORY

  BEGIN

  IMPORTING finite_set_props

  E, F: VAR finite_set[T]
  G: VAR non_empty_finite_set[T]

  n, m: VAR nat


  %--------------------------------------------------
  %  Various lemmas to show equality of finite sets
  %--------------------------------------------------

  equal_by_injection: LEMMA
      E = F IFF subset?(E, F) AND EXISTS (f: [(F) -> (E)]): injective?(f)

  equal_by_surjection: LEMMA
      E = F IFF subset?(E, F) AND EXISTS (f: [(E) -> (F)]): surjective?(f)

  equal_by_bijection: LEMMA
      E = F IFF subset?(E, F) AND EXISTS (f: [(E) -> (F)]): bijective?(f)



  %-------------------------------
  %  Mappings from below(n) to E
  %-------------------------------

  %% mappings [(E) -> below(n)] are considered in finite_sets@card_def

  F(n): finite_set[below(n)] = { x: below(n) | true }

  card_F: LEMMA card(F(n)) = n

  card_injection: LEMMA
      card(E) >= n IFF EXISTS (f: [below(n) -> (E)]): injective?(f)

  card_surjection: LEMMA
      (EXISTS (f: [below(n) -> (E)]): surjective?(f)) IMPLIES card(E) <= n

  card_surjection2: LEMMA
      card(G) <= n IFF EXISTS (f: [below(n) -> (G)]): surjective?(f)

  card_bijection: LEMMA
      card(E) = n IFF EXISTS (f: [below(n) -> (E)]): bijective?(f)

  END finite_set_props2


$$$finite_set_props2.prf
(|finite_set_props2|
 (|equal_by_injection| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (GRIND) NIL)
     ("2" (INST + "lambda (x: (F!1)): x") (("2" (GRIND) NIL)))
     ("3" (FORWARD-CHAIN "injection_and_cardinal")
      (("3" (FORWARD-CHAIN "card_subset")
        (("3" (REWRITE "same_card_subset") NIL)))))))))
 (|equal_by_surjection| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (GRIND) NIL)
     ("2" (INST + "lambda (x: (E!1)): x") (("2" (GRIND) NIL)))
     ("3" (FORWARD-CHAIN "surjection_and_cardinal")
      (("3" (FORWARD-CHAIN "card_subset")
        (("3" (REWRITE "same_card_subset") NIL)))))))))
 (|equal_by_bijection| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (GRIND) NIL)
     ("2" (INST + "lambda (x: (E!1)): x") (("2" (GRIND) NIL)))
     ("3" (REWRITE "same_card_subset")
      (("3" (REWRITE "equipotent_finite_sets") NIL)))))))
 (F_TCC1 "" (EXPAND "is_finite")
  (("" (SKOLEM!) (("" (INST + "n!1" "I") (("" (GRIND) NIL NIL)) NIL))
    NIL))
  NIL)
 (|card_F| "" (AUTO-REWRITE "card_def" "Card_bijection")
  (("" (SKOLEM!)
    (("" (ASSERT) (("" (INST + "I") (("" (GRIND) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|card_injection| "" (SKOLEM!)
  (("" (USE "injection_and_cardinal2" ("E" "F(n!1)" "F" "E!1"))
    (("" (AUTO-REWRITE "card_F" "F")
      (("" (SMASH)
        (("1" (SKOLEM!)
          (("1" (INST + "f!1") (("1" (GRIND) NIL NIL)) NIL)) NIL)
         ("2" (GRIND) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|card_surjection| "" (SKOSIMP*)
  (("" (USE "surjection_and_cardinal" ("E" "F(n!1)" "F" "E!1"))
    (("" (AUTO-REWRITE "card_F" "F")
      (("" (GROUND)
        (("" (INST?)
          (("" (GRIND :IF-MATCH BEST)
            (("" (INST? -) (("" (REDUCE) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|card_surjection2| "" (SKOLEM!)
  (("" (AUTO-REWRITE "card_F" "F")
    (("" (USE "surjection_and_cardinal2" ("E" "F(n!1)" "G" "G!1"))
      (("" (SMASH)
        (("1" (SKOLEM!) (("1" (INST?) (("1" (GRIND) NIL NIL)) NIL))
          NIL)
         ("2" (SKOLEM!)
          (("2" (INST?)
            (("2" (GRIND)
              (("2" (INST? -) (("2" (REDUCE) NIL NIL)) NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|card_bijection| "" (SKOLEM!)
  (("" (USE "equipotent_finite_sets" ("E" "F(n!1)" "F" "E!1"))
    (("" (AUTO-REWRITE "F" "card_F")
      (("" (ASSERT)
        (("" (SMASH)
          (("1" (SKOLEM!)
            (("1" (INST?)
              (("1" (GRIND :IF-MATCH BEST :POLARITY? T)
                (("1" (INST? -4)
                  (("1" (DELETE -3) (("1" (REDUCE) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL)
           ("2" (SKOLEM!)
            (("2" (INST?)
              (("2" (GRIND :IF-MATCH BEST :POLARITY? T)
                (("2" (INST? -3)
                  (("2" (DELETE -2) (("2" (REDUCE) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$bijection_inverse.pvs
bijection_inverse [ T1, T2 : TYPE] : THEORY

  BEGIN

  f : VAR (bijective?[T1, T2])

  x : VAR T1
  y : VAR T2

  inv(f)(y): T1 = epsilon! x: f(x) = y


  inverse_equiv: PROPOSITION inv(f)(y) = x IFF f(x) = y

  inverse_bijective: JUDGEMENT inv(f) HAS_TYPE (bijective?[T2, T1])


  comp_inverse_right : PROPOSITION f(inv(f)(y)) = y

  comp_inverse_left  : PROPOSITION inv(f)(f(x)) = x

  END bijection_inverse

$$$bijection_inverse.prf
(|bijection_inverse|
 (|inv_TCC1| "" (GRIND :IF-MATCH NIL)
  (("" (INST -2 "y!1") (("" (SKOLEM!) (("" (INST? +) NIL NIL)) NIL))
    NIL))
  NIL)
 (|inverse_equiv| "" (GRIND :IF-MATCH NIL)
  (("1" (INST - "y!1")
    (("1" (USE "epsilon_ax[T1]")
      (("1" (GROUND) NIL NIL) ("2" (INST + "x!1") NIL NIL)) NIL))
    NIL)
   ("2" (INST -2 "y!1")
    (("2" (USE "epsilon_ax[T1]")
      (("1" (GROUND)
        (("1" (INST? -2)
          (("1" (ASSERT) NIL NIL) ("2" (INST + "x!1") NIL NIL)) NIL))
        NIL)
       ("2" (INST + "x!1") NIL NIL))
      NIL))
    NIL))
  NIL)
 (|inverse_bijective| "" (SKOLEM!)
  (("" (GRIND :IF-MATCH NIL :EXCLUDE ("inv"))
    (("1" (INST + "f!1(y!1)") (("1" (REWRITE "inverse_equiv") NIL NIL))
      NIL)
     ("2" (NAME-REPLACE "y!2" "inv(f!1)(x2!1)" :HIDE? NIL)
      (("2" (REWRITE "inverse_equiv")
        (("2" (REWRITE "inverse_equiv") (("2" (ASSERT) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|comp_inverse_right| "" (SKOLEM!)
  (("" (USE "inverse_equiv") (("" (ASSERT) NIL NIL)) NIL)) NIL)
 (|comp_inverse_left| "" (SKOLEM!)
  (("" (REWRITE "inverse_equiv") NIL NIL)) NIL))


$$$more_function_props.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Composition of injective, surjective, bijective functions  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

more_function_props  [ T1, T2, T3 : TYPE ] : THEORY

  BEGIN

  f1 : VAR [T1 -> T2]
  f2 : VAR [T2 -> T3]


  %-------------------------------------------------
  %  Closure properties under function composition
  %-------------------------------------------------

  composition_injective : LEMMA
	injective?(f1) AND injective?(f2) IMPLIES injective?(f2 o f1)

  composition_surjective : LEMMA
	surjective?(f1) AND surjective?(f2) IMPLIES surjective?(f2 o f1)

  composition_bijective : LEMMA
	bijective?(f1) AND bijective?(f2) IMPLIES bijective?(f2 o f1)



  %---------------------
  %  Cancellation laws
  %---------------------

  f, g : VAR [T1 -> T2]
  h, k : VAR [T2 -> T3]


  composition_def : LEMMA
	FORALL (x : T1) : h(f(x)) = (h o f)(x)
  
  composition_left_cancel1 : LEMMA
	injective?(h)  IMPLIES  (h o f = h o g IFF f = g)
  
  composition_left_cancel2 : LEMMA
	bijective?(h)  IMPLIES  (h o f = h o g IFF f = g)

 
  composition_right_cancel1 : LEMMA
	surjective?(f)  IMPLIES  (h o f = k o f IFF h = k)
  
  composition_right_cancel2 : LEMMA
	bijective?(f)  IMPLIES  (h o f = k o f IFF h = k)

  
  END more_function_props


$$$more_function_props.prf
(|more_function_props|
 (|composition_injective| "" (GRIND :IF-MATCH NIL)
  (("" (INST -2 "f1!1(x1!1)" "f1!1(x2!1)") (("" (INST -1 "x1!1" "x2!1") (("" (GROUND) NIL)))))))
 (|composition_surjective| "" (GRIND) NIL)
 (|composition_bijective| "" (EXPAND "bijective?")
  (("" (SKOSIMP)
    (("" (SPLIT)
      (("1" (REWRITE "composition_injective") NIL)
       ("2" (REWRITE "composition_surjective") NIL)))))))
 (|composition_def| "" (EXPAND "o") (("" (PROPAX) NIL)))
 (|composition_left_cancel1| "" (SKOSIMP)
  (("" (PROP)
    (("1" (APPLY-EXTENSIONALITY :HIDE? T)
      (("1" (EXPAND "injective?")
        (("1" (INST? -2)
          (("1" (ASSERT)
            (("1" (REWRITE "composition_def")
              (("1" (REWRITE "composition_def") (("1" (ASSERT) NIL)))))))))))))
     ("2" (ASSERT) NIL)))))
 (|composition_left_cancel2| "" (EXPAND "bijective?")
  (("" (SKOSIMP) (("" (REWRITE "composition_left_cancel1") NIL)))))
 (|composition_right_cancel1| "" (SKOSIMP)
  (("" (PROP)
    (("1" (APPLY-EXTENSIONALITY :HIDE? T)
      (("1" (EXPAND "surjective?")
        (("1" (INST?)
          (("1" (SKOLEM!)
            (("1" (REPLACE -2 + RL)
              (("1" (REWRITE "composition_def")
                (("1" (REWRITE "composition_def") (("1" (ASSERT) NIL)))))))))))))))
     ("2" (ASSERT) NIL)))))
 (|composition_right_cancel2| "" (EXPAND "bijective?")
  (("" (SKOSIMP) (("" (REWRITE "composition_right_cancel1") NIL))))))
$$$finite_set_props.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Properties of finite sets   %
%  and mappings between them   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

finite_set_props [T1, T2 : TYPE] : THEORY

  BEGIN

  IMPORTING finite_sets@finite_sets, more_function_props, bijection_inverse

  E : VAR finite_set[T1]
  F : VAR finite_set[T2]  
  G : VAR non_empty_finite_set[T2]

  %-------------------------
  %  Relations on cardinal
  %-------------------------

  injection_and_cardinal : PROPOSITION
	(EXISTS (f : [(E) -> (F)]) : injective?(f)) IMPLIES card(E) <= card(F)

  injection_and_cardinal2 : PROPOSITION
	card(E) <= card(F) IFF (EXISTS (f : [(E) -> (F)]) : injective?(f)) 

  surjection_and_cardinal : PROPOSITION
	(EXISTS (f : [(E) -> (F)]) : surjective?(f)) IMPLIES card(F) <= card(E)

  surjection_and_cardinal2 : PROPOSITION
	card(G) <= card(E) IFF (EXISTS (f : [(E) -> (G)]) : surjective?(f))

  equipotent_finite_sets : PROPOSITION
	card(E) = card(F) IFF EXISTS (f : [(E) -> (F)]) : bijective?(f)


  %-------------------------------------------------
  %  If E and F have same cardinal
  %  - every injection in [E -> F] is bijective
  %  - every surjection  in [E -> F] is bijective
  %-------------------------------------------------

  same_card_injection : PROPOSITION
	card(E) = card(F) IMPLIES
	    FORALL (f : [(E) -> (F)]) : bijective?(f) IFF injective?(f)

  same_card_surjection : PROPOSITION
	card(E) = card(F) IMPLIES
	    FORALL (f : [(E) -> (F)]) : bijective?(f) IFF surjective?(f)



  %----------------------------------------
  %  Proving that S or U are finite using
  %   injections / surjections
  %----------------------------------------

  S : VAR set[T1]
  U : VAR set[T2]

  injection_to_finite_set : PROPOSITION
	(EXISTS (f : [(S) -> (F)]) : injective?(f)) IMPLIES is_finite(S)

  injection_to_finite_set2 : PROPOSITION
	FORALL S, F, (f : [(S) -> (F)]) : injective?(f) IMPLIES is_finite(S)

  injection_to_finite_set3 : PROPOSITION
	(EXISTS (f : [(S) -> (F)]) : injective?(f)) IMPLIES	
		is_finite(S) AND card(S) <= card(F)


  surjection_from_finite_set : PROPOSITION
	(EXISTS (f : [(E) -> (U)]) : surjective?(f)) IMPLIES is_finite(U)

  surjection_from_finite_set2 : PROPOSITION
	FORALL E, U, (f : [(E) -> (U)]) : surjective?(f) IMPLIES is_finite(U)

  surjection_from_finite_set3 : PROPOSITION
	(EXISTS (f : [(E) -> (U)]) : surjective?(f)) IMPLIES
		is_finite(U) AND card(U) <= card(E)



  bijection_finite_set1 : PROPOSITION
	(EXISTS (f : [(S) -> (F)]) : bijective?(f)) IMPLIES is_finite(S)

  bijection_finite_set2 : PROPOSITION
	(EXISTS (f : [(E) -> (U)]) : bijective?(f)) IMPLIES is_finite(U)

  bijection_finite_set3 : PROPOSITION
	(EXISTS (f : [(S) -> (F)]) : bijective?(f)) IMPLIES
		is_finite(S) AND card(S) = card(F)

  bijection_finite_set4 : PROPOSITION
	(EXISTS (f : [(E) -> (U)]) : bijective?(f)) IMPLIES
		is_finite(U) AND card(U) = card(E)



  %------------------------------------
  %  Images of finite sets are finite
  %------------------------------------

  f : VAR [T1 -> T2]

  finite_image : JUDGEMENT image(f, E) HAS_TYPE finite_set[T2]

  card_image : PROPOSITION card(image(f, E)) <= card(E)

  END finite_set_props

$$$finite_set_props.prf
(|finite_set_props|
 (|injection_and_cardinal| "" (SKOSIMP*)
  (("" (REWRITE "card_def")
    (("" (REWRITE "card_def")
      (("" (NAME-REPLACE "n" "Card(F!1)" :HIDE? NIL)
        (("" (REWRITE "Card_bijection")
          (("" (EXPAND "bijective?")
            (("" (SKOSIMP)
              (("" (REWRITE "Card_injection")
                (("" (INST + "f!2 o f!1")
                  (("" (REWRITE "composition_injective")
                    NIL)))))))))))))))))))
 (|injection_and_cardinal2| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (NAME-REPLACE "n!1" "card(F!1)" :HIDE? NIL)
      (("1" (NAME-REPLACE "m!1" "card(E!1)" :HIDE? NIL)
        (("1" (AUTO-REWRITE "card_def" "Card_bijection")
          (("1" (ASSERT)
            (("1" (SKOSIMP*)
              (("1" (ASSERT)
                (("1" (INST + "lambda (x: (E!1)): inv(f!2)(f!1(x))")
                  (("1" (EXPAND "injective?")
                    (("1" (SKOSIMP)
                      (("1"
                        (REWRITE "inverse_equiv[(F!1), below(n!1)]")
                        (("1"
                          (REWRITE
                           "comp_inverse_right[(F!1), below(n!1)]")
                          (("1" (DELETE -2)
                            (("1" (GRIND :EXCLUDE ("surjective?")) NIL
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (SKOLEM!) (("2" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (FORWARD-CHAIN "injection_and_cardinal") NIL NIL))
    NIL))
  NIL)
 (|surjection_and_cardinal| "" (SKOSIMP*)
  (("" (REWRITE "card_def")
    (("" (REWRITE "card_def")
      (("" (NAME-REPLACE "n" "Card(F!1)" :HIDE? NIL)
        (("" (REWRITE "Card_bijection")
          (("" (EXPAND "bijective?")
            (("" (SKOSIMP)
              (("" (REWRITE "Card_surjection")
                (("" (INST 1 "f!2 o f!1")
                  (("" (REWRITE "composition_surjective")
                    NIL)))))))))))))))))))
 (|surjection_and_cardinal2| "" (SKOLEM!)
  (("" (GROUND)
    (("1" (USE "nonempty_card" ("S" "G!1"))
      (("1" (EXPAND "nonempty?")
        (("1" (ASSERT)
          (("1" (NAME-REPLACE "n!1" "card(G!1)" :HIDE? NIL)
            (("1" (NAME-REPLACE "m!1" "card(E!1)" :HIDE? NIL)
              (("1" (AUTO-REWRITE "card_def" "Card_bijection")
                (("1" (ASSERT)
                  (("1" (SKOSIMP*)
                    (("1" (ASSERT)
                      (("1"
                        (INST +
                         "lambda (x: (E!1)): inv(f!2)(min(f!1(x), n!1 - 1))")
                        (("1" (EXPAND "surjective?")
                          (("1" (SKOLEM!)
                            (("1" (DELETE -2)
                              (("1"
                                (EXPAND* "bijective?" "surjective?")
                                (("1"
                                  (FLATTEN)
                                  (("1"
                                    (INST - "f!2(y!1)")
                                    (("1"
                                      (SKOLEM!)
                                      (("1"
                                        (INST + "x!1")
                                        (("1"
                                          (ASSERT)
                                          (("1"
                                            (EXPAND "min")
                                            (("1"
                                              (REPLACE*)
                                              (("1"
                                                (REWRITE
                                                 "comp_inverse_left[(G!1), below(n!1)]")
                                                NIL
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL)
                                     ("2" (ASSERT) NIL NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL)
                         ("2" (DELETE -1 -2) (("2" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (FORWARD-CHAIN "surjection_and_cardinal") NIL NIL))
    NIL))
  NIL)
 (|equipotent_finite_sets| "" (SKOLEM!)
  (("" (USE "empty_card[T2]")
    (("" (GROUND)
      (("1" (REPLACE -3)
        (("1" (REWRITE "empty_card[T1]" :DIR RL)
          (("1" (DELETE -3)
            (("1"
              (INST 1
               "LAMBDA (x : (E!1)) : epsilon! (y : (F!1)) : true")
              (("1" (GRIND :IF-MATCH NIL)
                (("1" (INST?) NIL) ("2" (INST?) NIL)))
               ("2" (DELETE -2) (("2" (GRIND) NIL)))))))))))
       ("2" (REPLACE -3)
        (("2" (REWRITE "empty_card[T1]" :DIR RL)
          (("2" (SKOLEM!)
            (("2" (DELETE -1 -3)
              (("2" (GRIND :IF-MATCH NIL)
                (("2" (INST - "f!1(x!1)")
                  (("2" (ASSERT) NIL)))))))))))))
       ("3" (DELETE 2)
        (("3" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
          (("3" (REWRITE "card_bij")
            (("3" (REWRITE "card_bij")
              (("3" (SKOSIMP*)
                (("3" (CASE "EXISTS (x:(F!1)): true")
                  (("1" (ASSERT)
                    (("1" (INST 1 "inverse(f!1) o f!2")
                      (("1" (REWRITE "composition_bijective")
                        (("1" (REWRITE "bij_inv_is_bij") NIL)))))))
                   ("2" (DELETE -1 -2 2)
                    (("2" (GRIND) NIL)))))))))))))))
       ("4" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
        (("4" (DELETE 2)
          (("4" (REWRITE "card_bij")
            (("4" (REWRITE "card_bij")
              (("4" (SKOSIMP*)
                (("4" (INST 1 "f!1 o f!2")
                  (("4" (REWRITE "composition_bijective")
                    NIL)))))))))))))))))))
 (|same_card_injection| "" (SKOSIMP*)
  (("" (EXPAND "bijective?")
    (("" (GROUND)
      (("" (EXPAND "surjective?")
        (("" (SKOLEM!)
          ((""
            (AUTO-REWRITE "finite_remove[T2]" "card_remove[T2]"
                          "member[T2]")
            ((""
              (USE "injection_and_cardinal" ("F" "remove(y!1, F!1)"))
              (("" (ASSERT)
                (("" (INST + "f!1")
                  (("1" (DELETE -2 2) (("1" (GRIND) NIL)))
                   ("2" (DELETE -)
                    (("2" (GRIND) NIL)))))))))))))))))))))
 (|same_card_surjection| "" (EXPAND "bijective?")
  (("" (SKOSIMP*)
    (("" (GROUND)
      (("" (EXPAND "injective?")
        (("" (SKOSIMP)
          ((""
            (AUTO-REWRITE "finite_remove[T1]" "card_remove[T1]"
                          "member[T1]")
            ((""
              (USE "surjection_and_cardinal" ("E" "remove(x1!1, E!1)"))
              (("" (ASSERT)
                ((""
                  (INST + "LAMBDA (x : (remove(x1!1, E!1))) : f!1(x)")
                  (("1" (DELETE -3)
                    (("1" (GRIND :IF-MATCH NIL)
                      (("1" (INST? -)
                        (("1" (SKOLEM!)
                          (("1" (CASE "x!1 = x1!1")
                            (("1" (INST + "x2!1") (("1" (ASSERT) NIL)))
                             ("2" (INST + "x!1")
                              (("2" (ASSERT) NIL)))))))))))))
                   ("2" (DELETE -)
                    (("2" (GRIND) NIL)))))))))))))))))))))
 (|injection_to_finite_set| "" (SKOSIMP*)
  (("" (NAME "n" "card(F!1)")
    (("" (REWRITE "card_bij")
      (("" (EXPAND "bijective?")
        (("" (SKOSIMP)
          (("" (EXPAND "is_finite")
            (("" (INST 1 "n" "f!2 o f!1")
              (("" (REWRITE "composition_injective") NIL)))))))))))))))
 (|injection_to_finite_set2| "" (SKOSIMP)
  (("" (USE "injection_to_finite_set" ("F" "F!1"))
    (("" (ASSERT) (("" (INST?) NIL)))))))
 (|injection_to_finite_set3| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "injection_to_finite_set")
    (("" (ASSERT)
      (("" (FORWARD-CHAIN "injection_and_cardinal") NIL)))))))
 (|surjection_from_finite_set| "" (SKOSIMP*)
  (("" (CASE "empty?(E!1)")
    (("1" (CASE "U!1 = emptyset[T2]")
      (("1" (REPLACE -1) (("1" (REWRITE "finite_emptyset") NIL)))
       ("2" (REWRITE "emptyset_is_empty?" :DIR RL)
        (("2" (DELETE 2) (("2" (GRIND) NIL)))))))
     ("2" (ASSERT)
      (("2" (NAME "g" "inverse(f!1)")
        (("1" (TYPEPRED "E!1")
          (("1" (EXPAND "is_finite")
            (("1" (SKOLEM!)
              (("1" (INST 2 "N!1" "f!2 o g")
                (("1" (REWRITE "composition_injective")
                  (("1" (REPLACE -2 1 RL)
                    (("1" (REWRITE "inj_inv") NIL)))))))))))))
         ("2" (DELETE -1 3) (("2" (GRIND) NIL)))))))))))
 (|surjection_from_finite_set2| "" (SKOSIMP)
  (("" (USE "surjection_from_finite_set" ("E" "E!1"))
    (("" (ASSERT) (("" (INST?) NIL)))))))
 (|surjection_from_finite_set3| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "surjection_from_finite_set")
    (("" (ASSERT)
      (("" (FORWARD-CHAIN "surjection_and_cardinal") NIL)))))))
 (|bijection_finite_set1| "" (EXPAND "bijective?")
  (("" (SKOSIMP*)
    (("" (LEMMA "injection_to_finite_set" ("S" "S!1" "F" "F!1"))
      (("" (ASSERT) (("" (INST?) NIL)))))))))
 (|bijection_finite_set2| "" (EXPAND "bijective?")
  (("" (SKOSIMP*)
    (("" (LEMMA "surjection_from_finite_set" ("E" "E!1" "U" "U!1"))
      (("" (ASSERT) (("" (INST?) NIL)))))))))
 (|bijection_finite_set3| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "bijection_finite_set1")
    (("" (ASSERT) (("" (REWRITE "equipotent_finite_sets") NIL)))))))
 (|bijection_finite_set4| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "bijection_finite_set2")
    (("" (ASSERT)
      (("" (USE "equipotent_finite_sets") (("" (ASSERT) NIL)))))))))
 (|finite_image| "" (SKOLEM!)
  (("" (USE "surjection_from_finite_set" ("E" "E!1"))
    (("" (ASSERT)
      (("" (DELETE 2)
        (("" (INST + "lambda (x : (E!1)) : f!1(x)")
          (("1" (GRIND) NIL) ("2" (GRIND) NIL)))))))))))
 (|card_image| "" (SKOLEM!)
  (("" (USE "surjection_and_cardinal")
    (("" (ASSERT)
      (("" (DELETE 2)
        (("" (INST + "lambda (x : (E!1)) : f!1(x)")
          (("1" (GRIND) NIL) ("2" (GRIND) NIL))))))))))))


$$$partitions.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Families of mutually disjoint finite sets   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

partitions [ T : TYPE ] : THEORY

  BEGIN

  IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_inductions,
	finite_sets@finite_sets_sum_real[finite_set[T]]

  E : VAR setof[finite_set[T]]

  F : VAR setof[T]

  A, B : VAR finite_set[T]

  G : VAR finite_set[finite_set[T]]

  x, y, z : VAR T


  %-----------------------
  %  Union of sets in E
  %----------------------

  union(E) : setof[T] = { x | EXISTS (X : (E)) : X(x) }


  union_emptyset : LEMMA  union(emptyset[finite_set[T]]) = emptyset

  union_add : LEMMA union(add(A, E)) = union(union(E), A)

  union_finite : JUDGEMENT union(G) HAS_TYPE finite_set[T]


  %---------------------------------------------------
  %  Case where the sets in G are mutually disjoints
  %---------------------------------------------------

  partition?(G) : bool =
	FORALL (X, Y : (G)) : X = Y OR disjoint?(X, Y)

  empty_partition : LEMMA  partition?(emptyset[finite_set[T]])

  add_partition : LEMMA
	not G(A) AND partition?(add(A, G)) IMPLIES disjoint?(union(G), A)

  card_union_partition : LEMMA 
	partition?(G) IMPLIES card(union(G)) = sum(G, card[T])



  %-----------------------------
  %  The pigeon hole principle
  %-----------------------------

  H : VAR (partition?)
  n : VAR nat

  pigeon_hole : PROPOSITION
   	union(H) = A and card(H) * n < card(A) IMPLIES 
	    (EXISTS (X : (H)) : card(X) >= n + 1)

  END partitions


$$$partitions.prf
(|partitions|
 (|union_emptyset| "" (APPLY-EXTENSIONALITY :HIDE? T)
  (("" (GRIND) NIL NIL)) NIL)
 (|union_add| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T)
    (("" (GRIND :EXCLUDE "is_finite" :IF-MATCH NIL)
      (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)
       ("3" (INST?) NIL NIL))
      NIL))
    NIL))
  NIL)
 (|union_finite| ""
  (INDUCT-AND-SIMPLIFY "G" :NAME "finite_set_induction[finite_set[T]]"
   :DEFS NIL :REWRITES
   ("union_add" "union_emptyset" "finite_emptyset[T]"
    "finite_union[T]"))
  NIL NIL)
 (|union_TCC1| "" (USE "union_finite") NIL)
 (|empty_partition| "" (GRIND) NIL NIL)
 (|add_partition| "" (GRIND :EXCLUDE "is_finite" :IF-MATCH NIL)
  (("" (INST - "A!1" "X!1")
    (("" (GROUND) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|card_union_partition_TCC1| "" (SUBTYPE-TCC))
 (|card_union_partition| ""
  (INDUCT-AND-SIMPLIFY "G" :NAME
   "finite_set_ind_modified[finite_set[T]]" :DEFS NIL :REWRITES
   ("empty_partition" "add_partition" "union_emptyset" "union_add"
    "sum_emptyset" "sum_add" "member[finite_set[T]]" "card_emptyset[T]"
    "card_disj_union[T]"))
  (("" (DELETE 3)
    (("" (AUTO-REWRITE "add")
      (("" (APPLY (THEN* (EXPAND "partition?") (SKOLEM!) (INST?)))
        NIL)))))))
 (|pigeon_hole| "" (SKOSIMP)
  (("" (REPLACE -1 * RL)
    (("" (REWRITE "card_union_partition")
      (("" (USE "sum_bound" ("N" "n!1" "f" "card[T]"))
        (("" (ASSERT)
          (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$pigeon_hole.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Other formulations of the pigeon hole principle   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pigeon_hole[T1: TYPE, T2: TYPE]: THEORY

  BEGIN
  
  IMPORTING partitions, finite_set_props
  
  A: VAR finite_set[T1]
  
  B: VAR finite_set[T2]
  
  x: VAR T1

  n: VAR nat

  invim(A, B, (f : [(A) -> (B)]), (y : (B))): finite_set[T1] = 
	{x | A(x) AND f(x) = y}
  
  pigeon_hole1: PROPOSITION
        card(B) * n < card(A)
            IMPLIES FORALL (f: [(A) -> (B)]):
            EXISTS (y: (B)): card(invim(A, B, f, y)) >= n + 1
  
  pigeon_hole2: PROPOSITION
        card(B) * n < card(A)
            IMPLIES FORALL (f: [(A) -> (B)]):
            EXISTS (y: (B)): card({ x | A(x) AND f(x) = y}) >= n + 1

  END pigeon_hole

$$$pigeon_hole.prf
(|pigeon_hole|
 (|invim_TCC1| "" (SKOLEM!)
  (("" (USE "finite_subset[T1]")
    (("" (GRIND :DEFS NIL :THEORIES "sets[T1]") NIL NIL)) NIL))
  NIL)
 (|pigeon_hole1| "" (SKOSIMP*)
  (("" (NAME "g!1" "lambda (y : (B!1)) : invim(A!1, B!1, f!1, y)")
    ((""
      (NAME "C!1"
            "{ X : finite_set[T1] | EXISTS (y : (B!1)) : g!1(y) = X }")
      (("" (CASE "EXISTS (f : [(B!1) -> (C!1)]) : surjective?(f)")
        (("1" (FORWARD-CHAIN "surjection_from_finite_set")
          (("1" (FORWARD-CHAIN "surjection_and_cardinal")
            (("1" (ASSERT)
              (("1" (DELETE -2 -3)
                (("1" (USE "pigeon_hole" ("H" "C!1" "n" "n!1"))
                  (("1" (GROUND)
                    (("1" (SKOLEM-TYPEPRED)
                      (("1" (REPLACE -5 -2 RL)
                        (("1" (REPLACE -6 -2 RL)
                          (("1" (ASSERT)
                            (("1" (SKOLEM!)
                              (("1"
                                (INST?)
                                (("1" (ASSERT) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("2" (DELETE -1 -4 2)
                      (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                        (("2" (REPLACE -1 + RL)
                          (("2"
                            (GRIND :EXCLUDE "is_finite" :IF-MATCH NIL)
                            (("1" (REPLACE -3 -4 RL)
                              (("1"
                                (REPLACE -6 -4 RL)
                                (("1" (ASSERT) NIL NIL))
                                NIL))
                              NIL)
                             ("2" (INST + "g!1(f!1(x!1))")
                              (("1"
                                (REPLACE -3 + RL)
                                (("1" (ASSERT) NIL NIL))
                                NIL)
                               ("2" (INST?) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL)
                     ("3" (DELETE -2 -3 2)
                      (("3"
                        (USE "both_sides_times_pos_le1" ("pz" "n!1"))
                        (("3" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL)
                   ("2" (DELETE -1 -4 2)
                    (("2" (REPLACE -1 + RL)
                      (("2" (REPLACE -2 + RL)
                        (("2" (GRIND :EXCLUDE ("is_finite"))
                          (("2" (REPLACE -4 -7 RL)
                            (("2" (REPLACE -6 -8 RL)
                              (("2"
                                (ASSERT)
                                (("2" (GROUND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (DELETE -3 2)
          (("2" (INST?)
            (("1" (GRIND :EXCLUDE ("is_finite"))
              (("1" (REPLACE -3 - RL) (("1" (ASSERT) NIL NIL)) NIL))
              NIL)
             ("2" (REPLACE -1 + RL)
              (("2" (SKOLEM!)
                (("2" (ASSERT) (("2" (INST?) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|pigeon_hole2_TCC1| "" (SKOSIMP*)
  (("" (USE "invim_TCC1" ("A" "A!1" "B" "B!1")) NIL NIL)) NIL)
 (|pigeon_hole2| "" (LEMMA "pigeon_hole1")
  (("" (EXPAND "invim") (("" (ASSERT) NIL NIL)) NIL)) NIL))