Theory "numpair"

Parents basicSize while

Signature

Constant	Type
invtri	:num -> num
invtri0	:num -> num -> num # num
invtri0_tupled	:num # num -> num # num
napp	:num -> num -> num
ncons	:num -> num -> num
nfoldl	:(num -> α -> α) -> α -> num -> α
nfst	:num -> num
nlen	:num -> num
nlistrec	:α -> (num -> num -> α -> α) -> num -> α
nlistrec_tupled	:α # (num -> num -> α -> α) # num -> α
nmap	:(num -> num) -> num -> num
npair	:num -> num -> num
nsnd	:num -> num
tri	:num -> num

Definitions

tri_def

|- (tri 0 = 0) ∧ ∀n. tri (SUC n) = SUC n + tri n

invtri0_tupled_primitive_def

|- invtri0_tupled =
   WFREC (@R. WF R ∧ ∀a n. ¬(n < a + 1) ⇒ R (n − (a + 1),a + 1) (n,a))
     (λinvtri0_tupled a'.
        case a' of
          (n,a) =>
            I
              (if n < a + 1 then (n,a)
               else invtri0_tupled (n − (a + 1),a + 1)))

invtri0_curried_def

|- ∀x x1. invtri0 x x1 = invtri0_tupled (x,x1)

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

nlistrec_tupled_primitive_def

|- nlistrec_tupled =
   WFREC (@R. WF R ∧ ∀f n l. l ≠ 0 ⇒ R (n,f,nsnd (l − 1)) (n,f,l))
     (λnlistrec_tupled a.
        case a of
          (n,f,l) =>
            I
              (if l = 0 then n
               else
                 f (nfst (l − 1)) (nsnd (l − 1))
                   (nlistrec_tupled (n,f,nsnd (l − 1)))))

nlistrec_curried_def

|- ∀x x1 x2. nlistrec x x1 x2 = nlistrec_tupled (x,x1,x2)

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_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