Structure ASCIInumbersTheory
signature ASCIInumbersTheory =
sig
type thm = Thm.thm
(* Definitions *)
val HEX_primitive_def : thm
val UNHEX_primitive_def : thm
val fromBinString_def : thm
val fromDecString_def : thm
val fromHexString_def : thm
val n2s_def : thm
val num_from_bin_string_def : thm
val num_from_dec_string_def : thm
val num_from_hex_string_def : thm
val num_from_oct_string_def : thm
val num_to_bin_string_def : thm
val num_to_dec_string_def : thm
val num_to_hex_string_def : thm
val num_to_oct_string_def : thm
val s2n_def : thm
(* Theorems *)
val BIT_num_from_bin_string : thm
val DEC_UNDEC : thm
val EVERY_isDigit_num_to_dec_string : thm
val EVERY_isHexDigit_num_to_hex_string : thm
val HEX_UNHEX : thm
val HEX_def : thm
val HEX_ind : thm
val STRCAT_toString_inj : thm
val SUB_num_to_bin_string : thm
val UNHEX_HEX : thm
val UNHEX_def : thm
val UNHEX_ind : thm
val isDigit_HEX : thm
val isHexDigit_HEX : thm
val n2s_compute : thm
val n2s_s2n : thm
val num_bin_string : thm
val num_dec_string : thm
val num_hex_string : thm
val num_oct_string : thm
val num_to_bin_string_nil : thm
val num_to_dec_string_nil : thm
val num_to_hex_string_nil : thm
val num_to_oct_string_nil : thm
val s2n_compute : thm
val s2n_n2s : thm
val toNum_toString : thm
val toString_11 : thm
val toString_inj : thm
val toString_toNum_cancel : thm
val ASCIInumbers_grammars : type_grammar.grammar * term_grammar.grammar
(*
[numposrep] Parent theory of "ASCIInumbers"
[string] Parent theory of "ASCIInumbers"
[HEX_primitive_def] Definition
⊢ 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] Definition
⊢ 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)
[fromBinString_def] Definition
⊢ ∀s. fromBinString s =
if s ≠ "" ∧ EVERY (λc. c = #"0" ∨ c = #"1") s then
SOME (num_from_bin_string s)
else NONE
[fromDecString_def] Definition
⊢ ∀s. fromDecString s =
if s ≠ "" ∧ EVERY isDigit s then SOME (toNum s) else NONE
[fromHexString_def] Definition
⊢ ∀s. fromHexString s =
if s ≠ "" ∧ EVERY isHexDigit s then
SOME (num_from_hex_string s)
else NONE
[n2s_def] Definition
⊢ ∀b f n. n2s b f n = REVERSE (MAP f (n2l b n))
[num_from_bin_string_def] Definition
⊢ num_from_bin_string = s2n 2 UNHEX
[num_from_dec_string_def] Definition
⊢ toNum = s2n 10 UNHEX
[num_from_hex_string_def] Definition
⊢ num_from_hex_string = s2n 16 UNHEX
[num_from_oct_string_def] Definition
⊢ num_from_oct_string = s2n 8 UNHEX
[num_to_bin_string_def] Definition
⊢ num_to_bin_string = n2s 2 HEX
[num_to_dec_string_def] Definition
⊢ toString = n2s 10 HEX
[num_to_hex_string_def] Definition
⊢ num_to_hex_string = n2s 16 HEX
[num_to_oct_string_def] Definition
⊢ num_to_oct_string = n2s 8 HEX
[s2n_def] Definition
⊢ ∀b f s. s2n b f s = l2n b (MAP f (REVERSE s))
[BIT_num_from_bin_string] Theorem
⊢ ∀x s.
EVERY ($> 2 ∘ UNHEX) s ∧ x < STRLEN s ⇒
(BIT x (num_from_bin_string s) ⇔
UNHEX (SUB (s,PRE (STRLEN s − x))) = 1)
[DEC_UNDEC] Theorem
⊢ ∀c. isDigit c ⇒ HEX (UNHEX c) = c
[EVERY_isDigit_num_to_dec_string] Theorem
⊢ ∀n. EVERY isDigit (toString n)
[EVERY_isHexDigit_num_to_hex_string] Theorem
⊢ ∀n. EVERY (λc. isHexDigit c ∧ (isAlpha c ⇒ isUpper c))
(num_to_hex_string n)
[HEX_UNHEX] Theorem
⊢ ∀c. isHexDigit c ⇒ HEX (UNHEX c) = toUpper c
[HEX_def] Theorem
⊢ 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"
[HEX_ind] Theorem
⊢ ∀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
[STRCAT_toString_inj] Theorem
⊢ ∀n m s. STRCAT s (toString n) = STRCAT s (toString m) ⇔ n = m
[SUB_num_to_bin_string] Theorem
⊢ ∀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)))
[UNHEX_HEX] Theorem
⊢ ∀n. n < 16 ⇒ UNHEX (HEX n) = n
[UNHEX_def] Theorem
⊢ 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
[UNHEX_ind] Theorem
⊢ ∀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
[isDigit_HEX] Theorem
⊢ ∀n. n < 10 ⇒ isDigit (HEX n)
[isHexDigit_HEX] Theorem
⊢ ∀n. n < 16 ⇒
isHexDigit (HEX n) ∧ (isAlpha (HEX n) ⇒ isUpper (HEX n))
[n2s_compute] Theorem
⊢ n2s b f n = IMPLODE (REVERSE (MAP f (n2l b n)))
[n2s_s2n] Theorem
⊢ ∀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_bin_string] Theorem
⊢ num_from_bin_string ∘ num_to_bin_string = I
[num_dec_string] Theorem
⊢ toNum ∘ toString = I
[num_hex_string] Theorem
⊢ num_from_hex_string ∘ num_to_hex_string = I
[num_oct_string] Theorem
⊢ num_from_oct_string ∘ num_to_oct_string = I
[num_to_bin_string_nil] Theorem
⊢ num_to_bin_string n ≠ ""
[num_to_dec_string_nil] Theorem
⊢ toString n ≠ ""
[num_to_hex_string_nil] Theorem
⊢ num_to_hex_string n ≠ ""
[num_to_oct_string_nil] Theorem
⊢ num_to_oct_string n ≠ ""
[s2n_compute] Theorem
⊢ s2n b f s = l2n b (MAP f (REVERSE (EXPLODE s)))
[s2n_n2s] Theorem
⊢ ∀c2n n2c b n.
1 < b ∧ (∀x. x < b ⇒ c2n (n2c x) = x) ⇒
s2n b c2n (n2s b n2c n) = n
[toNum_toString] Theorem
⊢ ∀n. toNum (toString n) = n
[toString_11] Theorem
⊢ ∀n m. toString n = toString m ⇔ n = m
[toString_inj] Theorem
⊢ ∀n m. toString n = toString m ⇔ n = m
[toString_toNum_cancel] Theorem
⊢ ∀n. toNum (toString n) = n
*)
end
HOL 4, Kananaskis-14