Theory: numeral

Parents

• arithmetic

Types

Constants

• iDUB  :num -> num
• iSQR  :num -> num
• iSUB  :bool -> num -> num -> num
• iZ  :num -> num
• iBIT_cases  :num -> 'a -> (num -> 'a) -> (num -> 'a) -> 'a
• iiSUC  :num -> num

Definitions

iBIT_cases

|- (!zf bf1 bf2. iBIT_cases ALT_ZERO zf bf1 bf2 = zf) /\
   (!n zf bf1 bf2. iBIT_cases (NUMERAL_BIT1 n) zf bf1 bf2 = bf1 n) /\
   !n zf bf1 bf2. iBIT_cases (NUMERAL_BIT2 n) zf bf1 bf2 = bf2 n

iDUB

|- !x. iDUB x = x + x

iiSUC

|- !n. iiSUC n = SUC (SUC n)

iSQR

|- !x. iSQR x = x * x

iSUB_DEF

|- (!b x. iSUB b ALT_ZERO x = ALT_ZERO) /\
   (!b n x.
      iSUB b (NUMERAL_BIT1 n) x =
      (if b then
         iBIT_cases x (NUMERAL_BIT1 n) (\m. iDUB (iSUB T n m))
           (\m. NUMERAL_BIT1 (iSUB F n m))
       else
         iBIT_cases x (iDUB n) (\m. NUMERAL_BIT1 (iSUB F n m))
           (\m. iDUB (iSUB F n m)))) /\
   !b n x.
     iSUB b (NUMERAL_BIT2 n) x =
     (if b then
        iBIT_cases x (NUMERAL_BIT2 n) (\m. NUMERAL_BIT1 (iSUB T n m))
          (\m. iDUB (iSUB T n m))
      else
        iBIT_cases x (NUMERAL_BIT1 n) (\m. iDUB (iSUB T n m))
          (\m. NUMERAL_BIT1 (iSUB F n m)))

iZ

|- !x. iZ x = x

Theorems

bit_initiality

|- !zf b1f b2f.
     ?f.
       (f ALT_ZERO = zf) /\ (!n. f (NUMERAL_BIT1 n) = b1f n (f n)) /\
       !n. f (NUMERAL_BIT2 n) = b2f n (f n)

iDUB_removal

|- !n.
     (iDUB (NUMERAL_BIT1 n) = NUMERAL_BIT2 (iDUB n)) /\
     (iDUB (NUMERAL_BIT2 n) = NUMERAL_BIT2 (NUMERAL_BIT1 n)) /\
     (iDUB ALT_ZERO = ALT_ZERO)

iSUB_THM

|- !b n m.
     (iSUB b ALT_ZERO x = ALT_ZERO) /\ (iSUB T n ALT_ZERO = n) /\
     (iSUB F (NUMERAL_BIT1 n) ALT_ZERO = iDUB n) /\
     (iSUB T (NUMERAL_BIT1 n) (NUMERAL_BIT1 m) = iDUB (iSUB T n m)) /\
     (iSUB F (NUMERAL_BIT1 n) (NUMERAL_BIT1 m) = NUMERAL_BIT1 (iSUB F n m)) /\
     (iSUB T (NUMERAL_BIT1 n) (NUMERAL_BIT2 m) = NUMERAL_BIT1 (iSUB F n m)) /\
     (iSUB F (NUMERAL_BIT1 n) (NUMERAL_BIT2 m) = iDUB (iSUB F n m)) /\
     (iSUB F (NUMERAL_BIT2 n) ALT_ZERO = NUMERAL_BIT1 n) /\
     (iSUB T (NUMERAL_BIT2 n) (NUMERAL_BIT1 m) = NUMERAL_BIT1 (iSUB T n m)) /\
     (iSUB F (NUMERAL_BIT2 n) (NUMERAL_BIT1 m) = iDUB (iSUB T n m)) /\
     (iSUB T (NUMERAL_BIT2 n) (NUMERAL_BIT2 m) = iDUB (iSUB T n m)) /\
     (iSUB F (NUMERAL_BIT2 n) (NUMERAL_BIT2 m) = NUMERAL_BIT1 (iSUB F n m))

numeral_add

|- !n m.
     (iZ (ALT_ZERO + n) = n) /\ (iZ (n + ALT_ZERO) = n) /\
     (iZ (NUMERAL_BIT1 n + NUMERAL_BIT1 m) = NUMERAL_BIT2 (iZ (n + m))) /\
     (iZ (NUMERAL_BIT1 n + NUMERAL_BIT2 m) = NUMERAL_BIT1 (SUC (n + m))) /\
     (iZ (NUMERAL_BIT2 n + NUMERAL_BIT1 m) = NUMERAL_BIT1 (SUC (n + m))) /\
     (iZ (NUMERAL_BIT2 n + NUMERAL_BIT2 m) = NUMERAL_BIT2 (SUC (n + m))) /\
     (SUC (ALT_ZERO + n) = SUC n) /\ (SUC (n + ALT_ZERO) = SUC n) /\
     (SUC (NUMERAL_BIT1 n + NUMERAL_BIT1 m) = NUMERAL_BIT1 (SUC (n + m))) /\
     (SUC (NUMERAL_BIT1 n + NUMERAL_BIT2 m) = NUMERAL_BIT2 (SUC (n + m))) /\
     (SUC (NUMERAL_BIT2 n + NUMERAL_BIT1 m) = NUMERAL_BIT2 (SUC (n + m))) /\
     (SUC (NUMERAL_BIT2 n + NUMERAL_BIT2 m) = NUMERAL_BIT1 (iiSUC (n + m))) /\
     (iiSUC (ALT_ZERO + n) = iiSUC n) /\ (iiSUC (n + ALT_ZERO) = iiSUC n) /\
     (iiSUC (NUMERAL_BIT1 n + NUMERAL_BIT1 m) = NUMERAL_BIT2 (SUC (n + m))) /\
     (iiSUC (NUMERAL_BIT1 n + NUMERAL_BIT2 m) =
      NUMERAL_BIT1 (iiSUC (n + m))) /\
     (iiSUC (NUMERAL_BIT2 n + NUMERAL_BIT1 m) =
      NUMERAL_BIT1 (iiSUC (n + m))) /\
     (iiSUC (NUMERAL_BIT2 n + NUMERAL_BIT2 m) = NUMERAL_BIT2 (iiSUC (n + m)))

numeral_distrib

|- (!n. 0 + n = n) /\ (!n. n + 0 = n) /\
   (!n m. NUMERAL n + NUMERAL m = 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 (NUMERAL_BIT1 n) = 0) /\
   (!n. 0 ** NUMERAL (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 = ALT_ZERO)) /\
   (!n. (0 = NUMERAL n) = (n = ALT_ZERO)) /\
   (!n m. (NUMERAL n = NUMERAL m) = (n = m)) /\ (!n. n < 0 = F) /\
   (!n. 0 < NUMERAL n = ALT_ZERO < n) /\
   (!n m. NUMERAL n < NUMERAL m = n < m) /\ (!n. 0 > n = F) /\
   (!n. NUMERAL n > 0 = ALT_ZERO < n) /\
   (!n m. NUMERAL n > NUMERAL m = m < n) /\ (!n. 0 <= n = T) /\
   (!n. NUMERAL n <= 0 = n <= ALT_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_eq

|- !n m.
     ((ALT_ZERO = NUMERAL_BIT1 n) = F) /\ ((NUMERAL_BIT1 n = ALT_ZERO) = F) /\
     ((ALT_ZERO = NUMERAL_BIT2 n) = F) /\ ((NUMERAL_BIT2 n = ALT_ZERO) = F) /\
     ((NUMERAL_BIT1 n = NUMERAL_BIT2 m) = F) /\
     ((NUMERAL_BIT2 n = NUMERAL_BIT1 m) = F) /\
     ((NUMERAL_BIT1 n = NUMERAL_BIT1 m) = (n = m)) /\
     ((NUMERAL_BIT2 n = NUMERAL_BIT2 m) = (n = m))

numeral_evenodd

|- !n.
     EVEN ALT_ZERO /\ EVEN (NUMERAL_BIT2 n) /\ ~EVEN (NUMERAL_BIT1 n) /\
     ~ODD ALT_ZERO /\ ~ODD (NUMERAL_BIT2 n) /\ ODD (NUMERAL_BIT1 n)

numeral_exp

|- (!n. n ** ALT_ZERO = NUMERAL_BIT1 ALT_ZERO) /\
   (!n m. n ** NUMERAL_BIT1 m = n * iSQR (n ** m)) /\
   !n m. n ** NUMERAL_BIT2 m = iSQR n * iSQR (n ** m)

numeral_iisuc

|- (iiSUC ALT_ZERO = NUMERAL_BIT2 ALT_ZERO) /\
   (iiSUC (NUMERAL_BIT1 n) = NUMERAL_BIT1 (SUC n)) /\
   (iiSUC (NUMERAL_BIT2 n) = NUMERAL_BIT2 (SUC n))

numeral_lt

|- !n m.
     (ALT_ZERO < NUMERAL_BIT1 n = T) /\ (ALT_ZERO < NUMERAL_BIT2 n = T) /\
     (n < ALT_ZERO = F) /\ (NUMERAL_BIT1 n < NUMERAL_BIT1 m = n < m) /\
     (NUMERAL_BIT2 n < NUMERAL_BIT2 m = n < m) /\
     (NUMERAL_BIT1 n < NUMERAL_BIT2 m = ~(m < n)) /\
     (NUMERAL_BIT2 n < NUMERAL_BIT1 m = n < m)

numeral_lte

|- !n m.
     (ALT_ZERO <= n = T) /\ (NUMERAL_BIT1 n <= ALT_ZERO = F) /\
     (NUMERAL_BIT2 n <= ALT_ZERO = F) /\
     (NUMERAL_BIT1 n <= NUMERAL_BIT1 m = n <= m) /\
     (NUMERAL_BIT1 n <= NUMERAL_BIT2 m = n <= m) /\
     (NUMERAL_BIT2 n <= NUMERAL_BIT1 m = ~(m <= n)) /\
     (NUMERAL_BIT2 n <= NUMERAL_BIT2 m = n <= m)

numeral_mult

|- !n m.
     (ALT_ZERO * n = ALT_ZERO) /\ (n * ALT_ZERO = ALT_ZERO) /\
     (NUMERAL_BIT1 n * m = iZ (iDUB (n * m) + m)) /\
     (NUMERAL_BIT2 n * m = iDUB (iZ (n * m + m)))

numeral_pre

|- (PRE ALT_ZERO = ALT_ZERO) /\ (PRE (NUMERAL_BIT1 ALT_ZERO) = ALT_ZERO) /\
   (!n.
      PRE (NUMERAL_BIT1 (NUMERAL_BIT1 n)) =
      NUMERAL_BIT2 (PRE (NUMERAL_BIT1 n))) /\
   (!n.
      PRE (NUMERAL_BIT1 (NUMERAL_BIT2 n)) = NUMERAL_BIT2 (NUMERAL_BIT1 n)) /\
   !n. PRE (NUMERAL_BIT2 n) = NUMERAL_BIT1 n

numeral_sub

|- !n m. NUMERAL (n - m) = (if m < n then NUMERAL (iSUB T n m) else 0)

numeral_suc

|- (SUC ALT_ZERO = NUMERAL_BIT1 ALT_ZERO) /\
   (!n. SUC (NUMERAL_BIT1 n) = NUMERAL_BIT2 n) /\
   !n. SUC (NUMERAL_BIT2 n) = NUMERAL_BIT1 (SUC n)