Theory Lib_Word_toString
theory Lib_Word_toString
imports Lib_Numbers_toString
Word_Lib.Word_Lemmas
begin
context unique_euclidean_semiring_numeral
begin
lemma exp_estimate [simp]:
‹numeral Num.One ≤ 2 ^ n› (is ‹?P1›)
‹numeral Num.One < 2 ^ n ⟷ 1 ≤ n› (is ‹?P2›)
‹numeral (Num.Bit0 k) ≤ 2 ^ n ⟷ 1 ≤ n ∧ numeral k ≤ 2 ^ (n - 1)› (is ‹?P3›)
‹numeral (Num.Bit0 k) < 2 ^ n ⟷ 1 ≤ n ∧ numeral k < 2 ^ (n - 1)› (is ‹?P4›)
‹numeral (Num.Bit1 k) ≤ 2 ^ n ⟷ 1 ≤ n ∧ numeral k < 2 ^ (n - 1)› (is ‹?P5›)
‹numeral (Num.Bit1 k) < 2 ^ n ⟷ 1 ≤ n ∧ numeral k < 2 ^ (n - 1)› (is ‹?P6›)
proof -
show ?P1
by simp
show ?P2
using one_less_power power_eq_if by auto
let ?K = ‹numeral k :: nat›
define m where ‹m = n - 1›
then consider ‹n = 0› | ‹n = Suc m›
by (cases n) simp_all
note Suc = this
have ‹2 * ?K ≤ 2 * 2 ^ m ⟷ ?K ≤ 2 ^ m›
by linarith
then have ‹of_nat (2 * ?K) ≤ of_nat (2 * 2 ^ m) ⟷ of_nat ?K ≤ of_nat (2 ^ m)›
by (simp only: of_nat_le_iff)
then show ?P3
by (auto intro: Suc)
have ‹2 * ?K < 2 * 2 ^ m ⟷ ?K < 2 ^ m›
by linarith
then have ‹of_nat (2 * ?K) < of_nat (2 * 2 ^ m) ⟷ of_nat ?K < of_nat (2 ^ m)›
by (simp only: of_nat_less_iff)
then show ?P4
by (auto intro: Suc)
have ‹Suc (2 * ?K) ≤ 2 * 2 ^ m ⟷ ?K < 2 ^ m›
by linarith
then have ‹of_nat (Suc (2 * ?K)) ≤ of_nat (2 * 2 ^ m) ⟷ of_nat ?K < of_nat (2 ^ m)›
by (simp only: of_nat_le_iff of_nat_less_iff)
then show ?P5
by (auto intro: Suc)
have ‹Suc (2 * ?K) < 2 * 2 ^ m ⟷ ?K < 2 ^ m›
by linarith
then have ‹of_nat (Suc (2 * ?K)) < of_nat (2 * 2 ^ m) ⟷ of_nat ?K < of_nat (2 ^ m)›
by (simp only: of_nat_less_iff)
then show ?P6
by (auto intro: Suc)
qed
end
section‹Printing Machine Words›
definition string_of_word_single :: "bool ⇒ 'a::len word ⇒ string" where
"string_of_word_single lc w ≡
(if
w < 10
then
[char_of (48 + unat w)]
else if
w < 36
then
[char_of ((if lc then 87 else 55) + unat w)]
else
undefined)"
text‹Example:›
lemma "let word_upto = ((λ i j. map (of_nat ∘ nat) [i .. j]) :: int ⇒ int ⇒ 32 word list)
in map (string_of_word_single False) (word_upto 1 35) =
[''1'', ''2'', ''3'', ''4'', ''5'', ''6'', ''7'', ''8'', ''9'',
''A'', ''B'', ''C'', ''D'', ''E'', ''F'', ''G'', ''H'', ''I'',
''J'', ''K'', ''L'', ''M'', ''N'', ''O'', ''P'', ''Q'', ''R'',
''S'', ''T'', ''U'', ''V'', ''W'', ''X'', ''Y'', ''Z'']" by eval
function string_of_word :: "bool ⇒ ('a :: len) word ⇒ nat ⇒ ('a :: len) word ⇒ string" where
"string_of_word lc base ml w =
(if
base < 2 ∨ LENGTH('a) < 2
then
undefined
else if
w < base ∧ ml = 0
then
string_of_word_single lc w
else
string_of_word lc base (ml - 1) (w div base) @ string_of_word_single lc (w mod base)
)"
by pat_completeness auto
definition "hex_string_of_word l ≡ string_of_word True (16 :: ('a::len) word) l"
definition "hex_string_of_word0 ≡ hex_string_of_word 0"
definition "dec_string_of_word0 ≡ string_of_word True 10 0"
termination string_of_word
apply(relation "measure (λ(a,b,c,d). unat d + c)")
apply(rule wf_measure)
apply(subst in_measure)
apply(clarsimp)
subgoal for base ml n
apply(case_tac "ml ≠ 0")
apply(simp add: less_eq_Suc_le unat_div)
apply(simp)
apply(subgoal_tac "(n div base) < n")
apply(blast intro: unat_mono)
apply(rule div_less_dividend_word)
apply (auto simp add: not_less word_le_nat_alt)
done
done
declare string_of_word.simps[simp del]
lemma "hex_string_of_word0 (0xdeadbeef42 :: 42 word) = ''deadbeef42''" by eval
lemma "hex_string_of_word 1 (0x1 :: 5 word) = ''01''" by eval
lemma "hex_string_of_word 8 (0xff::32 word) = ''0000000ff''" by eval
lemma "dec_string_of_word0 (8::32 word) = ''8''" by eval
lemma "dec_string_of_word0 (3::2 word) = ''11''" by eval
lemma "dec_string_of_word0 (-1::8 word) = ''255''" by eval
lemma string_of_word_single_atoi:
"n < 10 ⟹ string_of_word_single True n = [char_of (48 + unat n)]"
by(simp add: string_of_word_single_def)
lemma bintrunc_pos_eq: "x ≥ 0 ⟹ take_bit n x = x ⟷ x < 2^n" for x :: int
by (simp add: take_bit_int_eq_self_iff)
lemma string_of_word_base_ten_zeropad:
fixes w ::"'a::len word"
assumes lena: "LENGTH('a) ≥ 5"
shows "base = 10 ⟹ zero = 0 ⟹ string_of_word True base zero w = string_of_nat (unat w)"
proof(induction True base zero w rule: string_of_word.induct)
case (1 base ml n)
note Word.word_less_no[simp del]
note Word.uint_bintrunc[simp del]
define l where ‹l = LENGTH('a) - 5›
with lena have l: ‹LENGTH('a) = l + 5›
by simp
have [simp]: ‹take_bit LENGTH('a) (10 :: nat) = 10›
using lena by (auto simp add: take_bit_nat_eq_self_iff l Suc_lessI)
have [simp]: ‹take_bit LENGTH('a) (10 :: int) = 10›
using lena by (auto simp add: take_bit_int_eq_self_iff l)
(smt (verit) zero_less_power)
have unat_mod_ten: "unat (n mod 0xA) = unat n mod 10"
by (simp add: nat_take_bit_eq unat_mod)
have unat_div_ten: "(unat (n div 0xA)) = unat n div 10"
by (simp add: nat_take_bit_eq unat_div)
have n_less_ten_unat: "n < 0xA ⟹ (unat n < 10)"
by (simp add: unat_less_helper)
have "0xA ≤ n ⟹ 10 ≤ unat n"
by (simp add: nat_take_bit_eq word_le_nat_alt)
hence n_less_ten_unat_not: "¬ n < 0xA ⟹ ¬ unat n < 10" by fastforce
have not_wordlength_too_small: "¬ LENGTH('a) < 2" using lena by fastforce
have "2 ≤ (0xA::'a word)"
by simp
hence ten_not_less_two: "¬ (0xA::'a word) < 2" by (simp add: Word.word_less_no Word.uint_bintrunc)
with 1(2,3) have " ¬ (base < 2 ∨ LENGTH(32) < 2)"
by(simp)
with 1 not_wordlength_too_small have IH: "¬ n < 0xA ⟹ string_of_word True 0xA 0 (n div 0xA) = string_of_nat (unat (n div 0xA))"
by(simp)
show ?case
apply(simp add: 1)
apply(cases "n < 0xA")
subgoal
apply(subst(1) string_of_word.simps)
apply(subst(1) string_of_nat.simps)
apply(simp add: n_less_ten_unat)
using lena apply(simp add: not_wordlength_too_small ten_not_less_two string_of_word_single_atoi)
done
using sym[OF IH] apply(simp)
apply(subst(1) string_of_word.simps)
apply(simp)
apply(subst(1) string_of_nat.simps)
apply(simp)
apply (simp add: string_of_word_single_atoi Word.word_mod_less_divisor unat_div_ten unat_mod_ten)
using ‹10 ≤ n ⟹ 10 ≤ unat n› not_wordlength_too_small apply (auto simp add: not_less)
done
qed
lemma dec_string_of_word0:
"dec_string_of_word0 (w8:: 8 word) = string_of_nat (unat w8)"
"dec_string_of_word0 (w16:: 16 word) = string_of_nat (unat w16)"
"dec_string_of_word0 (w32:: 32 word) = string_of_nat (unat w32)"
"dec_string_of_word0 (w64:: 64 word) = string_of_nat (unat w64)"
"dec_string_of_word0 (w128:: 128 word) = string_of_nat (unat w128)"
unfolding dec_string_of_word0_def
using string_of_word_base_ten_zeropad by force+
end