Theory "pred_set"

Parents option numeral

Signature

Type	Arity
set	1
Constant	Type
partition	:('a -> 'a -> bool) -> ('a -> bool) -> ('a -> bool) -> bool
equiv_on	:('a -> 'a -> bool) -> ('a -> bool) -> bool
count	:num -> num -> bool
UNIV	:'a -> bool
UNION	:('a -> bool) -> ('a -> bool) -> 'a -> bool
SURJ	:('a -> 'b) -> ('a -> bool) -> ('b -> bool) -> bool
SUM_SET	:(num -> bool) -> num
SUM_IMAGE	:('a -> num) -> ('a -> bool) -> num
SUBSET	:('a -> bool) -> ('a -> bool) -> bool
SING	:('a -> bool) -> bool
RINV	:('a -> 'b) -> ('a -> bool) -> 'b -> 'a
REST	:('a -> bool) -> 'a -> bool
PSUBSET	:('a -> bool) -> ('a -> bool) -> bool
POW	:('a -> bool) -> ('a -> bool) -> bool
MIN_SET	:(num -> bool) -> num
MAX_SET	:(num -> bool) -> num
LINV	:('a -> 'b) -> ('a -> bool) -> 'b -> 'a
ITSET_tupled	:('a -> 'b -> 'b) -> ('a -> bool) # 'b -> 'b
ITSET	:('a -> 'b -> 'b) -> ('a -> bool) -> 'b -> 'b
INTER	:('a -> bool) -> ('a -> bool) -> 'a -> bool
INSERT	:'a -> ('a -> bool) -> 'a -> bool
INJ	:('a -> 'b) -> ('a -> bool) -> ('b -> bool) -> bool
INFINITE	:('a -> bool) -> bool
IMAGE	:('a -> 'b) -> ('a -> bool) -> 'b -> bool
GSPEC	:('b -> 'a # bool) -> 'a -> bool
FINITE	:('a -> bool) -> bool
EMPTY	:'a -> bool
DISJOINT	:('a -> bool) -> ('a -> bool) -> bool
DIFF	:('a -> bool) -> ('a -> bool) -> 'a -> bool
DELETE	:('a -> bool) -> 'a -> 'a -> bool
CROSS	:('a -> bool) -> ('b -> bool) -> 'a # 'b -> bool
COMPL	:('a -> bool) -> 'a -> bool
CHOICE	:('a -> bool) -> 'a
CARD	:('a -> bool) -> num
BIJ	:('a -> 'b) -> ('a -> bool) -> ('b -> bool) -> bool
BIGUNION	:(('a -> bool) -> bool) -> 'a -> bool
BIGINTER	:(('a -> bool) -> bool) -> 'a -> bool

Definitions

GSPECIFICATION

|- !f v. v IN GSPEC f = ?x. (v,T) = f x

EMPTY_DEF

|- {} = (\x. F)

UNIV_DEF

|- UNIV = (\x. T)

SUBSET_DEF

|- !s t. s SUBSET t = !x. x IN s ==> x IN t

PSUBSET_DEF

|- !s t. s PSUBSET t = s SUBSET t /\ ~(s = t)

UNION_DEF

|- !s t. s UNION t = {x | x IN s \/ x IN t}

INTER_DEF

|- !s t. s INTER t = {x | x IN s /\ x IN t}

DISJOINT_DEF

|- !s t. DISJOINT s t = (s INTER t = {})

DIFF_DEF

|- !s t. s DIFF t = {x | x IN s /\ ~(x IN t)}

INSERT_DEF

|- !x s. x INSERT s = {y | (y = x) \/ y IN s}

DELETE_DEF

|- !s x. s DELETE x = s DIFF {x}

CHOICE_DEF

|- !s. ~(s = {}) ==> CHOICE s IN s

REST_DEF

|- !s. REST s = s DELETE CHOICE s

SING_DEF

|- !s. SING s = ?x. s = {x}

IMAGE_DEF

|- !f s. IMAGE f s = {f x | x IN s}

INJ_DEF

|- !f s t.
     INJ f s t =
     (!x. x IN s ==> f x IN t) /\
     !x y. x IN s /\ y IN s ==> (f x = f y) ==> (x = y)

SURJ_DEF

|- !f s t.
     SURJ f s t =
     (!x. x IN s ==> f x IN t) /\ !x. x IN t ==> ?y. y IN s /\ (f y = x)

BIJ_DEF

|- !f s t. BIJ f s t = INJ f s t /\ SURJ f s t

LINV_DEF

|- !f s t. INJ f s t ==> !x. x IN s ==> (LINV f s (f x) = x)

RINV_DEF

|- !f s t. SURJ f s t ==> !x. x IN t ==> (f (RINV f s x) = x)

FINITE_DEF

|- !s. FINITE s = !P. P {} /\ (!s. P s ==> !e. P (e INSERT s)) ==> P s

CARD_DEF

|- (CARD {} = 0) /\
   !s.
     FINITE s ==>
     !x. CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD s))

INFINITE_DEF

|- !s. INFINITE s = ~FINITE s

BIGUNION

|- !P. BIGUNION P = {x | ?s. s IN P /\ x IN s}

BIGINTER

|- !P. BIGINTER P = {x | !s. s IN P ==> x IN s}

CROSS_DEF

|- !P Q. P CROSS Q = {p | FST p IN P /\ SND p IN Q}

COMPL_DEF

|- !P. COMPL P = UNIV DIFF P

count_def

|- !n. count n = {m | m < n}

ITSET_tupled_primitive_def

|- !f.
     ITSET_tupled f =
     WFREC
       (@R.
          WF R /\
          !b s. FINITE s /\ ~(s = {}) ==> R (REST s,f (CHOICE s) b) (s,b))
       (\ITSET_tupled a.
          case a of
             (s,b) ->
               I
                 (if FINITE s then
                    (if s = {} then
                       b
                     else
                       ITSET_tupled (REST s,f (CHOICE s) b))
                  else
                    ARB))

ITSET_curried_def

|- !f x x1. ITSET f x x1 = ITSET_tupled f (x,x1)

SUM_IMAGE_DEF

|- !f s. SIGMA f s = ITSET (\e acc. f e + acc) s 0

SUM_SET_DEF

|- SUM_SET = SIGMA I

MAX_SET_DEF

|- !s.
     FINITE s /\ ~(s = {}) ==> MAX_SET s IN s /\ !y. y IN s ==> y <= MAX_SET s

MIN_SET_DEF

|- MIN_SET = $LEAST

POW_DEF

|- !set. POW set = {s | s SUBSET set}

equiv_on_def

|- !R s.
     R equiv_on s =
     (!x. x IN s ==> R x x) /\ (!x y. x IN s /\ y IN s ==> (R x y = R y x)) /\
     !x y z. x IN s /\ y IN s /\ z IN s /\ R x y /\ R y z ==> R x z

partition_def

|- !R s. partition R s = {t | ?x. x IN s /\ (t = {y | y IN s /\ R x y})}

Theorems

SPECIFICATION

|- !P x. x IN P = P x

EXTENSION

|- !s t. (s = t) = !x. x IN s = x IN t

NOT_EQUAL_SETS

|- !s t. ~(s = t) = ?x. x IN t = ~(x IN s)

NUM_SET_WOP

|- !s. (?n. n IN s) = ?n. n IN s /\ !m. m IN s ==> n <= m

SET_MINIMUM

|- !s M. (?x. x IN s) = ?x. x IN s /\ !y. y IN s ==> M x <= M y

NOT_IN_EMPTY

|- !x. ~(x IN {})

MEMBER_NOT_EMPTY

|- !s. (?x. x IN s) = ~(s = {})

IN_UNIV

|- !x. x IN UNIV

UNIV_NOT_EMPTY

|- ~(UNIV = {})

EMPTY_NOT_UNIV

|- ~({} = UNIV)

EQ_UNIV

|- (!x. x IN s) = (s = UNIV)

SUBSET_TRANS

|- !s t u. s SUBSET t /\ t SUBSET u ==> s SUBSET u

SUBSET_REFL

|- !s. s SUBSET s

SUBSET_ANTISYM

|- !s t. s SUBSET t /\ t SUBSET s ==> (s = t)

EMPTY_SUBSET

|- !s. {} SUBSET s

SUBSET_EMPTY

|- !s. s SUBSET {} = (s = {})

SUBSET_UNIV

|- !s. s SUBSET UNIV

UNIV_SUBSET

|- !s. UNIV SUBSET s = (s = UNIV)

PSUBSET_TRANS

|- !s t u. s PSUBSET t /\ t PSUBSET u ==> s PSUBSET u

PSUBSET_IRREFL

|- !s. ~(s PSUBSET s)

NOT_PSUBSET_EMPTY

|- !s. ~(s PSUBSET {})

NOT_UNIV_PSUBSET

|- !s. ~(UNIV PSUBSET s)

PSUBSET_UNIV

|- !s. s PSUBSET UNIV = ?x. ~(x IN s)

IN_UNION

|- !s t x. x IN s UNION t = x IN s \/ x IN t

UNION_ASSOC

|- !s t u. s UNION (t UNION u) = s UNION t UNION u

UNION_IDEMPOT

|- !s. s UNION s = s

UNION_COMM

|- !s t. s UNION t = t UNION s

SUBSET_UNION

|- (!s t. s SUBSET s UNION t) /\ !s t. s SUBSET t UNION s

UNION_SUBSET

|- !s t u. s UNION t SUBSET u = s SUBSET u /\ t SUBSET u

SUBSET_UNION_ABSORPTION

|- !s t. s SUBSET t = (s UNION t = t)

UNION_EMPTY

|- (!s. {} UNION s = s) /\ !s. s UNION {} = s

UNION_UNIV

|- (!s. UNIV UNION s = UNIV) /\ !s. s UNION UNIV = UNIV

EMPTY_UNION

|- !s t. (s UNION t = {}) = (s = {}) /\ (t = {})

IN_INTER

|- !s t x. x IN s INTER t = x IN s /\ x IN t

INTER_ASSOC

|- !s t u. s INTER (t INTER u) = s INTER t INTER u

INTER_IDEMPOT

|- !s. s INTER s = s

INTER_COMM

|- !s t. s INTER t = t INTER s

INTER_SUBSET

|- (!s t. s INTER t SUBSET s) /\ !s t. t INTER s SUBSET s

SUBSET_INTER

|- !s t u. s SUBSET t INTER u = s SUBSET t /\ s SUBSET u

SUBSET_INTER_ABSORPTION

|- !s t. s SUBSET t = (s INTER t = s)

INTER_EMPTY

|- (!s. {} INTER s = {}) /\ !s. s INTER {} = {}

INTER_UNIV

|- (!s. UNIV INTER s = s) /\ !s. s INTER UNIV = s

UNION_OVER_INTER

|- !s t u. s INTER (t UNION u) = s INTER t UNION s INTER u

INTER_OVER_UNION

|- !s t u. s UNION t INTER u = (s UNION t) INTER (s UNION u)

IN_DISJOINT

|- !s t. DISJOINT s t = ~ ?x. x IN s /\ x IN t

DISJOINT_SYM

|- !s t. DISJOINT s t = DISJOINT t s

DISJOINT_EMPTY

|- !s. DISJOINT {} s /\ DISJOINT s {}

DISJOINT_EMPTY_REFL

|- !s. (s = {}) = DISJOINT s s

DISJOINT_EMPTY_REFL_RWT

|- !s. DISJOINT s s = (s = {})

DISJOINT_UNION

|- !s t u. DISJOINT (s UNION t) u = DISJOINT s u /\ DISJOINT t u

DISJOINT_UNION_BOTH

|- !s t u.
     (DISJOINT (s UNION t) u = DISJOINT s u /\ DISJOINT t u) /\
     (DISJOINT u (s UNION t) = DISJOINT s u /\ DISJOINT t u)

DISJOINT_SUBSET

|- !s t u. DISJOINT s t /\ u SUBSET t ==> DISJOINT s u

IN_DIFF

|- !s t x. x IN s DIFF t = x IN s /\ ~(x IN t)

DIFF_EMPTY

|- !s. s DIFF {} = s

EMPTY_DIFF

|- !s. {} DIFF s = {}

DIFF_UNIV

|- !s. s DIFF UNIV = {}

DIFF_DIFF

|- !s t. s DIFF t DIFF t = s DIFF t

DIFF_EQ_EMPTY

|- !s. s DIFF s = {}

DIFF_SUBSET

|- !s t. s DIFF t SUBSET s

IN_INSERT

|- !x y s. x IN y INSERT s = (x = y) \/ x IN s

COMPONENT

|- !x s. x IN x INSERT s

SET_CASES

|- !s. (s = {}) \/ ?x t. (s = x INSERT t) /\ ~(x IN t)

DECOMPOSITION

|- !s x. x IN s = ?t. (s = x INSERT t) /\ ~(x IN t)

ABSORPTION

|- !x s. x IN s = (x INSERT s = s)

INSERT_INSERT

|- !x s. x INSERT x INSERT s = x INSERT s

INSERT_COMM

|- !x y s. x INSERT y INSERT s = y INSERT x INSERT s

INSERT_UNIV

|- !x. x INSERT UNIV = UNIV

NOT_INSERT_EMPTY

|- !x s. ~(x INSERT s = {})

NOT_EMPTY_INSERT

|- !x s. ~({} = x INSERT s)

INSERT_UNION

|- !x s t.
     (x INSERT s) UNION t = (if x IN t then s UNION t else x INSERT s UNION t)

INSERT_UNION_EQ

|- !x s t. (x INSERT s) UNION t = x INSERT s UNION t

INSERT_INTER

|- !x s t.
     (x INSERT s) INTER t = (if x IN t then x INSERT s INTER t else s INTER t)

DISJOINT_INSERT

|- !x s t. DISJOINT (x INSERT s) t = DISJOINT s t /\ ~(x IN t)

INSERT_SUBSET

|- !x s t. x INSERT s SUBSET t = x IN t /\ s SUBSET t

SUBSET_INSERT

|- !x s. ~(x IN s) ==> !t. s SUBSET x INSERT t = s SUBSET t

INSERT_DIFF

|- !s t x.
     (x INSERT s) DIFF t = (if x IN t then s DIFF t else x INSERT s DIFF t)

IN_DELETE

|- !s x y. x IN s DELETE y = x IN s /\ ~(x = y)

DELETE_NON_ELEMENT

|- !x s. ~(x IN s) = (s DELETE x = s)

IN_DELETE_EQ

|- !s x x'. (x IN s = x' IN s) = (x IN s DELETE x' = x' IN s DELETE x)

EMPTY_DELETE

|- !x. {} DELETE x = {}

DELETE_DELETE

|- !x s. s DELETE x DELETE x = s DELETE x

DELETE_COMM

|- !x y s. s DELETE x DELETE y = s DELETE y DELETE x

DELETE_SUBSET

|- !x s. s DELETE x SUBSET s

SUBSET_DELETE

|- !x s t. s SUBSET t DELETE x = ~(x IN s) /\ s SUBSET t

SUBSET_INSERT_DELETE

|- !x s t. s SUBSET x INSERT t = s DELETE x SUBSET t

DIFF_INSERT

|- !s t x. s DIFF (x INSERT t) = s DELETE x DIFF t

PSUBSET_INSERT_SUBSET

|- !s t. s PSUBSET t = ?x. ~(x IN s) /\ x INSERT s SUBSET t

PSUBSET_MEMBER

|- !s t. s PSUBSET t = s SUBSET t /\ ?y. y IN t /\ ~(y IN s)

DELETE_INSERT

|- !x y s.
     (x INSERT s) DELETE y =
     (if x = y then s DELETE y else x INSERT s DELETE y)

INSERT_DELETE

|- !x s. x IN s ==> (x INSERT s DELETE x = s)

DELETE_INTER

|- !s t x. (s DELETE x) INTER t = s INTER t DELETE x

DISJOINT_DELETE_SYM

|- !s t x. DISJOINT (s DELETE x) t = DISJOINT (t DELETE x) s

CHOICE_NOT_IN_REST

|- !s. ~(CHOICE s IN REST s)

CHOICE_INSERT_REST

|- !s. ~(s = {}) ==> (CHOICE s INSERT REST s = s)

REST_SUBSET

|- !s. REST s SUBSET s

REST_PSUBSET

|- !s. ~(s = {}) ==> REST s PSUBSET s

SING

|- !x. SING {x}

IN_SING

|- !x y. x IN {y} = (x = y)

NOT_SING_EMPTY

|- !x. ~({x} = {})

NOT_EMPTY_SING

|- !x. ~({} = {x})

EQUAL_SING

|- !x y. ({x} = {y}) = (x = y)

DISJOINT_SING_EMPTY

|- !x. DISJOINT {x} {}

INSERT_SING_UNION

|- !s x. x INSERT s = {x} UNION s

SING_DELETE

|- !x. {x} DELETE x = {}

DELETE_EQ_SING

|- !s x. x IN s ==> ((s DELETE x = {}) = (s = {x}))

CHOICE_SING

|- !x. CHOICE {x} = x

REST_SING

|- !x. REST {x} = {}

SING_IFF_EMPTY_REST

|- !s. SING s = ~(s = {}) /\ (REST s = {})

IN_IMAGE

|- !y s f. y IN IMAGE f s = ?x. (y = f x) /\ x IN s

IMAGE_IN

|- !x s. x IN s ==> !f. f x IN IMAGE f s

IMAGE_EMPTY

|- !f. IMAGE f {} = {}

IMAGE_ID

|- !s. IMAGE (\x. x) s = s

IMAGE_COMPOSE

|- !f g s. IMAGE (f o g) s = IMAGE f (IMAGE g s)

IMAGE_INSERT

|- !f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s

IMAGE_EQ_EMPTY

|- !s f. (IMAGE f s = {}) = (s = {})

IMAGE_DELETE

|- !f x s. ~(x IN s) ==> (IMAGE f (s DELETE x) = IMAGE f s)

IMAGE_UNION

|- !f s t. IMAGE f (s UNION t) = IMAGE f s UNION IMAGE f t

IMAGE_SUBSET

|- !s t. s SUBSET t ==> !f. IMAGE f s SUBSET IMAGE f t

IMAGE_INTER

|- !f s t. IMAGE f (s INTER t) SUBSET IMAGE f s INTER IMAGE f t

INJ_ID

|- !s. INJ (\x. x) s s

INJ_COMPOSE

|- !f g s t u. INJ f s t /\ INJ g t u ==> INJ (g o f) s u

INJ_EMPTY

|- !f. (!s. INJ f {} s) /\ !s. INJ f s {} = (s = {})

INJ_DELETE

|- !s t f. INJ f s t ==> !e. e IN s ==> INJ f (s DELETE e) (t DELETE f e)

SURJ_ID

|- !s. SURJ (\x. x) s s

SURJ_COMPOSE

|- !f g s t u. SURJ f s t /\ SURJ g t u ==> SURJ (g o f) s u

SURJ_EMPTY

|- !f. (!s. SURJ f {} s = (s = {})) /\ !s. SURJ f s {} = (s = {})

IMAGE_SURJ

|- !f s t. SURJ f s t = (IMAGE f s = t)

BIJ_ID

|- !s. BIJ (\x. x) s s

BIJ_EMPTY

|- !f. (!s. BIJ f {} s = (s = {})) /\ !s. BIJ f s {} = (s = {})

BIJ_COMPOSE

|- !f g s t u. BIJ f s t /\ BIJ g t u ==> BIJ (g o f) s u

BIJ_DELETE

|- !s t f. BIJ f s t ==> !e. e IN s ==> BIJ f (s DELETE e) (t DELETE f e)

BIJ_LINV_INV

|- !f s t. BIJ f s t ==> !x. x IN t ==> (f (LINV f s x) = x)

BIJ_LINV_BIJ

|- !f s t. BIJ f s t ==> BIJ (LINV f s) t s

FINITE_EMPTY

|- FINITE {}

FINITE_INDUCT

|- !P.
     P {} /\ (!s. FINITE s /\ P s ==> !e. ~(e IN s) ==> P (e INSERT s)) ==>
     !s. FINITE s ==> P s

FINITE_INSERT

|- !x s. FINITE (x INSERT s) = FINITE s

FINITE_DELETE

|- !x s. FINITE (s DELETE x) = FINITE s

FINITE_UNION

|- !s t. FINITE (s UNION t) = FINITE s /\ FINITE t

INTER_FINITE

|- !s. FINITE s ==> !t. FINITE (s INTER t)

SUBSET_FINITE

|- !s. FINITE s ==> !t. t SUBSET s ==> FINITE t

PSUBSET_FINITE

|- !s. FINITE s ==> !t. t PSUBSET s ==> FINITE t

FINITE_DIFF

|- !s. FINITE s ==> !t. FINITE (s DIFF t)

FINITE_DIFF_down

|- !P Q. FINITE (P DIFF Q) /\ FINITE Q ==> FINITE P

FINITE_SING

|- !x. FINITE {x}

SING_FINITE

|- !s. SING s ==> FINITE s

IMAGE_FINITE

|- !s. FINITE s ==> !f. FINITE (IMAGE f s)

FINITELY_INJECTIVE_IMAGE_FINITE

|- !f. (!x. FINITE {y | x = f y}) ==> !s. FINITE (IMAGE f s) = FINITE s

INJECTIVE_IMAGE_FINITE

|- !f. (!x y. (f x = f y) = (x = y)) ==> !s. FINITE (IMAGE f s) = FINITE s

FINITE_INJ

|- !f s t. INJ f s t /\ FINITE t ==> FINITE s

CARD_EMPTY

|- CARD {} = 0

CARD_INSERT

|- !s.
     FINITE s ==>
     !x. CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD s))

CARD_EQ_0

|- !s. FINITE s ==> ((CARD s = 0) = (s = {}))

CARD_DELETE

|- !s.
     FINITE s ==>
     !x. CARD (s DELETE x) = (if x IN s then CARD s - 1 else CARD s)

CARD_INTER_LESS_EQ

|- !s. FINITE s ==> !t. CARD (s INTER t) <= CARD s

CARD_UNION

|- !s.
     FINITE s ==>
     !t. FINITE t ==> (CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t)

CARD_SUBSET

|- !s. FINITE s ==> !t. t SUBSET s ==> CARD t <= CARD s

CARD_PSUBSET

|- !s. FINITE s ==> !t. t PSUBSET s ==> CARD t < CARD s

SUBSET_EQ_CARD

|- !s.
     FINITE s ==> !t. FINITE t /\ (CARD s = CARD t) /\ s SUBSET t ==> (s = t)

CARD_SING

|- !x. CARD {x} = 1

SING_IFF_CARD1

|- !s. SING s = (CARD s = 1) /\ FINITE s

CARD_DIFF

|- !t.
     FINITE t ==>
     !s. FINITE s ==> (CARD (s DIFF t) = CARD s - CARD (s INTER t))

LESS_CARD_DIFF

|- !t. FINITE t ==> !s. FINITE s ==> CARD t < CARD s ==> 0 < CARD (s DIFF t)

FINITE_BIJ_CARD_EQ

|- !S. FINITE S ==> !t f. BIJ f S t /\ FINITE t ==> (CARD S = CARD t)

FINITE_COMPLETE_INDUCTION

|- !P.
     (!x. (!y. y PSUBSET x ==> P y) ==> FINITE x ==> P x) ==>
     !x. FINITE x ==> P x

INJ_CARD

|- !f s t. INJ f s t /\ FINITE t ==> CARD s <= CARD t

PHP

|- !f s t. FINITE t /\ CARD t < CARD s ==> ~INJ f s t

NOT_IN_FINITE

|- INFINITE UNIV = !s. FINITE s ==> ?x. ~(x IN s)

INFINITE_INHAB

|- !P. INFINITE P ==> ?x. x IN P

IMAGE_11_INFINITE

|- !f.
     (!x y. (f x = f y) ==> (x = y)) ==>
     !s. INFINITE s ==> INFINITE (IMAGE f s)

INFINITE_SUBSET

|- !s. INFINITE s ==> !t. s SUBSET t ==> INFINITE t

IN_INFINITE_NOT_FINITE

|- !s t. INFINITE s /\ FINITE t ==> ?x. x IN s /\ ~(x IN t)

INFINITE_UNIV

|- INFINITE UNIV = ?f. (!x y. (f x = f y) ==> (x = y)) /\ ?y. !x. ~(f x = y)

FINITE_PSUBSET_INFINITE

|- !s. INFINITE s = !t. FINITE t ==> t SUBSET s ==> t PSUBSET s

FINITE_PSUBSET_UNIV

|- INFINITE UNIV = !s. FINITE s ==> s PSUBSET UNIV

INFINITE_DIFF_FINITE

|- !s t. INFINITE s /\ FINITE t ==> ~(s DIFF t = {})

FINITE_ISO_NUM

|- !s.
     FINITE s ==>
     ?f.
       (!n m. n < CARD s /\ m < CARD s ==> (f n = f m) ==> (n = m)) /\
       (s = {f n | n < CARD s})

FINITE_WEAK_ENUMERATE

|- !s. FINITE s = ?f b. !e. e IN s = ?n. n < b /\ (e = f n)

IN_BIGUNION

|- !x sos. x IN BIGUNION sos = ?s. x IN s /\ s IN sos

BIGUNION_EMPTY

|- BIGUNION {} = {}

BIGUNION_EQ_EMPTY

|- !P.
     ((BIGUNION P = {}) = (P = {}) \/ (P = {{}})) /\
     (({} = BIGUNION P) = (P = {}) \/ (P = {{}}))

BIGUNION_SING

|- !x. BIGUNION {x} = x

BIGUNION_UNION

|- !s1 s2. BIGUNION (s1 UNION s2) = BIGUNION s1 UNION BIGUNION s2

DISJOINT_BIGUNION

|- (!s t. DISJOINT (BIGUNION s) t = !s'. s' IN s ==> DISJOINT s' t) /\
   !s t. DISJOINT t (BIGUNION s) = !s'. s' IN s ==> DISJOINT t s'

BIGUNION_INSERT

|- !s P. BIGUNION (s INSERT P) = s UNION BIGUNION P

BIGUNION_SUBSET

|- !X P. BIGUNION P SUBSET X = !Y. Y IN P ==> Y SUBSET X

FINITE_BIGUNION

|- !P. FINITE P /\ (!s. s IN P ==> FINITE s) ==> FINITE (BIGUNION P)

FINITE_BIGUNION_EQ

|- !P. FINITE (BIGUNION P) = FINITE P /\ !s. s IN P ==> FINITE s

IN_BIGINTER

|- x IN BIGINTER B = !P. P IN B ==> x IN P

BIGINTER_INSERT

|- !P B. BIGINTER (P INSERT B) = P INTER BIGINTER B

BIGINTER_EMPTY

|- BIGINTER {} = UNIV

BIGINTER_INTER

|- !P Q. BIGINTER {P; Q} = P INTER Q

BIGINTER_SING

|- !P. BIGINTER {P} = P

SUBSET_BIGINTER

|- !X P. X SUBSET BIGINTER P = !Y. Y IN P ==> X SUBSET Y

DISJOINT_BIGINTER

|- !X Y P.
     Y IN P /\ DISJOINT Y X ==>
     DISJOINT X (BIGINTER P) /\ DISJOINT (BIGINTER P) X

IN_CROSS

|- !P Q x. x IN P CROSS Q = FST x IN P /\ SND x IN Q

CROSS_EMPTY

|- !P. (P CROSS {} = {}) /\ ({} CROSS P = {})

CROSS_INSERT_LEFT

|- !P Q x. (x INSERT P) CROSS Q = {x} CROSS Q UNION P CROSS Q

CROSS_INSERT_RIGHT

|- !P Q x. P CROSS (x INSERT Q) = P CROSS {x} UNION P CROSS Q

FINITE_CROSS

|- !P Q. FINITE P /\ FINITE Q ==> FINITE (P CROSS Q)

CROSS_SINGS

|- !x y. {x} CROSS {y} = {(x,y)}

CARD_SING_CROSS

|- !x P. FINITE P ==> (CARD ({x} CROSS P) = CARD P)

CARD_CROSS

|- !P Q. FINITE P /\ FINITE Q ==> (CARD (P CROSS Q) = CARD P * CARD Q)

CROSS_SUBSET

|- !P Q P0 Q0.
     P0 CROSS Q0 SUBSET P CROSS Q =
     (P0 = {}) \/ (Q0 = {}) \/ P0 SUBSET P /\ Q0 SUBSET Q

FINITE_CROSS_EQ

|- !P Q. FINITE (P CROSS Q) = (P = {}) \/ (Q = {}) \/ FINITE P /\ FINITE Q

IN_COMPL

|- !x s. x IN COMPL s = ~(x IN s)

COMPL_COMPL

|- !s. COMPL (COMPL s) = s

COMPL_CLAUSES

|- !s. (COMPL s INTER s = {}) /\ (COMPL s UNION s = UNIV)

COMPL_SPLITS

|- !p q. p INTER q UNION COMPL p INTER q = q

INTER_UNION_COMPL

|- !s t. s INTER t = COMPL (COMPL s UNION COMPL t)

COMPL_EMPTY

|- COMPL {} = UNIV

COMPL_INTER

|- (x INTER COMPL x = {}) /\ (COMPL x INTER x = {})

IN_COUNT

|- !m n. m IN count n = m < n

COUNT_ZERO

|- count 0 = {}

COUNT_SUC

|- !n. count (SUC n) = n INSERT count n

FINITE_COUNT

|- !n. FINITE (count n)

CARD_COUNT

|- !n. CARD (count n) = n

ITSET_IND

|- !P.
     (!s b.
        (FINITE s /\ ~(s = {}) ==> P (REST s) (f (CHOICE s) b)) ==> P s b) ==>
     !v v1. P v v1

ITSET_THM

|- !s f b.
     FINITE s ==>
     (ITSET f s b = (if s = {} then b else ITSET f (REST s) (f (CHOICE s) b)))

ITSET_EMPTY

|- !f b. ITSET f {} b = b

ITSET_INSERT

|- !s.
     FINITE s ==>
     !f x b.
       ITSET f (x INSERT s) b =
       ITSET f (REST (x INSERT s)) (f (CHOICE (x INSERT s)) b)

COMMUTING_ITSET_INSERT

|- !f s.
     (!x y z. f x (f y z) = f y (f x z)) /\ FINITE s ==>
     !x b. ITSET f (x INSERT s) b = ITSET f (s DELETE x) (f x b)

COMMUTING_ITSET_RECURSES

|- !f e s b.
     (!x y z. f x (f y z) = f y (f x z)) /\ FINITE s ==>
     (ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b))

SUM_IMAGE_THM

|- !f.
     (SIGMA f {} = 0) /\
     !e s. FINITE s ==> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))

SUM_IMAGE_SING

|- !f e. SIGMA f {e} = f e

SUM_IMAGE_SUBSET_LE

|- !f s t. FINITE s /\ t SUBSET s ==> SIGMA f t <= SIGMA f s

SUM_IMAGE_IN_LE

|- !f s e. FINITE s /\ e IN s ==> f e <= SIGMA f s

SUM_IMAGE_DELETE

|- !f s.
     FINITE s ==>
     !e.
       SIGMA f (s DELETE e) = (if e IN s then SIGMA f s - f e else SIGMA f s)

SUM_IMAGE_UNION

|- !f s t.
     FINITE s /\ FINITE t ==>
     (SIGMA f (s UNION t) = SIGMA f s + SIGMA f t - SIGMA f (s INTER t))

SUM_IMAGE_lower_bound

|- !s. FINITE s ==> !n. (!x. x IN s ==> n <= f x) ==> CARD s * n <= SIGMA f s

SUM_IMAGE_upper_bound

|- !s. FINITE s ==> !n. (!x. x IN s ==> f x <= n) ==> SIGMA f s <= CARD s * n

SUM_SAME_IMAGE

|- !P.
     FINITE P ==>
     !f p.
       p IN P /\ (!q. q IN P ==> (f p = f q)) ==> (SIGMA f P = CARD P * f p)

SUM_SET_THM

|- (SUM_SET {} = 0) /\
   !x s. FINITE s ==> (SUM_SET (x INSERT s) = x + SUM_SET (s DELETE x))

SUM_SET_SING

|- !n. SUM_SET {n} = n

SUM_SET_SUBSET_LE

|- !s t. FINITE t /\ s SUBSET t ==> SUM_SET s <= SUM_SET t

SUM_SET_IN_LE

|- !x s. FINITE s /\ x IN s ==> x <= SUM_SET s

SUM_SET_DELETE

|- !s.
     FINITE s ==>
     !e. SUM_SET (s DELETE e) = (if e IN s then SUM_SET s - e else SUM_SET s)

SUM_SET_UNION

|- !s t.
     FINITE s /\ FINITE t ==>
     (SUM_SET (s UNION t) = SUM_SET s + SUM_SET t - SUM_SET (s INTER t))

MAX_SET_THM

|- (!e. MAX_SET {e} = e) /\
   !s.
     FINITE s ==>
     !e1 e2. MAX_SET (e1 INSERT e2 INSERT s) = MAX e1 (MAX_SET (e2 INSERT s))

MIN_SET_ELIM

|- !P Q.
     ~(P = {}) /\ (!x. (!y. y IN P ==> x <= y) /\ x IN P ==> Q x) ==>
     Q (MIN_SET P)

MIN_SET_THM

|- (!e. MIN_SET {e} = e) /\
   !s e1 e2. MIN_SET (e1 INSERT e2 INSERT s) = MIN e1 (MIN_SET (e2 INSERT s))

MIN_SET_LEM

|- !s. ~(s = {}) ==> MIN_SET s IN s /\ !x. x IN s ==> MIN_SET s <= x

SUBSET_MIN_SET

|- !I J n. ~(I = {}) /\ ~(J = {}) /\ I SUBSET J ==> MIN_SET J <= MIN_SET I

SUBSET_MAX_SET

|- !I J n.
     FINITE I /\ FINITE J /\ ~(I = {}) /\ ~(J = {}) /\ I SUBSET J ==>
     MAX_SET I <= MAX_SET J

MIN_SET_LEQ_MAX_SET

|- !s. ~(s = {}) /\ FINITE s ==> MIN_SET s <= MAX_SET s

MIN_SET_UNION

|- !A B.
     FINITE A /\ FINITE B /\ ~(A = {}) /\ ~(B = {}) ==>
     (MIN_SET (A UNION B) = MIN (MIN_SET A) (MIN_SET B))

MAX_SET_UNION

|- !A B.
     FINITE A /\ FINITE B /\ ~(A = {}) /\ ~(B = {}) ==>
     (MAX_SET (A UNION B) = MAX (MAX_SET A) (MAX_SET B))

IN_POW

|- !set e. e IN POW set = e SUBSET set

SUBSET_POW

|- !s1 s2. s1 SUBSET s2 ==> POW s1 SUBSET POW s2

SUBSET_INSERT_RIGHT

|- !e s1 s2. s1 SUBSET s2 ==> s1 SUBSET e INSERT s2

SUBSET_DELETE_BOTH

|- !s1 s2 x. s1 SUBSET s2 ==> s1 DELETE x SUBSET s2 DELETE x

POW_INSERT

|- !e s. POW (e INSERT s) = IMAGE ($INSERT e) (POW s) UNION POW s

POW_EQNS

|- (POW {} = {{}}) /\
   !e s. POW (e INSERT s) = (let ps = POW s in IMAGE ($INSERT e) ps UNION ps)

FINITE_POW

|- !s. FINITE s ==> FINITE (POW s)

CARD_POW

|- !s. FINITE s ==> (CARD (POW s) = 2 ** CARD s)

GSPEC_F

|- {x | F} = {}

GSPEC_T

|- {x | T} = UNIV

GSPEC_ID

|- {x | x IN y} = y

GSPEC_EQ

|- {x | x = y} = {y}

GSPEC_EQ2

|- {x | y = x} = {y}

GSPEC_F_COND

|- !f. (!x. ~SND (f x)) ==> (GSPEC f = {})

GSPEC_AND

|- !P Q. {x | P x /\ Q x} = {x | P x} INTER {x | Q x}

GSPEC_OR

|- !P Q. {x | P x \/ Q x} = {x | P x} UNION {x | Q x}

BIGUNION_partition

|- R equiv_on s ==> (BIGUNION (partition R s) = s)

EMPTY_NOT_IN_partition

|- R equiv_on s ==> ~({} IN partition R s)

partition_elements_disjoint

|- R equiv_on s ==>
   !t1 t2.
     t1 IN partition R s /\ t2 IN partition R s /\ ~(t1 = t2) ==>
     DISJOINT t1 t2

partition_elements_interrelate

|- R equiv_on s ==>
   !t. t IN partition R s ==> !x y. x IN t /\ y IN t ==> R x y

partition_SUBSET

|- !R s t. R equiv_on s /\ t IN partition R s ==> t SUBSET s

FINITE_partition

|- !R s.
     R equiv_on s /\ FINITE s ==>
     FINITE (partition R s) /\ !t. t IN partition R s ==> FINITE t

partition_CARD

|- !R s. R equiv_on s /\ FINITE s ==> (CARD s = SIGMA CARD (partition R s))

KoenigsLemma

|- !R.
     (!x. FINITE {y | R x y}) ==>
     !x. ~FINITE {y | RTC R x y} ==> ?f. (f 0 = x) /\ !n. R (f n) (f (SUC n))

KoenigsLemma_WF

|- !R. (!x. FINITE {y | R x y}) /\ WF (inv R) ==> !x. FINITE {y | RTC R x y}

SET_EQ_SUBSET

|- !s1 s2. (s1 = s2) = s1 SUBSET s2 /\ s2 SUBSET s1

PSUBSET_EQN

|- !s1 s2. s1 PSUBSET s2 = s1 SUBSET s2 /\ ~(s2 SUBSET s1)

CROSS_EQNS

|- !s1 s2.
     ({} CROSS s2 = {}) /\
     ((a INSERT s1) CROSS s2 = IMAGE (\y. (a,y)) s2 UNION s1 CROSS s2)

count_EQN

|- !n. count n = (if n = 0 then {} else (let p = PRE n in p INSERT count p))