Theory "nlist"

Signature

Definitions

listOfN_def

⊢ listOfN = nlistrec [] (λh tn t. h::t)

ncons_def

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

nel_def

⊢ ∀n nlist. nel n nlist = nhd (ndrop n nlist)

nfront_def

⊢ nfront = nlistrec 0 (λh tn rn. if tn = 0 then 0 else ncons h rn)

nhd_def

⊢ ∀nl. nhd nl = nfst (nl − 1)

nlast_def

⊢ nlast = nlistrec 0 (λh tn rn. if tn = 0 then h else rn)

nlist_of_def

⊢ (nlist_of [] = 0) ∧ ∀h t. nlist_of (h::t) = ncons h (nlist_of t)

ntl_def

⊢ ∀nlist. ntl nlist = nsnd (nlist − 1)

Theorems

LENGTH_nfront

⊢ ∀t. t ≠ 0 ⇒ (nlen (nfront t) = nlen t − 1)

MEM_listOfN_LESS

⊢ ∀l e. MEM e (listOfN l) ⇒ e < l

listOfN_EQ_CONS

⊢ (listOfN n = h::t) ⇔ ∃tn. (n = ncons h tn) ∧ (listOfN tn = t)

listOfN_EQ_NIL

⊢ ((listOfN l = []) ⇔ (l = 0)) ∧ (([] = listOfN l) ⇔ (l = 0))

listOfN_INJ

⊢ ∀l1 l2. (listOfN l1 = listOfN l2) ⇔ (l1 = l2)

listOfN_SURJ

⊢ ∀l. ∃n. listOfN n = l

listOfN_ncons

⊢ listOfN (ncons h t) = h::listOfN t

listOfN_nlist

⊢ ∀l. listOfN (nlist_of l) = l

listOfN_zero

⊢ listOfN 0 = []

lt_ncons1

⊢ h < ncons h t

lt_ncons2

⊢ t < ncons h t

napp_ndrop_l1_empty

⊢ ∀l1 l2. ndrop (nlen l1) (napp l1 l2) = l2

napp_nsnoc_lt

⊢ ∀l. l < napp l (ncons x 0)

napp_sing_eq

⊢ (napp l1 (ncons l 0) = ncons x 0) ⇔ (l1 = 0) ∧ (x = l)

ncons_11

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

ncons_nhd_ntl

⊢ ∀l. l ≠ 0 ⇒ (ncons (nhd l) (ntl l) = l)

ncons_not_nnil

⊢ ncons x y ≠ 0

ncons_x_0_LENGTH_1

⊢ (nlen l = 1) ⇔ ∃n. l = ncons n 0

ndrop_SUC

⊢ ∀l n. ndrop (SUC n) l = ntl (ndrop n l)

ndrop_nsingl

⊢ m ≠ 0 ⇒ (ndrop m (ncons x 0) = 0)

nel0_ncons

⊢ nel 0 (ncons h t) = h

nel_SUC_CONS

⊢ ∀n h t. nel (SUC n) (ncons h t) = nel n t

nel_correct

⊢ ∀l i. i < nlen l ⇒ (EL i (listOfN l) = nel i l)

nel_eq_nlist

⊢ ∀l1 l2.
    (l1 = l2) ⇔ (nlen l1 = nlen l2) ∧ ∀m. m < nlen l1 ⇒ (nel m l1 = nel m l2)

nel_napp

⊢ ∀l1 l2. n < nlen l1 ⇒ (nel n (napp l1 l2) = nel n l1)

nel_napp2

⊢ ∀y n x. nlen x ≤ n ⇒ (nel n (napp x y) = nel (n − nlen x) y)

nel_ncons_nonzero

⊢ 0 < n ⇒ (nel n (ncons h t) = nel (n − 1) t)

nel_nfront

⊢ ∀t. m < nlen (nfront t) ⇒ (nel m (nfront t) = nel m t)

nel_nhd

⊢ nel 0 l = nhd l

nel_nnil

⊢ nel x 0 = 0

nfront_napp_sing

⊢ ∀pfx. nfront (napp pfx (ncons e 0)) = pfx

nfront_nnil

⊢ nfront 0 = 0

nfront_nsingl

⊢ nfront (ncons x 0) = 0

nfront_thm

⊢ (nfront 0 = 0) ∧
  (nfront (ncons h t) = if t = 0 then 0 else ncons h (nfront t))

nhd0

⊢ nhd 0 = 0

nhd_napp

⊢ ∀l1 l2. l1 ≠ 0 ⇒ (nhd (napp l1 l2) = nhd l1)

nhd_nfront

⊢ ∀l. l ≠ 0 ∧ ntl l ≠ 0 ⇒ (nhd (nfront l) = nhd l)

nhd_thm

⊢ nhd (ncons h t) = h

nlast_napp

⊢ ∀l1 l2. l2 ≠ 0 ⇒ (nlast (napp l1 l2) = nlast l2)

nlast_ncons

⊢ nlast (ncons h tn) = if tn = 0 then h else nlast tn

nlast_nel

⊢ ∀l. nlast l = nel (nlen l − 1) l

nlast_nnil

⊢ nlast 0 = 0

nlist_cases

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

nlist_ind

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

nlist_listOfN

⊢ ∀l. nlist_of (listOfN l) = l

nlist_of_EQ0

⊢ ((nlist_of l = 0) ⇔ (l = [])) ∧ ((0 = nlist_of l) ⇔ (l = []))

nlist_of_INJ

⊢ ∀n1 n2. (nlist_of n1 = nlist_of n2) ⇔ (n1 = n2)

nlist_of_SURJ

⊢ ∀l. ∃n. nlist_of n = l

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

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

nsnoc_cases

⊢ ∀t. (t = 0) ∨ ∃f l. t = napp f (ncons l 0)

ntl_DROP

⊢ ∀l m. ntl (nlist_of (DROP m l)) = ndrop m (ntl (nlist_of l))

ntl_LE

⊢ ∀n. ntl n ≤ n

ntl_LT

⊢ 0 < n ⇒ ntl n < n

ntl_ndrop

⊢ ∀l. ntl (ndrop n l) = ndrop n (ntl l)

ntl_nonzero_LESS

⊢ ∀n. n ≠ 0 ⇒ ntl n < n

ntl_thm

⊢ ntl (ncons h t) = t

ntl_zero

⊢ ntl 0 = 0

ntl_zero_empty_OR_ncons

⊢ (ntl l = 0) ⇔ (l = 0) ∨ ∃x. l = ncons x 0