$$$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))))))))