$$$top.pvs
%------------------------------------------------------------------------
%
%  Top of finite sets theory   Version 2.2    5/22/97
%  --------------------------------------------------------------
%      Authors: Ricky W. Butler   NASA Langley Research Center
%               Bruno Dutertre    Royal Holloway & Bedford New College
%               Damir Jamsek      Odyssey Research Associates
%               Sam Owre          SRI International
%               David Griffioen   CWI and KUN (Catholic University 
%                                 Nijmegen), the Netherlands.
%   
%      Index:
%      ------
%        finite_sets            -- main theory that is imported
%                                  (provides basic type and cardinality)
%        finite_sets_sum        -- summation over a set
%        finite_sets_minmax     -- min and max over a set
%        finite_sets_inductions -- induction schemes
%        finite_sets_sum_real   -- additional properties for summations
%                                  over real-valued functions
%        finite_sets_int        -- special properties of integer sets
%        finite_sets_nat        -- special properties of natural sets
%        finite_sets_pred       -- lemmas involving predicate subtypes
%        finite_sets_below      -- lemmas involving sets of below and upto
%        finite_sets_eq         -- lemmas to show set is finite via mappings
%        finite_sets_card_eq    -- equal cardinality of two dissimilar sets
%        finite_sets_rules      -- experimental AUTO-REWRITE-THEORY rules
%
%
%  This theory was designed for making libraries and is not intended
%  for importing.  One should directly import one of the above listed
%  theories.
%
%------------------------------------------------------------------------
top: THEORY
BEGIN

  IMPORTING finite_sets, finite_sets_sum, 
             finite_sets_minmax, 
             finite_sets_inductions, finite_sets_sum_real, 
             finite_sets_int, finite_sets_nat, finite_sets_pred,
             finite_sets_below, finite_sets_card_eq, finite_sets_eq

END top

$$$top.prf
(|top| (IMPORTING1_TCC1 "" (REWRITE "zero_identity") NIL)
 (IMPORTING1_TCC2 "" (REWRITE "plus_ac") NIL))
$$$finite_sets_eq.pvs
finite_sets_eq[T1, T2 : TYPE] : THEORY
%-------------------------------------------------------------------------
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
% 
%      Equipotence of finite sets  
%
%-------------------------------------------------------------------------

BEGIN


  N: VAR nat

  IMPORTING finite_sets, func_composition

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

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

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

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

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

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

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

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

END finite_sets_eq

$$$finite_sets_eq.prf
(|finite_sets_eq|
 (|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)))))))))))))))
 (|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) (("2" (INST + "x!1") NIL)))))))))))))
 (|injection_to_finite_set2| "" (SKOSIMP)
  (("" (USE "injection_to_finite_set" ("F" "F!1"))
    (("" (ASSERT) (("" (INST?) NIL)))))))
 (|surjection_from_finite_set2| "" (SKOSIMP)
  (("" (USE "surjection_from_finite_set" ("E" "E!1"))
    (("" (ASSERT) (("" (INST?) 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))))))))))

$$$func_composition.pvs
func_composition  [ T1, T2, T3 : TYPE ] : THEORY
%------------------------------------------------------------------------
%      Author:  Bruno Dutertre 
%
%      Composition of injective, surjective, bijective functions
%------------------------------------------------------------------------

  BEGIN

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

  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 func_composition


$$$func_composition.prf
(|func_composition|
 (|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_sets_card_eq.pvs
finite_sets_card_eq[T1, T2 : TYPE] : THEORY
%-------------------------------------------------------------------------
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
% 
% Establishes:
%
%       card_eq_bij : LEMMA card(E) = card(F) IFF 
%                                  EXISTS (f: [(E)->(F)]): bijective?(f)
%
%-------------------------------------------------------------------------

BEGIN

  IMPORTING finite_sets, func_composition

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

  N: VAR nat
  card_injection         : LEMMA (EXISTS (f : [(E)->below[N]]) : injective?(f)) 
                                     IMPLIES card(E) <= N
  
  card_surjection        : LEMMA (EXISTS (f : [(E)->below[N]]) : surjective?(f)) 
                                     IMPLIES N <= card(E) 
  

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

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

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

END finite_sets_card_eq

$$$finite_sets_card_eq.prf
(|finite_sets_card_eq|
 (|card_injection| "" (SKOSIMP*)
  (("" (REWRITE "card_def") (("" (REWRITE "Card_injection") (("" (INST?) NIL)))))))
 (|card_surjection| "" (SKOSIMP*)
  (("" (REWRITE "card_def") (("" (REWRITE "Card_surjection") (("" (INST?) NIL)))))))
 (|injection_and_cardinal| "" (SKOSIMP*)
  (("" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
    (("" (REWRITE "card_bij")
      (("" (EXPAND "bijective?")
        (("" (SKOSIMP)
          (("" (REWRITE "card_injection")
            (("" (INST 1 "f!2 o f!1")
              (("" (REWRITE "composition_injective") NIL)))))))))))))))
 (|surjection_and_cardinal| "" (SKOSIMP*)
  (("" (NAME-REPLACE "n" "card(F!1)" :HIDE? NIL)
    (("" (REWRITE "card_bij")
      (("" (EXPAND "bijective?")
        (("" (SKOSIMP)
          (("" (REWRITE "card_surjection")
            (("" (INST 1 "f!2 o f!1")
              (("" (REWRITE "composition_surjective") NIL)))))))))))))))
 (|card_eq_bij| "" (SKOSIMP*)
  (("" (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" (INST 1 "inverse(f!1) o f!2")
                  (("1" (REWRITE "composition_bijective")
                    (("1" (REWRITE "bij_inv_is_bij")
                      (("1" (DELETE -1 -2 2 3) (("1" (GRIND) NIL)))))
                     ("2" (DELETE -)
                      (("2" (EXPAND "empty?")
                        (("2" (SKOSIMP*)
                          (("2" (EXPAND "member") (("2" (INST + "x!1") NIL)))))))))))
                   ("2" (EXPAND "empty?")
                    (("2" (EXPAND "member")
                      (("2" (SKOSIMP*) (("2" (INST + "x!1") 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))))))))))))))))))))

$$$finite_sets_below.pvs
finite_sets_below[N: nat]: THEORY
BEGIN

  IMPORTING finite_sets

  A,B,BS: VAR set[below(N)]
  US: VAR set[upto(N)]

  finite_below      : LEMMA is_finite[below(N)](BS)

  card_below_fullset: LEMMA card[below(N)](fullset[below(N)]) = N

  card_below        : LEMMA card[below(N)](BS) <= N

  finite_upto       : LEMMA is_finite[upto(N)](US)

  card_upto_fullset : LEMMA card[upto(N)](fullset[upto(N)]) = N + 1

  card_upto         : LEMMA card[upto(N)](US) <= N + 1

  k: VAR nat
  pidgeon_hole      : LEMMA card(A) + card(B) >= N + k IMPLIES 
                                card(intersection(A,B)) >= k


END finite_sets_below

$$$finite_sets_below.prf
(|finite_sets_below|
 (|finite_below| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "N" "(LAMBDA (i:(BS!1)): i)")
      (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))
 (|card_below_fullset_TCC1| "" (REWRITE "finite_below") NIL)
 (|card_below_fullset| "" (EXPAND "fullset")
  (("" (LEMMA "card_bij[below(N)]")
    (("" (INST -1 "N" "{x: below(N) | TRUE}")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1" (INST 1 "(LAMBDA (x: {x: below(N) | TRUE}): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*) (("2" (INST 1 "y!1") NIL)))))))))))))))
       ("2" (REWRITE "finite_below") NIL)))))))
 (|card_below_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_below") NIL)))
 (|card_below| "" (SKOSIMP*)
  (("" (LEMMA "card_subset[below(N)]")
    (("" (INST -1 "BS!1" "fullset[below(N)]")
      (("1" (LEMMA "card_below_fullset")
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (ASSERT)
              (("1" (HIDE 2)
                (("1" (EXPAND "subset?")
                  (("1" (EXPAND "fullset")
                    (("1" (EXPAND "member") (("1" (PROPAX) NIL)))))))))))))))))
       ("2" (REWRITE "finite_below") NIL)
       ("3" (REWRITE "finite_below") NIL)))))))
 (|finite_upto| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "N+1" "(LAMBDA (i:(US!1)): i)")
      (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))
 (|card_upto_fullset_TCC1| "" (REWRITE "finite_upto") NIL)
 (|card_upto_fullset| "" (EXPAND "fullset")
  (("" (LEMMA "card_bij[upto(N)]")
    (("" (INST -1 "N+1" "{x: upto(N) | TRUE}")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1" (INST 1 "(LAMBDA (x: {x: upto(N) | TRUE}): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*) (("2" (INST 1 "y!1") NIL)))))))))))))))
       ("2" (REWRITE "finite_upto") NIL)))))))
 (|card_upto_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_upto") NIL)))
 (|card_upto| "" (SKOSIMP*)
  (("" (LEMMA "card_subset[upto(N)]")
    (("" (INST -1 "US!1" "fullset[upto(N)]")
      (("1" (LEMMA "card_upto_fullset")
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (ASSERT)
              (("1" (HIDE 2)
                (("1" (EXPAND "subset?")
                  (("1" (EXPAND "fullset")
                    (("1" (EXPAND "member") (("1" (PROPAX) NIL)))))))))))))))))
       ("2" (REWRITE "finite_upto") NIL) ("3" (REWRITE "finite_upto") NIL)))))))
 (|pidgeon_hole_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_intersection")
    (("1" (REWRITE "finite_below") NIL) ("2" (REWRITE "finite_below") NIL)))))
 (|pidgeon_hole| "" (SKOSIMP*)
  (("" (LEMMA "card_union[below(N)]")
    (("" (INST?)
      (("1" (LEMMA "card_below") (("1" (INST?) (("1" (ASSERT) NIL)))))
       ("2" (REWRITE "finite_below") NIL)
       ("3" (REWRITE "finite_below") NIL))))))))
$$$finite_sets_pred.pvs
finite_sets_pred[T: TYPE]: THEORY
BEGIN

  IMPORTING finite_sets

  P, P1, P2: VAR pred[T]

  finite_pred: LEMMA is_finite(fullset[T]) IMPLIES
                        is_finite[T]({x: T | P(x)})


  card_implies: LEMMA is_finite(fullset[T]) AND
                      (FORALL (x: T): P1(x) IMPLIES P2(x)) 
             IMPLIES card({x: T | P1(x)}) <= card({x: T | P2(x)})

END finite_sets_pred

$$$finite_sets_pred.prf
(|finite_sets_pred|
 (|finite_pred| "" (EXPAND "fullset")
  (("" (EXPAND "is_finite")
    (("" (SKOSIMP*)
      (("" (INST 1 "N!1" "(LAMBDA (x: {x: T | P!1(x)}): f!1(x))")
        (("" (EXPAND "injective?")
          (("" (SKOSIMP*)
            (("" (INST?) (("" (ASSERT) NIL)))))))))))))))
 (|card_implies_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_pred") NIL)))
 (|card_implies_TCC2| "" (SKOSIMP*)
  (("" (REWRITE "finite_pred") NIL)))
 (|card_implies| "" (SKOSIMP*)
  (("" (CASE "subset?({x: T | P1!1(x)},{x: T | P2!1(x)})")
    (("1" (LEMMA "card_subset[T]")
      (("1" (INST?)
        (("1" (ASSERT) NIL)
         ("2" (HIDE -1 -3 2) (("2" (REWRITE "finite_pred") NIL)))
         ("3" (REWRITE "finite_pred") NIL)))))
     ("2" (HIDE -1 2)
      (("2" (EXPAND "subset?")
        (("2" (EXPAND "member") (("2" (PROPAX) NIL))))))))))))
$$$finite_sets_nat.pvs
finite_sets_nat: THEORY
 BEGIN
  IMPORTING finite_sets[nat]

  n, N: VAR nat
  i, j: VAR nat
  p: VAR pred[nat]

  finite_bounded       : LEMMA is_finite({j: nat | j < N })

  card_bounded         : LEMMA card({j: nat | j < N}) = N    

  finite_bounded_subset: LEMMA is_finite({j: nat | j < N AND p(j)})

  card_bounded_subset  : LEMMA card({j: nat | j < N AND p(j)}) <= N

% ------------------------------------------------------------------------
% The following lemmas apply is_finite[nat] and card[nat] to subtype
% sets.  This should be avoided if possible.  See finite_subint for
% preferred lemmas.
% ------------------------------------------------------------------------

  finite_nat_below   : LEMMA is_finite[nat]({x: below(n) | TRUE})

  card_nat_below     : LEMMA card[nat]({x: below(n) | TRUE}) = n

  finite_nat_upto    : LEMMA is_finite[nat]({x: upto(n) | TRUE})

  card_nat_upto      : LEMMA card[nat]({x: upto(n) | TRUE}) = n + 1

  finite_nat_subrange: LEMMA
      is_finite[nat](restrict[int, nat, bool]({x: subrange(i, j) | TRUE}))

  card_nat_subrange  : LEMMA
      card[nat](restrict[int, nat, bool]({x: subrange(i, j) | TRUE})) =
                               IF i <= j THEN j - i + 1 ELSE 0 ENDIF


END finite_sets_nat

$$$finite_sets_nat.prf
(|finite_sets_nat|
 (|finite_bounded| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "N!1" "(lambda (x: below(N!1)): x)")
      (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))
 (|card_bounded_TCC1| "" (SKOSIMP*)
  (("" (ASSERT)
    (("" (EXPAND "is_finite")
      (("" (INST 1 "N!1" "(lambda (x: below(N!1)): x)")
        (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))))
 (|card_bounded| "" (SKOSIMP*)
  (("" (REWRITE "card_bij")
    (("1" (INST 1 "(lambda (x:below(N!1)):x)")
      (("1" (EXPAND "bijective?")
        (("1" (SPLIT 1)
          (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
           ("2" (EXPAND "surjective?")
            (("2" (SKOSIMP*) (("2" (INST 1 "y!1") NIL)))))))))))
     ("2" (REWRITE "finite_bounded") NIL)))))
 (|finite_bounded_subset| "" (SKOSIMP*)
  (("" (LEMMA "finite_subset")
    (("" (INST -1 "{j: nat | j < N!1}" "{j: nat | j < N!1 AND p!1(j)}")
      (("1" (ASSERT)
        (("1" (HIDE 2)
          (("1" (EXPAND "subset?")
            (("1" (EXPAND "member") (("1" (SKOSIMP*) NIL)))))))))
       ("2" (REWRITE "finite_bounded") NIL)))))))
 (|card_bounded_subset_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_bounded_subset") (("" (INST?) NIL)))))
 (|card_bounded_subset| "" (SKOSIMP*)
  (("" (LEMMA "card_bounded")
    (("" (INST -1 "N!1")
      (("" (LEMMA "card_subset")
        ((""
          (INST -1 "{j: nat | j < N!1 AND p!1(j)}"
           "{j: nat | j < N!1}")
          (("1" (SPLIT -1)
            (("1" (ASSERT) NIL)
             ("2" (HIDE -1 2)
              (("2" (EXPAND "subset?")
                (("2" (SKOSIMP*)
                  (("2" (EXPAND "member") (("2" (ASSERT) NIL)))))))))))
           ("2" (REWRITE "finite_bounded") NIL)
           ("3" (REWRITE "finite_bounded_subset") NIL)))))))))))
 (|finite_nat_below| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    ((""
      (INST 1 "n!1"
       "(LAMBDA (x: (extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE}))): x)")
      (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
       ("2" (SKOSIMP*)
        (("2" (ASSERT)
          (("2" (TYPEPRED "x!1")
            (("2" (EXPAND "extend") (("2" (PROPAX) NIL)))))))))))))))
 (|card_nat_below_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_nat_below") (("" (INST?) NIL)))))
 (|card_nat_below| "" (SKOSIMP*)
  (("" (LEMMA "card_bij")
    ((""
      (INST -1 "n!1"
       "extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE})")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1"
            (INST 1
             "(LAMBDA (x: (extend[nat, below(n!1), bool, FALSE]({x: below(n!1) | TRUE}))): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*)
                    (("2" (INST 1 "y!1")
                      (("2" (EXPAND "extend")
                        (("2" (PROPAX) NIL)))))))))))))
             ("2" (SKOSIMP*)
              (("2" (TYPEPRED "x!1")
                (("2" (EXPAND "extend") (("2" (ASSERT) NIL)))))))))))))
       ("2" (LEMMA "finite_nat_below") (("2" (INST?) NIL)))))))))
 (|finite_nat_upto| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    ((""
      (INST 1 "n!1+1"
       "(LAMBDA (x: (extend[nat, upto(n!1), bool, FALSE]({x: upto(n!1) | TRUE}))): x)")
      (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
       ("2" (SKOSIMP*)
        (("2" (TYPEPRED "x!1")
          (("2" (EXPAND "extend") (("2" (ASSERT) NIL)))))))))))))
 (|card_nat_upto_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_nat_upto") (("" (INST?) NIL)))))
 (|card_nat_upto| "" (SKOSIMP*)
  (("" (LEMMA "card_bij")
    ((""
      (INST -1 "n!1+1"
       "extend[nat, upto(n!1), bool, FALSE]({x: upto(n!1) | TRUE})")
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1" (INST 1 "(LAMBDA (x: {x: upto(n!1) | TRUE}): x)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*)
                    (("2" (INST 1 "y!1")
                      (("2" (EXPAND "extend")
                        (("2" (PROPAX) NIL)))))))))))))
             ("2" (SKOSIMP*)
              (("2" (PROP)
                (("1" (EXPAND "extend") (("1" (ASSERT) NIL)))
                 ("2" (EXPAND "extend") (("2" (ASSERT) NIL)))))))
             ("3" (SKOSIMP*)
              (("3" (EXPAND "extend") (("3" (PROPAX) NIL)))))))))))
       ("2" (LEMMA "finite_nat_upto") (("2" (INST?) NIL)))))))))
 (|finite_nat_subrange| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    ((""
      (INST 1 "j!1+1" "(LAMBDA (x: (restrict[int, nat,
                   bool](extend[int, subrange(i!1, j!1), bool,
                                FALSE]({x: subrange(i!1, j!1) | TRUE})))): x)")
      (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
       ("2" (SKOSIMP*)
        (("2" (ASSERT)
          (("2" (TYPEPRED "x!1")
            (("2" (EXPAND "restrict")
              (("2" (EXPAND "extend")
                (("2" (PROPAX) NIL)))))))))))))))))
 (|card_nat_subrange_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_nat_subrange") (("" (INST?) NIL)))))
 (|card_nat_subrange| "" (SKOSIMP*)
  (("" (LEMMA "card_bij")
    (("" (INST?)
      (("1" (REPLACE -1)
        (("1" (HIDE -1)
          (("1"
            (INST 1 "(LAMBDA (x: (restrict[int, nat,
                          bool](extend[int, subrange(i!1, j!1), bool,
                                       FALSE]({x: subrange(i!1, j!1) | TRUE})))): 
                        IF i!1 <= j!1 THEN x-i!1 ELSE 0 ENDIF)")
            (("1" (EXPAND "bijective?")
              (("1" (PROP)
                (("1" (EXPAND "injective?")
                  (("1" (SKOSIMP*)
                    (("1" (TYPEPRED "x1!1")
                      (("1" (TYPEPRED "x2!1")
                        (("1" (GRIND) NIL)))))))))
                 ("2" (EXPAND "surjective?")
                  (("2" (SKOSIMP*)
                    (("2" (INST 1 "y!1+i!1")
                      (("1" (TYPEPRED "y!1") (("1" (GRIND) NIL)))
                       ("2" (TYPEPRED "y!1")
                        (("2" (GRIND) NIL)))))))))))))
             ("2" (SKOSIMP*)
              (("2" (TYPEPRED "x!1") (("2" (GRIND) NIL)))))
             ("3" (SKOSIMP*)
              (("3" (TYPEPRED "x!1") (("3" (GRIND) NIL)))))))))))
       ("2" (HIDE 2) (("2" (REWRITE "finite_nat_subrange") NIL)))
       ("3" (HIDE 2) (("3" (FLATTEN) (("3" (ASSERT) NIL))))))))))))

