Package bool-int: Intuitionistic boolean theorems

Information

name	bool-int
version	1.10
description	Intuitionistic boolean theorems
author	Joe Hurd <joe@gilith.com>
license	HOLLight
provenance	HOL Light theory extracted on 2011-11-16
requires	bool-def
show	Data.Bool

Files

Package tarball bool-int-1.10.tgz
Theory file bool-int.thy (included in the package tarball)

Theorems

⊦ T

⊦ ¬F ⇔ T

⊦ ¬T ⇔ F

⊦ ∀x. x = x

⊦ ∀t. t ⇒ t

⊦ ∀a. ∃x. x = a

⊦ ∀a. ∃!x. x = a

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀t. (T ⇔ t) ⇔ t

⊦ ∀t. (t ⇔ T) ⇔ t

⊦ ∀t. F ∧ t ⇔ F

⊦ ∀t. T ∧ t ⇔ t

⊦ ∀t. t ∧ F ⇔ F

⊦ ∀t. t ∧ T ⇔ t

⊦ ∀t. t ∧ t ⇔ t

⊦ ∀t. F ⇒ t ⇔ T

⊦ ∀t. T ⇒ t ⇔ t

⊦ ∀t. t ⇒ T ⇔ T

⊦ ∀t. F ∨ t ⇔ t

⊦ ∀t. T ∨ t ⇔ T

⊦ ∀t. t ∨ F ⇔ t

⊦ ∀t. t ∨ T ⇔ T

⊦ ∀t. t ∨ t ⇔ t

⊦ ∀t1 t2. (let x ← t2 in t1) = t1

⊦ ∀t. (F ⇔ t) ⇔ ¬t

⊦ ∀t. (t ⇔ F) ⇔ ¬t

⊦ ∀t. t ⇒ F ⇔ ¬t

⊦ ∀f y. (let x ← y in f x) = f y

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀t1 t2. t1 ∧ t2 ⇔ t2 ∧ t1

⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1

⊦ ∀a b. (a ⇔ b) ⇒ a ⇒ b

⊦ ∀A B. (B ⇒ A) ⇒ ¬A ⇒ ¬B

⊦ ∀P a. (∀x. a = x ⇒ P x) ⇔ P a

⊦ ∀P a. (∀x. x = a ⇒ P x) ⇔ P a

⊦ ∀P a. (∃x. a = x ∧ P x) ⇔ P a

⊦ ∀P a. (∃x. x = a ∧ P x) ⇔ P a

⊦ ∀P Q. (∀x. P ⇒ Q) ⇔ (∃x. P) ⇒ ∀x. Q

⊦ ∀P Q. (∀x. P ∨ Q) ⇔ (∀x. P) ∨ ∀x. Q

⊦ ∀P Q. (∃x. P ∧ Q) ⇔ (∃x. P) ∧ ∃x. Q

⊦ ∀P Q. (∃x. P ⇒ Q) ⇔ (∀x. P) ⇒ ∃x. Q

⊦ ∀P Q. (∃x. P) ∧ (∃x. Q) ⇔ ∃x. P ∧ Q

⊦ ∀P Q. (∀x. P) ∨ (∀x. Q) ⇔ ∀x. P ∨ Q

⊦ ∀P. (∀x y. P x y) ⇔ ∀y x. P x y

⊦ ∀P. (∃x y. P x y) ⇔ ∃y x. P x y

⊦ ∀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. P ∧ (∃x. Q x) ⇔ ∃x. P ∧ Q x

⊦ ∀P Q. P ⇒ (∀x. Q x) ⇔ ∀x. P ⇒ 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

⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q

⊦ ∀P Q. (∃x. P x) ∧ Q ⇔ ∃x. P x ∧ Q

⊦ ∀P Q. (∃x. P x) ⇒ Q ⇔ ∀x. P x ⇒ Q

⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q

⊦ ∀P. (∃!x. P x) ⇔ ∃x. ∀y. P y ⇔ x = y

⊦ ∀x y z. x = y ∧ y = z ⇒ x = z

⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r

⊦ ∀t1 t2 t3. (t1 ∧ t2) ∧ t3 ⇔ t1 ∧ t2 ∧ t3

⊦ ∀t1 t2 t3. (t1 ∨ t2) ∨ t3 ⇔ t1 ∨ t2 ∨ t3

⊦ ∀p q r. p ∧ (q ∨ r) ⇔ p ∧ q ∨ p ∧ r

⊦ ∀p q r. p ⇒ q ∧ r ⇔ (p ⇒ q) ∧ (p ⇒ r)

⊦ ∀p q r. p ∨ q ∧ r ⇔ (p ∨ q) ∧ (p ∨ r)

⊦ ∀p q r. (p ∨ q) ∧ r ⇔ p ∧ r ∨ q ∧ r

⊦ ∀p q r. p ∨ q ⇒ r ⇔ (p ⇒ r) ∧ (q ⇒ r)

⊦ ∀p q r. p ∧ q ∨ r ⇔ (p ∨ r) ∧ (q ∨ r)

⊦ ∀P. (∃!x. P x) ⇔ ∃x. P x ∧ ∀y. P y ⇒ y = x

⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x

⊦ ∀P Q. (∃x. P x ∨ Q x) ⇔ (∃x. P x) ∨ ∃x. Q x

⊦ ∀P Q. (∀x. P x ⇒ Q x) ⇒ (∀x. P x) ⇒ ∀x. Q x

⊦ ∀P Q. (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x

⊦ ∀P Q. (∀x. P x) ∧ (∀x. Q x) ⇔ ∀x. P x ∧ Q x

⊦ ∀P Q. (∃x. P x) ∨ (∃x. Q x) ⇔ ∃x. P x ∨ Q x

⊦ ∀A B C D. (A ⇒ B) ∧ (C ⇒ D) ⇒ A ∧ C ⇒ B ∧ D

⊦ ∀A B C D. (A ⇒ B) ∧ (C ⇒ D) ⇒ A ∨ C ⇒ B ∨ D

⊦ ∀A B C D. (B ⇒ A) ∧ (C ⇒ D) ⇒ (A ⇒ C) ⇒ B ⇒ D

⊦ ∀P. (∃!x. P x) ⇔ (∃x. P x) ∧ ∀x x'. P x ∧ P x' ⇒ x = x'

Input Type Operators

→
bool

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - F
  - T

Assumptions

⊦ F ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ F

⊦ T ⇔ (λp. p) = λp. p

⊦ (∀) = λp. p = λx. T

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ (∧) = λp q. (λf. f p q) = λf. f T T

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ (∃!) = λP. (∃) P ∧ ∀x y. P x ∧ P y ⇒ x = y