Package hol-res-quan: HOL theory about restricted quantifiers

Information

namehol-res-quan
version1.0
descriptionHOL theory about restricted quantifiers
authorHOL developers <hol-developers@lists.sourceforge.net>
licenseMIT
checksum30f68e14473cd9eaa83a5e3e4e2383aeb463515c
requiresbase
hol-base
showData.Bool
Function
HOL4

Files

Theorems

p. bool.RES_FORALL pred_set.EMPTY p

p. ¬bool.RES_EXISTS pred_set.EMPTY p

p. ¬bool.RES_EXISTS_UNIQUE pred_set.EMPTY p

p. bool.RES_SELECT pred_set.UNIV p = (select) p

p. bool.RES_EXISTS pred_set.UNIV p () p

p. bool.RES_EXISTS_UNIQUE pred_set.UNIV p (∃!) p

p. bool.RES_FORALL pred_set.UNIV p () p

p. bool.RES_SELECT pred_set.EMPTY p = select x.

P j. bool.RES_EXISTS ((=) j) (λx. P x) P j

P j. bool.RES_FORALL ((=) j) (λx. P x) P j

p m. bool.RES_ABSTRACT p (bool.RES_ABSTRACT p m) = bool.RES_ABSTRACT p m

p m. bool.RES_FORALL p (λx. m) p = pred_set.EMPTY m

p m. bool.RES_EXISTS p (λx. m) ¬(p = pred_set.EMPTY) m

P f. bool.RES_SELECT P f = select x. bool.IN x P f x

P f. bool.RES_EXISTS P f x. bool.IN x P f x

P f. bool.RES_FORALL P f x. bool.IN x P f x

p m x. bool.IN x p bool.RES_ABSTRACT p m x = m x

p m.
    bool.RES_EXISTS_UNIQUE p (λx. m)
    (x. p = pred_set.INSERT x pred_set.EMPTY) m

p m.
    bool.RES_EXISTS p m
    bool.IN (bool.RES_SELECT p m) p m (bool.RES_SELECT p m)

P R x.
    (x. bool.RES_FORALL P (λi. R i x)) bool.RES_FORALL P (λi. x. R i x)

p m.
    bool.RES_EXISTS_UNIQUE p m
    bool.RES_EXISTS p (λx. m x bool.RES_FORALL p (λy. m y y = x))

P Q R.
    bool.RES_EXISTS P (λi. bool.RES_EXISTS Q (λx. R i x))
    bool.RES_EXISTS Q (λj. bool.RES_EXISTS P (λi. R i j))

P Q R.
    bool.RES_FORALL P (λi. bool.RES_FORALL Q (λx. R i x))
    bool.RES_FORALL Q (λx. bool.RES_FORALL P (λi. R i x))

p m1 m2.
    bool.RES_ABSTRACT p m1 = bool.RES_ABSTRACT p m2
    x. bool.IN x p m1 x = m2 x

p m1 m2.
    (x. bool.IN x p m1 x = m2 x)
    bool.RES_ABSTRACT p m1 = bool.RES_ABSTRACT p m2

P Q R.
    bool.RES_EXISTS P (λi. Q i R i)
    bool.RES_EXISTS P (λx. Q x) bool.RES_EXISTS P (λi. R i)

P Q R.
    bool.RES_FORALL P (λi. Q i R i)
    bool.RES_FORALL P (λx. Q x) bool.RES_FORALL P (λi. R i)

P Q R.
    bool.RES_EXISTS (λj. P j Q j) (λi. R i)
    bool.RES_EXISTS P (λi. R i) bool.RES_EXISTS Q (λi. R i)

P Q R.
    bool.RES_FORALL (λj. P j Q j) (λi. R i)
    bool.RES_FORALL P (λi. R i) bool.RES_FORALL Q (λi. R i)

P f.
    bool.RES_EXISTS_UNIQUE P f
    bool.RES_EXISTS P (λx. f x)
    bool.RES_FORALL P (λx. bool.RES_FORALL P (λy. f x f y x = y))

External Type Operators

External Constants

Assumptions

x. bool.IN x pred_set.UNIV

t. t

¬¬p p

x. ¬bool.IN x pred_set.EMPTY

x. id x = x

(¬) = λt. t

() = λP. P ((select) P)

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

¬(p q) p

x. x = x

t. ¬¬t t

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

A. A ¬A

t. ¬t t

t. (t ) ¬t

() = λp q. p q p

t. (t ) (t )

P x. bool.IN x P P x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

A B. A B B A

(¬A ) (A )

() = λp q. (λf. f p q) = λf. f

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

x y. bool.IN x (pred_set.INSERT y pred_set.EMPTY) x = y

() = λt1 t2. t. (t1 t) (t2 t) t

t1 t2. (t1 t2) (t2 t1) (t1 t2)

(p ¬q) (p q) (¬q ¬p)

¬(¬A B) A ¬B

P f. bool.RES_SELECT P f = select x. bool.IN x P f x

P f. bool.RES_EXISTS P f x. bool.IN x P f x

P f. bool.RES_FORALL P f x. bool.IN x P f x

P Q. (x. P Q x) P x. Q x

P Q. (x. P Q x) P x. Q x

P Q. P (x. Q x) x. P Q x

P Q. (x. P x Q) (x. P x) Q

P Q. (x. P x) Q x. P x Q

¬(A B) (A ) ¬B

t1 t2 t3. t1 t2 t3 t1 t2 t3

A B C. A B C (A B) C

s t. s = t x. bool.IN x s bool.IN x t

P. (x. y. P x y) f. x. P x (f x)

(t. ¬¬t t) (¬ ) (¬ )

A B C. (B C) A B A C A

(∃!) = λP. () P x y. P x P y x = y

P Q. (j. P j Q j) (x. P x) x. Q x

(p q r) (p q) (p ¬r) (¬q r ¬p)

(p q r) (p ¬q) (p ¬r) (q r ¬p)

P = Q (x. bool.IN x Q (f x g x))
  (bool.RES_FORALL P f bool.RES_FORALL Q g)

x x' y y'. (x x') (x' (y y')) (x y x' y')

(p q r) (p ¬q ¬r) (q ¬p) (r ¬p)

A B. (¬(A B) ¬A ¬B) (¬(A B) ¬A ¬B)

t. (( t) t) ((t ) t) (( t) ¬t) ((t ) ¬t)

P f.
    bool.RES_EXISTS_UNIQUE P f
    bool.RES_EXISTS P (λx. f x)
    bool.RES_FORALL P (λx. bool.RES_FORALL P (λy. f x f y x = y))

t. ( t t) (t t) ( t ) (t ) (t t t)

t. ( t ) (t ) ( t t) (t t) (t t t)

t. ( t t) (t ) ( t ) (t t ) (t ¬t)

(p q r) (p q r) (p ¬r ¬q) (q ¬r ¬p) (r ¬q ¬p)

(p m x. bool.IN x p bool.RES_ABSTRACT p m x = m x)
  p m1 m2.
    (x. bool.IN x p m1 x = m2 x)
    bool.RES_ABSTRACT p m1 = bool.RES_ABSTRACT p m2