Package bool-class: Classical boolean theorems

Information

name	bool-class
version	1.13
description	Classical boolean theorems
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-12-18
requires	bool-def bool-int axiom-extensionality bool-ext axiom-choice
show	Data.Bool

Files

Package tarball bool-class-1.13.tgz
Theory file bool-class.thy (included in the package tarball)

Theorems

⊦ ∀t. t ∨ ¬t

⊦ (∃) = λp. p ((select) p)

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀x. (select y. y = x) = x

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀t1 t2. (if F then t1 else t2) = t2

⊦ ∀t1 t2. (if T then t1 else t2) = t1

⊦ ∀b t. (if b then t else t) = t

⊦ ∀p. (∀b. p b) ⇔ p T ∧ p F

⊦ ∀p. (∃b. p b) ⇔ p T ∨ p F

⊦ ∀p. p F ∧ p T ⇒ ∀x. p x

⊦ ∀p. (∀x. ¬p x) ⇔ ¬∃x. p x

⊦ ∀p. (∃x. ¬p x) ⇔ ¬∀x. p x

⊦ ∀p. ¬(∀x. p x) ⇔ ∃x. ¬p x

⊦ ∀p. ¬(∃x. p x) ⇔ ∀x. ¬p x

⊦ ∀t1 t2. ¬(t1 ⇒ t2) ⇔ t1 ∧ ¬t2

⊦ ∀t1 t2. (¬t1 ⇔ ¬t2) ⇔ t1 ⇔ t2

⊦ ∀t1 t2. ¬t1 ⇒ ¬t2 ⇔ t2 ⇒ t1

⊦ ∀t1 t2. ¬(t1 ∧ t2) ⇔ ¬t1 ∨ ¬t2

⊦ ∀t1 t2. ¬(t1 ∨ t2) ⇔ ¬t1 ∧ ¬t2

⊦ ∀a b. ∃f. f F = a ∧ f T = b

⊦ ∀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. (∀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. (∀y. p y ⇔ y = x) ⇒ (select) p = x

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

⊦ ∀p. (∀x. ∃!y. p x y) ⇔ ∃!f. ∀x. p x (f x)

⊦ ∀b f g. (λx. if b then f x else g x) = if b then f else g

⊦ ∀b t1 t2. (if b then t1 else t2) ⇔ (¬b ∨ t1) ∧ (b ∨ t2)

⊦ ∀b f x y. f (if b then x else y) = if b then f x else f y

⊦ ∀b f g x. (if b then f else g) x = if b then f x else g x

⊦ ∀p. (∀x. ∃!y. p x y) ⇔ ∃f. ∀x y. p x y ⇔ f x = y

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀b p q r s. (p ⇒ q) ∧ (r ⇒ s) ⇒ (if b then p else r) ⇒ if b then q else s

Input Type Operators

→
bool

Input Constants

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

Assumptions

⊦ T

⊦ ¬F ⇔ T

⊦ ¬T ⇔ F

⊦ ∀t. t ⇒ t

⊦ F ⇔ ∀p. p

⊦ (¬) = λp. p ⇒ F

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

⊦ ∀t. (λx. t x) = t

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

⊦ ∀t. (T ⇔ t) ⇔ t

⊦ ∀t. (t ⇔ T) ⇔ t

⊦ ∀t. F ∧ t ⇔ 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 ∨ T ⇔ T

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

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

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

⊦ ∀p x. p x ⇒ p ((select) p)

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

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

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

⊦ ∀f g. (∀x. f x = g x) ⇔ f = g

⊦ ∀f g. (∀x. f x = g x) ⇒ f = g

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

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

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

⊦ ∀p q. (∀x. p x ∧ q x) ⇔ (∀x. p x) ∧ ∀x. q x

⊦ cond = λt t1 t2. select x. ((t ⇔ T) ⇒ x = t1) ∧ ((t ⇔ F) ⇒ x = t2)

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