Theory "numposrep"

Signature

Definitions

l2n_def

|- (∀b. l2n b [] = 0) ∧ ∀b h t. l2n b (h::t) = h MOD b + b * l2n b t

n2l_tupled_primitive_def

|- n2l_tupled =
   WFREC (@R. WF R ∧ ∀b n. ¬(n < b ∨ b < 2) ⇒ R (b,n DIV b) (b,n))
     (λn2l_tupled a.
        case a of
          (b,n) =>
            I
              (if n < b ∨ b < 2 then [n MOD b]
               else n MOD b::n2l_tupled (b,n DIV b)))

n2l_curried_def

|- ∀x x1. n2l x x1 = n2l_tupled (x,x1)

num_from_bin_list_def

|- num_from_bin_list = l2n 2

num_from_oct_list_def

|- num_from_oct_list = l2n 8

num_from_dec_list_def

|- num_from_dec_list = l2n 10

num_from_hex_list_def

|- num_from_hex_list = l2n 16

num_to_bin_list_def

|- num_to_bin_list = n2l 2

num_to_oct_list_def

|- num_to_oct_list = n2l 8

num_to_dec_list_def

|- num_to_dec_list = n2l 10

num_to_hex_list_def

|- num_to_hex_list = n2l 16

BOOLIFY_def

|- (∀m a. BOOLIFY 0 m a = a) ∧
   ∀n m a. BOOLIFY (SUC n) m a = BOOLIFY n (DIV2 m) (ODD m::a)

l2n2

|- numposrep$l2n2 = l2n 2

Theorems

n2l_ind

|- ∀P. (∀b n. (¬(n < b ∨ b < 2) ⇒ P b (n DIV b)) ⇒ P b n) ⇒ ∀v v1. P v v1

n2l_def

|- ∀n b.
     n2l b n = if n < b ∨ b < 2 then [n MOD b] else n MOD b::n2l b (n DIV b)

LENGTH_n2l

|- ∀b n. 1 < b ⇒ (LENGTH (n2l b n) = if n = 0 then 1 else SUC (LOG b n))

l2n_n2l

|- ∀b n. 1 < b ⇒ (l2n b (n2l b n) = n)

l2n_lt

|- ∀l b. 0 < b ⇒ l2n b l < b ** LENGTH l

LENGTH_l2n

|- ∀b l.
     1 < b ∧ EVERY ($> b) l ∧ l2n b l ≠ 0 ⇒ SUC (LOG b (l2n b l)) ≤ LENGTH l

EL_TAKE

|- ∀x n l. x < n ∧ n ≤ LENGTH l ⇒ (EL x (TAKE n l) = EL x l)

l2n_DIGIT

|- ∀b l x.
     1 < b ∧ EVERY ($> b) l ∧ x < LENGTH l ⇒
     ((l2n b l DIV b ** x) MOD b = EL x l)

DIV_0_IMP_LT

|- ∀b n. 1 < b ∧ (n DIV b = 0) ⇒ n < b

EL_n2l

|- ∀b x n.
     1 < b ∧ x < LENGTH (n2l b n) ⇒ (EL x (n2l b n) = (n DIV b ** x) MOD b)

n2l_l2n

|- ∀b l.
     1 < b ∧ EVERY ($> b) l ⇒
     (n2l b (l2n b l) =
      if l2n b l = 0 then [0] else TAKE (SUC (LOG b (l2n b l))) l)

l2n_eq_0

|- ∀b. 0 < b ⇒ ∀l. (l2n b l = 0) ⇔ EVERY ($= 0 o combin$C $MOD b) l

l2n_SNOC_0

|- ∀b ls. 0 < b ⇒ (l2n b (SNOC 0 ls) = l2n b ls)

LOG_l2n

|- ∀b.
     1 < b ⇒
     ∀l.
       l ≠ [] ∧ 0 < LAST l ∧ EVERY ($> b) l ⇒
       (LOG b (l2n b l) = PRE (LENGTH l))

l2n_dropWhile_0

|- ∀b ls. 0 < b ⇒ (l2n b (REVERSE (dropWhile ($= 0) (REVERSE ls))) = l2n b ls)

LOG_l2n_dropWhile

|- ∀b l.
     1 < b ∧ EXISTS (λy. 0 ≠ y) l ∧ EVERY ($> b) l ⇒
     (LOG b (l2n b l) = PRE (LENGTH (dropWhile ($= 0) (REVERSE l))))

n2l_BOUND

|- ∀b n. 0 < b ⇒ EVERY ($> b) (n2l b n)

l2n_pow2_compute

|- (∀p. l2n (2 ** p) [] = 0) ∧
   ∀p h t. l2n (2 ** p) (h::t) = MOD_2EXP p h + TIMES_2EXP p (l2n (2 ** p) t)

n2l_pow2_compute

|- ∀p n.
     0 < p ⇒
     (n2l (2 ** p) n =
      (let (q,r) = DIVMOD_2EXP p n
       in
         if q = 0 then [r] else r::n2l (2 ** p) q))

l2n_2_thms

|- (∀t. l2n 2 (0::t) = NUMERAL (numposrep$l2n2 (0::t))) ∧
   (∀t. l2n 2 (1::t) = NUMERAL (numposrep$l2n2 (1::t))) ∧
   (numposrep$l2n2 [] = ZERO) ∧
   (∀t. numposrep$l2n2 (0::t) = numeral$iDUB (numposrep$l2n2 t)) ∧
   ∀t. numposrep$l2n2 (1::t) = BIT1 (numposrep$l2n2 t)

BIT_num_from_bin_list

|- ∀x l.
     EVERY ($> 2) l ∧ x < LENGTH l ⇒
     (BIT x (num_from_bin_list l) ⇔ (EL x l = 1))

EL_num_to_bin_list

|- ∀x n.
     x < LENGTH (num_to_bin_list n) ⇒ (EL x (num_to_bin_list n) = BITV n x)

num_bin_list

|- num_from_bin_list o num_to_bin_list = I

num_oct_list

|- num_from_oct_list o num_to_oct_list = I

num_dec_list

|- num_from_dec_list o num_to_dec_list = I

num_hex_list

|- num_from_hex_list o num_to_hex_list = I