Theory "ASCIInumbers"

Signature

Definitions

UNHEX_primitive_def

⊢ UNHEX =
  WFREC (@R. WF R)
    (λUNHEX a.
         case a of
           #"0" => I 0
         | #"1" => I 1
         | #"2" => I 2
         | #"3" => I 3
         | #"4" => I 4
         | #"5" => I 5
         | #"6" => I 6
         | #"7" => I 7
         | #"8" => I 8
         | #"9" => I 9
         | #"a" => I 10
         | #"b" => I 11
         | #"c" => I 12
         | #"d" => I 13
         | #"e" => I 14
         | #"f" => I 15
         | #"A" => I 10
         | #"B" => I 11
         | #"C" => I 12
         | #"D" => I 13
         | #"E" => I 14
         | #"F" => I 15
         | v => ARB)

s2n_def

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

num_to_oct_string_def

⊢ num_to_oct_string = n2s 8 HEX

num_to_hex_string_def

⊢ num_to_hex_string = n2s 16 HEX

num_to_dec_string_def

⊢ toString = n2s 10 HEX

num_to_bin_string_def

⊢ num_to_bin_string = n2s 2 HEX

num_from_oct_string_def

⊢ num_from_oct_string = s2n 8 UNHEX

num_from_hex_string_def

⊢ num_from_hex_string = s2n 16 UNHEX

num_from_dec_string_def

⊢ toNum = s2n 10 UNHEX

num_from_bin_string_def

⊢ num_from_bin_string = s2n 2 UNHEX

n2s_def

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

HEX_primitive_def

⊢ HEX =
  WFREC (@R. WF R)
    (λHEX a.
         case a of
           0 => I #"0"
         | 1 => I #"1"
         | 2 => I #"2"
         | 3 => I #"3"
         | 4 => I #"4"
         | 5 => I #"5"
         | 6 => I #"6"
         | 7 => I #"7"
         | 8 => I #"8"
         | 9 => I #"9"
         | 10 => I #"A"
         | 11 => I #"B"
         | 12 => I #"C"
         | 13 => I #"D"
         | 14 => I #"E"
         | 15 => I #"F"
         | v => ARB)

fromHexString_def

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

fromDecString_def

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

fromBinString_def

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

Theorems

UNHEX_ind

⊢ ∀P.
      P #"0" ∧ P #"1" ∧ P #"2" ∧ P #"3" ∧ P #"4" ∧ P #"5" ∧ P #"6" ∧ P #"7" ∧
      P #"8" ∧ P #"9" ∧ P #"a" ∧ P #"b" ∧ P #"c" ∧ P #"d" ∧ P #"e" ∧ P #"f" ∧
      P #"A" ∧ P #"B" ∧ P #"C" ∧ P #"D" ∧ P #"E" ∧ P #"F" ∧ (∀v24. P v24) ⇒
      ∀v. P v

UNHEX_HEX

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

UNHEX_def

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

toString_toNum_cancel

⊢ ∀n. toNum (toString n) = n

toString_inj

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

toString_11

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

toNum_toString

⊢ ∀n. toNum (toString n) = n

SUB_num_to_bin_string

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

STRCAT_toString_inj

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

s2n_n2s

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

s2n_compute

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

num_to_oct_string_nil

⊢ num_to_oct_string n ≠ ""

num_to_hex_string_nil

⊢ num_to_hex_string n ≠ ""

num_to_dec_string_nil

⊢ toString n ≠ ""

num_to_bin_string_nil

⊢ num_to_bin_string n ≠ ""

num_oct_string

⊢ num_from_oct_string ∘ num_to_oct_string = I

num_hex_string

⊢ num_from_hex_string ∘ num_to_hex_string = I

num_dec_string

⊢ toNum ∘ toString = I

num_bin_string

⊢ num_from_bin_string ∘ num_to_bin_string = I

n2s_s2n

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

n2s_compute

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

isHexDigit_HEX

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

isDigit_HEX

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

HEX_UNHEX

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

HEX_ind

⊢ ∀P.
      P 0 ∧ P 1 ∧ P 2 ∧ P 3 ∧ P 4 ∧ P 5 ∧ P 6 ∧ P 7 ∧ P 8 ∧ P 9 ∧ P 10 ∧
      P 11 ∧ P 12 ∧ P 13 ∧ P 14 ∧ P 15 ∧ (∀v18. P v18) ⇒
      ∀v. P v

HEX_def

⊢ (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")

EVERY_isHexDigit_num_to_hex_string

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

EVERY_isDigit_num_to_dec_string

⊢ ∀n. EVERY isDigit (toString n)

DEC_UNDEC

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

BIT_num_from_bin_string

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