Structure normalizerTheory

signature normalizerTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    val DIVMOD_ELIM_THM'' : thm
    val NOT_EVEN : thm
    val NOT_ODD : thm
    val NUM_INTEGRAL : thm
    val NUM_INTEGRAL_LEMMA : thm
    val NUM_NORMALIZE_CONV_sth : thm
    val NUM_SIMPLIFY_CONV_pth_evenodd : thm
    val PRE_ELIM_THM'' : thm
    val RING_FINAL_pth : thm
    val RING_pth_step : thm
    val SEMIRING_PTHS : thm
    val SUB_ELIM_THM'' : thm
(*
   [arithmetic] Parent theory of "normalizer"
   
   [DIVMOD_ELIM_THM'']  Theorem
      
      ⊢ 0 < n ⇒
        P (m DIV n) (m MOD n) ∧ (∀q r. (m ≠ q * n + r ∨ ¬(r < n)) ∨ P q r) ∨
        ¬P (m DIV n) (m MOD n) ∧ ∃q r. (m = q * n + r ∧ r < n) ∧ ¬P q r
   
   [NOT_EVEN]  Theorem
      
      ⊢ ∀n. ¬EVEN n ⇔ ODD n
   
   [NOT_ODD]  Theorem
      
      ⊢ ∀n. ¬ODD n ⇔ EVEN n
   
   [NUM_INTEGRAL]  Theorem
      
      ⊢ (∀x. 0 * x = 0) ∧ (∀x y z. x + y = x + z ⇔ y = z) ∧
        ∀w x y z. w * y + x * z = w * z + x * y ⇔ w = x ∨ y = z
   
   [NUM_INTEGRAL_LEMMA]  Theorem
      
      ⊢ w = x + d ∧ y = z + e ⇒
        (w * y + x * z = w * z + x * y ⇔ w = x ∨ y = z)
   
   [NUM_NORMALIZE_CONV_sth]  Theorem
      
      ⊢ 1 * x = x ∧ a * m + b * m = (a + b) * m ∧ a * m + m = (a + 1) * m ∧
        m + a * m = (a + 1) * m ∧ m + m = (1 + 1) * m ∧ 0 * m = 0 ∧
        0 + a = a ∧ a + 0 = a ∧ a * b = b * a ∧
        (a + b) * c = a * c + b * c ∧ 0 * a = 0 ∧ a * 0 = 0 ∧ 1 * a = a ∧
        a * 1 = a ∧ lx * ly * (rx * ry) = lx * rx * (ly * ry) ∧
        lx * ly * (rx * ry) = lx * (ly * (rx * ry)) ∧
        lx * ly * (rx * ry) = rx * (lx * ly * ry) ∧
        lx * ly * rx = lx * rx * ly ∧ lx * ly * rx = lx * (ly * rx) ∧
        lx * rx = rx * lx ∧ lx * (rx * ry) = lx * rx * ry ∧
        lx * (rx * ry) = rx * (lx * ry) ∧
        a + b + (c + d) = a + c + (b + d) ∧ a + b + c = a + (b + c) ∧
        a + (c + d) = c + (a + d) ∧ a + b + c = a + c + b ∧ a + c = c + a ∧
        a + (c + d) = a + c + d ∧ x ** p * x ** q = x ** (p + q) ∧
        x * x ** q = x ** SUC q ∧ x ** q * x = x ** SUC q ∧ x * x = x² ∧
        (x * y) ** q = x ** q * y ** q ∧ (x ** p) ** q = x ** (p * q) ∧
        x ** 0 = 1 ∧ x ** 1 = x ∧ x * (y + z) = x * y + x * z ∧
        x ** SUC q = x * x ** q
   
   [NUM_SIMPLIFY_CONV_pth_evenodd]  Theorem
      
      ⊢ (EVEN x ⇔ ∀y. x ≠ SUC (2 * y)) ∧ (ODD x ⇔ ∀y. x ≠ 2 * y) ∧
        (¬EVEN x ⇔ ∀y. x ≠ 2 * y) ∧ (¬ODD x ⇔ ∀y. x ≠ SUC (2 * y))
   
   [PRE_ELIM_THM'']  Theorem
      
      ⊢ P (PRE n) ⇔ ∀m. n ≠ SUC m ∧ (m ≠ 0 ∨ n ≠ 0) ∨ P m
   
   [RING_FINAL_pth]  Theorem
      
      ⊢ (p ⇒ F) ⇒ (¬q ⇔ p) ⇒ q
   
   [RING_pth_step]  Theorem
      
      ⊢ ∀add mul n0.
          (∀x. mul n0 x = n0) ∧ (∀x y z. add x y = add x z ⇔ y = z) ∧
          (∀w x y z.
             add (mul w y) (mul x z) = add (mul w z) (mul x y) ⇔
             w = x ∨ y = z) ⇒
          (∀a b c d.
             a ≠ b ∧ c ≠ d ⇔
             add (mul a c) (mul b d) ≠ add (mul a d) (mul b c)) ∧
          ∀n a b c d.
            n ≠ n0 ⇒ a = b ∧ c ≠ d ⇒ add a (mul n c) ≠ add b (mul n d)
   
   [SEMIRING_PTHS]  Theorem
      
      ⊢ (∀x y z. add x (add y z) = add (add x y) z) ∧
        (∀x y. add x y = add y x) ∧ (∀x. add r0 x = x) ∧
        (∀x y z. mul x (mul y z) = mul (mul x y) z) ∧
        (∀x y. mul x y = mul y x) ∧ (∀x. mul r1 x = x) ∧
        (∀x. mul r0 x = r0) ∧
        (∀x y z. mul x (add y z) = add (mul x y) (mul x z)) ∧
        (∀x. pwr x 0 = r1) ∧ (∀x n. pwr x (SUC n) = mul x (pwr x n)) ⇒
        mul r1 x = x ∧ add (mul a m) (mul b m) = mul (add a b) m ∧
        add (mul a m) m = mul (add a r1) m ∧
        add m (mul a m) = mul (add a r1) m ∧ add m m = mul (add r1 r1) m ∧
        mul r0 m = r0 ∧ add r0 a = a ∧ add a r0 = a ∧ mul a b = mul b a ∧
        mul (add a b) c = add (mul a c) (mul b c) ∧ mul r0 a = r0 ∧
        mul a r0 = r0 ∧ mul r1 a = a ∧ mul a r1 = a ∧
        mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry) ∧
        mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry)) ∧
        mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry) ∧
        mul (mul lx ly) rx = mul (mul lx rx) ly ∧
        mul (mul lx ly) rx = mul lx (mul ly rx) ∧ mul lx rx = mul rx lx ∧
        mul lx (mul rx ry) = mul (mul lx rx) ry ∧
        mul lx (mul rx ry) = mul rx (mul lx ry) ∧
        add (add a b) (add c d) = add (add a c) (add b d) ∧
        add (add a b) c = add a (add b c) ∧
        add a (add c d) = add c (add a d) ∧
        add (add a b) c = add (add a c) b ∧ add a c = add c a ∧
        add a (add c d) = add (add a c) d ∧
        mul (pwr x p) (pwr x q) = pwr x (p + q) ∧
        mul x (pwr x q) = pwr x (SUC q) ∧ mul (pwr x q) x = pwr x (SUC q) ∧
        mul x x = pwr x 2 ∧ pwr (mul x y) q = mul (pwr x q) (pwr y q) ∧
        pwr (pwr x p) q = pwr x (p * q) ∧ pwr x 0 = r1 ∧ pwr x 1 = x ∧
        mul x (add y z) = add (mul x y) (mul x z) ∧
        pwr x (SUC q) = mul x (pwr x q)
   
   [SUB_ELIM_THM'']  Theorem
      
      ⊢ P (a − b) ⇔ ∀d. a ≠ b + d ∧ (¬(a < b) ∨ d ≠ 0) ∨ P d
   
   
*)
end

HOL 4, Trindemossen-2