Theory: pred_set

Parents

• option
• numeral
• pair

Types

Constants

• CROSS  :('a -> bool) -> ('b -> bool) -> 'a # 'b -> bool
• BIGUNION  :(('a -> bool) -> bool) -> 'a -> bool
• EMPTY  :'a -> bool
• UNION  :('a -> bool) -> ('a -> bool) -> 'a -> bool
• IN  :'a -> ('a -> bool) -> bool
• LINV  :('a -> 'b) -> ('a -> bool) -> 'b -> 'a
• DISJOINT  :('a -> bool) -> ('a -> bool) -> bool
• PSUBSET  :('a -> bool) -> ('a -> bool) -> bool
• SUBSET  :('a -> bool) -> ('a -> bool) -> bool
• REST  :('a -> bool) -> 'a -> bool
• RINV  :('a -> 'b) -> ('a -> bool) -> 'b -> 'a
• SING  :('a -> bool) -> bool
• FINITE  :('a -> bool) -> bool
• IMAGE  :('a -> 'b) -> ('a -> bool) -> 'b -> bool
• UNIV  :'a -> bool
• SURJ  :('a -> 'b) -> ('a -> bool) -> ('b -> bool) -> bool
• GSPEC  :('b -> 'a # bool) -> 'a -> bool
• INFINITE  :('a -> bool) -> bool
• ITSET_tupled  :('a -> 'b -> 'b) -> ('a -> bool) # 'b -> 'b
• INTER  :('a -> bool) -> ('a -> bool) -> 'a -> bool
• BIJ  :('a -> 'b) -> ('a -> bool) -> ('b -> bool) -> bool
• INJ  :('a -> 'b) -> ('a -> bool) -> ('b -> bool) -> bool
• INSERT  :'a -> ('a -> bool) -> 'a -> bool
• CHOICE  :('a -> bool) -> 'a
• DELETE  :('a -> bool) -> 'a -> 'a -> bool
• CARD  :('a -> bool) -> num
• ITSET  :('a -> 'b -> 'b) -> ('a -> bool) -> 'b -> 'b
• DIFF  :('a -> bool) -> ('a -> bool) -> 'a -> bool

Definitions

BIGUNION

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

BIJ_DEF

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

CARD_DEF

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

CHOICE_DEF

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

CROSS_DEF

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

DELETE_DEF

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

DIFF_DEF

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

DISJOINT_DEF

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

EMPTY_DEF

|- {} = (\x. F)

FINITE_DEF

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

GSPECIFICATION

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

IMAGE_DEF

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

INFINITE_DEF

|- !s. INFINITE s = ~FINITE 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)

INSERT_DEF

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

INTER_DEF

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

ITSET_arg_munge_def

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

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.
          pair_case
            (\v v1.
               (if FINITE v then
                  (if v = {} then
                     v1
                   else
                     ITSET_tupled' (REST v,f (CHOICE v) v1))
                else
                  ARB)) a)

LINV_DEF

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

PSUBSET_DEF

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

REST_DEF

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

RINV_DEF

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

SING_DEF

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

SPECIFICATION

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

SUBSET_DEF

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

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)

UNION_DEF

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

UNIV_DEF

|- UNIV = (\x. T)

Theorems

ABSORPTION

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

BIGUNION_EMPTY

|- BIGUNION {} = {}

BIGUNION_INSERT

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

BIGUNION_SING

|- !x. BIGUNION {x} = x

BIGUNION_UNION

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

BIJ_COMPOSE

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

BIJ_EMPTY

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

BIJ_ID

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

CARD_CROSS

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

CARD_DELETE

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

CARD_DIFF

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

CARD_EMPTY

|- CARD {} = 0

CARD_EQ_0

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

CARD_INSERT

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

CARD_INTER_LESS_EQ

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

CARD_PSUBSET

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

CARD_SING

|- !x. CARD {x} = 1

CARD_SING_CROSS

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

CARD_SUBSET

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

CARD_UNION

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

CHOICE_INSERT_REST

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

CHOICE_NOT_IN_REST

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

CHOICE_SING

|- !x. CHOICE {x} = x

COMPONENT

|- !x s. x IN x INSERT s

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

CROSS_SINGS

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

CROSS_SUBSET

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

DECOMPOSITION

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

DELETE_COMM

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

DELETE_DELETE

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

DELETE_EQ_SING

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

DELETE_INSERT

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

DELETE_INTER

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

DELETE_NON_ELEMENT

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

DELETE_SUBSET

|- !x s. s DELETE x SUBSET s

DIFF_DIFF

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

DIFF_EMPTY

|- !s. s DIFF {} = s

DIFF_EQ_EMPTY

|- !s. s DIFF s = {}

DIFF_INSERT

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

DIFF_UNIV

|- !s. s DIFF UNIV = {}

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'

DISJOINT_DELETE_SYM

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

DISJOINT_EMPTY

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

DISJOINT_EMPTY_REFL

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

DISJOINT_INSERT

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

DISJOINT_SING_EMPTY

|- !x. DISJOINT {x} {}

DISJOINT_SYM

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

DISJOINT_UNION

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

EMPTY_DELETE

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

EMPTY_DIFF

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

EMPTY_NOT_UNIV

|- ~({} = UNIV)

EMPTY_SUBSET

|- !s. {} SUBSET s

EMPTY_UNION

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

EQ_UNIV

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

EQUAL_SING

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

EXTENSION

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

FINITE_BIGUNION

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

FINITE_COMPLETE_INDUCTION

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

FINITE_CROSS

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

FINITE_CROSS_EQ

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

FINITE_DELETE

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

FINITE_DIFF

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

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_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_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

FINITE_SING

|- !x. FINITE {x}

FINITE_UNION

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

FINITE_WEAK_ENUMERATE

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

IMAGE_11_INFINITE

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

IMAGE_COMPOSE

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

IMAGE_DELETE

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

IMAGE_EMPTY

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

IMAGE_EQ_EMPTY

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

IMAGE_FINITE

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

IMAGE_ID

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

IMAGE_IN

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

IMAGE_INSERT

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

IMAGE_INTER

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

IMAGE_SUBSET

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

IMAGE_SURJ

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

IMAGE_UNION

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

IN_BIGUNION

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

IN_CROSS

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

IN_DELETE

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

IN_DELETE_EQ

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

IN_DIFF

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

IN_DISJOINT

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

IN_IMAGE

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

IN_INFINITE_NOT_FINITE

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

IN_INSERT

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

IN_INTER

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

IN_SING

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

IN_UNION

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

IN_UNIV

|- !x. x IN UNIV

INFINITE_DIFF_FINITE

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

INFINITE_INHAB

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

INFINITE_SUBSET

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

INFINITE_UNIV

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

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_ID

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

INSERT_COMM

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

INSERT_DELETE

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

INSERT_DIFF

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

INSERT_INSERT

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

INSERT_INTER

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

INSERT_SING_UNION

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

INSERT_SUBSET

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

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_UNIV

|- !x. x INSERT UNIV = UNIV

INTER_ASSOC

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

INTER_COMM

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

INTER_EMPTY

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

INTER_FINITE

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

INTER_IDEMPOT

|- !s. s INTER s = s

INTER_OVER_UNION

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

INTER_SUBSET

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

INTER_UNIV

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

ITSET_EMPTY

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

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

LESS_CARD_DIFF

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

MEMBER_NOT_EMPTY

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

NOT_EMPTY_INSERT

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

NOT_EMPTY_SING

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

NOT_EQUAL_SETS

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

NOT_IN_EMPTY

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

NOT_IN_FINITE

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

NOT_INSERT_EMPTY

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

NOT_PSUBSET_EMPTY

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

NOT_SING_EMPTY

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

NOT_UNIV_PSUBSET

|- !s. ~(UNIV PSUBSET s)

NUM_SET_WOP

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

PSUBSET_FINITE

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

PSUBSET_INSERT_SUBSET

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

PSUBSET_IRREFL

|- !s. ~(s PSUBSET s)

PSUBSET_MEMBER

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

PSUBSET_TRANS

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

PSUBSET_UNIV

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

REST_PSUBSET

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

REST_SING

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

REST_SUBSET

|- !s. REST s SUBSET s

SET_CASES

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

SET_MINIMUM

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

SING

|- !x. SING {x}

SING_DELETE

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

SING_FINITE

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

SING_IFF_CARD1

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

SING_IFF_EMPTY_REST

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

SUBSET_ANTISYM

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

SUBSET_DELETE

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

SUBSET_EMPTY

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

SUBSET_FINITE

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

SUBSET_INSERT

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

SUBSET_INSERT_DELETE

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

SUBSET_INTER_ABSORPTION

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

SUBSET_REFL

|- !s. s SUBSET s

SUBSET_TRANS

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

SUBSET_UNION

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

SUBSET_UNION_ABSORPTION

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

SUBSET_UNIV

|- !s. s SUBSET UNIV

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 = {})

SURJ_ID

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

UNION_ASSOC

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

UNION_COMM

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

UNION_EMPTY

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

UNION_IDEMPOT

|- !s. s UNION s = s

UNION_OVER_INTER

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

UNION_UNIV

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

UNIV_NOT_EMPTY

|- ~(UNIV = {})

UNIV_SUBSET

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