Structure dividesTheory

signature dividesTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val divides_def : thm
    val prime_def : thm
  
  (*  Theorems  *)
    val ALL_DIVIDES_0 : thm
    val DIVIDES_ADD_1 : thm
    val DIVIDES_ADD_2 : thm
    val DIVIDES_ANTISYM : thm
    val DIVIDES_FACT : thm
    val DIVIDES_LE : thm
    val DIVIDES_MULT : thm
    val DIVIDES_MULT_LEFT : thm
    val DIVIDES_REFL : thm
    val DIVIDES_SUB : thm
    val DIVIDES_TRANS : thm
    val NOT_LT_DIV : thm
    val NOT_PRIME_0 : thm
    val NOT_PRIME_1 : thm
    val ONE_DIVIDES_ALL : thm
  
  val divides_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [numeral] Parent theory of "divides"
   
   [sum] Parent theory of "divides"
   
   [divides_def]  Definition
      
      |- !a b. divides a b = ?q. b = q * a
   
   [prime_def]  Definition
      
      |- !a. prime a = ~(a = 1) /\ !b. divides b a ==> (b = a) \/ (b = 1)
   
   [ALL_DIVIDES_0]  Theorem
      
      |- !a. divides a 0
   
   [DIVIDES_ADD_1]  Theorem
      
      |- !a b c. divides a b /\ divides a c ==> divides a (b + c)
   
   [DIVIDES_ADD_2]  Theorem
      
      |- !a b c. divides a b /\ divides a (b + c) ==> divides a c
   
   [DIVIDES_ANTISYM]  Theorem
      
      |- !a b. divides a b /\ divides b a ==> (a = b)
   
   [DIVIDES_FACT]  Theorem
      
      |- !b. 0 < b ==> divides b (FACT b)
   
   [DIVIDES_LE]  Theorem
      
      |- !a b. 0 < b /\ divides a b ==> a <= b
   
   [DIVIDES_MULT]  Theorem
      
      |- !a b c. divides a b ==> divides a (b * c)
   
   [DIVIDES_MULT_LEFT]  Theorem
      
      |- !n m. divides (n * m) m = (m = 0) \/ (n = 1)
   
   [DIVIDES_REFL]  Theorem
      
      |- !a. divides a a
   
   [DIVIDES_SUB]  Theorem
      
      |- !a b c. divides a b /\ divides a c ==> divides a (b - c)
   
   [DIVIDES_TRANS]  Theorem
      
      |- !p q r. divides p q ==> divides q r ==> divides p r
   
   [NOT_LT_DIV]  Theorem
      
      |- !a b. 0 < b /\ b < a ==> ~divides a b
   
   [NOT_PRIME_0]  Theorem
      
      |- ~prime 0
   
   [NOT_PRIME_1]  Theorem
      
      |- ~prime 1
   
   [ONE_DIVIDES_ALL]  Theorem
      
      |- !a. divides 1 a
   
   
*)
end