Structure numeralTheory

signature numeralTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val iBIT_cases : thm
    val iDUB : thm
    val iMOD_2EXP : thm
    val iSQR : thm
    val iSUB_DEF : thm
    val iZ : thm
    val iiSUC : thm
  
  (*  Theorems  *)
    val DIVMOD_NUMERAL_CALC : thm
    val DIV_2EXP : thm
    val MOD_2EXP : thm
    val bit_induction : thm
    val bit_initiality : thm
    val divmod_POS : thm
    val iDUB_removal : thm
    val iSUB_THM : thm
    val numeral_MAX : thm
    val numeral_MIN : thm
    val numeral_add : thm
    val numeral_distrib : thm
    val numeral_div2 : thm
    val numeral_eq : thm
    val numeral_evenodd : thm
    val numeral_exp : thm
    val numeral_fact : thm
    val numeral_funpow : thm
    val numeral_iisuc : thm
    val numeral_imod_2exp : thm
    val numeral_lt : thm
    val numeral_lte : thm
    val numeral_mult : thm
    val numeral_pre : thm
    val numeral_sub : thm
    val numeral_suc : thm
  
  val numeral_grammars : type_grammar.grammar * term_grammar.grammar
  
  
(*
   [while] Parent theory of "numeral"
   
   [iBIT_cases]  Definition
      
      |- (!zf bf1 bf2. iBIT_cases ZERO zf bf1 bf2 = zf) /\
         (!n zf bf1 bf2. iBIT_cases (BIT1 n) zf bf1 bf2 = bf1 n) /\
         !n zf bf1 bf2. iBIT_cases (BIT2 n) zf bf1 bf2 = bf2 n
   
   [iDUB]  Definition
      
      |- !x. numeral$iDUB x = x + x
   
   [iMOD_2EXP]  Definition
      
      |- numeral$iMOD_2EXP = MOD_2EXP
   
   [iSQR]  Definition
      
      |- !x. numeral$iSQR x = x * x
   
   [iSUB_DEF]  Definition
      
      |- (!b x. numeral$iSUB b ZERO x = ZERO) /\
         (!b n x.
            numeral$iSUB b (BIT1 n) x =
            (if b then
               iBIT_cases x (BIT1 n) (\m. numeral$iDUB (numeral$iSUB T n m))
                 (\m. BIT1 (numeral$iSUB F n m))
             else
               iBIT_cases x (numeral$iDUB n) (\m. BIT1 (numeral$iSUB F n m))
                 (\m. numeral$iDUB (numeral$iSUB F n m)))) /\
         !b n x.
           numeral$iSUB b (BIT2 n) x =
           (if b then
              iBIT_cases x (BIT2 n) (\m. BIT1 (numeral$iSUB T n m))
                (\m. numeral$iDUB (numeral$iSUB T n m))
            else
              iBIT_cases x (BIT1 n) (\m. numeral$iDUB (numeral$iSUB T n m))
                (\m. BIT1 (numeral$iSUB F n m)))
   
   [iZ]  Definition
      
      |- !x. numeral$iZ x = x
   
   [iiSUC]  Definition
      
      |- !n. numeral$iiSUC n = SUC (SUC n)
   
   [DIVMOD_NUMERAL_CALC]  Theorem
      
      |- (!m n. m DIV BIT1 n = FST (DIVMOD (ZERO,m,BIT1 n))) /\
         (!m n. m DIV BIT2 n = FST (DIVMOD (ZERO,m,BIT2 n))) /\
         (!m n. m MOD BIT1 n = SND (DIVMOD (ZERO,m,BIT1 n))) /\
         !m n. m MOD BIT2 n = SND (DIVMOD (ZERO,m,BIT2 n))
   
   [DIV_2EXP]  Theorem
      
      |- !n x. DIV_2EXP n x = FUNPOW DIV2 n x
   
   [MOD_2EXP]  Theorem
      
      |- (!x. MOD_2EXP x 0 = 0) /\
         !x n. MOD_2EXP x (NUMERAL n) = NUMERAL (numeral$iMOD_2EXP x n)
   
   [bit_induction]  Theorem
      
      |- !P.
           P ZERO /\ (!n. P n ==> P (BIT1 n)) /\ (!n. P n ==> P (BIT2 n)) ==> !n. P n
   
   [bit_initiality]  Theorem
      
      |- !zf b1f b2f.
           ?f.
             (f ZERO = zf) /\ (!n. f (BIT1 n) = b1f n (f n)) /\
             !n. f (BIT2 n) = b2f n (f n)
   
   [divmod_POS]  Theorem
      
      |- !n.
           0 < n ==>
           (DIVMOD (a,m,n) =
            (if m < n then
               (a,m)
             else
               (let q = findq (1,m,n) in DIVMOD (a + q,m - n * q,n))))
   
   [iDUB_removal]  Theorem
      
      |- !n.
           (numeral$iDUB (BIT1 n) = BIT2 (numeral$iDUB n)) /\
           (numeral$iDUB (BIT2 n) = BIT2 (BIT1 n)) /\ (numeral$iDUB ZERO = ZERO)
   
   [iSUB_THM]  Theorem
      
      |- !b n m.
           (numeral$iSUB b ZERO x = ZERO) /\ (numeral$iSUB T n ZERO = n) /\
           (numeral$iSUB F (BIT1 n) ZERO = numeral$iDUB n) /\
           (numeral$iSUB T (BIT1 n) (BIT1 m) = numeral$iDUB (numeral$iSUB T n m)) /\
           (numeral$iSUB F (BIT1 n) (BIT1 m) = BIT1 (numeral$iSUB F n m)) /\
           (numeral$iSUB T (BIT1 n) (BIT2 m) = BIT1 (numeral$iSUB F n m)) /\
           (numeral$iSUB F (BIT1 n) (BIT2 m) = numeral$iDUB (numeral$iSUB F n m)) /\
           (numeral$iSUB F (BIT2 n) ZERO = BIT1 n) /\
           (numeral$iSUB T (BIT2 n) (BIT1 m) = BIT1 (numeral$iSUB T n m)) /\
           (numeral$iSUB F (BIT2 n) (BIT1 m) = numeral$iDUB (numeral$iSUB T n m)) /\
           (numeral$iSUB T (BIT2 n) (BIT2 m) = numeral$iDUB (numeral$iSUB T n m)) /\
           (numeral$iSUB F (BIT2 n) (BIT2 m) = BIT1 (numeral$iSUB F n m))
   
   [numeral_MAX]  Theorem
      
      |- (MAX 0 x = x) /\ (MAX x 0 = x) /\
         (MAX (NUMERAL x) (NUMERAL y) = NUMERAL (if x < y then y else x))
   
   [numeral_MIN]  Theorem
      
      |- (MIN 0 x = 0) /\ (MIN x 0 = 0) /\
         (MIN (NUMERAL x) (NUMERAL y) = NUMERAL (if x < y then x else y))
   
   [numeral_add]  Theorem
      
      |- !n m.
           (numeral$iZ (ZERO + n) = n) /\ (numeral$iZ (n + ZERO) = n) /\
           (numeral$iZ (BIT1 n + BIT1 m) = BIT2 (numeral$iZ (n + m))) /\
           (numeral$iZ (BIT1 n + BIT2 m) = BIT1 (SUC (n + m))) /\
           (numeral$iZ (BIT2 n + BIT1 m) = BIT1 (SUC (n + m))) /\
           (numeral$iZ (BIT2 n + BIT2 m) = BIT2 (SUC (n + m))) /\
           (SUC (ZERO + n) = SUC n) /\ (SUC (n + ZERO) = SUC n) /\
           (SUC (BIT1 n + BIT1 m) = BIT1 (SUC (n + m))) /\
           (SUC (BIT1 n + BIT2 m) = BIT2 (SUC (n + m))) /\
           (SUC (BIT2 n + BIT1 m) = BIT2 (SUC (n + m))) /\
           (SUC (BIT2 n + BIT2 m) = BIT1 (numeral$iiSUC (n + m))) /\
           (numeral$iiSUC (ZERO + n) = numeral$iiSUC n) /\
           (numeral$iiSUC (n + ZERO) = numeral$iiSUC n) /\
           (numeral$iiSUC (BIT1 n + BIT1 m) = BIT2 (SUC (n + m))) /\
           (numeral$iiSUC (BIT1 n + BIT2 m) = BIT1 (numeral$iiSUC (n + m))) /\
           (numeral$iiSUC (BIT2 n + BIT1 m) = BIT1 (numeral$iiSUC (n + m))) /\
           (numeral$iiSUC (BIT2 n + BIT2 m) = BIT2 (numeral$iiSUC (n + m)))
   
   [numeral_distrib]  Theorem
      
      |- (!n. 0 + n = n) /\ (!n. n + 0 = n) /\
         (!n m. NUMERAL n + NUMERAL m = NUMERAL (numeral$iZ (n + m))) /\
         (!n. 0 * n = 0) /\ (!n. n * 0 = 0) /\
         (!n m. NUMERAL n * NUMERAL m = NUMERAL (n * m)) /\ (!n. 0 - n = 0) /\
         (!n. n - 0 = n) /\ (!n m. NUMERAL n - NUMERAL m = NUMERAL (n - m)) /\
         (!n. 0 ** NUMERAL (BIT1 n) = 0) /\ (!n. 0 ** NUMERAL (BIT2 n) = 0) /\
         (!n. n ** 0 = 1) /\ (!n m. NUMERAL n ** NUMERAL m = NUMERAL (n ** m)) /\
         (SUC 0 = 1) /\ (!n. SUC (NUMERAL n) = NUMERAL (SUC n)) /\ (PRE 0 = 0) /\
         (!n. PRE (NUMERAL n) = NUMERAL (PRE n)) /\
         (!n. (NUMERAL n = 0) = (n = ZERO)) /\ (!n. (0 = NUMERAL n) = (n = ZERO)) /\
         (!n m. (NUMERAL n = NUMERAL m) = (n = m)) /\ (!n. n < 0 = F) /\
         (!n. 0 < NUMERAL n = ZERO < n) /\ (!n m. NUMERAL n < NUMERAL m = n < m) /\
         (!n. 0 > n = F) /\ (!n. NUMERAL n > 0 = ZERO < n) /\
         (!n m. NUMERAL n > NUMERAL m = m < n) /\ (!n. 0 <= n = T) /\
         (!n. NUMERAL n <= 0 = n <= ZERO) /\
         (!n m. NUMERAL n <= NUMERAL m = n <= m) /\ (!n. n >= 0 = T) /\
         (!n. 0 >= n = (n = 0)) /\ (!n m. NUMERAL n >= NUMERAL m = m <= n) /\
         (!n. ODD (NUMERAL n) = ODD n) /\ (!n. EVEN (NUMERAL n) = EVEN n) /\
         ~ODD 0 /\ EVEN 0
   
   [numeral_div2]  Theorem
      
      |- (DIV2 0 = 0) /\ (!n. DIV2 (NUMERAL (BIT1 n)) = NUMERAL n) /\
         !n. DIV2 (NUMERAL (BIT2 n)) = NUMERAL (SUC n)
   
   [numeral_eq]  Theorem
      
      |- !n m.
           ((ZERO = BIT1 n) = F) /\ ((BIT1 n = ZERO) = F) /\ ((ZERO = BIT2 n) = F) /\
           ((BIT2 n = ZERO) = F) /\ ((BIT1 n = BIT2 m) = F) /\
           ((BIT2 n = BIT1 m) = F) /\ ((BIT1 n = BIT1 m) = (n = m)) /\
           ((BIT2 n = BIT2 m) = (n = m))
   
   [numeral_evenodd]  Theorem
      
      |- !n.
           EVEN ZERO /\ EVEN (BIT2 n) /\ ~EVEN (BIT1 n) /\ ~ODD ZERO /\
           ~ODD (BIT2 n) /\ ODD (BIT1 n)
   
   [numeral_exp]  Theorem
      
      |- (!n. n ** ZERO = BIT1 ZERO) /\
         (!n m. n ** BIT1 m = n * numeral$iSQR (n ** m)) /\
         !n m. n ** BIT2 m = numeral$iSQR n * numeral$iSQR (n ** m)
   
   [numeral_fact]  Theorem
      
      |- (FACT 0 = 1) /\
         (!n.
            FACT (NUMERAL (BIT1 n)) =
            NUMERAL (BIT1 n) * FACT (PRE (NUMERAL (BIT1 n)))) /\
         !n. FACT (NUMERAL (BIT2 n)) = NUMERAL (BIT2 n) * FACT (NUMERAL (BIT1 n))
   
   [numeral_funpow]  Theorem
      
      |- (FUNPOW f 0 x = x) /\
         (FUNPOW f (NUMERAL (BIT1 n)) x = FUNPOW f (PRE (NUMERAL (BIT1 n))) (f x)) /\
         (FUNPOW f (NUMERAL (BIT2 n)) x = FUNPOW f (NUMERAL (BIT1 n)) (f x))
   
   [numeral_iisuc]  Theorem
      
      |- (numeral$iiSUC ZERO = BIT2 ZERO) /\
         (numeral$iiSUC (BIT1 n) = BIT1 (SUC n)) /\
         (numeral$iiSUC (BIT2 n) = BIT2 (SUC n))
   
   [numeral_imod_2exp]  Theorem
      
      |- (!n. numeral$iMOD_2EXP 0 n = ZERO) /\
         (!x n. numeral$iMOD_2EXP x ZERO = ZERO) /\
         (!x n.
            numeral$iMOD_2EXP (NUMERAL (BIT1 x)) (BIT1 n) =
            BIT1 (numeral$iMOD_2EXP (NUMERAL (BIT1 x) - 1) n)) /\
         (!x n.
            numeral$iMOD_2EXP (NUMERAL (BIT2 x)) (BIT1 n) =
            BIT1 (numeral$iMOD_2EXP (NUMERAL (BIT1 x)) n)) /\
         (!x n.
            numeral$iMOD_2EXP (NUMERAL (BIT1 x)) (BIT2 n) =
            numeral$iDUB (numeral$iMOD_2EXP (NUMERAL (BIT1 x) - 1) (SUC n))) /\
         !x n.
           numeral$iMOD_2EXP (NUMERAL (BIT2 x)) (BIT2 n) =
           numeral$iDUB (numeral$iMOD_2EXP (NUMERAL (BIT1 x)) (SUC n))
   
   [numeral_lt]  Theorem
      
      |- !n m.
           (ZERO < BIT1 n = T) /\ (ZERO < BIT2 n = T) /\ (n < ZERO = F) /\
           (BIT1 n < BIT1 m = n < m) /\ (BIT2 n < BIT2 m = n < m) /\
           (BIT1 n < BIT2 m = ~(m < n)) /\ (BIT2 n < BIT1 m = n < m)
   
   [numeral_lte]  Theorem
      
      |- !n m.
           (ZERO <= n = T) /\ (BIT1 n <= ZERO = F) /\ (BIT2 n <= ZERO = F) /\
           (BIT1 n <= BIT1 m = n <= m) /\ (BIT1 n <= BIT2 m = n <= m) /\
           (BIT2 n <= BIT1 m = ~(m <= n)) /\ (BIT2 n <= BIT2 m = n <= m)
   
   [numeral_mult]  Theorem
      
      |- !n m.
           (ZERO * n = ZERO) /\ (n * ZERO = ZERO) /\
           (BIT1 n * m = numeral$iZ (numeral$iDUB (n * m) + m)) /\
           (BIT2 n * m = numeral$iDUB (numeral$iZ (n * m + m)))
   
   [numeral_pre]  Theorem
      
      |- (PRE ZERO = ZERO) /\ (PRE (BIT1 ZERO) = ZERO) /\
         (!n. PRE (BIT1 (BIT1 n)) = BIT2 (PRE (BIT1 n))) /\
         (!n. PRE (BIT1 (BIT2 n)) = BIT2 (BIT1 n)) /\ !n. PRE (BIT2 n) = BIT1 n
   
   [numeral_sub]  Theorem
      
      |- !n m. NUMERAL (n - m) = (if m < n then NUMERAL (numeral$iSUB T n m) else 0)
   
   [numeral_suc]  Theorem
      
      |- (SUC ZERO = BIT1 ZERO) /\ (!n. SUC (BIT1 n) = BIT2 n) /\
         !n. SUC (BIT2 n) = BIT1 (SUC n)
   
   
*)
end