$$$finite_sets_int.pvs
finite_sets_int: THEORY
 BEGIN
  IMPORTING finite_sets[int]

  i, j, x: VAR int

  p: VAR pred[int]

  in_subrng(x,i,j): bool = (i <= x) AND (x <= j)

  finite_subrng       : LEMMA is_finite({x | in_subrng(x,i,j)})

  finite_subrng_subset: LEMMA is_finite({x | in_subrng(x,i,j) AND p(x)})

  card_subrng         : LEMMA card({x | in_subrng(x,i,j)}) =
                                  IF i <= j THEN abs(j-i+1) ELSE 0 ENDIF


% ------------------------------------------------------------------------
% The following lemmas apply is_finite[nat] and card[nat] to subtype
% sets.  This should be avoided if possible.  See finite_subint for
% preferred lemmas.
% ------------------------------------------------------------------------

  finite_int_subrange     : LEMMA is_finite[int]({x: subrange(i, j) | TRUE})

  finite_int_subrange_pred: LEMMA is_finite[int]({x: subrange(i, j) | p(x)})

  card_int_subrange       : LEMMA card[int]({x: subrange(i, j) | TRUE}) =
                                    IF i <= j THEN abs(j-i+1) ELSE 0 ENDIF

END finite_sets_int

$$$finite_sets_int.prf
(|finite_sets_int|
 (|finite_subrng| "" (SKOSIMP*)
  (("" (EXPAND "in_subrng")
    (("" (EXPAND "is_finite")
      ((""
        (INST 1 "abs(j!1-i!1+1)"
         "(LAMBDA (x: {x: int | i!1 <= x AND x <= j!1}): x - i!1)")
        (("1" (GRIND) NIL) ("2" (SKOSIMP*) (("2" (GRIND) NIL)))))))))))
 (|finite_subrng_subset| "" (SKOSIMP*)
  ((""
    (CASE "subset?({x: int | in_subrng(x, i!1, j!1) AND p!1(x)},{x: int | in_subrng(x, i!1, j!1)})")
    (("1" (LEMMA "finite_subset")
      (("1" (INST?)
        (("1" (ASSERT) NIL)
         ("2" (HIDE -1 2) (("2" (REWRITE "finite_subrng") NIL)))))))
     ("2" (HIDE 2)
      (("2" (EXPAND "subset?")
        (("2" (EXPAND "member") (("2" (SKOSIMP*) NIL)))))))))))
 (|card_subrng_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_subrng") NIL)))
 (|card_subrng| "" (SKOSIMP*)
  (("" (CASE "i!1 > j!1")
    (("1" (ASSERT)
      (("1" (CASE "{x: int | in_subrng(x, i!1, j!1)} = emptyset")
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (LEMMA "card_emptyset") (("1" (PROPAX) NIL)))))))
         ("2" (HIDE 2)
          (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("2" (GRIND) NIL)))))))))
     ("2" (ASSERT)
      (("2" (LEMMA "card_bij")
        (("2" (INST -1 "abs(j!1-i!1+1)" "{x | in_subrng(x, i!1, j!1)}")
          (("1" (REPLACE -1)
            (("1" (HIDE -1)
              (("1"
                (INST 2
                 "(LAMBDA (x: {x | in_subrng(x, i!1, j!1)}): abs(x -i!1))")
                (("1" (EXPAND "bijective?")
                  (("1" (PROP)
                    (("1" (EXPAND "injective?")
                      (("1" (SKOSIMP*)
                        (("1" (TYPEPRED "x1!1")
                          (("1" (TYPEPRED "x2!1") (("1" (GRIND) NIL)))))))))
                     ("2" (EXPAND "surjective?")
                      (("2" (SKOSIMP*)
                        (("2" (TYPEPRED "y!1")
                          (("2" (INST 1 "y!1+i!1")
                            (("1" (GRIND) NIL) ("2" (GRIND) NIL)))))))))))))
                 ("2" (SKOSIMP*)
                  (("2" (TYPEPRED "x!1")
                    (("2" (EXPAND "in_subrng")
                      (("2" (FLATTEN) (("2" (GRIND) NIL)))))))))))))))
           ("2" (HIDE 2 3) (("2" (REWRITE "finite_subrng") NIL)))))))))))))
 (|finite_int_subrange| "" (SKOSIMP*)
  (("" (EXPAND "is_finite")
    ((""
      (INST 1 "abs(j!1-i!1+1)"
       "(LAMBDA (x: (extend[int, subrange(i!1, j!1), bool,
                 FALSE]({x: subrange(i!1, j!1) | TRUE}))): x - i!1)")
      (("1" (EXPAND "injective?") (("1" (SKOSIMP*) NIL)))
       ("2" (SKOSIMP*)
        (("2" (EXPAND "abs")
          (("2" (GROUND)
            (("1" (TYPEPRED "x!1")
              (("1" (EXPAND "extend") (("1" (ASSERT) NIL)))))
             ("2" (LIFT-IF)
              (("2" (GROUND)
                (("1" (TYPEPRED "x!1")
                  (("1" (EXPAND "extend") (("1" (ASSERT) NIL)))))
                 ("2" (TYPEPRED "x!1")
                  (("2" (EXPAND "extend")
                    (("2" (ASSERT) NIL)))))))))))))))))))))
 (|finite_int_subrange_pred| "" (SKOSIMP*)
  (("" (CASE "is_finite({x: subrange(i!1, j!1) | TRUE})")
    (("1" (LEMMA "finite_subset")
      (("1"
        (INST -1 "extend[int, subrange(i!1, j!1),
                       bool, FALSE]({x: subrange(i!1, j!1) | TRUE})"
         "extend[int, subrange(i!1, j!1),
                            bool,
                            FALSE]({x: subrange(i!1, j!1)
                                   | p!1(x)})")
        (("1" (ASSERT)
          (("1" (HIDE -1 2)
            (("1" (EXPAND "subset?")
              (("1" (SKOSIMP*)
                (("1" (EXPAND "member")
                  (("1" (EXPAND "extend") (("1" (PROP) NIL)))))))))))))))))
     ("2" (HIDE 2) (("2" (REWRITE "finite_int_subrange") NIL)))))))
 (|card_int_subrange_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_int_subrange") NIL)))
 (|card_int_subrange| "" (SKOSIMP*)
  (("" (CASE "i!1 > j!1")
    (("1" (ASSERT)
      (("1"
        (CASE "extend[int, subrange(i!1, j!1),
                       bool, FALSE]({x: subrange(i!1, j!1)
                                    | TRUE}) = emptyset")
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (LEMMA "card_emptyset") (("1" (PROPAX) NIL)))))))
         ("2" (HIDE 2)
          (("2" (EXPAND "extend")
            (("2" (APPLY-EXTENSIONALITY)
              (("2" (LIFT-IF) (("2" (HIDE 2) (("2" (GRIND) NIL)))))))))))))))
     ("2" (ASSERT)
      (("2" (LEMMA "card_bij")
        (("2"
          (INST -1 "abs(j!1-i!1+1)" "extend[int, subrange(i!1, j!1),
                       bool, FALSE]({x: subrange(i!1, j!1)
                                    | TRUE})")
          (("1" (REPLACE -1)
            (("1" (HIDE -1)
              (("1"
                (INST 2 "(LAMBDA (x: (extend[int, subrange(i!1, j!1), bool,
                        FALSE]({x: subrange(i!1, j!1) | TRUE}))): abs(x -i!1))")
                (("1" (EXPAND "bijective?")
                  (("1" (PROP)
                    (("1" (EXPAND "injective?")
                      (("1" (SKOSIMP*)
                        (("1" (TYPEPRED "x1!1")
                          (("1" (TYPEPRED "x2!1")
                            (("1" (EXPAND "extend")
                              (("1" (EXPAND "abs")
                                (("1" (PROP) (("1" (ASSERT) NIL)))))))))))))))
                     ("2" (EXPAND "surjective?")
                      (("2" (SKOSIMP*)
                        (("2" (INST 1 "y!1+i!1")
                          (("1" (EXPAND "abs") (("1" (PROPAX) NIL)))
                           ("2" (EXPAND "extend")
                            (("2" (ASSERT)
                              (("2" (PROP)
                                (("2" (TYPEPRED "y!1")
                                  (("2" (EXPAND "abs")
                                    (("2" (ASSERT) NIL)))))))))))))))))))))
                 ("2" (SKOSIMP*)
                  (("2" (EXPAND "abs")
                    (("2" (TYPEPRED "x!1")
                      (("2" (EXPAND "extend")
                        (("2" (PROP) (("2" (ASSERT) NIL)))))))))))))))))
           ("2" (REWRITE "finite_int_subrange") NIL))))))))))))
$$$prelude_aux.pvs
prelude_aux[T: TYPE]: THEORY

BEGIN

  % these lemmas should go in prelude

  rest_emptyset: LEMMA (FORALL (S: set[T], t:T): rest(S) = emptyset[T]
                           AND S(t) IMPLIES choose(S) = t)


END prelude_aux

$$$prelude_aux.prf
(|prelude_aux| (|rest_emptyset_TCC1| "" (SUBTYPE-TCC) NIL)
 (|rest_emptyset| "" (SKOSIMP*)
  (("" (LEMMA "rest_empty_lem[T]")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SPLIT -1)
          (("1" (EXPAND "singleton")
            (("1" (EXPAND "extend")
              (("1" (REPLACE -1)
                (("1" (HIDE -1) (("1" (HIDE -1) (("1" (ASSERT) NIL)))))))))))
           ("2" (ASSERT)
            (("2" (EXPAND "empty?")
              (("2" (EXPAND "member") (("2" (INST?) NIL)))))))
           ("3" (REWRITE "emptyset_is_empty?[T]") NIL))))))))))))
