Package natural-order: Natural number orderings

Information

name	natural-order
version	1.45
description	Natural number orderings
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
requires	bool natural-def natural-thm
show	Data.Bool Number.Natural

Files

Package tarball natural-order-1.45.tgz
Theory source file natural-order.thy (included in the package tarball)

Defined Constants

Number
- Natural
  - <
  - ≤
  - >
  - ≥
  - max
  - min
  - minimal

Theorems

⊦ ∀n. 0 ≤ n

⊦ ∀n. n ≤ n

⊦ (minimal n. ⊤) = 0

⊦ ∀m. ¬(m < 0)

⊦ ∀n. ¬(n < n)

⊦ ∀n. 0 < suc n

⊦ ∀n. n < suc n

⊦ ∀n. n ≤ suc n

⊦ ∀n. max 0 n = n

⊦ ∀n. max n 0 = n

⊦ ∀n. max n n = n

⊦ ∀n. min 0 n = 0

⊦ ∀n. min n 0 = 0

⊦ ∀n. min n n = n

⊦ ∀m n. m ≤ max m n

⊦ ∀m n. n ≤ max m n

⊦ ∀m n. min m n ≤ m

⊦ ∀m n. min m n ≤ n

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀n. 0 < n ⇔ ¬(n = 0)

⊦ ∀m n. m > n ⇔ n < m

⊦ ∀m n. m ≥ n ⇔ n ≤ m

⊦ ∀m n. max m n = max n m

⊦ ∀m n. min m n = min n m

⊦ ∀m n. m = n ⇒ m ≤ n

⊦ ∀m n. m < n ⇒ m ≤ n

⊦ ∀m n. m < n ∨ n ≤ m

⊦ ∀m n. m ≤ n ∨ n < m

⊦ ∀m n. m ≤ n ∨ n ≤ m

⊦ ∀m n. ¬(m < n ∧ n < m)

⊦ ∀m n. ¬(m < n ∧ n ≤ m)

⊦ ∀m n. ¬(m ≤ n ∧ n < m)

⊦ ∀m n. m < n ⇒ ¬(m = n)

⊦ ∀m n. ¬(m < n) ⇔ n ≤ m

⊦ ∀m n. ¬(m ≤ n) ⇔ n < m

⊦ ∀m n. m < suc n ⇔ m ≤ n

⊦ ∀m n. suc m ≤ n ⇔ m < n

⊦ ∀m n. suc m < suc n ⇔ m < n

⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n

⊦ ∀m n. max m n = if m ≤ n then n else m

⊦ ∀m n. min m n = if m ≤ n then m else n

⊦ ∀m n. max (suc m) (suc n) = suc (max m n)

⊦ ∀m n. min (suc m) (suc n) = suc (min m n)

⊦ ∀m n. m ≤ n ⇔ m < n ∨ m = n

⊦ ∀m n. m < n ∨ n < m ∨ m = n

⊦ ∀m n. m ≤ n ∧ n ≤ m ⇔ m = n

⊦ ∀m n. m < n ⇔ m ≤ n ∧ ¬(m = n)

⊦ ∀m n. m < suc n ⇔ m = n ∨ m < n

⊦ ∀m n p. m < n ∧ n < p ⇒ m < p

⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n < p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n

⊦ ∀m n p. m ≤ min n p ⇔ m ≤ n ∧ m ≤ p

⊦ ∀m n p. max n p ≤ m ⇔ n ≤ m ∧ p ≤ m

⊦ ∀p. (∀n. (∀m. m < n ⇒ p m) ⇒ p n) ⇒ ∀n. p n

⊦ ∀p. (∃n. p n) ⇔ ∃n. p n ∧ ∀m. m < n ⇒ ¬p m

⊦ ∀p n. p n ∧ (∀m. m < n ⇒ ¬p m) ⇒ (minimal) p = n

⊦ ∀p. (∃n. p n) ⇔ p ((minimal) p) ∧ ∀m. m < (minimal) p ⇒ ¬p m

⊦ ∀p. (∃n. p n) ∧ (∃m. ∀n. p n ⇒ n ≤ m) ⇔ ∃m. p m ∧ ∀n. p n ⇒ n ≤ m

External Type Operators

→
bool
Number
- Natural
  - natural

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
Number
- Natural
  - suc
  - zero

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ ∀t. t ⇒ t

⊦ ⊥ ⇔ ∀p. p

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

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

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

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

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

⊦ ∀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. t ⇒ ⊤ ⇔ ⊤

⊦ ∀t. ⊥ ∨ t ⇔ t

⊦ ∀t. ⊤ ∨ t ⇔ ⊤

⊦ ∀t. t ∨ ⊥ ⇔ t

⊦ ∀t. t ∨ ⊤ ⇔ ⊤

⊦ ∀t. t ∨ t ⇔ t

⊦ ∀n. ¬(suc n = 0)

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

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

⊦ ∀t. t ⇒ ⊥ ⇔ ¬t

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

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

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

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

⊦ ∀t₁ t₂. t₁ ∨ t₂ ⇔ t₂ ∨ t₁

⊦ (∧) = λ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

⊦ ∀t₁ t₂. ¬t₁ ⇒ ¬t₂ ⇔ t₂ ⇒ t₁

⊦ ∀m n. suc m = suc n ⇔ m = n

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

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

⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

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

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

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n

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