Structure numpairTheory

signature numpairTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val invtri_def : thm
    val napp_def : thm
    val ncons_def : thm
    val nfoldl_def : thm
    val nfst_def : thm
    val nlen_def : thm
    val nmap_def : thm
    val npair_def : thm
    val nsnd_def : thm
    val tri_def : thm
  
  (*  Theorems  *)
    val SND_invtri0 : thm
    val invtri0_def : thm
    val invtri0_ind : thm
    val invtri0_thm : thm
    val invtri_le : thm
    val invtri_linverse : thm
    val invtri_linverse_r : thm
    val invtri_lower : thm
    val invtri_unique : thm
    val invtri_upper : thm
    val napp_thm : thm
    val ncons_11 : thm
    val ncons_not_nnil : thm
    val nfoldl_thm : thm
    val nfst_le : thm
    val nfst_npair : thm
    val nlen_thm : thm
    val nlist_cases : thm
    val nlist_ind : thm
    val nlistrec_def : thm
    val nlistrec_ind : thm
    val nlistrec_thm : thm
    val nmap_thm : thm
    val npair : thm
    val npair_11 : thm
    val npair_cases : thm
    val nsnd_le : thm
    val nsnd_npair : thm
    val tri_11 : thm
    val tri_LE : thm
    val tri_LT : thm
    val tri_LT_I : thm
    val tri_def_compute : thm
    val tri_eq_0 : thm
    val tri_formula : thm
    val tri_le : thm
    val twotri_formula : thm
  
  val numpair_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [basicSize] Parent theory of "numpair"
   
   [while] Parent theory of "numpair"
   
   [invtri_def]  Definition
      
      ⊢ ∀n. tri⁻¹ n = SND (invtri0 n 0)
   
   [napp_def]  Definition
      
      ⊢ ∀l1 l2. napp l1 l2 = nlistrec l2 (λn t r. ncons n r) l1
   
   [ncons_def]  Definition
      
      ⊢ ∀h t. ncons h t = h ⊗ t + 1
   
   [nfoldl_def]  Definition
      
      ⊢ ∀f a l. nfoldl f a l = nlistrec (λa. a) (λn t r a. r (f n a)) l a
   
   [nfst_def]  Definition
      
      ⊢ ∀n. nfst n = tri (tri⁻¹ n) + tri⁻¹ n − n
   
   [nlen_def]  Definition
      
      ⊢ nlen = nlistrec 0 (λn t r. r + 1)
   
   [nmap_def]  Definition
      
      ⊢ ∀f. nmap f = nlistrec 0 (λn t r. ncons (f n) r)
   
   [npair_def]  Definition
      
      ⊢ ∀m n. m ⊗ n = tri (m + n) + n
   
   [nsnd_def]  Definition
      
      ⊢ ∀n. nsnd n = n − tri (tri⁻¹ n)
   
   [tri_def]  Definition
      
      ⊢ (tri 0 = 0) ∧ ∀n. tri (SUC n) = SUC n + tri n
   
   [SND_invtri0]  Theorem
      
      ⊢ ∀n a. FST (invtri0 n a) < SUC (SND (invtri0 n a))
   
   [invtri0_def]  Theorem
      
      ⊢ ∀n a.
            invtri0 n a =
            if n < a + 1 then (n,a)
            else invtri0 (n − (a + 1)) (a + 1)
   
   [invtri0_ind]  Theorem
      
      ⊢ ∀P.
            (∀n a. (¬(n < a + 1) ⇒ P (n − (a + 1)) (a + 1)) ⇒ P n a) ⇒
            ∀v v1. P v v1
   
   [invtri0_thm]  Theorem
      
      ⊢ ∀n a. tri (SND (invtri0 n a)) + FST (invtri0 n a) = n + tri a
   
   [invtri_le]  Theorem
      
      ⊢ tri⁻¹ n ≤ n
   
   [invtri_linverse]  Theorem
      
      ⊢ tri⁻¹ (tri n) = n
   
   [invtri_linverse_r]  Theorem
      
      ⊢ y ≤ x ⇒ (tri⁻¹ (tri x + y) = x)
   
   [invtri_lower]  Theorem
      
      ⊢ tri (tri⁻¹ n) ≤ n
   
   [invtri_unique]  Theorem
      
      ⊢ tri y ≤ n ∧ n < tri (y + 1) ⇒ (tri⁻¹ n = y)
   
   [invtri_upper]  Theorem
      
      ⊢ n < tri (tri⁻¹ n + 1)
   
   [napp_thm]  Theorem
      
      ⊢ (napp 0 nlist = nlist) ∧
        (napp (ncons h t) nlist = ncons h (napp t nlist))
   
   [ncons_11]  Theorem
      
      ⊢ (ncons x y = ncons h t) ⇔ (x = h) ∧ (y = t)
   
   [ncons_not_nnil]  Theorem
      
      ⊢ ncons x y ≠ 0
   
   [nfoldl_thm]  Theorem
      
      ⊢ (nfoldl f a 0 = a) ∧ (nfoldl f a (ncons h t) = nfoldl f (f h a) t)
   
   [nfst_le]  Theorem
      
      ⊢ nfst n ≤ n
   
   [nfst_npair]  Theorem
      
      ⊢ nfst (x ⊗ y) = x
   
   [nlen_thm]  Theorem
      
      ⊢ (nlen 0 = 0) ∧ (nlen (ncons h t) = nlen t + 1)
   
   [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
   
   [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))
   
   [nmap_thm]  Theorem
      
      ⊢ (nmap f 0 = 0) ∧ (nmap f (ncons h t) = ncons (f h) (nmap f t))
   
   [npair]  Theorem
      
      ⊢ ∀n. nfst n ⊗ nsnd n = n
   
   [npair_11]  Theorem
      
      ⊢ (x1 ⊗ y1 = x2 ⊗ y2) ⇔ (x1 = x2) ∧ (y1 = y2)
   
   [npair_cases]  Theorem
      
      ⊢ ∀n. ∃x y. n = x ⊗ y
   
   [nsnd_le]  Theorem
      
      ⊢ nsnd n ≤ n
   
   [nsnd_npair]  Theorem
      
      ⊢ nsnd (x ⊗ y) = y
   
   [tri_11]  Theorem
      
      ⊢ ∀m n. (tri m = tri n) ⇔ (m = n)
   
   [tri_LE]  Theorem
      
      ⊢ ∀m n. tri m ≤ tri n ⇔ m ≤ n
   
   [tri_LT]  Theorem
      
      ⊢ ∀n m. tri n < tri m ⇔ n < m
   
   [tri_LT_I]  Theorem
      
      ⊢ ∀n m. n < m ⇒ tri n < tri m
   
   [tri_def_compute]  Theorem
      
      ⊢ (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))
   
   [tri_eq_0]  Theorem
      
      ⊢ ((tri n = 0) ⇔ (n = 0)) ∧ ((0 = tri n) ⇔ (n = 0))
   
   [tri_formula]  Theorem
      
      ⊢ tri n = n * (n + 1) DIV 2
   
   [tri_le]  Theorem
      
      ⊢ n ≤ tri n
   
   [twotri_formula]  Theorem
      
      ⊢ 2 * tri n = n * (n + 1)
   
   
*)
end

HOL 4, Kananaskis-11