$$$finite_sets_sum_real.pvs
finite_sets_sum_real[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% finite sum over real-valued functions   
%
%   Authors: Ricky W. Butler
%            David Griffioen
%
%   NOTES:
%      -- there are several theorems which are virtually idential to
%         theorems in finite_sets_sum.  They are repeated here to prevent
%         the need for commands such as (LEMMA sum_emptyset[T,real,0,+])
%      -- the theorems with names ending in "_rew" are especially useful
%         for rewriting.  Some of these take advantage of the fact that
%         since we have real-valued functions we have a "-" available.
%------------------------------------------------------------------------
BEGIN


  IMPORTING finite_sets_sum[T,real,0,+], prelude_aux

  S, A, B: VAR finite_set[T]
  t: VAR T
  c,N: VAR real
  f,g: VAR function[T -> real]

  sum_const        : THEOREM sum(S, (LAMBDA t: c)) = c*card(S) 

  sum_1_is_card    : COROLLARY sum(S,(LAMBDA t: 1)) = card(S)

  sum_mult         : THEOREM sum(S,(LAMBDA t: c*f(t))) = c*sum(S,f) 

% ----------- Some rewrite rules using "-" ------------------

  sum_empty?       : THEOREM empty?(S) IMPLIES sum(S,f) = 0

  sum_emptyset_rew : THEOREM S = emptyset[T] IMPLIES sum(S,f) = 0

  sum_singleton_rew: THEOREM card(S) = 1 AND S(t) IMPLIES sum(S,f) = f(t)

  sum_remove_rew   : THEOREM sum(remove(t,S),f) = sum(S,f) -
                                IF member(t,S) THEN f(t) ELSE 0 ENDIF 


  sum_rest_rew     : THEOREM NOT empty?(S) IMPLIES
                                sum(rest(S),f) = sum(S,f) - f(choose(S))

  sum_union_rew    : THEOREM sum(union(A,B),f) = sum(A,f) + sum(B,f)
                                 - sum(intersection(A,B),f) 


% -------- sums of slightly modified functions ----------

  sum_eq_funs       : THEOREM (FORALL (t: (S)): f(t) = g(t)) 
                               IMPLIES sum(S, f) = sum(S, g)

  sum_particular_gen: THEOREM sum(S,f) = sum(S, f WITH [t := c])
			       + IF S(t) THEN f(t) - c ELSE 0 ENDIF 


% ----- some order relationships involving sum -----

  sum_bound    : THEOREM (FORALL (t: (S)): f(t) <= N) 
                             IMPLIES sum(S,f) <= N*card(S)

  sum_order    : THEOREM (FORALL (t:T): f(t) <= g(t)) IMPLIES
                           sum(S,f) <= sum(S,g)

  sum_nonneg   : LEMMA (FORALL (t: (S)): f(t) >= 0) IMPLIES sum(S,f) >= 0

  sum_pos      : LEMMA (FORALL (t: (S)): f(t) > 0) IMPLIES sum(S,f) > 0 OR
                                                    S = emptyset[T]

  JUDGEMENT sum HAS_TYPE [non_empty_finite_set[T],[T -> posreal] -> posreal]

  JUDGEMENT sum HAS_TYPE [finite_set[T],[T -> int] -> int]

  JUDGEMENT sum HAS_TYPE [finite_set[T],[T -> nat] -> nat]

% ----- Special properties non-negative valued functions -----

  fnr,gnr: VAR [T -> nonneg_real]

  sum_subset   : THEOREM subset?(A,B) IMPLIES sum(A,fnr) <= sum(B,fnr)

  sum_order_sub: THEOREM subset?(A,B) AND (FORALL (t:T): fnr(t) <= gnr(t))
                           IMPLIES sum(A,fnr) <= sum(B,gnr)

  gn:  VAR function[T -> nat]
  gi:  VAR function[T -> nonneg_int]

  sum_0_nat       : THEOREM sum(S,gn) = 0 IMPLIES  S = emptyset[T] OR
                                          (FORALL (t:(S)): gn(t) = 0)

  sum_is_null     : COROLLARY sum(S,gn) = 0 => (S(t) => gn(t) = 0)

  sum_0_int       : THEOREM sum(S,gi) = 0 IMPLIES S = emptyset[T]
                                               OR (FORALL (t:(S)): gi(t) = 0)

  sum_0_non_neg   : THEOREM sum(S,f) = 0 AND (FORALL (t: (S)): f(t) >= 0) 
                             IMPLIES S = emptyset[T] 
                                      OR (FORALL (t:(S)): f(t) = 0)

  JUDGEMENT sum HAS_TYPE [finite_set[T],[T -> nonneg_real] -> nonneg_real]
  JUDGEMENT sum HAS_TYPE [finite_set[T],[T -> nonneg_int] -> nonneg_int]
  JUDGEMENT sum HAS_TYPE [non_empty_finite_set[T],[T->posnat] -> posnat]

%  JUDGEMENT sum HAS_TYPE [non_empty_finite_set[T],[T->negreal] -> negreal]
%  JUDGEMENT sum HAS_TYPE [finite_set[T],[T -> nonpos_real] -> nonpos_real]
%  JUDGEMENT sum HAS_TYPE [finite_set[T],[T -> negint] -> negint]

END finite_sets_sum_real


$$$finite_sets_sum_real.prf
(|finite_sets_sum_real| (IMPORTING1_TCC1 "" (TCC :DEFS !) NIL)
 (IMPORTING1_TCC2 "" (TCC :DEFS !) NIL)
 (|sum_const| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*)
    (("1" (REWRITE "sum_emptyset")
      (("1" (LEMMA "card_emptyset") (("1" (ASSERT) NIL)))))))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" 1)
      (("2" (INST?)
        (("2" (REPLACE -1)
          (("2" (HIDE -1)
            (("2" (LEMMA "card_rest")
              (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))
 (|sum_1_is_card| "" (LEMMA "sum_const")
  (("" (SKOSIMP*) (("" (INST -1 "S!1" "1") (("" (ASSERT) NIL)))))))
 (|sum_mult| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*)
    (("1" (LEMMA "sum_emptyset")
      (("1" (INST?)
        (("1" (REPLACE -1)
          (("1" (HIDE -1)
            (("1" (LEMMA "sum_emptyset")
              (("1" (INST?) (("1" (ASSERT) NIL)))))))))))))))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" 1)
      (("2" (INST?) (("2" (REPLACE -1) (("2" (ASSERT) NIL)))))))))))
 (|sum_empty?| "" (SKOSIMP*)
  (("" (REWRITE "emptyset_is_empty?[T]")
    (("" (LEMMA "sum_emptyset[T,real,0,+]")
      (("" (INST?) (("" (ASSERT) NIL)))))))))
 (|sum_emptyset_rew| "" (SKOSIMP*)
  (("" (LEMMA "sum_emptyset[T,real,0,+]")
    (("" (INST?) (("" (ASSERT) NIL)))))))
 (|sum_singleton_rew| "" (SKOSIMP*)
  (("" (REWRITE "card_one")
    (("" (SKOSIMP*)
      (("" (REPLACE -1)
        (("" (REWRITE "sum_singleton[T,real,0,+]")
          (("" (HIDE -1) (("" (GRIND) NIL)))))))))))))
 (|sum_remove_rew| "" (SKOSIMP*)
  (("" (LEMMA "sum_remove[T,real,0,+]")
    (("" (INST?)
      (("" (REPLACE -1 + RL)
        (("" (HIDE -1)
          (("" (ASSERT)
            (("" (GROUND)
              (("" (LIFT-IF) (("" (GROUND) NIL)))))))))))))))))
 (|sum_rest_rew_TCC1| "" (SUBTYPE-TCC) NIL)
 (|sum_rest_rew| "" (SKOSIMP*)
  (("" (LEMMA "sum_rest") (("" (INST?) (("" (ASSERT) NIL)))))))
 (|sum_union_rew| "" (SKOSIMP*)
  (("" (LEMMA "sum_union") (("" (INST?) (("" (ASSERT) NIL)))))))
 (|sum_eq_funs| "" (SKOSIMP*) (("" (REWRITE "sum_f_g") NIL)))
 (|sum_particular_gen| "" (AUTO-REWRITE "member")
  (("" (INDUCT "S" 1 "finite_set_induction_rest[T]")
    (("1" (SKOSIMP*)
      (("1" (REWRITE "sum_emptyset")
        (("1" (REWRITE "sum_emptyset")
          (("1" (EXPAND "emptyset") (("1" (PROPAX) NIL)))))))))
     ("2" (SKOSIMP*)
      (("2" (EXPAND "sum" 1)
        (("2" (LIFT-IF)
          (("2" (SPLIT 1)
            (("1" (FLATTEN)
              (("1" (INST?)
                (("1" (ASSERT)
                  (("1" (REPLACE -2 :HIDE? T)
                    (("1" (CASE "rest(SS!1)(t!1)")
                      (("1" (EXPAND "rest")
                        (("1" (REPLACE -2 * RL)
                          (("1" (EXPAND "remove")
                            (("1" (PROPAX) NIL)))))))
                       ("2" (ASSERT) NIL)))))))))))
             ("2" (FLATTEN)
              (("2" (INST?)
                (("2" (CASE " SS!1(t!1)")
                  (("1" (ASSERT)
                    (("1" (REPLACE -2 :HIDE? T)
                      (("1" (EXPAND "rest")
                        (("1" (EXPAND "remove")
                          (("1" (ASSERT) NIL)))))))))
                   ("2" (REPLACE -1 :HIDE? T)
                    (("2" (EXPAND "rest")
                      (("2" (EXPAND "remove")
                        (("2" (GROUND) NIL)))))))))))))))))))))))))
 (|sum_bound| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*)
    (("1" (REWRITE "sum_emptyset")
      (("1" (REWRITE "card_emptyset")
        (("1" (HIDE -1) (("1" (ASSERT) NIL)))))))))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" 1)
      (("2" (INST -1 "N!1" "f!1")
        (("2" (SPLIT -1)
          (("1" (INST -2 "choose(SS!1)")
            (("1" (REWRITE "card_rest") (("1" (ASSERT) NIL)))))
           ("2" (HIDE 2)
            (("2" (SKOSIMP*)
              (("2" (INST -1 "t!1")
                (("2" (TYPEPRED "t!1")
                  (("2" (GRIND :EXCLUDE "choose")
                    NIL)))))))))))))))))))
 (|sum_order| ""
  (INDUCT-AND-SIMPLIFY "S" 1 "finite_set_induction_rest" :EXCLUDE
   ("rest" "choose"))
  NIL)
 (|sum_nonneg| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*)
    (("1" (REWRITE "sum_emptyset") (("1" (ASSERT) NIL)))))
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" 1)
      (("2" (INST?)
        (("2" (SPLIT -1)
          (("1" (INST -2 "choose(SS!1)") (("1" (ASSERT) NIL)))
           ("2" (HIDE 2)
            (("2" (SKOSIMP*)
              (("2" (INST?)
                (("2" (TYPEPRED "t!1")
                  (("2" (LEMMA "rest_member[T]")
                    (("2" (EXPAND "member")
                      (("2" (INST -1 "SS!1" "t!1")
                        (("2" (ASSERT) NIL)))))))))))))))))))))))))
 (|sum_pos| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*) NIL)
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" 1)
      (("2" (INST?)
        (("2" (SPLIT -1)
          (("1" (INST -2 "choose(SS!1)") (("1" (ASSERT) NIL)))
           ("2" (HIDE 2)
            (("2" (REPLACE -1)
              (("2" (HIDE -1)
                (("2" (REWRITE "sum_emptyset")
                  (("2" (ASSERT) (("2" (INST?) NIL)))))))))))
           ("3" (HIDE 2)
            (("3" (SKOSIMP*)
              (("3" (INST?)
                (("3" (TYPEPRED "t!1")
                  (("3" (LEMMA "rest_member[T]")
                    (("3" (EXPAND "member")
                      (("3" (INST -1 "SS!1" "t!1")
                        (("3" (ASSERT) NIL)))))))))))))))))))))))))
 (|sum_TCC1| "" (AUTO-REWRITE-THEORY "rationals")
  (("" (AUTO-REWRITE-THEORY "integers")
    (("" (INDUCT "x1" 1 "finite_set_induction_rest")
      (("1" (TYPEPRED "x1!1") (("1" (PROPAX) NIL)))
       ("2" (SKOSIMP*)
        (("2" (HIDE 2)
          (("2" (LEMMA "emptyset_is_empty?[T]")
            (("2" (INST?) (("2" (ASSERT) NIL)))))))))
       ("3" (SKOSIMP*)
        (("3" (ASSERT)
          (("3" (SPLIT -1)
            (("1" (INST?)
              (("1" (FLATTEN)
                (("1" (ASSERT)
                  (("1" (EXPAND "sum" 2)
                    (("1" (ASSERT)
                      (("1" (TYPEPRED "x2!1(choose(SS!1))")
                        (("1" (ASSERT) NIL)))))))))))))
             ("2" (EXPAND "sum" 2)
              (("2" (TYPEPRED "x2!1(choose(SS!1))")
                (("2" (CASE "rest(SS!1) = emptyset")
                  (("1" (REPLACE -1)
                    (("1" (HIDE -1)
                      (("1" (REWRITE "sum_emptyset")
                        (("1" (ASSERT) NIL)))))))
                   ("2" (HIDE -1 -2 2 3)
                    (("2" (LEMMA "emptyset_is_empty?[T]")
                      (("2" (INST?)
                        (("2" (ASSERT) NIL)))))))))))))))))))))))))
 (|sum_TCC2| "" (AUTO-REWRITE-THEORY "rationals")
  (("" (AUTO-REWRITE-THEORY "integers")
    (("" (INDUCT-AND-SIMPLIFY "x1" 1 "finite_set_induction_rest")
      NIL)))))
 (|sum_TCC3| "" (SKOSIMP*)
  (("" (LEMMA "sum_nonneg")
    (("" (INST?)
      (("" (ASSERT) (("" (SKOSIMP*) (("" (ASSERT) NIL)))))))))))
 (|sum_subset| "" (SKOSIMP*)
  (("" (CASE "B!1 = union(A!1,difference(B!1,A!1))")
    (("1" (REPLACE -1 +)
      (("1" (HIDE -1)
        (("1" (LEMMA "sum_union")
          (("1" (INST?)
            (("1"
              (CASE "sum(intersection(A!1, difference(B!1, A!1)), fnr!1) = 0")
              (("1" (REPLACE -1)
                (("1" (HIDE -1)
                  (("1" (ASSERT)
                    (("1" (REPLACE -1)
                      (("1" (HIDE -1)
                        (("1" (LEMMA "sum_nonneg")
                          (("1"
                            (INST -1 "difference(B!1, A!1)" "fnr!1")
                            (("1" (ASSERT)
                              (("1"
                                (HIDE -1)
                                (("1"
                                  (SKOSIMP*)
                                  (("1"
                                    (ASSERT)
                                    NIL)))))))))))))))))))))
               ("2" (HIDE -1 2)
                (("2"
                  (CASE "intersection(A!1, difference(B!1, A!1)) = emptyset")
                  (("1" (REPLACE -1)
                    (("1" (HIDE -1)
                      (("1" (REWRITE "sum_emptyset") NIL)))))
                   ("2" (HIDE 2)
                    (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                      (("2" (GRIND) NIL)))))))))))))))))))
     ("2" (HIDE 2)
      (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T)
        (("2" (GRIND) NIL)))))))))
 (|sum_order_sub| "" (SKOSIMP*)
  (("" (LEMMA "sum_subset")
    (("" (INST?)
      (("" (INST -1 "B!1")
        (("" (ASSERT)
          (("" (LEMMA "sum_order")
            (("" (INST -1 "B!1" "fnr!1" "gnr!1")
              (("" (ASSERT) NIL)))))))))))))))
 (|sum_0_nat| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*) NIL)
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" -2)
      (("2" (INST?)
        (("2" (TYPEPRED "sum(rest(SS!1), gn!1)")
          (("2" (ASSERT)
            (("2" (TYPEPRED "t!1")
              (("2" (SPLIT -5)
                (("1" (ASSERT)
                  (("1" (LEMMA "rest_emptyset[T]")
                    (("1" (INST?) (("1" (ASSERT) NIL)))))))
                 ("2" (LEMMA "choose_rest_or[T]")
                  (("2" (INST?)
                    (("2" (EXPAND "member")
                      (("2" (INST?)
                        (("2" (ASSERT)
                          (("2" (INST?) NIL)))))))))))))))))))))))))))
 (|sum_is_null| "" (SKOSIMP*)
  (("" (LEMMA "sum_0_nat")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SPLIT -1)
          (("1" (HIDE -2 1)
            (("1" (REWRITE "emptyset_is_empty?[T]" :DIR RL)
              (("1" (EXPAND "empty?")
                (("1" (EXPAND "member") (("1" (INST?) NIL)))))))))
           ("2" (INST?) NIL)))))))))))
 (|sum_0_int| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*) NIL)
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" -2)
      (("2" (INST?)
        (("2" (TYPEPRED "sum(rest(SS!1), gi!1)")
          (("2" (ASSERT)
            (("2" (TYPEPRED "t!1")
              (("2" (SPLIT -5)
                (("1" (LEMMA "rest_emptyset[T]")
                  (("1" (INST?) (("1" (ASSERT) NIL)))))
                 ("2" (LEMMA "choose_rest_or[T]")
                  (("2" (INST?)
                    (("2" (EXPAND "member")
                      (("2" (INST?)
                        (("2" (ASSERT)
                          (("2" (INST?) NIL)))))))))))))))))))))))))))
 (|sum_0_non_neg| "" (INDUCT "S" 1 "finite_set_induction_rest")
  (("1" (SKOSIMP*) NIL)
   ("2" (SKOSIMP*)
    (("2" (EXPAND "sum" -2)
      (("2" (INST?)
        (("2" (LEMMA "sum_nonneg")
          (("2" (INST?)
            (("2" (CASE "(FORALL (t: (rest(SS!1))): f!1(t) >= 0)")
              (("1" (REPLACE -1)
                (("1" (ASSERT)
                  (("1" (CASE "f!1(choose(SS!1)) = 0")
                    (("1" (REPLACE -1)
                      (("1" (HIDE -1)
                        (("1" (ASSERT)
                          (("1" (SPLIT -3)
                            (("1" (CASE "t!1 = choose(SS!1)")
                              (("1" (REVEAL -1) (("1" (ASSERT) NIL)))
                               ("2"
                                (HIDE -2 -3 -4 -5 3)
                                (("2"
                                  (LEMMA "rest_emptyset[T]")
                                  (("2"
                                    (INST?)
                                    (("2"
                                      (INST -1 "t!1")
                                      (("2" (ASSERT) NIL)))))))))))
                             ("2" (LEMMA "choose_rest_or[T]")
                              (("2"
                                (EXPAND "member")
                                (("2"
                                  (INST?)
                                  (("2"
                                    (INST -1 "t!1")
                                    (("2"
                                      (ASSERT)
                                      (("2"
                                        (INST -2 "t!1")
                                        NIL)))))))))))))))))))
                     ("2" (ASSERT)
                      (("2" (INST -5 "choose(SS!1)")
                        (("2" (ASSERT) NIL)))))))))))
               ("2" (HIDE -1 -2 -3 3)
                (("2" (SKOSIMP*)
                  (("2" (INST -1 "t!2")
                    (("2" (TYPEPRED "t!2")
                      (("2" (LEMMA "rest_member[T]")
                        (("2" (INST?)
                          (("2" (EXPAND "member")
                            (("2" (INST?)
                              (("2"
                                (ASSERT)
                                NIL)))))))))))))))))))))))))))))))
 (|sum_TCC4| "" (LEMMA "sum_nonneg")
  (("" (SKOSIMP*)
    (("" (INST?)
      (("" (ASSERT)
        (("" (HIDE 2)
          (("" (SKOSIMP*)
            (("" (TYPEPRED "x2!1(t!1)")
              (("" (PROPAX) NIL)))))))))))))))
 (|sum_TCC5| "" (SUBTYPE-TCC) NIL))

