Theory: res_quan

Parents

• bool

Types

Constants

• RES_EXISTS  :('a -> bool) -> ('a -> bool) -> bool
• RES_FORALL  :('a -> bool) -> ('a -> bool) -> bool
• RES_SELECT  :('a -> bool) -> ('a -> bool) -> 'a
• RES_ABSTRACT  :('a -> bool) -> ('a -> 'b) -> 'a -> 'b

Definitions

RES_ABSTRACT

|- !P B. RES_ABSTRACT P B = (\x. (if P x then B x else ARB))

RES_EXISTS

|- !P B. RES_EXISTS P B = ?x. P x /\ B x

RES_FORALL

|- !P B. RES_FORALL P B = !x. P x ==> B x

RES_SELECT

|- !P B. RES_SELECT P B = @x. P x /\ B x

Theorems

RESQ_DISJ_EXISTS_DIST

|- !P Q R. (?i::(\i. P i \/ Q i). R i) = (?i::P. R i) \/ ?i::Q. R i

RESQ_EXISTS_DISJ_DIST

|- !P Q R. (?i::P. Q i \/ R i) = (?i::P. Q i) \/ ?i::P. R i

RESQ_EXISTS_REORDER

|- !P Q R. (?(i::P) (j::Q). R i j) = ?(j::Q) (i::P). R i j

RESQ_EXISTS_UNIQUE

|- !P j. (?i::$= j. P i) = P j

RESQ_FORALL_CONJ_DIST

|- !P Q R. (!i::P. Q i /\ R i) = (!i::P. Q i) /\ !i::P. R i

RESQ_FORALL_DISJ_DIST

|- !P Q R. (!i::(\i. P i \/ Q i). R i) = (!i::P. R i) /\ !i::Q. R i

RESQ_FORALL_FORALL

|- !P R x. (!x (i::P). R i x) = !(i::P) x. R i x

RESQ_FORALL_REORDER

|- !P Q R. (!(i::P) (j::Q). R i j) = !(j::Q) (i::P). R i j

RESQ_FORALL_UNIQUE

|- !P j. (!i::$= j. P i) = P j