Structure nlistTheory

signature nlistTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val listOfN_def : thm
    val ncons_def : thm
    val nel_def : thm
    val nfront_def : thm
    val nhd_def : thm
    val nlast_def : thm
    val nlist_of_def : thm
    val ntl_def : thm
  
  (*  Theorems  *)
    val LENGTH_nfront : thm
    val MEM_listOfN_LESS : thm
    val listOfN_EQ_CONS : thm
    val listOfN_EQ_NIL : thm
    val listOfN_INJ : thm
    val listOfN_SURJ : thm
    val listOfN_ncons : thm
    val listOfN_nlist : thm
    val listOfN_zero : thm
    val lt_ncons1 : thm
    val lt_ncons2 : thm
    val napp_ndrop_l1_empty : thm
    val napp_nsnoc_lt : thm
    val napp_sing_eq : thm
    val ncons_11 : thm
    val ncons_nhd_ntl : thm
    val ncons_not_nnil : thm
    val ncons_x_0_LENGTH_1 : thm
    val ndrop_SUC : thm
    val ndrop_nsingl : thm
    val nel0_ncons : thm
    val nel_SUC_CONS : thm
    val nel_correct : thm
    val nel_eq_nlist : thm
    val nel_napp : thm
    val nel_napp2 : thm
    val nel_ncons_nonzero : thm
    val nel_nfront : thm
    val nel_nhd : thm
    val nel_nnil : thm
    val nfront_napp_sing : thm
    val nfront_nnil : thm
    val nfront_nsingl : thm
    val nfront_thm : thm
    val nhd0 : thm
    val nhd_napp : thm
    val nhd_nfront : thm
    val nhd_thm : thm
    val nlast_napp : thm
    val nlast_ncons : thm
    val nlast_nel : thm
    val nlast_nnil : thm
    val nlist_cases : thm
    val nlist_ind : thm
    val nlist_listOfN : thm
    val nlist_of_EQ0 : thm
    val nlist_of_INJ : thm
    val nlist_of_SURJ : thm
    val nlistrec_def : thm
    val nlistrec_ind : thm
    val nlistrec_thm : thm
    val nsnoc_cases : thm
    val ntl_DROP : thm
    val ntl_LE : thm
    val ntl_LT : thm
    val ntl_ndrop : thm
    val ntl_nonzero_LESS : thm
    val ntl_thm : thm
    val ntl_zero : thm
    val ntl_zero_empty_OR_ncons : thm
  
  val nlist_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [rich_list] Parent theory of "nlist"
   
   [set_relation] Parent theory of "nlist"
   
   [listOfN_def]  Definition
      
      ⊢ listOfN = nlistrec [] (λh tn t. h::t)
   
   [ncons_def]  Definition
      
      ⊢ ∀h t. ncons h t = h ⊗ t + 1
   
   [nel_def]  Definition
      
      ⊢ ∀n nlist. nel n nlist = nhd (ndrop n nlist)
   
   [nfront_def]  Definition
      
      ⊢ nfront = nlistrec 0 (λh tn rn. if tn = 0 then 0 else ncons h rn)
   
   [nhd_def]  Definition
      
      ⊢ ∀nl. nhd nl = nfst (nl − 1)
   
   [nlast_def]  Definition
      
      ⊢ nlast = nlistrec 0 (λh tn rn. if tn = 0 then h else rn)
   
   [nlist_of_def]  Definition
      
      ⊢ nlist_of [] = 0 ∧ ∀h t. nlist_of (h::t) = ncons h (nlist_of t)
   
   [ntl_def]  Definition
      
      ⊢ ∀nlist. ntl nlist = nsnd (nlist − 1)
   
   [LENGTH_nfront]  Theorem
      
      ⊢ ∀t. t ≠ 0 ⇒ nlen (nfront t) = nlen t − 1
   
   [MEM_listOfN_LESS]  Theorem
      
      ⊢ ∀l e. MEM e (listOfN l) ⇒ e < l
   
   [listOfN_EQ_CONS]  Theorem
      
      ⊢ listOfN n = h::t ⇔ ∃tn. n = ncons h tn ∧ listOfN tn = t
   
   [listOfN_EQ_NIL]  Theorem
      
      ⊢ (listOfN l = [] ⇔ l = 0) ∧ ([] = listOfN l ⇔ l = 0)
   
   [listOfN_INJ]  Theorem
      
      ⊢ ∀l1 l2. listOfN l1 = listOfN l2 ⇔ l1 = l2
   
   [listOfN_SURJ]  Theorem
      
      ⊢ ∀l. ∃n. listOfN n = l
   
   [listOfN_ncons]  Theorem
      
      ⊢ listOfN (ncons h t) = h::listOfN t
   
   [listOfN_nlist]  Theorem
      
      ⊢ ∀l. listOfN (nlist_of l) = l
   
   [listOfN_zero]  Theorem
      
      ⊢ listOfN 0 = []
   
   [lt_ncons1]  Theorem
      
      ⊢ h < ncons h t
   
   [lt_ncons2]  Theorem
      
      ⊢ t < ncons h t
   
   [napp_ndrop_l1_empty]  Theorem
      
      ⊢ ∀l1 l2. ndrop (nlen l1) (napp l1 l2) = l2
   
   [napp_nsnoc_lt]  Theorem
      
      ⊢ ∀l. l < napp l (ncons x 0)
   
   [napp_sing_eq]  Theorem
      
      ⊢ napp l1 (ncons l 0) = ncons x 0 ⇔ l1 = 0 ∧ x = l
   
   [ncons_11]  Theorem
      
      ⊢ ncons x y = ncons h t ⇔ x = h ∧ y = t
   
   [ncons_nhd_ntl]  Theorem
      
      ⊢ ∀l. l ≠ 0 ⇒ ncons (nhd l) (ntl l) = l
   
   [ncons_not_nnil]  Theorem
      
      ⊢ ncons x y ≠ 0
   
   [ncons_x_0_LENGTH_1]  Theorem
      
      ⊢ nlen l = 1 ⇔ ∃n. l = ncons n 0
   
   [ndrop_SUC]  Theorem
      
      ⊢ ∀l n. ndrop (SUC n) l = ntl (ndrop n l)
   
   [ndrop_nsingl]  Theorem
      
      ⊢ m ≠ 0 ⇒ ndrop m (ncons x 0) = 0
   
   [nel0_ncons]  Theorem
      
      ⊢ nel 0 (ncons h t) = h
   
   [nel_SUC_CONS]  Theorem
      
      ⊢ ∀n h t. nel (SUC n) (ncons h t) = nel n t
   
   [nel_correct]  Theorem
      
      ⊢ ∀l i. i < nlen l ⇒ EL i (listOfN l) = nel i l
   
   [nel_eq_nlist]  Theorem
      
      ⊢ ∀l1 l2.
            l1 = l2 ⇔
            nlen l1 = nlen l2 ∧ ∀m. m < nlen l1 ⇒ nel m l1 = nel m l2
   
   [nel_napp]  Theorem
      
      ⊢ ∀l1 l2. n < nlen l1 ⇒ nel n (napp l1 l2) = nel n l1
   
   [nel_napp2]  Theorem
      
      ⊢ ∀y n x. nlen x ≤ n ⇒ nel n (napp x y) = nel (n − nlen x) y
   
   [nel_ncons_nonzero]  Theorem
      
      ⊢ 0 < n ⇒ nel n (ncons h t) = nel (n − 1) t
   
   [nel_nfront]  Theorem
      
      ⊢ ∀t. m < nlen (nfront t) ⇒ nel m (nfront t) = nel m t
   
   [nel_nhd]  Theorem
      
      ⊢ nel 0 l = nhd l
   
   [nel_nnil]  Theorem
      
      ⊢ nel x 0 = 0
   
   [nfront_napp_sing]  Theorem
      
      ⊢ ∀pfx. nfront (napp pfx (ncons e 0)) = pfx
   
   [nfront_nnil]  Theorem
      
      ⊢ nfront 0 = 0
   
   [nfront_nsingl]  Theorem
      
      ⊢ nfront (ncons x 0) = 0
   
   [nfront_thm]  Theorem
      
      ⊢ nfront 0 = 0 ∧
        nfront (ncons h t) = if t = 0 then 0 else ncons h (nfront t)
   
   [nhd0]  Theorem
      
      ⊢ nhd 0 = 0
   
   [nhd_napp]  Theorem
      
      ⊢ ∀l1 l2. l1 ≠ 0 ⇒ nhd (napp l1 l2) = nhd l1
   
   [nhd_nfront]  Theorem
      
      ⊢ ∀l. l ≠ 0 ∧ ntl l ≠ 0 ⇒ nhd (nfront l) = nhd l
   
   [nhd_thm]  Theorem
      
      ⊢ nhd (ncons h t) = h
   
   [nlast_napp]  Theorem
      
      ⊢ ∀l1 l2. l2 ≠ 0 ⇒ nlast (napp l1 l2) = nlast l2
   
   [nlast_ncons]  Theorem
      
      ⊢ nlast (ncons h tn) = if tn = 0 then h else nlast tn
   
   [nlast_nel]  Theorem
      
      ⊢ ∀l. nlast l = nel (nlen l − 1) l
   
   [nlast_nnil]  Theorem
      
      ⊢ nlast 0 = 0
   
   [nlist_cases]  Theorem
      
      ⊢ ∀n. n = 0 ∨ ∃h t. n = ncons h t
   
   [nlist_ind]  Theorem
      
      ⊢ ∀P. P 0 ∧ (∀h t. P t ⇒ P (ncons h t)) ⇒ ∀n. P n
   
   [nlist_listOfN]  Theorem
      
      ⊢ ∀l. nlist_of (listOfN l) = l
   
   [nlist_of_EQ0]  Theorem
      
      ⊢ (nlist_of l = 0 ⇔ l = []) ∧ (0 = nlist_of l ⇔ l = [])
   
   [nlist_of_INJ]  Theorem
      
      ⊢ ∀n1 n2. nlist_of n1 = nlist_of n2 ⇔ n1 = n2
   
   [nlist_of_SURJ]  Theorem
      
      ⊢ ∀l. ∃n. nlist_of n = l
   
   [nlistrec_def]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ nlistrec n f 0 = n ∧
        nlistrec n f (ncons h t) = f h t (nlistrec n f t)
   
   [nsnoc_cases]  Theorem
      
      ⊢ ∀t. t = 0 ∨ ∃f l. t = napp f (ncons l 0)
   
   [ntl_DROP]  Theorem
      
      ⊢ ∀l m. ntl (nlist_of (DROP m l)) = ndrop m (ntl (nlist_of l))
   
   [ntl_LE]  Theorem
      
      ⊢ ∀n. ntl n ≤ n
   
   [ntl_LT]  Theorem
      
      ⊢ 0 < n ⇒ ntl n < n
   
   [ntl_ndrop]  Theorem
      
      ⊢ ∀l. ntl (ndrop n l) = ndrop n (ntl l)
   
   [ntl_nonzero_LESS]  Theorem
      
      ⊢ ∀n. n ≠ 0 ⇒ ntl n < n
   
   [ntl_thm]  Theorem
      
      ⊢ ntl (ncons h t) = t
   
   [ntl_zero]  Theorem
      
      ⊢ ntl 0 = 0
   
   [ntl_zero_empty_OR_ncons]  Theorem
      
      ⊢ ntl l = 0 ⇔ l = 0 ∨ ∃x. l = ncons x 0
   
   
*)
end

HOL 4, Kananaskis-13