Structure dividesTheory

signature dividesTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val PRIMES_def : thm
    val divides_def : thm
    val prime_def : thm
  
  (*  Theorems  *)
    val ADD_DIV_EQ : thm
    val ALL_DIVIDES_0 : thm
    val DIVIDES_ADD_1 : thm
    val DIVIDES_ADD_2 : thm
    val DIVIDES_ANTISYM : thm
    val DIVIDES_COMMON_MULT_I : thm
    val DIVIDES_DIV : thm
    val DIVIDES_EQN : thm
    val DIVIDES_EQN_COMM : thm
    val DIVIDES_EVEN : thm
    val DIVIDES_FACT : thm
    val DIVIDES_LE : thm
    val DIVIDES_LEQ_OR_ZERO : thm
    val DIVIDES_MOD_0 : thm
    val DIVIDES_MULT : thm
    val DIVIDES_MULTIPLE : thm
    val DIVIDES_MULT_LCANCEL : thm
    val DIVIDES_MULT_LEFT : thm
    val DIVIDES_MULT_RCANCEL : thm
    val DIVIDES_ODD : thm
    val DIVIDES_ONE : thm
    val DIVIDES_PROD : thm
    val DIVIDES_REFL : thm
    val DIVIDES_SUB : thm
    val DIVIDES_TRANS : thm
    val DIV_EQ : thm
    val DIV_EQUAL_0 : thm
    val DIV_EQ_MULT : thm
    val DIV_LE : thm
    val DIV_LE_MONOTONE_REVERSE : thm
    val DIV_MOD_EQ_0 : thm
    val DIV_MULT_EQ : thm
    val DIV_MULT_LE : thm
    val DIV_POS : thm
    val DIV_SOLVE : thm
    val DIV_SOLVE_COMM : thm
    val EUCLID : thm
    val EUCLID_PRIMES : thm
    val EVEN_ALT : thm
    val EXP_DIVIDES : thm
    val EXP_divides : thm
    val FACT_0 : thm
    val FACT_1 : thm
    val FACT_2 : thm
    val FACT_DIV : thm
    val FACT_EQ_1 : thm
    val FACT_EQ_SELF : thm
    val FACT_GE_SELF : thm
    val INDEX_LESS_PRIMES : thm
    val INFINITE_PRIMES : thm
    val LEQ_DIVIDES_FACT : thm
    val LE_MULT_LE_DIV : thm
    val LT_PRIMES : thm
    val MULT_LT_DIV : thm
    val NEXT_LARGER_PRIME : thm
    val NOT_LT_DIVIDES : thm
    val NOT_PRIME_0 : thm
    val NOT_PRIME_1 : thm
    val ODD_ALT : thm
    val ONE_DIV : thm
    val ONE_DIVIDES_ALL : thm
    val ONE_LT_PRIME : thm
    val ONE_LT_PRIMES : thm
    val PRIMES_11 : thm
    val PRIMES_NO_GAP : thm
    val PRIMES_ONTO : thm
    val PRIME_2 : thm
    val PRIME_3 : thm
    val PRIME_FACTOR : thm
    val PRIME_INDEX : thm
    val PRIME_POS : thm
    val SUB_DIV : thm
    val ZERO_DIVIDES : thm
    val ZERO_LT_PRIMES : thm
    val compute_divides : thm
    val divide_by_cofactor : thm
    val divides_exp : thm
    val divides_linear : thm
    val divides_linear_sub : thm
    val divides_pos : thm
    val divisor_pos : thm
    val factor_divides : thm
    val primePRIMES : thm
    val prime_MULT : thm
    val prime_always_bigger : thm
    val prime_divides_only_self : thm
