Structure numpairTheory

signature numpairTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val invtri_def : thm
    val nfst_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 nfst0 : thm
    val nfst_le : thm
    val nfst_le_npair : thm
    val nfst_npair : thm
    val npair : thm
    val npair00 : thm
    val npair2_lt : thm
    val npair2_lt_E : thm
    val npair2_lt_I : thm
    val npair_11 : thm
    val npair_EQ_0 : thm
    val npair_cases : thm
    val npairs_lt_I : thm
    val nsnd0 : thm
    val nsnd_le : thm
    val nsnd_le_npair : thm
    val nsnd_npair : thm
    val tri_11 : thm
    val tri_LE : thm
    val tri_LT : thm
    val tri_LT_I : 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)
   
   [nfst_def]  Definition
      
      ⊢ ∀n. nfst n = tri (tri⁻¹ n) + tri⁻¹ n − n
   
   [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)
   
   [nfst0]  Theorem
      
      ⊢ nfst 0 = 0
   
   [nfst_le]  Theorem
      
      ⊢ nfst n ≤ n
   
   [nfst_le_npair]  Theorem
      
      ⊢ ∀m n. n ≤ n ⊗ m
   
   [nfst_npair]  Theorem
      
      ⊢ nfst (x ⊗ y) = x
   
   [npair]  Theorem
      
      ⊢ ∀n. nfst n ⊗ nsnd n = n
   
   [npair00]  Theorem
      
      ⊢ 0 ⊗ 0 = 0
   
   [npair2_lt]  Theorem
      
      ⊢ ∀n n1 n2. n ⊗ n1 < n ⊗ n2 ⇔ n1 < n2
   
   [npair2_lt_E]  Theorem
      
      ⊢ ∀n n1 n2. n ⊗ n1 < n ⊗ n2 ⇒ n1 < n2
   
   [npair2_lt_I]  Theorem
      
      ⊢ ∀n n1 n2. n1 < n2 ⇒ n ⊗ n1 < n ⊗ n2
   
   [npair_11]  Theorem
      
      ⊢ x1 ⊗ y1 = x2 ⊗ y2 ⇔ x1 = x2 ∧ y1 = y2
   
   [npair_EQ_0]  Theorem
      
      ⊢ ∀x y. x ⊗ y = 0 ⇔ x = 0 ∧ y = 0
   
   [npair_cases]  Theorem
      
      ⊢ ∀n. ∃x y. n = x ⊗ y
   
   [npairs_lt_I]  Theorem
      
      ⊢ ∀a b c d. a ≤ b ∧ c < d ⇒ a ⊗ c < b ⊗ d
   
   [nsnd0]  Theorem
      
      ⊢ nsnd 0 = 0
   
   [nsnd_le]  Theorem
      
      ⊢ nsnd n ≤ n
   
   [nsnd_le_npair]  Theorem
      
      ⊢ ∀m n. m ≤ n ⊗ m
   
   [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_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-14