Theory ASCIInumbers

⊢ ∀n. HEX n =
      if n < 10 then CHR (ORD #"0" + n)
      else if n < 16 then CHR (ORD #"A" + (n − 10))
      else #"\^@"

⊢ ∀c. UNHEX c =
      (let
         n = ORD c
       in
         if ORD #"0" ≤ n ∧ n ≤ ORD #"9" then n − ORD #"0"
         else if ORD #"a" ≤ n ∧ n ≤ ORD #"f" then 10 + n − ORD #"a"
         else if ORD #"A" ≤ n ∧ n ≤ ORD #"F" then 10 + n − ORD #"A"
         else 0)

⊢ ∀s. fromBinString s =
      if s ≠ "" ∧ EVERY (λc. c = #"0" ∨ c = #"1") s then
        SOME (num_from_bin_string s)
      else NONE

⊢ ∀s. fromDecString s =
      if s ≠ "" ∧ EVERY isDigit s then SOME (toNum s) else NONE

⊢ ∀s. fromHexString s =
      if s ≠ "" ∧ EVERY isHexDigit s then SOME (num_from_hex_string s)
      else NONE

⊢ ∀b f n. n2s b f n = REVERSE (MAP f (n2l b n))

⊢ num_from_bin_string = s2n 2 UNHEX

⊢ toNum = s2n 10 UNHEX

⊢ num_from_hex_string = s2n 16 UNHEX

⊢ num_from_oct_string = s2n 8 UNHEX

⊢ num_to_bin_string = n2s 2 HEX

⊢ toString = n2s 10 HEX

⊢ num_to_hex_string = n2s 16 HEX

⊢ num_to_oct_string = n2s 8 HEX

⊢ ∀b f s. s2n b f s = l2n b (MAP f (REVERSE s))

⊢ ∀x s.
    EVERY ($> 2 ∘ UNHEX) s ∧ x < STRLEN s ⇒
    (BIT x (num_from_bin_string s) ⇔ UNHEX (SUB (s,PRE (STRLEN s − x))) = 1)

⊢ ∀c. isDigit c ⇒ HEX (UNHEX c) = c

⊢ ∀n. EVERY isDigit (toString n)

⊢ ∀n. EVERY (λc. isHexDigit c ∧ (isAlpha c ⇒ isUpper c))
        (num_to_hex_string n)

⊢ ∀c. isHexDigit c ⇒ HEX (UNHEX c) = toUpper c

⊢ HEX 0 = #"0" ∧ HEX 1 = #"1" ∧ HEX 2 = #"2" ∧ HEX 3 = #"3" ∧
  HEX 4 = #"4" ∧ HEX 5 = #"5" ∧ HEX 6 = #"6" ∧ HEX 7 = #"7" ∧
  HEX 8 = #"8" ∧ HEX 9 = #"9" ∧ HEX 10 = #"A" ∧ HEX 11 = #"B" ∧
  HEX 12 = #"C" ∧ HEX 13 = #"D" ∧ HEX 14 = #"E" ∧ HEX 15 = #"F"

⊢ STRLEN (num_to_bin_string n) = if n = 0 then 1 else LOG2 n + 1

⊢ STRLEN (toString n) = if n = 0 then 1 else LOG 10 n + 1

⊢ STRLEN (num_to_hex_string n) = if n = 0 then 1 else LOG 16 n + 1

⊢ STRLEN (num_to_oct_string n) = if n = 0 then 1 else LOG 8 n + 1

⊢ ∀n m s. STRCAT s (toString n) = STRCAT s (toString m) ⇔ n = m

⊢ ∀x n.
    x < STRLEN (num_to_bin_string n) ⇒
    SUB (num_to_bin_string n,x) =
    HEX (BITV n (PRE (STRLEN (num_to_bin_string n) − x)))

⊢ ∀n. n < 16 ⇒ UNHEX (HEX n) = n

⊢ UNHEX #"0" = 0 ∧ UNHEX #"1" = 1 ∧ UNHEX #"2" = 2 ∧ UNHEX #"3" = 3 ∧
  UNHEX #"4" = 4 ∧ UNHEX #"5" = 5 ∧ UNHEX #"6" = 6 ∧ UNHEX #"7" = 7 ∧
  UNHEX #"8" = 8 ∧ UNHEX #"9" = 9 ∧ UNHEX #"a" = 10 ∧ UNHEX #"b" = 11 ∧
  UNHEX #"c" = 12 ∧ UNHEX #"d" = 13 ∧ UNHEX #"e" = 14 ∧ UNHEX #"f" = 15 ∧
  UNHEX #"A" = 10 ∧ UNHEX #"B" = 11 ∧ UNHEX #"C" = 12 ∧ UNHEX #"D" = 13 ∧
  UNHEX #"E" = 14 ∧ UNHEX #"F" = 15

⊢ ∀n. n < 10 ⇒ isDigit (HEX n)

⊢ ∀n. n < 16 ⇒ isHexDigit (HEX n) ∧ (isAlpha (HEX n) ⇒ isUpper (HEX n))

⊢ n2s b f n = IMPLODE (REVERSE (MAP f (n2l b n)))

⊢ ∀c2n n2c b s.
    1 < b ∧ EVERY ($> b ∘ c2n) s ⇒
    n2s b n2c (s2n b c2n s) =
    if s2n b c2n s = 0 then STRING (n2c 0) ""
    else MAP (n2c ∘ c2n) (LASTN (SUC (LOG b (s2n b c2n s))) s)

⊢ num_from_bin_string ∘ num_to_bin_string = I

⊢ toNum ∘ toString = I

⊢ num_from_bin_string (STRING #"0" t) = num_from_bin_string t ∧
  num_from_oct_string (STRING #"0" t) = num_from_oct_string t ∧
  toNum (STRING #"0" t) = toNum t ∧
  num_from_hex_string (STRING #"0" t) = num_from_hex_string t

⊢ num_from_hex_string ∘ num_to_hex_string = I

⊢ num_from_oct_string ∘ num_to_oct_string = I

⊢ num_to_bin_string n ≠ ""

⊢ toString = n2lA "" HEX 10

⊢ toString n ≠ ""

⊢ num_to_hex_string n ≠ ""

⊢ num_to_oct_string n ≠ ""

⊢ s2n b f s = l2n b (MAP f (REVERSE (EXPLODE s)))

⊢ 0 < b ⇒ s2n b UNHEX (STRING #"0" t) = s2n b UNHEX t

⊢ ∀c2n n2c b n.
    1 < b ∧ (∀x. x < b ⇒ c2n (n2c x) = x) ⇒ s2n b c2n (n2s b n2c n) = n

⊢ ∀n. toNum (toString n) = n

⊢ ∀n m. toString n = toString m ⇔ n = m

⊢ ∀n m. toString n = toString m ⇔ n = m

⊢ ∀n. toNum (toString n) = n