(*
   [basicSize] Parent theory of "divides"
   
   [cv] Parent theory of "divides"
   
   [reduce] Parent theory of "divides"
   
   [while] Parent theory of "divides"
   
   [PRIMES_def]  Definition
      
      ⊢ PRIMES 0 = 2 ∧ ∀n. PRIMES (SUC n) = LEAST p. prime p ∧ PRIMES n < p
   
   [divides_def]  Definition
      
      ⊢ ∀a b. a divides b ⇔ ∃q. b = q * a
   
   [prime_def]  Definition
      
      ⊢ ∀a. prime a ⇔ a ≠ 1 ∧ ∀b. b divides a ⇒ b = a ∨ b = 1
   
   [ADD_DIV_EQ]  Theorem
      
      ⊢ ∀n a b. a MOD n + b < n ⇒ (a + b) DIV n = a DIV n
   
   [ALL_DIVIDES_0]  Theorem
      
      ⊢ ∀a. a divides 0
   
   [DIVIDES_ADD_1]  Theorem
      
      ⊢ ∀a b c. a divides b ∧ a divides c ⇒ a divides b + c
   
   [DIVIDES_ADD_2]  Theorem
      
      ⊢ ∀a b c. a divides b ∧ a divides b + c ⇒ a divides c
   
   [DIVIDES_ANTISYM]  Theorem
      
      ⊢ ∀a b. a divides b ∧ b divides a ⇒ a = b
   
   [DIVIDES_COMMON_MULT_I]  Theorem
      
      ⊢ ∀a b c. a divides b ⇒ c * a divides c * b
   
   [DIVIDES_DIV]  Theorem
      
      ⊢ ∀p n. 0 < p ∧ p divides n ⇒ p * (n DIV p) = n
   
   [DIVIDES_EQN]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀m. n divides m ⇔ m = m DIV n * n
   
   [DIVIDES_EQN_COMM]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀m. n divides m ⇔ m = n * (m DIV n)
   
   [DIVIDES_EVEN]  Theorem
      
      ⊢ ∀m. EVEN m ⇒ ∀n. m divides n ⇒ EVEN n
   
   [DIVIDES_FACT]  Theorem
      
      ⊢ ∀b. 0 < b ⇒ b divides FACT b
   
   [DIVIDES_LE]  Theorem
      
      ⊢ ∀a b. 0 < b ∧ a divides b ⇒ a ≤ b
   
   [DIVIDES_LEQ_OR_ZERO]  Theorem
      
      ⊢ ∀m n. m divides n ⇒ m ≤ n ∨ n = 0
   
   [DIVIDES_MOD_0]  Theorem
      
      ⊢ ∀p n. 0 < p ⇒ (p divides n ⇔ n MOD p = 0)
   
   [DIVIDES_MULT]  Theorem
      
      ⊢ ∀a b c. a divides b ⇒ a divides b * c
   
   [DIVIDES_MULTIPLE]  Theorem
      
      ⊢ ∀m n. n divides m ⇒ ∀k. n divides k * m
   
   [DIVIDES_MULT_LCANCEL]  Theorem
      
      ⊢ ∀a b c. c ≠ 0 ⇒ (c * a divides c * b ⇔ a divides b)
   
   [DIVIDES_MULT_LEFT]  Theorem
      
      ⊢ ∀n m. n * m divides m ⇔ m = 0 ∨ n = 1
   
   [DIVIDES_MULT_RCANCEL]  Theorem
      
      ⊢ ∀a b c. c ≠ 0 ⇒ (a * c divides b * c ⇔ a divides b)
   
   [DIVIDES_ODD]  Theorem
      
      ⊢ ∀n. ODD n ⇒ ∀m. m divides n ⇒ ODD m
   
   [DIVIDES_ONE]  Theorem
      
      ⊢ ∀x. x divides 1 ⇔ x = 1
   
   [DIVIDES_PROD]  Theorem
      
      ⊢ ∀a b c d. a divides c ∧ b divides d ⇒ a * b divides c * d
   
   [DIVIDES_REFL]  Theorem
      
      ⊢ ∀a. a divides a
   
   [DIVIDES_SUB]  Theorem
      
      ⊢ ∀a b c. a divides b ∧ a divides c ⇒ a divides b − c
   
   [DIVIDES_TRANS]  Theorem
      
      ⊢ ∀a b c. a divides b ∧ b divides c ⇒ a divides c
   
   [DIV_EQ]  Theorem
      
      ⊢ ∀x y z. 0 < z ⇒ (x DIV z = y DIV z ⇔ x − x MOD z = y − y MOD z)
   
   [DIV_EQUAL_0]  Theorem
      
      ⊢ ∀m n. 0 < n ⇒ (m DIV n = 0 ⇔ m < n)
   
   [DIV_EQ_MULT]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀k m. m MOD n = 0 ⇒ (k * n = m ⇔ k = m DIV n)
   
   [DIV_LE]  Theorem
      
      ⊢ ∀x y z. 0 < y ∧ x ≤ y * z ⇒ x DIV y ≤ z
   
   [DIV_LE_MONOTONE_REVERSE]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ∧ x ≤ y ⇒ ∀n. n DIV y ≤ n DIV x
   
   [DIV_MOD_EQ_0]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ (n DIV m = 0 ∧ n MOD m = 0 ⇔ n = 0)
   
   [DIV_MULT_EQ]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀q. n divides q ⇔ q DIV n * n = q
   
   [DIV_MULT_LE]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀q. q DIV n * n ≤ q
   
   [DIV_POS]  Theorem
      
      ⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ 0 < n DIV m
   
   [DIV_SOLVE]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀x y. x * n = y ⇒ x = y DIV n
   
   [DIV_SOLVE_COMM]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀x y. n * x = y ⇒ x = y DIV n
   
   [EUCLID]  Theorem
      
      ⊢ ∀n. ∃p. n < p ∧ prime p
   
   [EUCLID_PRIMES]  Theorem
      
      ⊢ ∀n. ∃i. n < PRIMES i
   
   [EVEN_ALT]  Theorem
      
      ⊢ ∀n. EVEN n ⇔ 2 divides n
   
   [EXP_DIVIDES]  Theorem
      
      ⊢ a ** b divides a ** c ⇔
        b ≤ c ∨ a = 0 ∧ 0 < c ∨ a = 0 ∧ b = 0 ∨ a = 1
   
   [EXP_divides]  Theorem
      
      ⊢ ∀a b n. 0 < n ∧ a ** n divides b ⇒ a divides b
   
   [FACT_0]  Theorem
      
      ⊢ FACT 0 = 1
   
   [FACT_1]  Theorem
      
      ⊢ FACT 1 = 1
   
   [FACT_2]  Theorem
      
      ⊢ FACT 2 = 2
   
   [FACT_DIV]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ FACT (n − 1) = FACT n DIV n
   
   [FACT_EQ_1]  Theorem
      
      ⊢ ∀n. FACT n = 1 ⇔ n ≤ 1
   
   [FACT_EQ_SELF]  Theorem
      
      ⊢ ∀n. FACT n = n ⇔ n = 1 ∨ n = 2
   
   [FACT_GE_SELF]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ n ≤ FACT n
   
   [INDEX_LESS_PRIMES]  Theorem
      
      ⊢ ∀n. n < PRIMES n
   
   [INFINITE_PRIMES]  Theorem
      
      ⊢ ∀n. PRIMES n < PRIMES (SUC n)
   
   [LEQ_DIVIDES_FACT]  Theorem
      
      ⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ m divides FACT n
   
   [LE_MULT_LE_DIV]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀k m. m MOD n = 0 ⇒ (m ≤ n * k ⇔ m DIV n ≤ k)
   
   [LT_PRIMES]  Theorem
      
      ⊢ ∀m n. m < n ⇒ PRIMES m < PRIMES n
   
   [MULT_LT_DIV]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀k m. m MOD n = 0 ⇒ (k * n < m ⇔ k < m DIV n)
   
   [NEXT_LARGER_PRIME]  Theorem
      
      ⊢ ∀n. ∃i. n < PRIMES i ∧ ∀j. j < i ⇒ PRIMES j ≤ n
   
   [NOT_LT_DIVIDES]  Theorem
      
      ⊢ ∀a b. 0 < b ∧ b < a ⇒ ¬(a divides b)
   
   [NOT_PRIME_0]  Theorem
      
      ⊢ ¬prime 0
   
   [NOT_PRIME_1]  Theorem
      
      ⊢ ¬prime 1
   
   [ODD_ALT]  Theorem
      
      ⊢ ∀n. ODD n ⇔ ¬(2 divides n)
   
   [ONE_DIV]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ 1 DIV n = 0
   
   [ONE_DIVIDES_ALL]  Theorem
      
      ⊢ ∀a. 1 divides a
   
   [ONE_LT_PRIME]  Theorem
      
      ⊢ ∀p. prime p ⇒ 1 < p
   
   [ONE_LT_PRIMES]  Theorem
      
      ⊢ ∀n. 1 < PRIMES n
   
   [PRIMES_11]  Theorem
      
      ⊢ ∀m n. PRIMES m = PRIMES n ⇒ m = n
   
   [PRIMES_NO_GAP]  Theorem
      
      ⊢ ∀n p. PRIMES n < p ∧ p < PRIMES (SUC n) ∧ prime p ⇒ F
   
   [PRIMES_ONTO]  Theorem
      
      ⊢ ∀p. prime p ⇒ ∃i. PRIMES i = p
   
   [PRIME_2]  Theorem
      
      ⊢ prime 2
   
   [PRIME_3]  Theorem
      
      ⊢ prime 3
   
   [PRIME_FACTOR]  Theorem
      
      ⊢ ∀n. n ≠ 1 ⇒ ∃p. prime p ∧ p divides n
   
   [PRIME_INDEX]  Theorem
      
      ⊢ ∀p. prime p ⇔ ∃i. p = PRIMES i
   
   [PRIME_POS]  Theorem
      
      ⊢ ∀p. prime p ⇒ 0 < p
   
   [SUB_DIV]  Theorem
      
      ⊢ ∀m n. 0 < n ∧ n ≤ m ⇒ (m − n) DIV n = m DIV n − 1
   
   [ZERO_DIVIDES]  Theorem
      
      ⊢ 0 divides m ⇔ m = 0
   
   [ZERO_LT_PRIMES]  Theorem
      
      ⊢ ∀n. 0 < PRIMES n
   
   [compute_divides]  Theorem
      
      ⊢ ∀a b.
          a divides b ⇔
          if a = 0 then b = 0
          else if a = 1 then T
          else if b = 0 then T
          else b MOD a = 0
   
   [divide_by_cofactor]  Theorem
      
      ⊢ ∀m n. 0 < n ∧ m divides n ⇒ n DIV (n DIV m) = m
   
   [divides_exp]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀a b. a divides b ⇒ a divides b ** n
   
   [divides_linear]  Theorem
      
      ⊢ ∀a b c. c divides a ∧ c divides b ⇒ ∀h k. c divides h * a + k * b
   
   [divides_linear_sub]  Theorem
      
      ⊢ ∀a b c.
          c divides a ∧ c divides b ⇒
          ∀h k d. h * a = k * b + d ⇒ c divides d
   
   [divides_pos]  Theorem
      
      ⊢ ∀m n. 0 < n ∧ m divides n ⇒ 0 < m ∧ m ≤ n
   
   [divisor_pos]  Theorem
      
      ⊢ ∀m n. 0 < n ∧ m divides n ⇒ 0 < m
   
   [factor_divides]  Theorem
      
      ⊢ ∀m n. n divides m * n ∧ n divides n * m
   
   [primePRIMES]  Theorem
      
      ⊢ ∀n. prime (PRIMES n)
   
   [prime_MULT]  Theorem
      
      ⊢ ∀n m.
          prime (n * m) ⇔
          (n ≤ m ⇒ n = 1 ∧ prime m) ∧ (m ≤ n ⇒ m = 1 ∧ prime n)
   
   [prime_always_bigger]  Theorem
      
      ⊢ ∀n. ∃p. prime p ∧ n < p
   
   [prime_divides_only_self]  Theorem
      
      ⊢ ∀m n. prime m ∧ prime n ∧ m divides n ⇒ m = n
   
   
*)
end

HOL 4, Trindemossen-2