Theory "ASCIInumbers"

Signature

Definitions

s2n_def

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

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)

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)

num_from_bin_string_def

|- num_from_bin_string = s2n 2 UNHEX

num_from_oct_string_def

|- num_from_oct_string = s2n 8 UNHEX

num_from_dec_string_def

|- toNum = s2n 10 UNHEX

num_from_hex_string_def

|- num_from_hex_string = s2n 16 UNHEX

num_to_bin_string_def

|- num_to_bin_string = n2s 2 HEX

num_to_oct_string_def

|- num_to_oct_string = n2s 8 HEX

num_to_dec_string_def

|- toString = n2s 10 HEX

num_to_hex_string_def

|- num_to_hex_string = n2s 16 HEX

fromBinString_def

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

fromDecString_def

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

fromHexString_def

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

Theorems

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

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

s2n_compute

|- s2n b f s = l2n b (MAP f (REVERSE (EXPLODE s)))

n2s_compute

|- n2s b f n = IMPLODE (REVERSE (MAP f (n2l b n)))

UNHEX_HEX

|- ∀n. n < 16 ⇒ (UNHEX (HEX n) = n)

HEX_UNHEX

|- ∀c. isHexDigit c ⇒ (HEX (UNHEX c) = toUpper c)

DEC_UNDEC

|- ∀c. isDigit c ⇒ (HEX (UNHEX c) = c)

s2n_n2s

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

n2s_s2n

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

toNum_toString

|- ∀n. toNum (toString n) = n

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)

STRCAT_toString_inj

|- ∀n m s. (STRCAT s (toString n) = STRCAT s (toString m)) ⇔ (n = m)

BIT_num_from_bin_string

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

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

num_bin_string

|- num_from_bin_string o num_to_bin_string = I

num_oct_string

|- num_from_oct_string o num_to_oct_string = I

num_dec_string

|- toNum o toString = I

num_hex_string

|- num_from_hex_string o num_to_hex_string = I