$$$finite_sets_minmax.pvs
finite_sets_minmax[T: TYPE, <= : (total_order?[T])]: THEORY
BEGIN

  IMPORTING  finite_sets_inductions[T] %, sets_aux[T]

  min(x,y:T): T = IF x <= y THEN x ELSE y ENDIF
  max(x,y:T): T = IF x <= y THEN y ELSE x ENDIF

  a,x,y: VAR T
  SS: VAR non_empty_finite_set

  minrec(SS): RECURSIVE T = 
                IF empty?(rest(SS)) THEN choose(SS)
                ELSE min(choose(SS),minrec(rest(SS)))
                ENDIF
              MEASURE (LAMBDA SS: card(SS))

  maxrec(SS): RECURSIVE T = 
                IF empty?(rest(SS)) THEN choose(SS)
                ELSE max(choose(SS),maxrec(rest(SS)))
                ENDIF
              MEASURE (LAMBDA SS: card(SS))

  lt_reflexive:     LEMMA FORALL (x: T): <=(x, x)
  lt_transitive:    LEMMA FORALL (x,y,z:T): <=(x, y) & <=(y, z) => <=(x, z)
  lt_total:         LEMMA FORALL (x,y:T) : x <= y OR y <= x
  lt_antisymmetric: LEMMA FORALL (x,y: T): <=(x, y) & <=(y, x) => x = y

  min(SS): {a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}
  max(SS): {a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}
 

  min_lem: LEMMA (min(SS) = a IFF
                  SS(a) AND (FORALL (x: (SS)): a <= x))

  max_lem: LEMMA (max(SS) = a IFF
                  SS(a) AND (FORALL (x: (SS)): x <= a))

  A,B:   VAR non_empty_finite_set

  min_union: LEMMA min(A) = x AND min(B) = y IMPLIES
                      min(union(A,B)) = min(x,y)

  max_union: LEMMA max(A) = x AND max(B) = y IMPLIES
                      max(union(A,B)) = max(x,y)


END finite_sets_minmax

