- 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
- 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 ∘ 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)
- 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 ∘ 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 ∘ num_to_bin_string = I
- num_oct_string
-
⊢ num_from_oct_string ∘ num_to_oct_string = I
- num_dec_string
-
⊢ toNum ∘ toString = I
- num_hex_string
-
⊢ num_from_hex_string ∘ num_to_hex_string = I