| name | natural-cases |
| version | 1.0 |
| description | natural-cases |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2011-02-19 |
| show | Data.Bool |
⊦ ∀m. m = Number.Numeral.zero ∨ ∃n. m = Number.Natural.suc n
⊦ ∀e f.
∃fn.
fn Number.Numeral.zero = e ∧
∀n. fn (Number.Natural.suc n) = f (fn n) n
⊦ ∀e f.
∃fn.
fn Number.Numeral.zero = e ∧
∀n. fn (Number.Natural.suc n) = f n (fn n)
⊦ T
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λP. P = λx. T
⊦ ∀x. x = x ⇔ T
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)
⊦ (¬T ⇔ F) ∧ (¬F ⇔ T)
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀P.
P Number.Numeral.zero ∧ (∀n. P n ⇒ P (Number.Natural.suc n)) ⇒ ∀n. P n
⊦ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)
⊦ (∃!) = λP. (∃) P ∧ ∀x y. P x ∧ P y ⇒ x = y
⊦ ∀e f.
∃!fn.
fn Number.Numeral.zero = e ∧
∀n. fn (Number.Natural.suc n) = f (fn n) n
⊦ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)
⊦ ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)
⊦ ∀t. (T ∨ t ⇔ T) ∧ (t ∨ T ⇔ T) ∧ (F ∨ t ⇔ t) ∧ (t ∨ F ⇔ t) ∧ (t ∨ t ⇔ t)
⊦ ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)