$$$finite_sets_minmax.prf
(|finite_sets_minmax|
 (|minrec_TCC1| "" (SKOSIMP*) (("" (REWRITE "card_rest") (("" (ASSERT) NIL)))))
 (|lt_reflexive| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -2 3)
            (("" (EXPAND "preorder?")
              (("" (FLATTEN)
                (("" (EXPAND "reflexive?") (("" (INST?) NIL)))))))))))))))))))
 (|lt_transitive| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -2 3)
            (("" (EXPAND "preorder?")
              (("" (FLATTEN)
                (("" (HIDE -1 -3)
                  (("" (EXPAND "transitive?")
                    (("" (INST -1 "x!1" "y!1" "z!1")
                      (("" (ASSERT) NIL)))))))))))))))))))))))
 (|lt_total| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -1 -2)
            (("" (EXPAND "dichotomous?")
              (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))
 (|lt_antisymmetric| "" (SKOSIMP*)
  (("" (TYPEPRED "finite_sets_minmax.<=")
    (("" (EXPAND "total_order?")
      (("" (EXPAND "partial_order?")
        (("" (FLATTEN)
          (("" (HIDE -1 -3)
            (("" (EXPAND "antisymmetric?")
              (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))
 (|min_TCC1| "" (INST 1 "(LAMBDA SS: minrec(SS))")
  (("" (INDUCT "SS" 1 "finite_set_induction_rest")
    (("1" (TYPEPRED "SS!1") (("1" (PROPAX) NIL)))
     ("2" (TYPEPRED "SS!1") (("2" (PROPAX) NIL)))
     ("3" (ASSERT) (("3" (AUTO-REWRITE-THEORY "sets[T]") (("3" (ASSERT) NIL)))))
     ("4" (SKOSIMP*)
      (("4" (EXPAND "minrec" +)
        (("4" (SPLIT 2)
          (("1" (ASSERT) NIL)
           ("2" (FLATTEN)
            (("2" (AUTO-REWRITE-THEORY "sets[T]")
              (("2" (ASSERT)
                (("2" (SKOSIMP*)
                  (("2" (EXPAND "min")
                    (("2" (ASSERT)
                      (("2" (SPLIT)
                        (("1" (FLATTEN)
                          (("1" (LEMMA "epsilon_ax[T]")
                            (("1" (INST?)
                              (("1" (ASSERT) (("1" (INST 1 "x!1") NIL)))))))))
                         ("2" (ASSERT) NIL)))))))))))))))
           ("3" (SKOSIMP*)
            (("3" (LIFT-IF)
              (("3" (SPLIT 1)
                (("1" (HIDE -2)
                  (("1" (FLATTEN)
                    (("1" (LEMMA "choose_rest_or[T]")
                      (("1" (INST?)
                        (("1" (EXPAND "member")
                          (("1" (INST?)
                            (("1" (ASSERT)
                              (("1" (SPLIT -1)
                                (("1" (EXPAND "empty?")
                                  (("1" (INST?)
                                    (("1" (EXPAND "member")
                                      (("1" (PROPAX) NIL)))))))
                                 ("2" (REPLACE -1)
                                  (("2" (HIDE -1)
                                    (("2" (REWRITE "lt_reflexive")
                                      NIL)))))))))))))))))))))
                 ("2" (FLATTEN)
                  (("2" (ASSERT)
                    (("2" (FLATTEN)
                      (("2" (EXPAND "min")
                        (("2" (LIFT-IF)
                          (("2" (ASSERT)
                            (("2" (GROUND)
                              (("1" (LEMMA "choose_rest_or[T]")
                                (("1" (EXPAND "member")
                                  (("1" (INST -1 "SS!1" "x!1")
                                    (("1" (ASSERT)
                                      (("1" (SPLIT -1)
                                        (("1"
                                          (INST -5 "x!1")
                                          (("1"
                                            (ASSERT)
                                            (("1"
                                              (HIDE -1 -3 -4 2 3)
                                              (("1"
                                                (LEMMA "lt_transitive")
                                                (("1"
                                                  (INST
                                                   -1
                                                   "choose(SS!1)"
                                                   " minrec(rest(SS!1))"
                                                   "x!1")
                                                  (("1" (ASSERT) NIL)))))))))))
                                         ("2"
                                          (REPLACE -1)
                                          (("2"
                                            (HIDE -1)
                                            (("2"
                                              (HIDE -1 -2 -3 -4)
                                              (("2"
                                                (REWRITE "lt_reflexive")
                                                NIL)))))))))))))))))
                               ("2" (INST -3 "x!1")
                                (("2" (SPLIT -3)
                                  (("1" (PROPAX) NIL)
                                   ("2" (CASE-REPLACE "x!1 = choose(SS!1)")
                                    (("1" (HIDE -1 -2 -3 1 4 5)
                                      (("1" (LEMMA "lt_total")
                                        (("1" (INST?) (("1" (GROUND) NIL)))))))
                                     ("2" (HIDE 3 4 5 6)
                                      (("2" (LEMMA "choose_rest_or[T]")
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (EXPAND "member")
                                            (("2"
                                              (GROUND)
                                              NIL)))))))))))))))))))))))))))))))))))))))))))))
 (|max_TCC1| "" (INST 1 "(LAMBDA SS: maxrec(SS))")
  (("" (INDUCT "SS" 1 "finite_set_induction_rest")
    (("1" (TYPEPRED "SS!1") (("1" (PROPAX) NIL)))
     ("2" (TYPEPRED "SS!1") (("2" (PROPAX) NIL)))
     ("3" (ASSERT) (("3" (AUTO-REWRITE-THEORY "sets[T]") (("3" (ASSERT) NIL)))))
     ("4" (SKOSIMP*)
      (("4" (EXPAND "maxrec" +)
        (("4" (SPLIT 2)
          (("1" (ASSERT) NIL)
           ("2" (FLATTEN)
            (("2" (AUTO-REWRITE-THEORY "sets[T]")
              (("2" (ASSERT)
                (("2" (SKOSIMP*)
                  (("2" (EXPAND "max")
                    (("2" (ASSERT)
                      (("2" (SPLIT 2)
                        (("1" (ASSERT) NIL)
                         ("2" (FLATTEN)
                          (("2" (LEMMA "epsilon_ax[T]")
                            (("2" (INST?)
                              (("2" (ASSERT)
                                (("2" (INST 1 "x!1") NIL)))))))))))))))))))))))
           ("3" (SKOSIMP*)
            (("3" (LIFT-IF)
              (("3" (SPLIT 1)
                (("1" (HIDE -2)
                  (("1" (FLATTEN)
                    (("1" (CASE-REPLACE "x!1=choose(SS!1)")
                      (("1" (REWRITE "lt_reflexive") NIL)
                       ("2" (HIDE 2)
                        (("2" (LEMMA "choose_rest_or[T]")
                          (("2" (EXPAND "member")
                            (("2" (INST?)
                              (("2" (ASSERT)
                                (("2" (EXPAND "empty?")
                                  (("2" (EXPAND "member")
                                    (("2" (INST?) NIL)))))))))))))))))))))
                 ("2" (FLATTEN)
                  (("2" (ASSERT)
                    (("2" (FLATTEN)
                      (("2" (EXPAND "max")
                        (("2" (LIFT-IF)
                          (("2" (ASSERT)
                            (("2" (PROP)
                              (("1" (HIDE -4)
                                (("1" (LEMMA "choose_rest_or[T]")
                                  (("1" (EXPAND "member")
                                    (("1" (INST -1 "SS!1" "x!1")
                                      (("1" (ASSERT)
                                        (("1"
                                          (REVEAL -2)
                                          (("1"
                                            (INST -1 "x!1")
                                            (("1" (ASSERT) NIL)))))))))))))))
                               ("2" (ASSERT)
                                (("2" (INST -3 "x!1")
                                  (("2" (SPLIT -3)
                                    (("1" (HIDE -2 -3 3 4)
                                      (("1" (LEMMA "lt_total")
                                        (("1"
                                          (INST
                                           -1
                                           "maxrec(rest(SS!1))"
                                           "choose(SS!1) ")
                                          (("1"
                                            (PROP)
                                            (("1"
                                              (LEMMA "lt_transitive")
                                              (("1"
                                                (INST
                                                 -1
                                                 "x!1"
                                                 "maxrec(rest(SS!1))"
                                                 "choose(SS!1)")
                                                (("1" (ASSERT) NIL)))))))))))))
                                     ("2" (LEMMA "choose_rest_or[T]")
                                      (("2" (EXPAND "member")
                                        (("2"
                                          (INST?)
                                          (("2"
                                            (ASSERT)
                                            (("2"
                                              (REPLACE -1)
                                              (("2"
                                                (HIDE -1)
                                                (("2"
                                                  (REWRITE "lt_reflexive")
                                                  NIL)))))))))))))))))))))))))))))))))))))))))))))))))
 (|min_lem| "" (SKOSIMP*)
  (("" (TYPEPRED "min(SS!1)")
    (("" (PROP)
      (("1" (ASSERT) NIL)
       ("2" (SKOSIMP*)
        (("2" (REPLACE -1)
          (("2" (HIDE -1)
            (("2" (TYPEPRED "x!1") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))
       ("3" (INST -4 "a!1")
        (("3" (ASSERT)
          (("3" (INST -2 "min(SS!1)")
            (("3" (ASSERT)
              (("3" (HIDE -1 -3)
                (("3" (REWRITE "lt_antisymmetric") NIL)))))))))))))))))
 (|max_lem| "" (SKOSIMP*)
  (("" (TYPEPRED "max(SS!1)")
    (("" (PROP)
      (("1" (ASSERT) NIL)
       ("2" (SKOSIMP*)
        (("2" (REPLACE -1)
          (("2" (HIDE -1)
            (("2" (TYPEPRED "x!1") (("2" (INST?) (("2" (ASSERT) NIL)))))))))))
       ("3" (INST -4 "a!1")
        (("3" (ASSERT)
          (("3" (INST -2 "max(SS!1)")
            (("3" (ASSERT)
              (("3" (HIDE -1 -3)
                (("3" (REWRITE "lt_antisymmetric") NIL)))))))))))))))))
 (|min_union| "" (SKOSIMP*)
  (("" (AUTO-REWRITE "member" "union")
    (("" (LEMMA "min_lem")
      (("" (INST-CP -1 "A!1" "x!1")
        (("" (INST -1 "B!1" "y!1")
          (("" (ASSERT)
            (("" (LEMMA "min_lem")
              (("" (INST -1 "union(A!1,B!1)" "min(x!1, y!1)")
                (("" (FLATTEN)
                  (("" (HIDE -1)
                    (("" (ASSERT)
                      (("" (HIDE 2)
                        (("" (SPLIT 1)
                          (("1" (FLATTEN)
                            (("1" (EXPAND "min")
                              (("1" (CASE "x!1 <= y!1")
                                (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
                           ("2" (SKOSIMP*)
                            (("2" (TYPEPRED "x!2")
                              (("2" (EXPAND "union")
                                (("2" (EXPAND "min")
                                  (("2" (EXPAND "member")
                                    (("2" (LIFT-IF)
                                      (("2" (SPLIT 1)
                                        (("1"
                                          (FLATTEN)
                                          (("1"
                                            (SPLIT -2)
                                            (("1" (INST -4 "x!2") NIL)
                                             ("2"
                                              (INST -3 "x!2")
                                              (("2"
                                                (HIDE -1 -4 -5 -6)
                                                (("2"
                                                  (LEMMA "lt_transitive")
                                                  (("2"
                                                    (INST -1 "x!1" "y!1" "x!2")
                                                    (("2"
                                                      (ASSERT)
                                                      NIL)))))))))))))
                                         ("2"
                                          (FLATTEN)
                                          (("2"
                                            (SPLIT -1)
                                            (("1"
                                              (INST -3 "x!2")
                                              (("1"
                                                (ASSERT)
                                                (("1"
                                                  (HIDE -1 -2 -4 -5)
                                                  (("1"
                                                    (LEMMA "lt_transitive")
                                                    (("1"
                                                      (INST
                                                       -1
                                                       "x!1"
                                                       "x!2"
                                                       "y!1")
                                                      (("1"
                                                        (ASSERT)
                                                        (("1"
                                                          (HIDE -1 2)
                                                          (("1"
                                                            (LEMMA "lt_total")
                                                            (("1"
                                                              (INST?)
                                                              (("1"
                                                                (ASSERT)
                                                                NIL)))))))))))))))))))
                                             ("2"
                                              (INST -2 "x!2")
                                              NIL)))))))))))))))))))))))))))))))))))))))))))))
 (|max_union| "" (SKOSIMP*)
  (("" (AUTO-REWRITE "member" "union")
    (("" (LEMMA "max_lem")
      (("" (INST-CP -1 "A!1" "x!1")
        (("" (INST -1 "B!1" "y!1")
          (("" (ASSERT)
            (("" (LEMMA "max_lem")
              (("" (INST -1 "union(A!1,B!1)" "max(x!1, y!1)")
                (("" (FLATTEN)
                  (("" (HIDE -1)
                    (("" (ASSERT)
                      (("" (HIDE 2)
                        (("" (SPLIT 1)
                          (("1" (FLATTEN)
                            (("1" (EXPAND "max")
                              (("1" (CASE "x!1 <= y!1")
                                (("1" (ASSERT) NIL) ("2" (ASSERT) NIL)))))))
                           ("2" (SKOSIMP*)
                            (("2" (TYPEPRED "x!2")
                              (("2" (EXPAND "union")
                                (("2" (EXPAND "max")
                                  (("2" (EXPAND "member")
                                    (("2" (LIFT-IF)
                                      (("2" (SPLIT 1)
                                        (("1"
                                          (FLATTEN)
                                          (("1"
                                            (SPLIT -2)
                                            (("1"
                                              (INST -4 "x!2")
                                              (("1"
                                                (HIDE -1 -3 -5 -6)
                                                (("1"
                                                  (LEMMA "lt_transitive")
                                                  (("1"
                                                    (INST -1 "x!2" "x!1" "y!1")
                                                    (("1" (ASSERT) NIL)))))))))
                                             ("2" (INST -3 "x!2") NIL)))))
                                         ("2"
                                          (FLATTEN)
                                          (("2"
                                            (SPLIT -1)
                                            (("1" (INST -3 "x!2") NIL)
                                             ("2"
                                              (INST -2 "x!2")
                                              (("2"
                                                (HIDE -1 -3 -4 -5)
                                                (("2"
                                                  (LEMMA "lt_transitive")
                                                  (("2"
                                                    (INST -1 "x!2" "y!1" "x!1")
                                                    (("2"
                                                      (ASSERT)
                                                      (("2"
                                                        (HIDE -1 3)
                                                        (("2"
                                                          (LEMMA "lt_total")
                                                          (("2"
                                                            (INST?)
                                                            (("2"
                                                              (ASSERT)
                                                              NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
$$$finite_sets_inductions.pvs
finite_sets_inductions[T: TYPE]: THEORY

BEGIN

  IMPORTING finite_sets[T]

  S, S1, S2 : VAR finite_set
  SS,U : VAR non_empty_finite_set
  e : VAR T
  P : VAR pred[finite_set]
  Q : VAR pred[non_empty_finite_set]
  n : VAR nat

  cardinal_induction       : LEMMA (FORALL S : P(S)) IFF 
                                      (FORALL n, S : card(S) = n IMPLIES P(S)) 

  finite_set_induction     : THEOREM P(emptyset[T])
                                      AND (FORALL e,S: P(S) IMPLIES P(add(e,S)))
                                         IMPLIES (FORALL S: P(S))

  finite_set_ind_modified  : THEOREM  P(emptyset[T]) AND 
                             (FORALL e,S: NOT S(e) AND P(S) IMPLIES P(add(e,S)))
                                       IMPLIES (FORALL S: P(S))

  finite_set_induction_rest: THEOREM P(emptyset[T])
                                     AND (FORALL SS : P(rest(SS)) IMPLIES P(SS))
                                             IMPLIES (FORALL S : P(S))

  finite_set_induction_union: THEOREM P(emptyset[T])
                                      AND (FORALL e: P(singleton(e)))
                  AND (FORALL S1,S2: P(S1) AND P(S2) IMPLIES P(union(S1,S2)))
                                     IMPLIES (FORALL S: P(S))


  finite_set_induction_gen: THEOREM (FORALL S:
                                 (FORALL S2: card(S2) < card(S) IMPLIES P(S2))
                                                IMPLIES P(S))
                                  IMPLIES (FORALL S: P(S))


% -------- Induction rules for non empty sets ----------------


  nonempty_card_induction : LEMMA (FORALL U : Q(U)) IFF 
	                      (FORALL S, n : n > 0 AND card(S) = n IMPLIES Q(S))

  nonempty_finite_set_induct : THEOREM (FORALL e : Q(singleton(e)))
       AND (FORALL e, U : Q(U) AND NOT U(e) IMPLIES Q(add(e, U)))
                                        IMPLIES (FORALL U : Q(U))

END finite_sets_inductions


$$$finite_sets_inductions.prf
(|finite_sets_inductions| (|cardinal_induction| "" (GRIND :DEFS NIL) NIL)
 (|finite_set_induction_TCC1| "" (REWRITE "finite_emptyset") NIL)
 (|finite_set_induction| "" (SKOSIMP)
  (("" (REWRITE "cardinal_induction")
    (("" (INDUCT "n")
      (("1" (SKOSIMP)
        (("1" (REWRITE "empty_card" :DIR RL)
          (("1" (REWRITE "emptyset_is_empty?")
            (("1" (EXPAND "emptyset") (("1" (ASSERT) NIL)))))))))
       ("2" (SKOSIMP*)
        (("2" (USE "nonempty_card")
          (("2" (ASSERT)
            (("2" (REWRITE "nonempty_member")
              (("2" (SKOLEM!)
                (("2" (INST -2 "remove(x!1, S!1)")
                  (("2" (INST -5 "x!1" "remove(x!1, S!1)")
                    (("2" (AUTO-REWRITE "card_remove" "add_remove_member")
                      (("2" (ASSERT)
                        (("2" (EXPAND "member")
                          (("2" (ASSERT) NIL)))))))))))))))))))))))))))
 (|finite_set_ind_modified| "" (SKOSIMP*)
  (("" (LEMMA "finite_set_induction")
    (("" (INST?)
      (("" (SPLIT -1)
        (("1" (INST -1 "S!1") NIL) ("2" (PROPAX) NIL)
         ("3" (SKOSIMP*)
          (("3" (INST -3 "e!1" "S!2")
            (("3" (ASSERT)
              (("3" (CASE-REPLACE "add(e!1, S!2) = S!2")
                (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T)
                  (("3" (GRIND) NIL)))))))))))))))))))
 (|finite_set_induction_rest| "" (SKOSIMP)
  (("" (REWRITE "cardinal_induction" 1)
    (("" (INDUCT "n")
      (("1" (SKOSIMP*)
        (("1" (HIDE -3)
          (("1" (CASE-REPLACE "S!1 = emptyset")
            (("1" (REWRITE "card_empty?")
              (("1" (REWRITE "emptyset_is_empty?") NIL)))))))))
       ("2" (AUTO-REWRITE "card_rest" "nonempty?")
        (("2" (SKOSIMP*)
          (("2" (USE "nonempty_card")
            (("2" (ASSERT)
              (("2" (INST? -4)
                (("2" (INST -1 "rest(S!1)") (("2" (ASSERT) NIL)))))))))))))))))))
 (|finite_set_induction_union_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_singleton") NIL)))
 (|finite_set_induction_union| "" (SKOSIMP)
  (("" (REWRITE "finite_set_induction")
    (("" (SKOSIMP)
      (("" (INST? -3)
        (("" (AUTO-REWRITE "add_as_union" "singleton")
          (("" (INST -4 "S!1" "singleton(e!1)")
            (("1" (ASSERT) NIL) ("2" (REWRITE "finite_singleton") NIL)))))))))))))
 (|finite_set_induction_gen| "" (SKOSIMP)
  (("" (REWRITE "cardinal_induction" +)
    (("" (INDUCT "n" 1 "NAT_induction")
      (("" (SKOSIMP*)
        (("" (INST -3 "S!1")
          (("" (SPLIT -3)
            (("1" (PROPAX) NIL)
             ("2" (SKOSIMP*)
              (("2" (INST -2 "card(S2!1)")
                (("2" (ASSERT)
                  (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))))))
 (|nonempty_card_induction_TCC1| "" (SKOSIMP)
  (("" (REWRITE "empty_card") (("" (ASSERT) NIL)))))
 (|nonempty_card_induction| "" (SKOLEM!)
  (("" (PROP)
    (("1" (SKOSIMP)
      (("1" (INST? -1) (("1" (REWRITE "empty_card") (("1" (ASSERT) NIL)))))))
     ("2" (SKOSIMP :PREDS? T)
      (("2" (REWRITE "empty_card")
        (("2" (INST -2 "U!1" "card(U!1)") (("2" (ASSERT) NIL)))))))))))
 (|nonempty_finite_set_induct_TCC1| "" (SKOSIMP*)
  (("" (REWRITE "finite_singleton") (("" (GRIND) NIL)))))
 (|nonempty_finite_set_induct| "" (SKOSIMP*)
  (("" (CASE "FORALL S : empty?(S) OR Q!1(S)")
    (("1" (INST? -1) (("1" (ASSERT) NIL)))
     ("2"
      (AUTO-REWRITE "emptyset_is_empty?[T]" "Emptyset" "Singleton"
                    "singleton_as_add")
      (("2" (REWRITE "finite_set_ind_modified")
        (("2" (HIDE 2 3)
          (("2" (SKOSIMP*)
            (("2" (SPLIT -1)
              (("1" (ASSERT) (("1" (INST? -2) (("1" (ASSERT) NIL)))))
               ("2" (GROUND)
                (("2" (INST?)
                  (("2" (INST?)
                    (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))))))))))))))
$$$finite_sets_sum.pvs
finite_sets_sum[T, R: TYPE, zero:R, +:[R,R -> R] ]: THEORY
%----------------------------------------------------------------------
%  
%                                              ----
%                                              \     
%  sum(S: finite_set[T], f:[T->R]) = zero +       f(i) 
%                                              /
%                                              ----
%                                              member(i,S)
%  
%----------------------------------------------------------------------
BEGIN

  ASSUMING
     r,r1,r2,r3 : VAR R
     zero_identity: ASSUMPTION identity?(+)(zero)
     plus_ac:       ASSUMPTION associative?(+) AND commutative?(+)
  ENDASSUMING

  plus_zero_right: LEMMA r + zero = r 
  plus_zero_left : LEMMA zero + r = r
  plus_assoc     : LEMMA (r1 + r2) + r3 = r1 + (r2 + r3) 
  plus_comm      : LEMMA r1 + r2 = r2 + r1

  IMPORTING finite_sets[T], finite_sets_inductions[T]

  f,g: VAR [T -> R]
  S, A, B: VAR finite_set
  x: VAR T

  sum(S,f) : RECURSIVE R = 
    IF (empty?(S)) THEN zero
    ELSE f(choose(S)) + sum(rest(S),f)
    ENDIF MEASURE (LAMBDA S,f: card(S))

  sum_emptyset  : THEOREM sum(emptyset[T],f) = zero

  sum_singleton : THEOREM sum(singleton(x),f) = f(x) + zero ;

  sum_x         : THEOREM (FORALL (x: (S)): 
                              sum(S, f) = f(x) + sum(remove(x, S), f))

  sum_x1_x2     : LEMMA (FORALL (x1,x2: (S)): f(x1) + sum(remove(x1,S),f) 
                              = f(x2) + sum(remove(x2,S),f))

  sum_add       : THEOREM sum(add(x,S),f) 
                          = sum(S,f) + IF member(x,S) THEN zero ELSE f(x) ENDIF

  sum_remove    : THEOREM sum(remove(x,S),f) 
                          + IF member(x,S) THEN f(x) ELSE zero ENDIF = sum(S,f)

  sum_rest      : THEOREM NOT empty?(S) IMPLIES
                            f(choose(S)) + sum(rest(S),f) = sum(S,f)
 
  sum_disj_union: THEOREM disjoint?(A,B) IMPLIES 
                            sum(union(A,B),f) = sum(A,f) + sum(B,f) 

  sum_diff_subset: THEOREM subset?(A, B) IMPLIES 
		            sum(difference(B, A), f) + sum(A, f) = sum(B, f) 

  sum_union      : THEOREM sum(union(A,B),f) + sum(intersection(A,B),f) =
                                         sum(A,f) + sum(B,f) 

  sum_diff_intersection: THEOREM sum(A,f) = 
                            sum(difference(A,B),f) + sum(intersection(A,B),f) 

  sum_f_g         : LEMMA (FORALL (x: (S)): f(x) = g(x)) 
                               IMPLIES sum(S, f) = sum(S, g)

  sum_particular  : THEOREM sum(S,f) = sum(S, f WITH [x := zero])
			       + IF S(x) THEN f(x) ELSE zero ENDIF 

  sum_distributive: THEOREM sum(A,f) + sum(A,g) = 
                                sum(A,(LAMBDA x: f(x) + g(x))) 

END finite_sets_sum

$$$finite_sets_sum.prf
(|finite_sets_sum|
 (|plus_zero_right| "" (SKOSIMP*)
  (("" (LEMMA "zero_identity")
    (("" (EXPAND "identity?") (("" (INST?) (("" (ASSERT) NIL)))))))))
 (|plus_zero_left| "" (SKOSIMP*)
  (("" (LEMMA "zero_identity")
    (("" (EXPAND "identity?") (("" (INST?) (("" (ASSERT) NIL)))))))))
 (|plus_assoc| "" (LEMMA "plus_ac")
  (("" (FLATTEN) (("" (EXPAND "associative?") (("" (PROPAX) NIL)))))))
 (|plus_comm| "" (LEMMA "plus_ac")
  (("" (FLATTEN) (("" (EXPAND "commutative?") (("" (PROPAX) NIL)))))))
 (|sum_TCC1| "" (GRIND) NIL)
 (|sum_TCC2| "" (SKOSIMP*) (("" (REWRITE "card_rest") (("" (ASSERT) NIL)))))
 (|sum_emptyset_TCC1| "" (REWRITE "finite_emptyset") NIL)
 (|sum_emptyset| "" (GRIND) NIL)
 (|sum_singleton_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_singleton") (("" (INST?) NIL)))))
 (|sum_singleton| "" (SKOLEM!)
  (("" (EXPAND "sum")
    (("" (AUTO-REWRITE "choose_singleton[T]" "rest_singleton[T]" "sum_emptyset")
      (("" (SMASH) (("" (GRIND) NIL)))))))))
 (|sum_x| "" (INDUCT "S" :NAME "finite_set_induction_gen")
  (("" (AUTO-REWRITE "card_rest" "card_remove" "nonempty?[T]")
    (("" (SKOSIMP*)
      (("" (EXPAND "sum" 1 1)
        (("" (SMASH)
          (("1" (DELETE -1) (("1" (GRIND :EXCLUDE "sum") NIL)))
           ("2" (INST-CP - "rest(S!1)")
            (("2" (INST - "remove(x!1, S!1)")
              (("2" (ASSERT)
                (("2" (INST - "f!1" "choose(S!1)")
                  (("1" (INST - "f!1" "x!1")
                    (("1"
                      (CASE-REPLACE
                       "remove(choose(S!1), remove(x!1, S!1)) = remove(x!1, rest(S!1))")
                      (("1" (REPLACE*)
                        (("1" (REWRITE "plus_assoc" :DIR RL)
                          (("1" (REWRITE "plus_assoc" :DIR RL)
                            (("1"
                              (LEMMA "plus_comm"
                               ("r1" "f!1(x!1)" "r2" "f!1(choose(S!1))"))
                              (("1" (ASSERT) NIL)))))))))
                       ("2" (DELETE -1 -2 2 3)
                        (("2" (APPLY-EXTENSIONALITY :HIDE? T)
                          (("2" (GRIND :EXCLUDE ("choose")) NIL)))))))
                     ("2" (DELETE -1 2)
                      (("2" (GRIND :EXCLUDE ("sum" "choose")) NIL)))))
                   ("2" (DELETE -1 2)
                    (("2" (GRIND :EXCLUDE ("sum" "choose"))
                      NIL)))))))))))))))))))))
 (|sum_x1_x2| "" (SKOLEM!)
  (("" (REWRITE "sum_x" :DIR RL) (("" (REWRITE "sum_x" :DIR RL) NIL)))))
 (|sum_add| "" (SKOLEM!)
  (("" (SMASH)
    (("1" (REWRITE "member_add") (("1" (REWRITE "plus_zero_right") NIL)))
     ("2" (USE "sum_x" ("S" "add(x!1, S!1)"))
      (("1" (REWRITE "remove_add_member") (("1" (REWRITE "plus_comm") NIL)))
       ("2" (EXPAND "add") (("2" (PROPAX) NIL)))))))))
 (|sum_remove| "" (SKOLEM!)
  (("" (SMASH)
    (("1" (USE "sum_x")
      (("1" (REWRITE "plus_comm") (("1" (ASSERT) NIL)))
       ("2" (EXPAND "member") (("2" (PROPAX) NIL)))))
     ("2" (REWRITE "member_remove") (("2" (REWRITE "plus_zero_right") NIL)))))))
 (|sum_rest| "" (SKOSIMP)
  (("" (ASSERT) (("" (EXPAND "sum" 2 2) (("" (PROPAX) NIL)))))))
 (|sum_disj_union| "" (SKOLEM + ("A!1" _ "f!1"))
  ((""
    (AUTO-REWRITE "union_empty[T]" "sum_emptyset" "sum_add" "plus_zero_left"
                  "plus_zero_right" "plus_assoc" "member")
    (("" (INDUCT "B" :NAME "finite_set_ind_modified")
      (("1" (ASSERT) NIL)
       ("2" (SKOSIMP)
        (("2" (GROUND)
          (("1"
            (CASE-REPLACE "union(A!1, add(e!1, S!1)) = add(e!1, union(A!1, S!1))")
            (("1" (ASSERT)
              (("1" (SMASH)
                (("1" (DELETE -1 -2 2) (("1" (GRIND) NIL)))
                 ("2" (REPLACE -2) (("2" (ASSERT) NIL)))))))
             ("2" (DELETE -1 -2 2 3)
              (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL)))))))
           ("2" (DELETE 2 3)
            (("2" (GRIND :IF-MATCH NIL)
              (("2" (INST?) (("2" (ASSERT) NIL)))))))))))))))))
 (|sum_diff_subset| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "union_diff_subset")
    (("" (USE "sum_disj_union" ("A" "A!1"))
      (("" (REWRITE "difference_disjoint")
        (("" (GROUND)
          (("" (REPLACE*)
            (("" (REWRITE "plus_comm") (("" (ASSERT) NIL)))))))))))))))
 (|sum_union| ""
  (AUTO-REWRITE "union_subset1[T]" "intersection_subset1[T]" "plus_assoc")
  (("" (SKOLEM!)
    (("" (LEMMA "sum_diff_subset" ("f" "f!1"))
      (("" (INST-CP - "A!1" "union(A!1, B!1)")
        (("" (INST - "intersection(A!1, B!1)" "B!1")
          (("" (GROUND)
            (("1" (USE "diff_union_inter")
              (("1" (REWRITE "plus_comm" -2)
                (("1" (REPLACE -2 + RL)
                  (("1" (REPLACE -3 + RL) (("1" (ASSERT) NIL)))))))))
             ("2" (REWRITE "intersection_commutative")
              (("2" (ASSERT) NIL)))))))))))))))
 (|sum_diff_intersection| "" (SKOLEM!)
  ((""
    (AUTO-REWRITE "sum_emptyset" "plus_zero_right" "plus_zero_left" "plus_assoc")
    (("" (REWRITE "sum_union" :DIR RL)
      ((""
        (CASE-REPLACE "union(difference(A!1, B!1), intersection(A!1, B!1)) = A!1")
        (("1"
          (CASE-REPLACE
           "intersection(difference(A!1, B!1), intersection(A!1, B!1)) = emptyset")
          (("1" (ASSERT) NIL)
           ("2" (DELETE -1 2)
            (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL)))))))
         ("2" (DELETE 2)
          (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL)))))))))))))
 (|sum_f_g| "" (AUTO-REWRITE "sum_emptyset" "sum_add" "member")
  (("" (SKOLEM + (_ "f!1" "g!1"))
    (("" (INDUCT "S" :NAME "finite_set_ind_modified")
      (("1" (ASSERT) NIL)
       ("2" (SKOSIMP)
        (("2" (GROUND)
          (("1" (INST?)
            (("1" (ASSERT) NIL) ("2" (EXPAND "add") (("2" (PROPAX) NIL)))))
           ("2" (DELETE 2 3) (("2" (GRIND) NIL)))))))))))))
 (|sum_particular| "" (AUTO-REWRITE "plus_zero_right" "plus_zero_left")
  (("" (SKOLEM!)
    (("" (SMASH)
      (("1" (USE "sum_x")
        (("1" (USE "sum_x" ("f" "f!1 WITH [x!1 := zero]"))
          (("1" (ASSERT)
            (("1" (REWRITE "plus_comm" -2)
              (("1" (USE "sum_f_g" ("S" "remove(x!1, S!1)" "f" "f!1"))
                (("1" (ASSERT)
                  (("1" (DELETE -1 -2 -3 2) (("1" (GRIND) NIL)))))))))))))))
       ("2" (REWRITE "sum_f_g") NIL)))))))
 (|sum_distributive| ""
  (AUTO-REWRITE "sum_emptyset" "sum_add" "plus_zero_right" "plus_zero_left"
                "plus_assoc" "member")
  (("" (SKOLEM + (_ "f!1" "g!1"))
    (("" (INDUCT "A" :NAME "finite_set_ind_modified")
      (("1" (ASSERT) NIL)
       ("2" (SKOSIMP)
        (("2" (ASSERT)
          (("2" (REPLACE -1 + RL)
            (("2"
              (LEMMA "plus_comm"
               ("r1" "f!1(e!1)" "r2" "sum(S!1, g!1) + g!1(e!1)"))
              (("2" (LEMMA "plus_comm" ("r1" "f!1(e!1)" "r2" "g!1(e!1)"))
                (("2" (ASSERT) NIL))))))))))))))))))
$$$nat_fun_props.pvs
nat_fun_props : THEORY
%------------------------------------------------------------------------
%      Author:  Bruno Dutertre 
%
%      Special properties of injective/surgective functions over nats
%------------------------------------------------------------------------

BEGIN

  n, m : VAR nat

  injection_n_to_m : THEOREM
	(EXISTS (f : [below[n] -> below[m]]) : injective?(f)) IMPLIES n <= m

  surjection_n_to_m : THEOREM
	(EXISTS (f : [below[n] -> below[m]]) : surjective?(f)) IMPLIES m <= n

  bijection_n_to_m : THEOREM
	(EXISTS (f : [below[n] -> below[m]]) : bijective?(f)) IFF n = m

END nat_fun_props

$$$nat_fun_props.prf
(|nat_fun_props|
 (|injection_n_to_m| "" (INDUCT "n")
  (("1" (ASSERT) NIL)
   ("2" (SKOSIMP*)
    (("2" (TYPEPRED "f!1(0)")
      (("2" (ASSERT)
        (("2" (HIDE -1)
          (("2" (INST -1 "m!1 - 1")
            (("2" (ASSERT)
              (("2" (DELETE 2)
                (("2"
                  (INST 1
                   "LAMBDA (x : below[j!1]) : IF f!1(x) = m!1 - 1 THEN f!1(j!1) ELSE f!1(x) ENDIF")
                  (("1" (EXPAND "injective?")
                    (("1" (SKOSIMP)
                      (("1" (LIFT-IF)
                        (("1" (LIFT-IF)
                          (("1" (INST-CP -2 "x1!1" "j!1")
                            (("1" (INST-CP -2 "x2!1" "j!1")
                              (("1" (INST -2 "x1!1" "x2!1")
                                (("1" (ASSERT) (("1" (ASSERT) NIL)))))))))))))))))
                   ("2" (SKOSIMP) (("2" (ASSERT) NIL)))
                   ("3" (SKOSIMP)
                    (("3" (EXPAND "injective?")
                      (("3" (INST -2 "x!1" "j!1") (("3" (ASSERT) NIL)))))))))))))))))))))))))
 (|surjection_n_to_m| "" (SKOSIMP*)
  (("" (REWRITE "injection_n_to_m")
    (("" (EXPAND "surjective?")
      (("" (INST -1 "0")
        (("" (SKOSIMP)
          (("" (ASSERT)
            (("" (INST 1 "inverse(f!1)")
              (("1" (REWRITE "inj_inv") (("1" (INST 1 "x!1") NIL)))
               ("2" (INST 1 "x!1") NIL)))))))))))))))
 (|bijection_n_to_m| "" (SKOLEM!)
  (("" (PROP)
    (("1" (EXPAND "bijective?")
      (("1" (SKOSIMP)
        (("1" (LEMMA "injection_n_to_m" ("n" "n!1" "m" "m!1"))
          (("1" (LEMMA "surjection_n_to_m" ("n" "n!1" "m" "m!1"))
            (("1" (SPLIT) (("1" (ASSERT) (("1" (INST?) NIL))) ("2" (INST?) NIL)))))))))))
     ("2" (INST 1 "LAMBDA (x : below[n!1]) : x")
      (("1" (GRIND) NIL) ("2" (SKOLEM!) (("2" (ASSERT) NIL))))))))))
$$$min_nat.pvs
min_nat: THEORY
BEGIN

  S: VAR (nonempty?[nat])
  n,a,x: VAR nat

  min(S): {a: nat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}

  minimum?(a, S) : bool = S(a) AND (FORALL x: S(x) IMPLIES a <= x)

  min_def         : LEMMA min(S) = a IFF minimum?(a, S)

END min_nat

$$$min_nat.prf
(|min_nat|
 (|min_TCC1| ""
  (INST +
   "lambda S : choose({a : nat | S(a) AND (FORALL (x : nat) : S(x) IMPLIES a <= x)})")
  (("" (LEMMA "wf_nat")
    (("" (GRIND :IF-MATCH NIL)
      (("" (INST - "S!1")
        (("" (PROP)
          (("1" (SKOLEM!)
            (("1" (INST -4 "y!1")
              (("1" (ASSERT)
                (("1" (SKOSIMP)
                  (("1" (INST - "x!2") (("1" (ASSERT) NIL)))))))))))
           ("2" (INST?) NIL)))))))))))
 (|min_def| "" (SKOLEM-TYPEPRED)
  (("" (TYPEPRED "min(S!1)")
    (("" (PROP)
      (("1" (EXPAND "minimum?")
        (("1" (ASSERT)
          (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL)))))))))
       ("2" (EXPAND "minimum?")
        (("2" (FLATTEN)
          (("2" (INST -4 "a!1")
            (("2" (ASSERT)
              (("2" (INST -2 "min(S!1)") (("2" (ASSERT) NIL))))))))))))))))))
$$$more_set_lemmas.pvs
more_set_lemmas[T : TYPE] : THEORY
%------------------------------------------------------------------------
%      Author:  Bruno Dutertre 
%------------------------------------------------------------------------
BEGIN

  A, B, C : VAR set[T]
  x : VAR T

  %------------------------------------
  %  Inclusion as an order relation
  %  - empty set is smallest element
  %  - full set is greatest element
  %  - union is upper bound
  %  - intersection is lower bound
  %------------------------------------

  emptyset_min      : LEMMA subset?(A, emptyset) IMPLIES A = emptyset

  fullset_max       : LEMMA subset?(fullset, A)  IMPLIES A = fullset

  union_upper_bound : LEMMA subset?(A, C) and subset?(B, C) IMPLIES 
                                subset?(union(A, B), C)

  intersection_lower_bound : LEMMA subset?(C, A) and subset?(C, B) IMPLIES 
                                subset?(C, intersection(A, B))

  % ---------- More about set operations and inclusion ---------

  difference_subset : LEMMA  subset?(difference(A, B), A)

  remove_subset     : LEMMA  subset?(remove(x, A), A)

  rest_subset       : LEMMA subset?(rest(A), A)

  add_subset        : LEMMA subset?(A, add(x, A))
  
  singleton_subset  : LEMMA member(x, A) IFF subset?(singleton(x), A)

  %  --- Identities: rewrite operations as unions or differences ---

  add_as_union      : LEMMA add(x, A) = union(A, singleton(x))

  remove_as_difference: LEMMA remove(x, A) = difference(A, singleton(x))


  singleton_as_add  : LEMMA singleton(x) = add(x, emptyset[T])

  nonempty_add      : LEMMA NOT empty?(add(x, A))

  remove_member_singleton: LEMMA remove(x, singleton(x)) = emptyset

  % ---------- Operations as disjoint unions ------------

  difference_disjoint: LEMMA disjoint?(A, difference(B, A))
  
  union_difference   : LEMMA union(A, B) = union(A, difference(B, A))

  singleton_disjoint : LEMMA NOT member(x, A) IMPLIES disjoint?(singleton(x), A)


  add_remove_member  : LEMMA member(x, A) IMPLIES add(x, remove(x, A)) = A

  remove_add_member  : LEMMA NOT member(x, A) IMPLIES remove(x, add(x, A)) = A

  union_diff_subset  : LEMMA subset?(A, B) IMPLIES union(A, difference(B, A)) = B

  diff_union_inter   : LEMMA difference(union(A, B), A) 
                                = difference(B, intersection(A, B))

  % ------------ More about disjoint sets ------------

  disjoint_remove_left   : LEMMA disjoint?(A, B) 
                                   IMPLIES disjoint?(remove(x, A), B)

  disjoint_remove_right  : LEMMA	disjoint?(A, B) 
                                   IMPLIES disjoint?(A, remove(x, B))

  union_disj_remove_left : LEMMA disjoint?(A, B) AND A(x) IMPLIES
	                           union(remove(x, A), B) = remove(x, union(A, B))

  union_disj_remove_right: LEMMA disjoint?(A, B) AND B(x) IMPLIES
	                           union(A, remove(x, B)) = remove(x, union(A, B))

END more_set_lemmas

$$$more_set_lemmas.prf
(|more_set_lemmas|
 (|emptyset_min| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|fullset_max| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|union_upper_bound| "" (GRIND) NIL) (|intersection_lower_bound| "" (GRIND) NIL)
 (|difference_subset| "" (GRIND) NIL) (|remove_subset| "" (GRIND) NIL)
 (|rest_subset| "" (GRIND) NIL) (|add_subset| "" (GRIND) NIL) (|singleton_subset| "" (GRIND) NIL)
 (|add_as_union| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|remove_as_difference| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|singleton_as_add| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|nonempty_add| "" (GRIND) NIL)
 (|remove_member_singleton| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|difference_disjoint| "" (GRIND) NIL)
 (|union_difference| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|singleton_disjoint| "" (GRIND) NIL)
 (|add_remove_member| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|remove_add_member| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|union_diff_subset| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|diff_union_inter| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|disjoint_remove_left| "" (GRIND) NIL) (|disjoint_remove_right| "" (GRIND) NIL)
 (|union_disj_remove_left| "" (SKOSIMP) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|union_disj_remove_right| "" (SKOSIMP)
  (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL))))))
$$$finite_sets_def.pvs
finite_sets_def[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
%  finite sets (basic definitions and closure properties)
%  -----------------------------------------------------
%      Authors:  Damir Jamsek
%                Ricky W. Butler
%                Sam Owre
%                C. Michael Holloway
%
%  This theory defines finite sets as the subtype of sets[T] that
%  satisfy the predicate "is_finite".  This predicate states
%  that there is an injective function into below[N] for some N.
%
%------------------------------------------------------------------------

BEGIN

  x, y, z: VAR T
  S: VAR set[T]
  N: VAR nat

  IMPORTING  more_set_lemmas[T]  % For proofs only


  is_finite(S): bool = (EXISTS N, (f: [(S) -> below[N]]):
                          injective?(f)) 

  finite_set: TYPE = (is_finite) CONTAINING emptyset[T]

  non_empty_finite_set: TYPE = {s: finite_set | NOT empty?(s)}


  A,B: VAR finite_set
  

  finite_union:        LEMMA is_finite(union(A,B))
  finite_subset:       LEMMA subset?(S,A) IMPLIES is_finite(S)
  finite_emptyset:     LEMMA is_finite(emptyset[T])
  finite_singleton:    LEMMA is_finite(singleton(x))
  finite_intersection: LEMMA is_finite(intersection(A,B))
  finite_difference:   LEMMA is_finite(difference(A,B))
  finite_add:          LEMMA is_finite(add(x,A))
  finite_remove:       LEMMA is_finite(remove(x,A))
  finite_rest:         LEMMA is_finite(rest(A))

% -------- Judgements --------------------------------------------------

  JUDGEMENT non_empty_finite_set SUBTYPE_OF (nonempty?[T])

  JUDGEMENT singleton HAS_TYPE [T -> finite_set]

  JUDGEMENT union, intersection, difference
    HAS_TYPE [finite_set, finite_set -> finite_set]

  JUDGEMENT union HAS_TYPE
    [non_empty_finite_set, finite_set -> non_empty_finite_set]

  JUDGEMENT union HAS_TYPE
    [finite_set, non_empty_finite_set -> non_empty_finite_set]

  JUDGEMENT union HAS_TYPE
    [non_empty_finite_set, non_empty_finite_set -> non_empty_finite_set]

  JUDGEMENT add HAS_TYPE [T, finite_set -> non_empty_finite_set]

  JUDGEMENT remove HAS_TYPE [T, finite_set -> finite_set]

  JUDGEMENT rest HAS_TYPE [finite_set -> finite_set]

  JUDGEMENT emptyset HAS_TYPE finite_set

  JUDGEMENT singleton HAS_TYPE [T -> non_empty_finite_set]


% -------- Base type is finite -----------------------------------------

  is_finite_type: bool = (EXISTS N, (g:[T -> below[N]]): injective?(g))

  finite_full:         LEMMA is_finite_type IFF is_finite(fullset[T])
  finite_type_set:     LEMMA is_finite_type IMPLIES is_finite(S)
  finite_complement:   LEMMA is_finite_type IMPLIES is_finite(complement(S))

END finite_sets_def

$$$finite_sets_def.prf
(|finite_sets_def|
 (|finite_set_TCC1| "" (EXPAND "emptyset")
  (("" (EXPAND "is_finite")
    (("" (INST 1 "1" "(LAMBDA (x: {t: T | FALSE}): 0)")
      (("" (EXPAND "injective?") (("" (SKOSIMP*) NIL)))))))))
 (|finite_union| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "is_finite")
    (("" (SKOLEM!)
      (("" (SKOLEM!)
        ((""
          (INST 1 "N!1 + N!2"
           "LAMBDA (x : (union(A!1, B!1))) : IF A!1(x) THEN f!1(x) ELSE N!1 + f!2(x) ENDIF")
          (("1" (GRIND) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL)))
           ("3" (DELETE -) (("3" (GRIND) NIL)))
           ("4" (SKOSIMP) (("4" (ASSERT) NIL)))))))))))))
 (|finite_subset| "" (SKOLEM-TYPEPRED)
  (("" (FLATTEN)
    (("" (EXPAND "is_finite")
      (("" (SKOLEM!)
        (("" (INST 1 "N!1" "LAMBDA (x : (S!1)) : f!1(x)")
          (("1" (GRIND) NIL) ("2" (DELETE -1) (("2" (GRIND) NIL)))))))))))))
 (|finite_emptyset| "" (LEMMA "finite_set_TCC1") (("" (PROPAX) NIL)))
 (|finite_singleton| "" (SKOLEM!)
  (("" (EXPAND "is_finite")
    (("" (INST 1 "1" "LAMBDA (x : (singleton(x!1))) : 0")
      (("" (GRIND) NIL)))))))
 (|finite_intersection| "" (SKOLEM!)
  (("" (USE "intersection_subset1[T]")
    (("" (FORWARD-CHAIN "finite_subset") NIL)))))
 (|finite_difference| "" (SKOLEM!)
  (("" (USE "difference_subset[T]")
    (("" (FORWARD-CHAIN "finite_subset") NIL)))))
 (|finite_add| "" (SKOLEM!)
  (("" (REWRITE "add_as_union")
    (("" (REWRITE "finite_union") (("" (REWRITE "finite_singleton") NIL)))))))
 (|finite_remove| "" (SKOLEM!)
  (("" (USE "remove_subset[T]") (("" (FORWARD-CHAIN "finite_subset") NIL)))))
 (|finite_rest| "" (SKOLEM!)
  (("" (USE "rest_subset[T]") (("" (FORWARD-CHAIN "finite_subset") NIL)))))
 (SUBTYPE_TCC1 "" (SUBTYPE-TCC) NIL)
 (|singleton_TCC1| "" (SKOSIMP*) (("" (REWRITE "finite_singleton") NIL)))
 (|union_TCC1| "" (LEMMA "finite_union") (("" (PROPAX) NIL)))
 (|intersection_TCC1| "" (LEMMA "finite_intersection") (("" (PROPAX) NIL)))
 (|difference_TCC1| "" (LEMMA "finite_difference") (("" (PROPAX) NIL)))
 (|union_TCC2| "" (SKOLEM-TYPEPRED) (("" (DELETE -1 -2) (("" (GRIND) NIL)))))
 (|union_TCC3| "" (SUBTYPE-TCC) NIL)
 (|union_TCC4| "" (SKOSIMP*)
  (("" (REWRITE "finite_union")
    (("" (EXPAND "empty?")
      (("" (EXPAND "member")
        (("" (TYPEPRED "x1!1")
          (("" (EXPAND "empty?")
            (("" (SKOSIMP*)
              (("" (EXPAND "member")
                (("" (INST?) (("" (GRIND) NIL)))))))))))))))))))
 (|add_TCC1| "" (SKOLEM!)
  (("" (SPLIT) (("1" (REWRITE "finite_add") NIL) ("2" (GRIND) NIL)))))
 (|remove_TCC1| "" (LEMMA "finite_remove") (("" (GRIND :DEFS NIL) NIL)))
 (|rest_TCC1| "" (LEMMA "finite_rest") (("" (PROPAX) NIL)))
 (|singleton_TCC2| "" (SUBTYPE-TCC) NIL)
 (|finite_full| "" (GRIND)
  (("1" (INST 1 "LAMBDA (x : (fullset[T])): g!1(x)")
    (("1" (SKOSIMP*) (("1" (INST?) (("1" (ASSERT) NIL)))))))
   ("2" (INST 1 "f!1")
    (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL)))))))))
 (|finite_type_set| "" (SKOSIMP)
  (("" (REWRITE "finite_full")
    (("" (USE "subset_fullset" ("a" "S!1"))
      (("" (FORWARD-CHAIN "finite_subset") NIL)))))))
 (|finite_complement| "" (SKOSIMP) (("" (REWRITE "finite_type_set") NIL))))

$$$card_def.pvs
card_def[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
%  Fundamental definition of card
%
%      Authors:  Bruno Dutertre 
%                Ricky W. Butler
%------------------------------------------------------------------------

BEGIN

  IMPORTING finite_sets_def[T],  min_nat,
            nat_fun_props %,  more_function_props   % For proof only

  S, S2: VAR finite_set
  n,m: VAR nat
  x: VAR T
  p : VAR posnat

  inj_set(S): (nonempty?[nat]) = 
                 { n | EXISTS (f : [(S)->below[n]]) : injective?(f) }

  Card(S): nat = min(inj_set(S))

  inj_Card    : LEMMA Card(S) = n IMPLIES 
                          (EXISTS (f : [(S) -> below[n]]) : injective?(f))

  reduce_inj  : LEMMA (FORALL (f : [(S)->below[p]]) :
                          injective?(f) AND NOT surjective?(f) IMPLIES 
                              (EXISTS (g: [(S)->below[p-1]]): injective?(g)))

  Card_injection: LEMMA (EXISTS (f : [(S)->below[n]]) : injective?(f)) 
                            IMPLIES Card(S) <= n
  
  Card_surjection : LEMMA (EXISTS (f : [(S)->below[n]]) : surjective?(f)) 
                              IMPLIES n <= Card(S) 
        
  Card_bijection : THEOREM
        Card(S) = n IFF (EXISTS (f : [(S)->below[n]]) : bijective?(f))

  Card_disj_union: THEOREM disjoint?(S,S2) IMPLIES 
                              Card(union(S,S2)) = Card(S) + Card(S2)

% ------------------------------------------------------------------------
  card(S): {n: nat| n = Card(S)}               % inhibit expansion

  card_def        : THEOREM card(S) = Card(S)  % But if you really need to

END card_def

$$$card_def.prf
(|card_def|
 (|inj_set_TCC1| "" (SKOLEM-TYPEPRED)
  (("" (EXPAND "is_finite")
    (("" (SKOSIMP*)
      (("" (EXPAND "nonempty?")
        (("" (EXPAND "empty?")
          (("" (EXPAND "member") (("" (INST -2 "N!1") (("" (INST?) NIL)))))))))))))))
 (|inj_Card| "" (SKOSIMP)
  (("" (EXPAND "Card")
    (("" (REWRITE "min_def")
      (("" (EXPAND "minimum?")
        (("" (FLATTEN) (("" (EXPAND "inj_set") (("" (PROPAX) NIL)))))))))))))
 (|reduce_inj_TCC1| "" (ASSERT) NIL) (|reduce_inj_TCC2| "" (ASSERT) NIL)
 (|reduce_inj| "" (SKOSIMP)
  (("" (GRIND :IF-MATCH NIL)
    ((""
      (INST 2 "LAMBDA (x : (S!1)) : IF f!1(x) = p!1 - 1 THEN y!1 ELSE f!1(x) ENDIF")
      (("1" (BETA)
        (("1" (SKOSIMP)
          (("1" (INST -2 "x1!1" "x2!1")
            (("1" (LIFT-IF)
              (("1" (LIFT-IF)
                (("1" (ASSERT)
                  (("1" (PROP)
                    (("1" (INST?) NIL)
                     ("2" (INST 3 "x2!1") (("2" (ASSERT) NIL)))))))))))))))))
       ("2" (SKOSIMP) (("2" (ASSERT) NIL)))
       ("3" (SKOSIMP) (("3" (INST 2 "x!1") (("3" (ASSERT) NIL)))))))))))
 (|Card_injection| "" (SKOSIMP*)
  (("" (EXPAND "Card")
    (("" (TYPEPRED "min(inj_set(S!1))")
      (("" (INST?) (("" (ASSERT) (("" (EXPAND "inj_set") (("" (INST?) NIL)))))))))))))
 (|Card_surjection| "" (SKOSIMP*)
  (("" (NAME "CS" "Card(S!1)")
    (("" (REPLACE -1)
      (("" (FORWARD-CHAIN "inj_Card")
        (("" (SKOLEM!)
          (("" (REWRITE "injection_n_to_m")
            (("" (COPY -3)
              (("" (EXPAND "surjective?" -1)
                (("" (INST -1 "0")
                  (("" (SKOSIMP*)
                    (("" (INST 1 "f!2 o inverse(f!1)")
                      (("1" (HIDE -3 2)
                        (("1" (FORWARD-CHAIN "inj_inv[(S!1),below[n!1]]")
                          (("1" (HIDE -4)
                            (("1" (GRIND :IF-MATCH NIL :EXCLUDE INVERSE)
                              (("1"
                                (INST -6 "epsilon! (x: (S!1)): f!1(x) = x1!1"
                                 "epsilon! (x: (S!1)): f!1(x) = x2!1")
                                (("1" (INST -3 "x1!1" "x2!1") (("1" (ASSERT) NIL)))
                                 ("2" (INST 1 "x!1") NIL)))))))
                           ("2" (INST 1 "x!1") NIL)))))
                       ("2" (INST 1 "x!1") NIL)))))))))))))))))))))))
 (|Card_bijection| "" (SKOLEM!)
  (("" (PROP)
    (("1" (FORWARD-CHAIN "inj_Card")
      (("1" (SKOLEM!)
        (("1" (INST?)
          (("1" (EXPAND "bijective?")
            (("1" (ASSERT)
              (("1" (CASE "n!1 = 0")
                (("1" (DELETE -2 -3) (("1" (GRIND) NIL)))
                 ("2" (ASSERT)
                  (("2" (FORWARD-CHAIN "reduce_inj")
                    (("2" (FORWARD-CHAIN "Card_injection")
                      (("2" (ASSERT) NIL)))))))))))))))))))
     ("2" (EXPAND "bijective?")
      (("2" (SKOSIMP)
        (("2" (LEMMA "Card_injection" ("S" "S!1" "n" "n!1"))
          (("2" (SPLIT)
            (("1" (LEMMA "Card_surjection" ("S" "S!1" "n" "n!1"))
              (("1" (GROUND) (("1" (INST?) NIL)))))
             ("2" (INST?) NIL)))))))))))))
 (|Card_disj_union| "" (SKOSIMP)
  (("" (NAME-REPLACE "N1" "Card(S!1)" :HIDE? NIL)
    (("" (NAME-REPLACE "N2" "Card(S2!1)" :HIDE? NIL)
      (("" (AUTO-REWRITE "Card_bijection")
        (("" (DO-REWRITE)
          (("" (SKOSIMP*)
            ((""
              (INST 1
               "LAMBDA (x : (union(S!1, S2!1))) : IF S!1(x) THEN f!2(x) ELSE N1 + f!1(x) ENDIF")
              (("1" (EXPAND "bijective?")
                (("1" (PROP)
                  (("1" (DELETE -2 -4) (("1" (GRIND) NIL)))
                   ("2" (DELETE -1 -3)
                    (("2" (GRIND :IF-MATCH NIL)
                      (("2" (INST -3 "y!1")
                        (("1" (SKOLEM!) (("1" (INST? 1) (("1" (ASSERT) NIL)))))
                         ("2" (ASSERT)
                          (("2" (INST -2 "y!1 - N1")
                            (("2" (SKOLEM!) (("2" (GRIND) NIL)))))))))))))))))
               ("2" (SKOSIMP) (("2" (ASSERT) NIL)))
               ("3" (DELETE -1 -2) (("3" (GRIND) NIL)))
               ("4" (SKOSIMP) (("4" (ASSERT) NIL)))))))))))))))))
 (|card_TCC1| "" (INST 1 "(LAMBDA S: Card(S))") NIL)
 (|card_def| "" (SKOSIMP*) (("" (ASSERT) NIL))))

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

BEGIN

  IMPORTING card_def[T] 

  A, B, S: VAR finite_set
  x: VAR T
  n: VAR nat

  card_emptyset   : THEOREM card(emptyset[T]) = 0

  empty_card      : THEOREM empty?(S) IFF card(S) = 0

  card_empty?     : THEOREM (card(S) = 0) = empty?(S)

  card_is_0       : THEOREM (card(S) = 0) = (S = emptyset)

  nonempty_card   : THEOREM nonempty?(S) IFF card(S) > 0

  card_singleton  : THEOREM card(singleton(x)) = 1

  card_one        : THEOREM card(S) = 1 IFF (EXISTS x : S = singleton(x))

  card_disj_union : THEOREM disjoint?(A,B) IMPLIES 
                              card(union(A,B)) = card(A) + card(B)

  card_diff_subset: THEOREM subset?(A, B) IMPLIES 
                                  card(difference(B, A)) = card(B) - card(A)

  card_subset     : THEOREM subset?(A,B) IMPLIES card(A) <= card(B)

  card_plus       : THEOREM card(A) + card(B) = 
                                card(union(A, B)) + card(intersection(A,B))  

  card_union      : THEOREM card(union(A,B)) = card(A) + card(B) -
                                               card(intersection(A,B))

  card_add        : THEOREM card(add(x, S)) = card(S) 
                                                   + IF S(x) THEN 0 ELSE 1 ENDIF

  card_remove     : THEOREM card(remove(x, S)) = card(S)
                                                   - IF S(x) THEN 1 ELSE 0 ENDIF

  card_rest       : THEOREM NOT empty?(S) IMPLIES card(rest(S)) = card(S) - 1

  same_card_subset: THEOREM subset?(A, B) AND card(A) = card(B) 
                               IMPLIES A = B

  smaller_card_subset : THEOREM subset?(A, B) AND card(A) < card(B) IMPLIES
                                 (EXISTS x : member(x, B) AND NOT member(x, A))

  card_1_has_1    : THEOREM card(S) >= 1 IMPLIES (EXISTS (x: T): S(x))

  card_2_has_2    : THEOREM card(S) >= 2 IMPLIES
                              (EXISTS (x,y: T): x /= y AND S(x) AND S(y))

  card_intersection_le: THEOREM card(intersection(A,B)) <= card(A) AND
                              card(intersection(A,B)) <= card(B)

  N: VAR nat
  card_bij        : THEOREM card(S) = N
                             IFF (EXISTS (f: [(S) -> below[N]]): bijective?(f))

  bij_exists      : COROLLARY (EXISTS (f: [(S) -> below(card(S))]):
                                       bijective?(f))

%  card_n_has_n    : THEOREM card(S) >= n IMPLIES
%                              (EXISTS (X: [below[N] -> T]):
%                                   (FORALL (i: below[N]): S(X(i))) AND
%                                   (FORALL (i,j: below[N]): X(i) /= X(j)))
               
END finite_sets

$$$finite_sets.prf
(|finite_sets|
 (|card_emptyset| "" (REWRITE "card_def")
  (("" (REWRITE "Card_bijection")
    (("" (INST 1 "LAMBDA (x : {x: T | FALSE}) : 0")
      (("1" (EXPAND "bijective?")
        (("1" (PROP)
          (("1" (EXPAND "injective?")
            (("1" (SKOSIMP*)
              (("1" (TYPEPRED "x1!1")
                (("1" (EXPAND "emptyset") (("1" (PROPAX) NIL)))))))))
           ("2" (EXPAND "surjective?") (("2" (SKOSIMP*) NIL)))))))
       ("2" (SKOSIMP*)
        (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL)))))
       ("3" (SKOSIMP*) NIL) ("4" (SKOSIMP*) NIL)))))))
 (|empty_card| "" (SKOLEM!)
  (("" (PROP)
    (("1" (REWRITE "emptyset_is_empty?[T]")
      (("1" (REPLACE -1) (("1" (USE "card_emptyset") NIL)))))
     ("2" (REWRITE "card_def")
      (("2" (REWRITE "Card_bijection")
        (("2" (SKOLEM!)
          (("2" (DELETE -)
            (("2" (GRIND)
              (("2" (TYPEPRED "f!1(x!1)")
                (("2" (PROPAX) NIL)))))))))))))))))
 (|card_empty?| "" (SKOSIMP*) (("" (REWRITE "empty_card") NIL)))
 (|card_is_0| "" (SKOSIMP*)
  (("" (REWRITE "card_empty?")
    (("" (REWRITE "emptyset_is_empty?") NIL)))))
 (|nonempty_card| "" (SKOSIMP)
  (("" (EXPAND "nonempty?")
    (("" (REWRITE "empty_card") (("" (GROUND) NIL)))))))
 (|card_singleton_TCC1| "" (SKOSIMP*)
  (("" (LEMMA "finite_singleton") (("" (INST?) NIL)))))
 (|card_singleton| "" (SKOSIMP*)
  (("" (REWRITE "card_def")
    (("" (REWRITE "Card_bijection")
      (("" (INST 1 "LAMBDA (y : (singleton(x!1))) : 0")
        (("" (GRIND) (("" (INST 1 "x!1") NIL)))))))))))
 (|card_one| "" (SKOSIMP*)
  (("" (REWRITE "card_def")
    (("" (PROP)
      (("1" (REWRITE "Card_bijection")
        (("1" (SKOLEM!)
          (("1" (GRIND :IF-MATCH NIL)
            (("1" (INST -2 "0")
              (("1" (SKOLEM!)
                (("1" (INST? 1)
                  (("1" (APPLY-EXTENSIONALITY :HIDE? T)
                    (("1" (IFF)
                      (("1" (GROUND)
                        (("1" (INST?)
                          (("1" (ASSERT) NIL)))))))))))))))))))))
       ("2" (SKOLEM!)
        (("2" (REPLACE -1)
          (("2" (HIDE -1)
            (("2" (REWRITE "card_def" :DIR RL)
              (("2" (REWRITE "card_singleton") NIL)))))))))))))))
 (|card_disj_union| "" (SKOSIMP*)
  (("" (REWRITE "card_def")
    (("" (REWRITE "card_def")
      (("" (REWRITE "card_def")
        (("" (REWRITE "Card_disj_union") NIL)))))))))
 (|card_diff_subset| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "union_diff_subset")
    (("" (LEMMA "card_disj_union")
      (("" (INST?)
        (("" (ASSERT)
          (("" (REWRITE "difference_disjoint") NIL)))))))))))
 (|card_subset| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "card_diff_subset") (("" (ASSERT) NIL)))))
 (|card_plus| ""
  (AUTO-REWRITE "union_subset1[T]" "intersection_subset1[T]")
  (("" (SKOLEM!)
    (("" (LEMMA "card_diff_subset")
      (("" (INST-CP -1 "A!1" "union(A!1, B!1)")
        (("" (REWRITE "diff_union_inter[T]")
          (("" (INST? -1)
            (("" (GROUND)
              (("" (REWRITE "intersection_commutative" 1)
                (("" (ASSERT) NIL)))))))))))))))))
 (|card_union| "" (SKOSIMP*)
  (("" (LEMMA "card_plus") (("" (INST?) (("" (ASSERT) NIL)))))))
 (|card_add| "" (SKOSIMP*)
  (("" (LIFT-IF)
    (("" (PROP)
      (("1" (REWRITE "member_add")
        (("1" (ASSERT) NIL)
         ("2" (EXPAND "member") (("2" (PROPAX) NIL)))))
       ("2" (REWRITE "add_as_union")
        (("2" (REWRITE "singleton" :DIR RL)
          (("1" (REWRITE "union_commutative")
            (("1" (REWRITE "card_disj_union")
              (("1" (REWRITE "card_singleton")
                (("1" (ASSERT)
                  (("1" (EXPAND "singleton") (("1" (PROPAX) NIL)))))))
               ("2" (REWRITE "singleton_disjoint")
                (("2" (EXPAND "member") (("2" (PROPAX) NIL)))))))))
           ("2" (REWRITE "finite_union") NIL)))))))))))
 (|card_remove| "" (SKOLEM!)
  (("" (LIFT-IF)
    (("" (PROP)
      (("1" (REWRITE "remove_as_difference")
        (("1" (REWRITE "card_diff_subset")
          (("1" (REWRITE "card_singleton") NIL)
           ("2" (LEMMA "singleton_subset")
            (("2" (INST?)
              (("2" (EXPAND "member") (("2" (PROPAX) NIL)))))))))))
       ("2" (REWRITE "member_remove")
        (("1" (ASSERT) NIL)
         ("2" (EXPAND "member") (("2" (PROPAX) NIL)))))))))))
 (|card_rest| "" (SKOSIMP)
  (("" (EXPAND "rest")
    (("" (REWRITE "card_remove")
      (("1" (LEMMA "choose_member[T]")
        (("1" (INST?) (("1" (ASSERT) NIL)))))
       ("2" (EXPAND "nonempty?") (("2" (PROPAX) NIL)))))))))
 (|same_card_subset| "" (SKOSIMP)
  ((""
    (CASE "EXISTS x : member(x, B!1) AND subset?(A!1, remove(x, B!1))")
    (("1" (SKOSIMP)
      (("1" (EXPAND "member")
        (("1" (FORWARD-CHAIN "card_subset")
          (("1" (REWRITE "card_remove") (("1" (ASSERT) NIL)))))))))
     ("2" (APPLY-EXTENSIONALITY :HIDE? T)
      (("2" (GRIND :EXCLUDE "Card" :IF-MATCH NIL)
        (("1" (INST? -) (("1" (ASSERT) NIL)))
         ("2" (INST? +)
          (("2" (ASSERT)
            (("2" (SKOSIMP)
              (("2" (ASSERT)
                (("2" (INST - "x!2")
                  (("2" (ASSERT) NIL)))))))))))))))))))
 (|smaller_card_subset| "" (SKOSIMP)
  (("" (FORWARD-CHAIN "card_subset")
    (("" (CASE-REPLACE "A!1 = B!1")
      (("1" (ASSERT) NIL)
       ("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL)))))))))
 (|card_1_has_1| "" (SKOSIMP*)
  (("" (USE "card_empty?")
    (("" (IFF)
      (("" (FLATTEN)
        (("" (ASSERT)
          (("" (EXPAND "empty?")
            (("" (SKOSIMP*)
              (("" (EXPAND "member") (("" (INST?) NIL)))))))))))))))))
 (|card_2_has_2| "" (SKOSIMP*)
  (("" (LEMMA "card_1_has_1")
    (("" (INST?)
      (("" (ASSERT)
        (("" (SKOSIMP*)
          (("" (LEMMA "card_1_has_1")
            (("" (INST -1 "remove(x!1,S!1)")
              (("" (REWRITE "card_remove")
                (("" (LIFT-IF)
                  (("" (ASSERT)
                    (("" (SKOSIMP*)
                      (("" (EXPAND "remove")
                        (("" (EXPAND "member")
                          (("" (FLATTEN)
                            (("" (INST 2 "x!1" "x!2")
                              ((""
                                (GROUND)
                                NIL)))))))))))))))))))))))))))))))
 (|card_intersection_le| "" (SKOSIMP*)
  ((""
    (CASE "subset?(intersection(A!1, B!1),A!1) AND
             subset?(intersection(A!1, B!1),B!1)")
    (("1" (FLATTEN)
      (("1" (LEMMA "card_subset")
        (("1" (SPLIT 1)
          (("1" (INST -1 "intersection(A!1, B!1)" "A!1")
            (("1" (ASSERT) NIL)))
           ("2" (INST -1 "intersection(A!1, B!1)" "B!1")
            (("2" (ASSERT) NIL)))))))))
     ("2" (HIDE 2)
      (("2" (EXPAND "subset?")
        (("2" (EXPAND "intersection")
          (("2" (EXPAND "member")
            (("2" (SPLIT 1)
              (("1" (SKOSIMP*) NIL) ("2" (SKOSIMP*) NIL)))))))))))))))
 (|card_bij| "" (SKOSIMP*)
  (("" (REWRITE "card_def") (("" (REWRITE "Card_bijection") NIL)))))
 (|bij_exists| "" (SKOSIMP*)
  (("" (LEMMA "card_bij") (("" (INST?) (("" (ASSERT) NIL))))))))