Structure gcdTheory

signature gcdTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val gcd_curried_def : thm
    val gcd_tupled_primitive_def : thm
    val is_gcd_def : thm
  
  (*  Theorems  *)
    val FACTOR_OUT_GCD : thm
    val GCD_0L : thm
    val GCD_0R : thm
    val GCD_ADD_L : thm
    val GCD_ADD_R : thm
    val GCD_EFFICIENTLY : thm
    val GCD_EQ_0 : thm
    val GCD_IS_GCD : thm
    val GCD_REF : thm
    val GCD_SYM : thm
    val IS_GCD_0R : thm
    val IS_GCD_MINUS_L : thm
    val IS_GCD_MINUS_R : thm
    val IS_GCD_REF : thm
    val IS_GCD_SYM : thm
    val IS_GCD_UNIQUE : thm
    val LINEAR_GCD : thm
    val L_EUCLIDES : thm
    val PRIME_GCD : thm
    val PRIME_IS_GCD : thm
    val P_EUCLIDES : thm
    val gcd_def : thm
    val gcd_ind : thm
  
  val gcd_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [divides] Parent theory of "gcd"
   
   [option] Parent theory of "gcd"
   
   [gcd_curried_def]  Definition
      
      |- !x x1. gcd x x1 = gcd_tupled (x,x1)
   
   [gcd_tupled_primitive_def]  Definition
      
      |- gcd_tupled =
         WFREC
           (@R.
              WF R /\ (!x y. ~(y <= x) ==> R (SUC x,y - x) (SUC x,SUC y)) /\
              !x y. y <= x ==> R (x - y,SUC y) (SUC x,SUC y))
           (\gcd_tupled a.
              case a of
                 (0,y) -> I y
              || (SUC x,0) -> I (SUC x)
              || (SUC x,SUC y') ->
                   I
                     (if y' <= x then
                        gcd_tupled (x - y',SUC y')
                      else
                        gcd_tupled (SUC x,y' - x)))
   
   [is_gcd_def]  Definition
      
      |- !a b c.
           is_gcd a b c =
           divides c a /\ divides c b /\
           !d. divides d a /\ divides d b ==> divides d c
   
   [FACTOR_OUT_GCD]  Theorem
      
      |- !n m.
           ~(n = 0) /\ ~(m = 0) ==>
           ?p q. (n = p * gcd n m) /\ (m = q * gcd n m) /\ (gcd p q = 1)
   
   [GCD_0L]  Theorem
      
      |- !a. gcd 0 a = a
   
   [GCD_0R]  Theorem
      
      |- !a. gcd a 0 = a
   
   [GCD_ADD_L]  Theorem
      
      |- !a b. gcd (a + b) a = gcd a b
   
   [GCD_ADD_R]  Theorem
      
      |- !a b. gcd a (a + b) = gcd a b
   
   [GCD_EFFICIENTLY]  Theorem
      
      |- !a b. gcd a b = (if a = 0 then b else gcd (b MOD a) a)
   
   [GCD_EQ_0]  Theorem
      
      |- !n m. (gcd n m = 0) = (n = 0) /\ (m = 0)
   
   [GCD_IS_GCD]  Theorem
      
      |- !a b. is_gcd a b (gcd a b)
   
   [GCD_REF]  Theorem
      
      |- !a. gcd a a = a
   
   [GCD_SYM]  Theorem
      
      |- !a b. gcd a b = gcd b a
   
   [IS_GCD_0R]  Theorem
      
      |- !a. is_gcd 0 a a
   
   [IS_GCD_MINUS_L]  Theorem
      
      |- !a b c. b <= a /\ is_gcd (a - b) b c ==> is_gcd a b c
   
   [IS_GCD_MINUS_R]  Theorem
      
      |- !a b c. a <= b /\ is_gcd a (b - a) c ==> is_gcd a b c
   
   [IS_GCD_REF]  Theorem
      
      |- !a. is_gcd a a a
   
   [IS_GCD_SYM]  Theorem
      
      |- !a b c. is_gcd a b c = is_gcd b a c
   
   [IS_GCD_UNIQUE]  Theorem
      
      |- !a b c d. is_gcd a b c /\ is_gcd a b d ==> (c = d)
   
   [LINEAR_GCD]  Theorem
      
      |- !n m. ~(n = 0) ==> ?p q. p * n = q * m + gcd m n
   
   [L_EUCLIDES]  Theorem
      
      |- !a b c. (gcd a b = 1) /\ divides b (a * c) ==> divides b c
   
   [PRIME_GCD]  Theorem
      
      |- !p b. prime p ==> divides p b \/ (gcd p b = 1)
   
   [PRIME_IS_GCD]  Theorem
      
      |- !p b. prime p ==> divides p b \/ is_gcd p b 1
   
   [P_EUCLIDES]  Theorem
      
      |- !p a b. prime p /\ divides p (a * b) ==> divides p a \/ divides p b
   
   [gcd_def]  Theorem
      
      |- (gcd 0 y = y) /\ (gcd (SUC x) 0 = SUC x) /\
         (gcd (SUC x) (SUC y) =
          (if y <= x then gcd (x - y) (SUC y) else gcd (SUC x) (y - x)))
   
   [gcd_ind]  Theorem
      
      |- !P.
           (!y. P 0 y) /\ (!x. P (SUC x) 0) /\
           (!x y.
              (~(y <= x) ==> P (SUC x) (y - x)) /\ (y <= x ==> P (x - y) (SUC y)) ==>
              P (SUC x) (SUC y)) ==>
           !v v1. P v v1
   
   
*)
end