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

Information

name	hol-res-quan
version	1.1
description	HOL theory about restricted quantifiers
author	HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
license	MIT
checksum	f09012313c4018fc861516cbd78a9a7f46157ff7
requires	base hol-base
show	Data.Bool Function HOL4

Files

Package tarball hol-res-quan-1.1.tgz
Theory source file hol-res-quan.thy (included in the package tarball)

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 m₁ m₂.
bool.RES_ABSTRACT p m₁ = bool.RES_ABSTRACT p m₂ ⇔
∀x. bool.IN x p ⇒ m₁ x = m₂ x

⊦ ∀p m₁ m₂.
(∀x. bool.IN x p ⇒ m₁ x = m₂ x) ⇒
bool.RES_ABSTRACT p m₁ = bool.RES_ABSTRACT p m₂

⊦ ∀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

→
bool

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - ⊥
  - ⊤
Function
- id
HOL4
- bool
  - bool.IN
  - bool.RES_ABSTRACT
  - bool.RES_EXISTS
  - bool.RES_EXISTS_UNIQUE
  - bool.RES_FORALL
  - bool.RES_SELECT
- pred_set
  - pred_set.EMPTY
  - pred_set.INSERT
  - pred_set.UNIV

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

⊦ ∀t₁ t₂. t₁ ∧ t₂ ⇔ t₂ ∧ t₁

⊦ ∀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

⊦ (∨) = λt₁ t₂. ∀t. (t₁ ⇒ t) ⇒ (t₂ ⇒ t) ⇒ t

⊦ ∀t₁ t₂. (t₁ ⇒ t₂) ⇒ (t₂ ⇒ t₁) ⇒ (t₁ ⇔ t₂)

⊦ (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 ⇒ ⊥

⊦ ∀t₁ t₂ t₃. t₁ ⇒ t₂ ⇒ t₃ ⇔ t₁ ∧ t₂ ⇒ t₃

⊦ ∀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 m₁ m₂.
    (∀x. bool.IN x p ⇒ m₁ x = m₂ x) ⇒
    bool.RES_ABSTRACT p m₁ = bool.RES_ABSTRACT p m₂