Package option-thm: option-thm
Information
| name | option-thm |
| version | 1.10 |
| description | option-thm |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| provenance | HOL Light theory extracted on 2011-09-21 |
| show | Data.Bool |
Files
- Package tarball option-thm-1.10.tgz
- Theory file option-thm.thy (included in the package tarball)
Theorems
⊦ ∀a'. ¬(Data.Option.none = Data.Option.some a')
⊦ ∀x. x = Data.Option.none ∨ ∃a. x = Data.Option.some a
⊦ ∀a a'. Data.Option.some a = Data.Option.some a' ⇔ a = a'
Input Type Operators
- →
- bool
- Data
- Option
- Data.Option.option
- Option
- Number
- Natural
- Number.Natural.natural
- Natural
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- F
- T
- Option
- Data.Option.none
- Data.Option.some
- Bool
- Number
- Natural
- Number.Natural.*
- Number.Natural.+
- Number.Natural.<
- Number.Natural.≤
- Number.Natural.bit0
- Number.Natural.bit1
- Number.Natural.even
- Number.Natural.suc
- Number.Natural.zero
- Natural
Assumptions
⊦ T
⊦ ∀n. Number.Natural.≤ 0 n
⊦ F ⇔ ∀p. p
⊦ (¬) = λp. p ⇒ F
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. T
⊦ ∀x. x = x ⇔ T
⊦ ∀n. ¬(Number.Natural.suc n = 0)
⊦ ∀n. Number.Natural.bit0 n = Number.Natural.+ n n
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀n. Number.Natural.bit1 n = Number.Natural.suc (Number.Natural.+ n n)
⊦ (¬T ⇔ F) ∧ (¬F ⇔ T)
⊦ ∀t1 t2. t1 ∨ t2 ⇔ t2 ∨ t1
⊦ ∀n. Number.Natural.* 2 n = Number.Natural.+ n n
⊦ ∀m n. Number.Natural.≤ (Number.Natural.suc m) n ⇔ Number.Natural.< m n
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀m n. Number.Natural.suc m = Number.Natural.suc n ⇔ m = n
⊦ ∀m n.
Number.Natural.even (Number.Natural.* m n) ⇔
Number.Natural.even m ∨ Number.Natural.even n
⊦ ∀m n.
Number.Natural.even (Number.Natural.+ m n) ⇔ Number.Natural.even m ⇔
Number.Natural.even n
⊦ ∀P. P Data.Option.none ∧ (∀a. P (Data.Option.some a)) ⇒ ∀x. P x
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ (Number.Natural.even 0 ⇔ T) ∧
∀n. Number.Natural.even (Number.Natural.suc n) ⇔ ¬Number.Natural.even n
⊦ ∀m n. Number.Natural.≤ m n ⇔ Number.Natural.< m n ∨ m = n
⊦ ∀m n. Number.Natural.≤ m n ∧ Number.Natural.≤ n m ⇔ m = n
⊦ ∀m n. Number.Natural.* m n = 0 ⇔ m = 0 ∨ n = 0
⊦ ∀NONE' SOME'.
∃fn.
fn Data.Option.none = NONE' ∧ ∀a. fn (Data.Option.some a) = SOME' a
⊦ ∀m n p. Number.Natural.* m n = Number.Natural.* m p ⇔ m = 0 ∨ n = p
⊦ ∀m n p.
Number.Natural.≤ (Number.Natural.* m n) (Number.Natural.* m p) ⇔
m = 0 ∨ Number.Natural.≤ n p
⊦ ∀m n p.
Number.Natural.< (Number.Natural.* m n) (Number.Natural.* m p) ⇔
¬(m = 0) ∧ Number.Natural.< n p
⊦ (∀m. Number.Natural.≤ m 0 ⇔ m = 0) ∧
∀m n.
Number.Natural.≤ m (Number.Natural.suc n) ⇔
m = Number.Natural.suc n ∨ Number.Natural.≤ m 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)
⊦ (∀n. Number.Natural.+ 0 n = n) ∧ (∀m. Number.Natural.+ m 0 = m) ∧
(∀m n.
Number.Natural.+ (Number.Natural.suc m) n =
Number.Natural.suc (Number.Natural.+ m n)) ∧
∀m n.
Number.Natural.+ m (Number.Natural.suc n) =
Number.Natural.suc (Number.Natural.+ m n)