Theory "numpair"

Signature

Definitions

tri_def

⊢ tri 0 = 0 ∧ ∀n. tri (SUC n) = SUC n + tri n

invtri_def

⊢ ∀n. tri⁻¹ n = SND (invtri0 n 0)

npair_def

⊢ ∀m n. m ⊗ n = tri (m + n) + n

nfst_def

⊢ ∀n. nfst n = tri (tri⁻¹ n) + tri⁻¹ n − n

nsnd_def

⊢ ∀n. nsnd n = n − tri (tri⁻¹ n)

ncons_def

⊢ ∀h t. ncons h t = h ⊗ t + 1

nlen_def

⊢ nlen = nlistrec 0 (λn t r. r + 1)

nmap_def

⊢ ∀f. nmap f = nlistrec 0 (λn t r. ncons (f n) r)

nfoldl_def

⊢ ∀f a l. nfoldl f a l = nlistrec (λa. a) (λn t r a. r (f n a)) l a

napp_def

⊢ ∀l1 l2. napp l1 l2 = nlistrec l2 (λn t r. ncons n r) l1

Theorems

tri_def_compute

⊢ tri 0 = 0 ∧
  (∀n. tri (NUMERAL (BIT1 n)) = NUMERAL (BIT1 n) + tri (NUMERAL (BIT1 n) − 1)) ∧
  ∀n. tri (NUMERAL (BIT2 n)) = NUMERAL (BIT2 n) + tri (NUMERAL (BIT1 n))

twotri_formula

⊢ 2 * tri n = n * (n + 1)

tri_formula

⊢ tri n = n * (n + 1) DIV 2

tri_eq_0

⊢ (tri n = 0 ⇔ n = 0) ∧ (0 = tri n ⇔ n = 0)

tri_LT_I

⊢ ∀n m. n < m ⇒ tri n < tri m

tri_LT

⊢ ∀n m. tri n < tri m ⇔ n < m

tri_11

⊢ ∀m n. tri m = tri n ⇔ m = n

tri_LE

⊢ ∀m n. tri m ≤ tri n ⇔ m ≤ n

invtri0_ind

⊢ ∀P. (∀n a. (¬(n < a + 1) ⇒ P (n − (a + 1)) (a + 1)) ⇒ P n a) ⇒ ∀v v1. P v v1

invtri0_def

⊢ ∀n a.
      invtri0 n a = if n < a + 1 then (n,a) else invtri0 (n − (a + 1)) (a + 1)

invtri0_thm

⊢ ∀n a. tri (SND (invtri0 n a)) + FST (invtri0 n a) = n + tri a

SND_invtri0

⊢ ∀n a. FST (invtri0 n a) < SUC (SND (invtri0 n a))

invtri_lower

⊢ tri (tri⁻¹ n) ≤ n

invtri_upper

⊢ n < tri (tri⁻¹ n + 1)

invtri_linverse

⊢ tri⁻¹ (tri n) = n

invtri_unique

⊢ tri y ≤ n ∧ n < tri (y + 1) ⇒ tri⁻¹ n = y

invtri_linverse_r

⊢ y ≤ x ⇒ tri⁻¹ (tri x + y) = x

tri_le

⊢ n ≤ tri n

invtri_le

⊢ tri⁻¹ n ≤ n

nfst_npair

⊢ nfst (x ⊗ y) = x

nsnd_npair

⊢ nsnd (x ⊗ y) = y

npair_cases

⊢ ∀n. ∃x y. n = x ⊗ y

npair

⊢ ∀n. nfst n ⊗ nsnd n = n

npair_11

⊢ x1 ⊗ y1 = x2 ⊗ y2 ⇔ x1 = x2 ∧ y1 = y2

nfst_le

⊢ nfst n ≤ n

nsnd_le

⊢ nsnd n ≤ n

ncons_11

⊢ ncons x y = ncons h t ⇔ x = h ∧ y = t

ncons_not_nnil

⊢ ncons x y ≠ 0

nlistrec_ind

⊢ ∀P. (∀n f l. (l ≠ 0 ⇒ P n f (nsnd (l − 1))) ⇒ P n f l) ⇒ ∀v v1 v2. P v v1 v2

nlistrec_def

⊢ ∀n l f.
      nlistrec n f l = if l = 0 then n
      else f (nfst (l − 1)) (nsnd (l − 1)) (nlistrec n f (nsnd (l − 1)))

nlistrec_thm

⊢ nlistrec n f 0 = n ∧ nlistrec n f (ncons h t) = f h t (nlistrec n f t)

nlist_ind

⊢ ∀P. P 0 ∧ (∀h t. P t ⇒ P (ncons h t)) ⇒ ∀n. P n

nlen_thm

⊢ nlen 0 = 0 ∧ nlen (ncons h t) = nlen t + 1

nmap_thm

⊢ nmap f 0 = 0 ∧ nmap f (ncons h t) = ncons (f h) (nmap f t)

nfoldl_thm

⊢ nfoldl f a 0 = a ∧ nfoldl f a (ncons h t) = nfoldl f (f h a) t

napp_thm

⊢ napp 0 nlist = nlist ∧ napp (ncons h t) nlist = ncons h (napp t nlist)

nlist_cases

⊢ ∀n. n = 0 ∨ ∃h t. n = ncons h t