Structure intReduceTheory

signature intReduceTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    val INT_ADD_CONV_pth0 : thm
    val INT_ADD_CONV_pth1 : thm
    val INT_EQ_CONV_pth : thm
    val INT_GE_CONV_pth : thm
    val INT_GT_CONV_pth : thm
    val INT_LE_CONV_nth : thm
    val INT_LE_CONV_pth : thm
    val INT_LE_CONV_tth : thm
    val INT_LT_CONV_pth : thm
    val INT_MUL_CONV_pth0 : thm
    val INT_MUL_CONV_pth1 : thm
    val INT_NEG_CONV_pth : thm
    val INT_POW_CONV_pth : thm
    val INT_POW_CONV_tth : thm
(*
   [integer] Parent theory of "intReduce"
   
   [INT_ADD_CONV_pth0]  Theorem
      
      ⊢ -&m + &m = 0 ∧ &m + -&m = 0
   
   [INT_ADD_CONV_pth1]  Theorem
      
      ⊢ -&m + -&n = -&(m + n) ∧ -&m + &(m + n) = &n ∧
        -&(m + n) + &m = -&n ∧ &(m + n) + -&m = &n ∧ &m + -&(m + n) = -&n ∧
        &m + &n = &(m + n)
   
   [INT_EQ_CONV_pth]  Theorem
      
      ⊢ (&m = &n ⇔ m = n) ∧ (-&m = -&n ⇔ m = n) ∧
        (-&m = &n ⇔ m = 0 ∧ n = 0) ∧ (&m = -&n ⇔ m = 0 ∧ n = 0)
   
   [INT_GE_CONV_pth]  Theorem
      
      ⊢ (&m ≥ -&n ⇔ T) ∧ (&m ≥ &n ⇔ n ≤ m) ∧ (-&m ≥ -&n ⇔ m ≤ n) ∧
        (-&m ≥ &n ⇔ m = 0 ∧ n = 0)
   
   [INT_GT_CONV_pth]  Theorem
      
      ⊢ (-&m > &n ⇔ F) ∧ (&m > &n ⇔ n < m) ∧ (-&m > -&n ⇔ m < n) ∧
        (&m > -&n ⇔ ¬(m = 0 ∧ n = 0))
   
   [INT_LE_CONV_nth]  Theorem
      
      ⊢ (¬T ⇔ F) ∧ (¬F ⇔ T)
   
   [INT_LE_CONV_pth]  Theorem
      
      ⊢ (-&m ≤ &n ⇔ T) ∧ (&m ≤ &n ⇔ m ≤ n) ∧ (-&m ≤ -&n ⇔ n ≤ m) ∧
        (&m ≤ -&n ⇔ m = 0 ∧ n = 0)
   
   [INT_LE_CONV_tth]  Theorem
      
      ⊢ (F ∧ F ⇔ F) ∧ (F ∧ T ⇔ F) ∧ (T ∧ F ⇔ F) ∧ (T ∧ T ⇔ T)
   
   [INT_LT_CONV_pth]  Theorem
      
      ⊢ (&m < -&n ⇔ F) ∧ (&m < &n ⇔ m < n) ∧ (-&m < -&n ⇔ n < m) ∧
        (-&m < &n ⇔ ¬(m = 0 ∧ n = 0))
   
   [INT_MUL_CONV_pth0]  Theorem
      
      ⊢ 0 * &x = 0 ∧ 0 * -&x = 0 ∧ &x * 0 = 0 ∧ -&x * 0 = 0
   
   [INT_MUL_CONV_pth1]  Theorem
      
      ⊢ (&m * &n = &(m * n) ∧ -&m * -&n = &(m * n)) ∧
        -&m * &n = -&(m * n) ∧ &m * -&n = -&(m * n)
   
   [INT_NEG_CONV_pth]  Theorem
      
      ⊢ -0 = 0 ∧ --&x = &x
   
   [INT_POW_CONV_pth]  Theorem
      
      ⊢ &x ** n = &(x ** n) ∧
        -&x ** n = if EVEN n then &(x ** n) else -&(x ** n)
   
   [INT_POW_CONV_tth]  Theorem
      
      ⊢ (if T then x else y) = x ∧ (if F then x else y) = y
   
   
*)
end

HOL 4, Trindemossen-2