Theory "numposrep"

Signature

Definitions

num_to_oct_list_def

⊢ num_to_oct_list = n2l 8

num_to_hex_list_def

⊢ num_to_hex_list = n2l 16

num_to_dec_list_def

⊢ num_to_dec_list = n2l 10

num_to_bin_list_def

⊢ num_to_bin_list = n2l 2

num_from_oct_list_def

⊢ num_from_oct_list = l2n 8

num_from_hex_list_def

⊢ num_from_hex_list = l2n 16

num_from_dec_list_def

⊢ num_from_dec_list = l2n 10

num_from_bin_list_def

⊢ num_from_bin_list = l2n 2

l2n_def

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

l2n2

⊢ numposrep$l2n2 = l2n 2

BOOLIFY_def

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

Theorems

num_oct_list

⊢ num_from_oct_list ∘ num_to_oct_list = I

num_hex_list

⊢ num_from_hex_list ∘ num_to_hex_list = I

num_dec_list

⊢ num_from_dec_list ∘ num_to_dec_list = I

num_bin_list

⊢ num_from_bin_list ∘ num_to_bin_list = I

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))

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)

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)

n2l_BOUND

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

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))))

LOG_l2n

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

LENGTH_n2l

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

LENGTH_l2n

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

l2n_SNOC_0

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

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)

l2n_n2l

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

l2n_lt

⊢ ∀l b. 0 < b ⇒ l2n b l < b ** LENGTH l

l2n_eq_0

⊢ ∀b. 0 < b ⇒ ∀l. (l2n b l = 0) ⇔ EVERY ($= 0 ∘ combin$C $MOD b) l

l2n_dropWhile_0

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

l2n_DIGIT

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

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)

EL_num_to_bin_list

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

EL_n2l

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

BIT_num_from_bin_list

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