theory WB_Word
imports "HOL-Word.Word" "Native_Word.Uint64" "Native_Word.Uint32" WB_More_Refinement "HOL-Imperative_HOL.Heap"
Collections.HashCode Bits_Natural
begin
lemma less_upper_bintrunc_id: ‹n < 2 ^b ⟹ n ≥ 0 ⟹ bintrunc b n = n›
unfolding uint32_of_nat_def
by (simp add: no_bintr_alt1)
definition word_nat_rel :: "('a :: len0 Word.word × nat) set" where
‹word_nat_rel = br unat (λ_. True)›
lemma bintrunc_eq_bits_eqI: ‹ (⋀n. (n < r ∧ bin_nth c n) = (n < r ∧ bin_nth a n)) ⟹
bintrunc r (a) = bintrunc r c›
proof (induction r arbitrary: a c)
case 0
then show ?case by (simp_all flip: bin_nth.Z)
next
case (Suc r a c) note IH = this(1) and eq = this(2)
have 1: ‹(n < r ∧ bin_nth (bin_rest a) n) = (n < r ∧ bin_nth (bin_rest c) n)› for n
using eq[of ‹Suc n›] eq[of 1] by (clarsimp simp flip: bin_nth.Z)
show ?case
using IH[OF 1] eq[of 0] by (simp_all flip: bin_nth.Z)
qed
lemma and_eq_bits_eqI: ‹(⋀n. c !! n = (a !! n ∧ b !! n))⟹ a AND b = c› for a b c :: ‹_ word›
by transfer
(rule bintrunc_eq_bits_eqI, auto simp add: bin_nth_ops)
lemma pow2_mono_word_less:
‹m < LENGTH('a) ⟹ n < LENGTH('a) ⟹ m < n ⟹ (2 :: 'a :: len word) ^m < 2 ^ n›
proof (induction n arbitrary: m)
case 0
then show ?case by auto
next
case (Suc n m) note IH = this(1) and le = this(2-)
have [simp]: ‹nat (bintrunc LENGTH('a) (2::int)) = 2›
by (metis add_lessD1 le(2) plus_1_eq_Suc power_one_right uint_bintrunc unat_def unat_p2)
have 1: ‹unat ((2 :: 'a word) ^ n) ≤ (2 :: nat) ^ n›
by (metis Suc.prems(2) eq_imp_le le_SucI linorder_not_less unat_p2)
have 2: ‹unat ((2 :: 'a word)) ≤ (2 :: nat)›
by (metis le_unat_uoi nat_le_linear of_nat_numeral)
have ‹unat (2 :: 'a word) * unat ((2 :: 'a word) ^ n) ≤ (2 :: nat) ^ Suc n›
using mult_le_mono[OF 2 1] by auto
also have ‹(2 :: nat) ^ Suc n < (2 :: nat) ^ LENGTH('a)›
using le(2) by (metis unat_lt2p unat_p2)
finally have ‹unat (2 :: 'a word) * unat ((2 :: 'a word) ^ n) < 2 ^ LENGTH('a)›
.
then have [simp]: ‹unat (2 * (2 :: 'a word) ^ n) = unat (2 :: 'a word) * unat ((2 :: 'a word) ^ n)›
using unat_mult_lem[of ‹2 :: 'a word› ‹(2 :: 'a word) ^ n›]
by auto
have [simp]: ‹(0::nat) < unat ((2::'a word) ^ n)›
by (simp add: Suc_lessD le(2) unat_p2)
show ?case
using IH(1)[of m] le(2-)
by (auto simp: less_Suc_eq word_less_nat_alt
simp del: unat_lt2p)
qed
lemma pow2_mono_word_le:
‹m < LENGTH('a) ⟹ n < LENGTH('a) ⟹ m ≤ n ⟹ (2 :: 'a :: len word) ^m ≤ 2 ^ n›
using pow2_mono_word_less[of m n, where 'a = 'a]
by (cases ‹m = n›) auto
definition uint32_max :: nat where
‹uint32_max = 2 ^32 - 1›
lemma unat_le_uint32_max_no_bit_set:
fixes n :: ‹'a::len word›
assumes less: ‹unat n ≤ uint32_max› and
n: ‹n !! na› and
32: ‹32 < LENGTH('a)›
shows ‹na < 32›
proof (rule ccontr)
assume H: ‹¬ ?thesis›
have na_le: ‹na < LENGTH('a)›
using test_bit_bin[THEN iffD1, OF n]
by auto
have ‹(2 :: nat) ^ 32 < (2 :: nat) ^ LENGTH('a)›
using 32 power_strict_increasing_iff rel_simps(49) semiring_norm(76) by blast
then have [simp]: ‹(4294967296::nat) mod (2::nat) ^ LENGTH('a) = (4294967296::nat)›
by (auto simp: word_le_nat_alt unat_numeral uint32_max_def mod_less
simp del: unat_bintrunc)
have ‹(2 :: 'a word) ^ na ≥ 2 ^ 32›
using pow2_mono_word_le[OF 32 na_le] H by auto
also have ‹n ≥ (2 :: 'a word) ^ na›
using assms
unfolding uint32_max_def
by (auto dest!: bang_is_le)
finally have ‹unat n > uint32_max›
supply [[show_sorts]]
unfolding word_le_nat_alt
by (auto simp: word_le_nat_alt unat_numeral uint32_max_def
simp del: unat_bintrunc)
then show False
using less by auto
qed
definition uint32_max' where
[simp, symmetric, code]: ‹uint32_max' = uint32_max›
lemma [code]: ‹uint32_max' = 4294967295›
by (auto simp: uint32_max_def)
text ‹This lemma is very trivial but maps an \<^typ>‹64 word› to its list counterpart. This
especially allows to combine two numbers together via ther bit representation (which should be
faster than enumerating all numbers).
›
lemma ex_rbl_word64:
‹∃a64 a63 a62 a61 a60 a59 a58 a57 a56 a55 a54 a53 a52 a51 a50 a49 a48 a47 a46 a45 a44 a43 a42 a41
a40 a39 a38 a37 a36 a35 a34 a33 a32 a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17
a16 a15 a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1.
to_bl (n :: 64 word) =
[a64, a63, a62, a61, a60, a59, a58, a57, a56, a55, a54, a53, a52, a51, a50, a49, a48, a47,
a46, a45, a44, a43, a42, a41, a40, a39, a38, a37, a36, a35, a34, a33, a32, a31, a30, a29,
a28, a27, a26, a25, a24, a23, a22, a21, a20, a19, a18, a17, a16, a15, a14, a13, a12, a11,
a10, a9, a8, a7, a6, a5, a4, a3, a2, a1]› (is ?A) and
ex_rbl_word64_le_uint32_max:
‹unat n ≤ uint32_max ⟹ ∃a31 a30 a29 a28 a27 a26 a25 a24 a23 a22 a21 a20 a19 a18 a17 a16 a15
a14 a13 a12 a11 a10 a9 a8 a7 a6 a5 a4 a3 a2 a1 a32.
to_bl (n :: 64 word) =
[False, False, False, False, False, False, False, False, False, False, False, False, False,
False, False, False, False, False, False, False, False, False, False, False, False, False,
False, False, False, False, False, False,
a32, a31, a30, a29, a28, a27, a26, a25, a24, a23, a22, a21, a20, a19, a18, a17, a16, a15,
a14, a13, a12, a11, a10, a9, a8, a7, a6, a5, a4, a3, a2, a1]› (is ‹_ ⟹ ?B›) and
ex_rbl_word64_ge_uint32_max:
‹n AND (2^32 - 1) = 0 ⟹ ∃a64 a63 a62 a61 a60 a59 a58 a57 a56 a55 a54 a53 a52 a51 a50 a49 a48
a47 a46 a45 a44 a43 a42 a41 a40 a39 a38 a37 a36 a35 a34 a33.
to_bl (n :: 64 word) =
[a64, a63, a62, a61, a60, a59, a58, a57, a56, a55, a54, a53, a52, a51, a50, a49, a48, a47,
a46, a45, a44, a43, a42, a41, a40, a39, a38, a37, a36, a35, a34, a33,
False, False, False, False, False, False, False, False, False, False, False, False, False,
False, False, False, False, False, False, False, False, False, False, False, False, False,
False, False, False, False, False, False]› (is ‹_ ⟹ ?C›)
proof -
have [simp]: "n > 0 ⟹ length xs = n ⟷
(∃y ys. xs = y # ys ∧ length ys = n - 1)" for ys n xs
by (cases xs) auto
show H: ?A
using word_bl_Rep'[of n]
by (auto simp del: word_bl_Rep')
show ?B if ‹unat n ≤ uint32_max›
proof -
have H': ‹m ≥ 32 ⟹ ¬n !! m› for m
using unat_le_uint32_max_no_bit_set[of n m, OF that] by auto
show ?thesis using that H'[of 64] H'[of 63] H'[of 62] H'[of 61] H'[of 60] H'[of 59] H'[of 58]
H'[of 57] H'[of 56] H'[of 55] H'[of 54] H'[of 53] H'[of 52] H'[of 51] H'[of 50] H'[of 49]
H'[of 48] H'[of 47] H'[of 46] H'[of 45] H'[of 44] H'[of 43] H'[of 42] H'[of 41] H'[of 40]
H'[of 39] H'[of 38] H'[of 37] H'[of 36] H'[of 35] H'[of 34] H'[of 33] H'[of 32]
H'[of 31]
using H unfolding unat_def
by (clarsimp simp add: test_bit_bl word_size)
qed
show ?C if ‹n AND (2^32 - 1) = 0›
proof -
note H' = test_bit_bl[of ‹n AND (2^32 - 1)› m for m, unfolded word_size, simplified]
have [simp]: ‹(n AND 4294967295) !! m = False› for m
using that by auto
show ?thesis
using H H'[of 0]
H'[of 32] H'[of 31] H'[of 30] H'[of 29] H'[of 28] H'[of 27] H'[of 26] H'[of 25] H'[of 24]
H'[of 23] H'[of 22] H'[of 21] H'[of 20] H'[of 19] H'[of 18] H'[of 17] H'[of 16] H'[of 15]
H'[of 14] H'[of 13] H'[of 12] H'[of 11] H'[of 10] H'[of 9] H'[of 8] H'[of 7] H'[of 6]
H'[of 5] H'[of 4] H'[of 3] H'[of 2] H'[of 1]
unfolding unat_def word_size that
by (clarsimp simp add: word_size bl_word_and word_add_rbl)
qed
qed
subsubsection ‹32-bits›
lemma word_nat_of_uint32_Rep_inject[simp]: ‹nat_of_uint32 ai = nat_of_uint32 bi ⟷ ai = bi›
by transfer simp
lemma nat_of_uint32_012[simp]: ‹nat_of_uint32 0 = 0› ‹nat_of_uint32 2 = 2› ‹nat_of_uint32 1 = 1›
by (transfer, auto)+
lemma nat_of_uint32_3: ‹nat_of_uint32 3 = 3›
by (transfer, auto)+
lemma nat_of_uint32_Suc03_iff:
‹nat_of_uint32 a = Suc 0 ⟷ a = 1›
‹nat_of_uint32 a = 3 ⟷ a = 3›
using word_nat_of_uint32_Rep_inject nat_of_uint32_3 by fastforce+
lemma nat_of_uint32_013_neq:
"(1::uint32) ≠ (0 :: uint32)" "(0::uint32) ≠ (1 :: uint32)"
"(3::uint32) ≠ (0 :: uint32)"
"(3::uint32) ≠ (1 :: uint32)"
"(0::uint32) ≠ (3 :: uint32)"
"(1::uint32) ≠ (3 :: uint32)"
by (auto dest: arg_cong[of _ _ nat_of_uint32] simp: nat_of_uint32_3)
definition uint32_nat_rel :: "(uint32 × nat) set" where
‹uint32_nat_rel = br nat_of_uint32 (λ_. True)›
lemma unat_shiftr: ‹unat (xi >> n) = unat xi div (2^n)›
proof -
have [simp]: ‹nat (2 * 2 ^ n) = 2 * 2 ^ n› for n :: nat
by (metis nat_numeral nat_power_eq power_Suc rel_simps(27))
show ?thesis
unfolding unat_def
by (induction n arbitrary: xi) (auto simp: shiftr_div_2n nat_div_distrib)
qed
instantiation uint32 :: default
begin
definition default_uint32 :: uint32 where
‹default_uint32 = 0›
instance
..
end
instance uint32 :: heap
by standard (auto simp: inj_def exI[of _ nat_of_uint32])
instance uint32 :: semiring_numeral
by standard
instantiation uint32 :: hashable
begin
definition hashcode_uint32 :: ‹uint32 ⇒ uint32› where
‹hashcode_uint32 n = n›
definition def_hashmap_size_uint32 :: ‹uint32 itself ⇒ nat› where
‹def_hashmap_size_uint32 = (λ_. 16)›
instance
by standard (simp add: def_hashmap_size_uint32_def)
end
abbreviation uint32_rel :: ‹(uint32 × uint32) set› where
‹uint32_rel ≡ Id›
lemma nat_bin_trunc_ao:
‹nat (bintrunc n a) AND nat (bintrunc n b) = nat (bintrunc n (a AND b))›
‹nat (bintrunc n a) OR nat (bintrunc n b) = nat (bintrunc n (a OR b))›
unfolding bitAND_nat_def bitOR_nat_def
by (auto simp add: bin_trunc_ao bintr_ge0)
lemma nat_of_uint32_ao:
‹nat_of_uint32 n AND nat_of_uint32 m = nat_of_uint32 (n AND m)›
‹nat_of_uint32 n OR nat_of_uint32 m = nat_of_uint32 (n OR m)›
subgoal apply (transfer, unfold unat_def, transfer, unfold nat_bin_trunc_ao) ..
subgoal apply (transfer, unfold unat_def, transfer, unfold nat_bin_trunc_ao) ..
done
lemma nat_of_uint32_mod_2:
‹nat_of_uint32 L mod 2 = nat_of_uint32 (L mod 2)›
by transfer (auto simp: uint_mod unat_def nat_mod_distrib)
lemma bitAND_1_mod_2_uint32: ‹bitAND L 1 = L mod 2› for L :: uint32
proof -
have H: ‹unat L mod 2 = 1 ∨ unat L mod 2 = 0› for L
by auto
show ?thesis
apply (subst word_nat_of_uint32_Rep_inject[symmetric])
apply (subst nat_of_uint32_ao[symmetric])
apply (subst nat_of_uint32_012)
unfolding bitAND_1_mod_2
by (rule nat_of_uint32_mod_2)
qed
lemma nat_uint_XOR: ‹nat (uint (a XOR b)) = nat (uint a) XOR nat (uint b)›
if len: ‹LENGTH('a) > 0›
for a b :: ‹'a ::len0 Word.word›
proof -
have 1: ‹uint ((word_of_int:: int ⇒ 'a Word.word)(uint a)) = uint a›
by (subst (2) word_of_int_uint[of a, symmetric]) (rule refl)
have H: ‹nat (bintrunc n (a XOR b)) = nat (bintrunc n a XOR bintrunc n b)›
if ‹n> 0› for n and a :: int and b :: int
using that
proof (induction n arbitrary: a b)
case 0
then show ?case by auto
next
case (Suc n) note IH = this(1) and Suc = this(2)
then show ?case
proof (cases n)
case (Suc m)
moreover have
‹nat (bintrunc m (bin_rest (bin_rest a) XOR bin_rest (bin_rest b)) BIT
((bin_last (bin_rest a) ∨ bin_last (bin_rest b)) ∧
(bin_last (bin_rest a) ⟶ ¬ bin_last (bin_rest b))) BIT
((bin_last a ∨ bin_last b) ∧ (bin_last a ⟶ ¬ bin_last b))) =
nat ((bintrunc m (bin_rest (bin_rest a)) XOR bintrunc m (bin_rest (bin_rest b))) BIT
((bin_last (bin_rest a) ∨ bin_last (bin_rest b)) ∧
(bin_last (bin_rest a) ⟶ ¬ bin_last (bin_rest b))) BIT
((bin_last a ∨ bin_last b) ∧ (bin_last a ⟶ ¬ bin_last b)))›
(is ‹nat (?n1 BIT ?b) = nat (?n2 BIT ?b)›)
proof -
have a1: "nat ?n1 = nat ?n2"
using IH Suc by auto
have f2: "0 ≤ ?n2"
by (simp add: bintr_ge0)
have "0 ≤ ?n1"
using bintr_ge0 by auto
then have "?n2 = ?n1"
using f2 a1 by presburger
then show ?thesis by simp
qed
ultimately show ?thesis by simp
qed simp
qed
have ‹nat (bintrunc LENGTH('a) (a XOR b)) = nat (bintrunc LENGTH('a) a XOR bintrunc LENGTH('a) b)› for a b
using len H[of ‹LENGTH('a)› a b] by auto
then have ‹nat (uint (a XOR b)) = nat (uint a XOR uint b)›
by transfer
then show ?thesis
unfolding bitXOR_nat_def by auto
qed
lemma nat_of_uint32_XOR: ‹nat_of_uint32 (a XOR b) = nat_of_uint32 a XOR nat_of_uint32 b›
by transfer (auto simp: unat_def nat_uint_XOR)
lemma nat_of_uint32_0_iff: ‹nat_of_uint32 xi = 0 ⟷ xi = 0› for xi
by transfer (auto simp: unat_def uint_0_iff)
lemma nat_0_AND: ‹0 AND n = 0› for n :: nat
unfolding bitAND_nat_def by auto
lemma uint32_0_AND: ‹0 AND n = 0› for n :: uint32
by transfer auto
definition uint32_safe_minus where
‹uint32_safe_minus m n = (if m < n then 0 else m - n)›
lemma nat_of_uint32_le_minus: ‹ai ≤ bi ⟹ 0 = nat_of_uint32 ai - nat_of_uint32 bi›
by transfer (auto simp: unat_def word_le_def)
lemma nat_of_uint32_notle_minus:
‹¬ ai < bi ⟹
nat_of_uint32 (ai - bi) = nat_of_uint32 ai - nat_of_uint32 bi›
apply transfer
unfolding unat_def
by (subst uint_sub_lem[THEN iffD1])
(auto simp: unat_def uint_nonnegative nat_diff_distrib word_le_def[symmetric] intro: leI)
lemma nat_of_uint32_uint32_of_nat_id: ‹n ≤ uint32_max ⟹ nat_of_uint32 (uint32_of_nat n) = n›
unfolding uint32_of_nat_def uint32_max_def
apply simp
apply transfer
apply (auto simp: unat_def)
apply transfer
by (auto simp: less_upper_bintrunc_id)
lemma uint32_less_than_0[iff]: ‹(a::uint32) ≤ 0 ⟷ a = 0›
by transfer auto
lemma nat_of_uint32_less_iff: ‹nat_of_uint32 a < nat_of_uint32 b ⟷ a < b›
apply transfer
apply (auto simp: unat_def word_less_def)
apply transfer
by (smt bintr_ge0)
lemma nat_of_uint32_le_iff: ‹nat_of_uint32 a ≤ nat_of_uint32 b ⟷ a ≤ b›
apply transfer
by (auto simp: unat_def word_less_def nat_le_iff word_le_def)
lemma nat_of_uint32_max:
‹nat_of_uint32 (max ai bi) = max (nat_of_uint32 ai) (nat_of_uint32 bi)›
by (auto simp: max_def nat_of_uint32_le_iff split: if_splits)
lemma mult_mod_mod_mult:
‹b < n div a ⟹ a > 0 ⟹ b > 0 ⟹ a * b mod n = a * (b mod n)› for a b n :: int
apply (subst int_mod_eq')
subgoal using not_le zdiv_mono1 by fastforce
subgoal using not_le zdiv_mono1 by fastforce
subgoal
apply (subst int_mod_eq')
subgoal by auto
subgoal by (metis (full_types) le_cases not_le order_trans pos_imp_zdiv_nonneg_iff zdiv_le_dividend)
subgoal by auto
done
done
lemma nat_of_uint32_distrib_mult2:
assumes ‹nat_of_uint32 xi ≤ uint32_max div 2›
shows ‹nat_of_uint32 (2 * xi) = 2 * nat_of_uint32 xi›
proof -
have H: ‹⋀xi::32 Word.word. nat (uint xi) < (2147483648::nat) ⟹
nat (uint xi mod (4294967296::int)) = nat (uint xi)›
proof -
fix xia :: "32 Word.word"
assume a1: "nat (uint xia) < 2147483648"
have f2: "⋀n. (numeral n::nat) ≤ numeral (num.Bit0 n)"
by (metis (no_types) add_0_right add_mono_thms_linordered_semiring(1)
dual_order.order_iff_strict numeral_Bit0 rel_simps(51))
have "unat xia ≤ 4294967296"
using a1 by (metis (no_types) add_0_right add_mono_thms_linordered_semiring(1)
dual_order.order_iff_strict nat_int numeral_Bit0 rel_simps(51) uint_nat)
then show "nat (uint xia mod 4294967296) = nat (uint xia)"
using f2 a1 by auto
qed
have [simp]: ‹xi ≠ (0::32 Word.word) ⟹ (0::int) < uint xi› for xi
by (metis (full_types) uint_eq_0 word_gt_0 word_less_def)
show ?thesis
using assms unfolding uint32_max_def
apply (case_tac ‹xi = 0›)
subgoal by auto
subgoal by transfer (auto simp: unat_def uint_word_ariths nat_mult_distrib mult_mod_mod_mult H)
done
qed
lemma nat_of_uint32_distrib_mult2_plus1:
assumes ‹nat_of_uint32 xi ≤ uint32_max div 2›
shows ‹nat_of_uint32 (2 * xi + 1) = 2 * nat_of_uint32 xi + 1›
proof -
have mod_is_id: ‹⋀xi::32 Word.word. nat (uint xi) < (2147483648::nat) ⟹
(uint xi mod (4294967296::int)) = uint xi›
by (subst zmod_trival_iff) auto
have [simp]: ‹xi ≠ (0::32 Word.word) ⟹ (0::int) < uint xi› for xi
by (metis (full_types) uint_eq_0 word_gt_0 word_less_def)
show ?thesis
using assms by transfer (auto simp: unat_def uint_word_ariths nat_mult_distrib mult_mod_mod_mult
mod_is_id nat_mod_distrib nat_add_distrib uint32_max_def)
qed
lemma nat_of_uint32_add:
‹nat_of_uint32 ai + nat_of_uint32 bi ≤ uint32_max ⟹
nat_of_uint32 (ai + bi) = nat_of_uint32 ai + nat_of_uint32 bi›
by transfer (auto simp: unat_def uint_plus_if' nat_add_distrib uint32_max_def)
definition zero_uint32_nat where
[simp]: ‹zero_uint32_nat = (0 :: nat)›
definition one_uint32_nat where
[simp]: ‹one_uint32_nat = (1 :: nat)›
definition two_uint32_nat where [simp]: ‹two_uint32_nat = (2 :: nat)›
definition two_uint32 where
[simp]: ‹two_uint32 = (2 :: uint32)›
definition fast_minus :: ‹'a::{minus} ⇒ 'a ⇒ 'a› where
[simp]: ‹fast_minus m n = m - n›
definition fast_minus_code :: ‹'a::{minus,ord} ⇒ 'a ⇒ 'a› where
[simp]: ‹fast_minus_code m n = (SOME p. (p = m - n ∧ m ≥ n))›
definition fast_minus_nat :: ‹nat ⇒ nat ⇒ nat› where
[simp, code del]: ‹fast_minus_nat = fast_minus_code›
definition fast_minus_nat' :: ‹nat ⇒ nat ⇒ nat› where
[simp, code del]: ‹fast_minus_nat' = fast_minus_code›
lemma [code]: ‹fast_minus_nat = fast_minus_nat'›
unfolding fast_minus_nat_def fast_minus_nat'_def ..
lemma word_of_int_int_unat[simp]: ‹word_of_int (int (unat x)) = x›
unfolding unat_def
apply transfer
by (simp add: bintr_ge0)
lemma uint32_of_nat_nat_of_uint32[simp]: ‹uint32_of_nat (nat_of_uint32 x) = x›
unfolding uint32_of_nat_def
by transfer auto
definition sum_mod_uint32_max where
‹sum_mod_uint32_max a b = (a + b) mod (uint32_max + 1)›
lemma nat_of_uint32_plus:
‹nat_of_uint32 (a + b) = (nat_of_uint32 a + nat_of_uint32 b) mod (uint32_max + 1)›
by transfer (auto simp: unat_word_ariths uint32_max_def)
definition one_uint32 where
‹one_uint32 = (1::uint32)›
text ‹This lemma is meant to be used to simplify expressions like \<^term>‹nat_of_uint32 5› and therefore
we add the bound explicitely instead of keeping \<^term>‹uint32_max›.
Remark the types are non trivial here: we convert a \<^typ>‹uint32› to a \<^typ>‹nat›, even if the
experession \<^term>‹numeral n› looks the same.›
lemma nat_of_uint32_numeral[simp]:
‹numeral n ≤ ((2 ^32 - 1)::nat) ⟹ nat_of_uint32 (numeral n) = numeral n›
proof (induction n)
case One
then show ?case by auto
next
case (Bit0 n) note IH = this(1)[unfolded uint32_max_def[symmetric]] and le = this(2)
define m :: nat where ‹m ≡ numeral n›
have n_le: ‹numeral n ≤ uint32_max›
using le
by (subst (asm) numeral.numeral_Bit0) (auto simp: m_def[symmetric] uint32_max_def)
have n_le_div2: ‹nat_of_uint32 (numeral n) ≤ uint32_max div 2›
apply (subst IH[OF n_le])
using le by (subst (asm) numeral.numeral_Bit0) (auto simp: m_def[symmetric] uint32_max_def)
have ‹nat_of_uint32 (numeral (num.Bit0 n)) = nat_of_uint32 (2 * numeral n)›
by (subst numeral.numeral_Bit0)
(metis comm_monoid_mult_class.mult_1 distrib_right_numeral one_add_one)
also have ‹… = 2 * nat_of_uint32 (numeral n)›
by (subst nat_of_uint32_distrib_mult2[OF n_le_div2]) (rule refl)
also have ‹… = 2 * numeral n›
by (subst IH[OF n_le]) (rule refl)
also have ‹… = numeral (num.Bit0 n)›
by (subst (2) numeral.numeral_Bit0, subst mult_2)
(rule refl)
finally show ?case by simp
next
case (Bit1 n) note IH = this(1)[unfolded uint32_max_def[symmetric]] and le = this(2)
define m :: nat where ‹m ≡ numeral n›
have n_le: ‹numeral n ≤ uint32_max›
using le
by (subst (asm) numeral.numeral_Bit1) (auto simp: m_def[symmetric] uint32_max_def)
have n_le_div2: ‹nat_of_uint32 (numeral n) ≤ uint32_max div 2›
apply (subst IH[OF n_le])
using le by (subst (asm) numeral.numeral_Bit1) (auto simp: m_def[symmetric] uint32_max_def)
have ‹nat_of_uint32 (numeral (num.Bit1 n)) = nat_of_uint32 (2 * numeral n + 1)›
by (subst numeral.numeral_Bit1)
(metis comm_monoid_mult_class.mult_1 distrib_right_numeral one_add_one)
also have ‹… = 2 * nat_of_uint32 (numeral n) + 1›
by (subst nat_of_uint32_distrib_mult2_plus1[OF n_le_div2]) (rule refl)
also have ‹… = 2 * numeral n + 1›
by (subst IH[OF n_le]) (rule refl)
also have ‹… = numeral (num.Bit1 n)›
by (subst numeral.numeral_Bit1) linarith
finally show ?case by simp
qed
lemma nat_of_uint32_mod_232:
shows ‹nat_of_uint32 xi = nat_of_uint32 xi mod 2^32›
proof -
show ?thesis
unfolding uint32_max_def
subgoal apply transfer
subgoal for xi
by (use word_unat.norm_Rep[of xi] in
‹auto simp: uint_word_ariths nat_mult_distrib mult_mod_mod_mult
simp del: word_unat.norm_Rep›)
done
done
qed
lemma transfer_pow_uint32:
‹Transfer.Rel (rel_fun cr_uint32 (rel_fun (=) cr_uint32)) ((^)) ((^))›
proof -
have [simp]: ‹Rep_uint32 y ^ x = Rep_uint32 (y ^ x)› for y :: uint32 and x :: nat
by (induction x)
(auto simp: one_uint32.rep_eq times_uint32.rep_eq)
show ?thesis
by (auto simp: Transfer.Rel_def rel_fun_def cr_uint32_def)
qed
lemma uint32_mod_232_eq:
fixes xi :: uint32
shows ‹xi = xi mod 2^32›
proof -
have H: ‹nat_of_uint32 (xi mod 2 ^ 32) = nat_of_uint32 xi›
apply transfer
prefer 2
apply (rule transfer_pow_uint32)
subgoal for xi
using uint_word_ariths(1)[of xi 0]
supply [[show_types]]
apply auto
apply (rule word_uint_eq_iff[THEN iffD2])
apply (subst uint_mod_alt)
by auto
done
show ?thesis
by (rule word_nat_of_uint32_Rep_inject[THEN iffD1, OF H[symmetric]])
qed
lemma nat_of_uint32_numeral_mod_232:
‹nat_of_uint32 (numeral n) = numeral n mod 2^32›
apply transfer
apply (subst unat_numeral)
by auto
lemma int_of_uint32_alt_def: ‹int_of_uint32 n = int (nat_of_uint32 n)›
by (simp add: int_of_uint32.rep_eq nat_of_uint32.rep_eq unat_def)
lemma int_of_uint32_numeral[simp]:
‹numeral n ≤ ((2 ^ 32 - 1)::nat) ⟹ int_of_uint32 (numeral n) = numeral n›
by (subst int_of_uint32_alt_def) simp
lemma nat_of_uint32_numeral_iff[simp]:
‹numeral n ≤ ((2 ^ 32 - 1)::nat) ⟹ nat_of_uint32 a = numeral n ⟷ a = numeral n›
apply (rule iffI)
prefer 2 apply (solves simp)
using word_nat_of_uint32_Rep_inject by fastforce
lemma nat_of_uint32_mult_le:
‹nat_of_uint32 ai * nat_of_uint32 bi ≤ uint32_max ⟹
nat_of_uint32 (ai * bi) = nat_of_uint32 ai * nat_of_uint32 bi›
apply transfer
by (auto simp: unat_word_ariths uint32_max_def)
lemma nat_and_numerals [simp]:
"(numeral (Num.Bit0 x) :: nat) AND (numeral (Num.Bit0 y) :: nat) = (2 :: nat) * (numeral x AND numeral y)"
"numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (2 :: nat) * (numeral x AND numeral y)"
"numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (2 :: nat) * (numeral x AND numeral y)"
"numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (2 :: nat) * (numeral x AND numeral y)+1"
"(1::nat) AND numeral (Num.Bit0 y) = 0"
"(1::nat) AND numeral (Num.Bit1 y) = 1"
"numeral (Num.Bit0 x) AND (1::nat) = 0"
"numeral (Num.Bit1 x) AND (1::nat) = 1"
"(Suc 0::nat) AND numeral (Num.Bit0 y) = 0"
"(Suc 0::nat) AND numeral (Num.Bit1 y) = 1"
"numeral (Num.Bit0 x) AND (Suc 0::nat) = 0"
"numeral (Num.Bit1 x) AND (Suc 0::nat) = 1"
"Suc 0 AND Suc 0 = 1"
supply [[show_types]]
by (auto simp: bitAND_nat_def Bit_def nat_add_distrib)
lemma nat_of_uint32_div:
‹nat_of_uint32 (a div b) = nat_of_uint32 a div nat_of_uint32 b›
by transfer (auto simp: unat_div)
subsubsection ‹64-bits›
definition uint64_nat_rel :: "(uint64 × nat) set" where
‹uint64_nat_rel = br nat_of_uint64 (λ_. True)›
abbreviation uint64_rel :: ‹(uint64 × uint64) set› where
‹uint64_rel ≡ Id›
lemma word_nat_of_uint64_Rep_inject[simp]: ‹nat_of_uint64 ai = nat_of_uint64 bi ⟷ ai = bi›
by transfer simp
instantiation uint64 :: default
begin
definition default_uint64 :: uint64 where
‹default_uint64 = 0›
instance
..
end
instance uint64 :: heap
by standard (auto simp: inj_def exI[of _ nat_of_uint64])
instance uint64 :: semiring_numeral
by standard
lemma nat_of_uint64_012[simp]: ‹nat_of_uint64 0 = 0› ‹nat_of_uint64 2 = 2› ‹nat_of_uint64 1 = 1›
by (transfer, auto)+
definition zero_uint64_nat where
[simp]: ‹zero_uint64_nat = (0 :: nat)›
definition uint64_max :: nat where
‹uint64_max = 2 ^64 - 1›
definition uint64_max' where
[simp, symmetric, code]: ‹uint64_max' = uint64_max›
lemma [code]: ‹uint64_max' = 18446744073709551615›
by (auto simp: uint64_max_def)
lemma nat_of_uint64_uint64_of_nat_id: ‹n ≤ uint64_max ⟹ nat_of_uint64 (uint64_of_nat n) = n›
unfolding uint64_of_nat_def uint64_max_def
apply simp
apply transfer
apply (auto simp: unat_def)
apply transfer
by (auto simp: less_upper_bintrunc_id)
lemma nat_of_uint64_add:
‹nat_of_uint64 ai + nat_of_uint64 bi ≤ uint64_max ⟹
nat_of_uint64 (ai + bi) = nat_of_uint64 ai + nat_of_uint64 bi›
by transfer (auto simp: unat_def uint_plus_if' nat_add_distrib uint64_max_def)
definition one_uint64_nat where
[simp]: ‹one_uint64_nat = (1 :: nat)›
lemma uint64_less_than_0[iff]: ‹(a::uint64) ≤ 0 ⟷ a = 0›
by transfer auto
lemma nat_of_uint64_less_iff: ‹nat_of_uint64 a < nat_of_uint64 b ⟷ a < b›
apply transfer
apply (auto simp: unat_def word_less_def)
apply transfer
by (smt bintr_ge0)
lemma nat_of_uint64_distrib_mult2:
assumes ‹nat_of_uint64 xi ≤ uint64_max div 2›
shows ‹nat_of_uint64 (2 * xi) = 2 * nat_of_uint64 xi›
proof -
show ?thesis
using assms unfolding uint64_max_def
apply (case_tac ‹xi = 0›)
subgoal by auto
subgoal by transfer (auto simp: unat_def uint_word_ariths nat_mult_distrib mult_mod_mod_mult)
done
qed
lemma (in -)nat_of_uint64_distrib_mult2_plus1:
assumes ‹nat_of_uint64 xi ≤ uint64_max div 2›
shows ‹nat_of_uint64 (2 * xi + 1) = 2 * nat_of_uint64 xi + 1›
proof -
show ?thesis
using assms by transfer (auto simp: unat_def uint_word_ariths nat_mult_distrib mult_mod_mod_mult
nat_mod_distrib nat_add_distrib uint64_max_def)
qed
lemma nat_of_uint64_numeral[simp]:
‹numeral n ≤ ((2 ^ 64 - 1)::nat) ⟹ nat_of_uint64 (numeral n) = numeral n›
proof (induction n)
case One
then show ?case by auto
next
case (Bit0 n) note IH = this(1)[unfolded uint64_max_def[symmetric]] and le = this(2)
define m :: nat where ‹m ≡ numeral n›
have n_le: ‹numeral n ≤ uint64_max›
using le
by (subst (asm) numeral.numeral_Bit0) (auto simp: m_def[symmetric] uint64_max_def)
have n_le_div2: ‹nat_of_uint64 (numeral n) ≤ uint64_max div 2›
apply (subst IH[OF n_le])
using le by (subst (asm) numeral.numeral_Bit0) (auto simp: m_def[symmetric] uint64_max_def)
have ‹nat_of_uint64 (numeral (num.Bit0 n)) = nat_of_uint64 (2 * numeral n)›
by (subst numeral.numeral_Bit0)
(metis comm_monoid_mult_class.mult_1 distrib_right_numeral one_add_one)
also have ‹… = 2 * nat_of_uint64 (numeral n)›
by (subst nat_of_uint64_distrib_mult2[OF n_le_div2]) (rule refl)
also have ‹… = 2 * numeral n›
by (subst IH[OF n_le]) (rule refl)
also have ‹… = numeral (num.Bit0 n)›
by (subst (2) numeral.numeral_Bit0, subst mult_2)
(rule refl)
finally show ?case by simp
next
case (Bit1 n) note IH = this(1)[unfolded uint64_max_def[symmetric]] and le = this(2)
define m :: nat where ‹m ≡ numeral n›
have n_le: ‹numeral n ≤ uint64_max›
using le
by (subst (asm) numeral.numeral_Bit1) (auto simp: m_def[symmetric] uint64_max_def)
have n_le_div2: ‹nat_of_uint64 (numeral n) ≤ uint64_max div 2›
apply (subst IH[OF n_le])
using le by (subst (asm) numeral.numeral_Bit1) (auto simp: m_def[symmetric] uint64_max_def)
have ‹nat_of_uint64 (numeral (num.Bit1 n)) = nat_of_uint64 (2 * numeral n + 1)›
by (subst numeral.numeral_Bit1)
(metis comm_monoid_mult_class.mult_1 distrib_right_numeral one_add_one)
also have ‹… = 2 * nat_of_uint64 (numeral n) + 1›
by (subst nat_of_uint64_distrib_mult2_plus1[OF n_le_div2]) (rule refl)
also have ‹… = 2 * numeral n + 1›
by (subst IH[OF n_le]) (rule refl)
also have ‹… = numeral (num.Bit1 n)›
by (subst numeral.numeral_Bit1) linarith
finally show ?case by simp
qed
lemma int_of_uint64_alt_def: ‹int_of_uint64 n = int (nat_of_uint64 n)›
by (simp add: int_of_uint64.rep_eq nat_of_uint64.rep_eq unat_def)
lemma int_of_uint64_numeral[simp]:
‹numeral n ≤ ((2 ^ 64 - 1)::nat) ⟹ int_of_uint64 (numeral n) = numeral n›
by (subst int_of_uint64_alt_def) simp
lemma nat_of_uint64_numeral_iff[simp]:
‹numeral n ≤ ((2 ^ 64 - 1)::nat) ⟹ nat_of_uint64 a = numeral n ⟷ a = numeral n›
apply (rule iffI)
prefer 2 apply (solves simp)
using word_nat_of_uint64_Rep_inject by fastforce
lemma numeral_uint64_eq_iff[simp]:
‹numeral m ≤ (2^64-1 :: nat) ⟹ numeral n ≤ (2^64-1 :: nat) ⟹ ((numeral m :: uint64) = numeral n) ⟷ numeral m = (numeral n :: nat)›
by (subst word_nat_of_uint64_Rep_inject[symmetric])
(auto simp: uint64_max_def)
lemma numeral_uint64_eq0_iff[simp]:
‹numeral n ≤ (2^64-1 :: nat) ⟹ ((0 :: uint64) = numeral n) ⟷ 0 = (numeral n :: nat)›
by (subst word_nat_of_uint64_Rep_inject[symmetric])
(auto simp: uint64_max_def)
lemma transfer_pow_uint64: ‹Transfer.Rel (rel_fun cr_uint64 (rel_fun (=) cr_uint64)) (^) (^)›
apply (auto simp: Transfer.Rel_def rel_fun_def cr_uint64_def)
subgoal for x y
by (induction y)
(auto simp: one_uint64.rep_eq times_uint64.rep_eq)
done
lemma shiftl_t2n_uint64: ‹n << m = n * 2 ^ m› for n :: uint64
apply transfer
prefer 2 apply (rule transfer_pow_uint64)
by (auto simp: shiftl_t2n)
lemma mod2_bin_last: ‹a mod 2 = 0 ⟷ ¬bin_last a›
by (auto simp: bin_last_def)
lemma bitXOR_1_if_mod_2_int: ‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)› for L :: int
apply (rule bin_rl_eqI)
unfolding bin_rest_OR bin_last_OR
apply (auto simp: bin_rest_def bin_last_def)
done
lemma bitOR_1_if_mod_2_nat:
‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)›
‹bitOR L (Suc 0) = (if L mod 2 = 0 then L + 1 else L)› for L :: nat
proof -
have H: ‹bitOR L 1 = L + (if bin_last (int L) then 0 else 1)›
unfolding bitOR_nat_def
apply (auto simp: bitOR_nat_def bin_last_def
bitXOR_1_if_mod_2_int)
done
show ‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)›
unfolding H
apply (auto simp: bitOR_nat_def bin_last_def)
apply presburger+
done
then show ‹bitOR L (Suc 0) = (if L mod 2 = 0 then L + 1 else L)›
by simp
qed
lemma uint64_max_uint_def: ‹unat (-1 :: 64 Word.word) = uint64_max›
proof -
have ‹unat (-1 :: 64 Word.word) = unat (- Numeral1 :: 64 Word.word)›
unfolding numeral.numeral_One ..
also have ‹… = uint64_max›
unfolding unat_bintrunc_neg
apply (simp add: uint64_max_def)
apply (subst numeral_eq_Suc; subst bintrunc.Suc; simp)+
done
finally show ?thesis .
qed
lemma nat_of_uint64_le_uint64_max: ‹nat_of_uint64 x ≤ uint64_max›
apply transfer
subgoal for x
using word_le_nat_alt[of x ‹- 1›]
unfolding uint64_max_def[symmetric] uint64_max_uint_def
by auto
done
lemma bitOR_1_if_mod_2_uint64: ‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)› for L :: uint64
proof -
have H: ‹bitOR L 1 = a ⟷ bitOR (nat_of_uint64 L) 1 = nat_of_uint64 a› for a
apply transfer
apply (rule iffI)
subgoal for L a
by (auto simp: unat_def uint_or bitOR_nat_def)
subgoal for L a
by (auto simp: unat_def uint_or bitOR_nat_def eq_nat_nat_iff
word_or_def)
done
have K: ‹L mod 2 = 0 ⟷ nat_of_uint64 L mod 2 = 0›
apply transfer
subgoal for L
using unat_mod[of L 2]
by (auto simp: unat_eq_0)
done
have L: ‹nat_of_uint64 (if L mod 2 = 0 then L + 1 else L) =
(if nat_of_uint64 L mod 2 = 0 then nat_of_uint64 L + 1 else nat_of_uint64 L)›
using nat_of_uint64_le_uint64_max[of L]
by (auto simp: K nat_of_uint64_add uint64_max_def)
show ?thesis
apply (subst H)
unfolding bitOR_1_if_mod_2_nat[symmetric] L ..
qed
lemma nat_of_uint64_plus:
‹nat_of_uint64 (a + b) = (nat_of_uint64 a + nat_of_uint64 b) mod (uint64_max + 1)›
by transfer (auto simp: unat_word_ariths uint64_max_def)
lemma nat_and:
‹ai≥ 0 ⟹ bi ≥ 0 ⟹ nat (ai AND bi) = nat ai AND nat bi›
by (auto simp: bitAND_nat_def)
lemma nat_of_uint64_and:
‹nat_of_uint64 ai ≤ uint64_max ⟹ nat_of_uint64 bi ≤ uint64_max ⟹
nat_of_uint64 (ai AND bi) = nat_of_uint64 ai AND nat_of_uint64 bi›
unfolding uint64_max_def
by transfer (auto simp: unat_def uint_and nat_and)
definition two_uint64_nat :: nat where
[simp]: ‹two_uint64_nat = 2›
lemma nat_or:
‹ai≥ 0 ⟹ bi ≥ 0 ⟹ nat (ai OR bi) = nat ai OR nat bi›
by (auto simp: bitOR_nat_def)
lemma nat_of_uint64_or:
‹nat_of_uint64 ai ≤ uint64_max ⟹ nat_of_uint64 bi ≤ uint64_max ⟹
nat_of_uint64 (ai OR bi) = nat_of_uint64 ai OR nat_of_uint64 bi›
unfolding uint64_max_def
by transfer (auto simp: unat_def uint_or nat_or)
lemma Suc_0_le_uint64_max: ‹Suc 0 ≤ uint64_max›
by (auto simp: uint64_max_def)
lemma nat_of_uint64_le_iff: ‹nat_of_uint64 a ≤ nat_of_uint64 b ⟷ a ≤ b›
apply transfer
by (auto simp: unat_def word_less_def nat_le_iff word_le_def)
lemma nat_of_uint64_notle_minus:
‹¬ ai < bi ⟹
nat_of_uint64 (ai - bi) = nat_of_uint64 ai - nat_of_uint64 bi›
apply transfer
unfolding unat_def
by (subst uint_sub_lem[THEN iffD1])
(auto simp: unat_def uint_nonnegative nat_diff_distrib word_le_def[symmetric] intro: leI)
lemma le_uint32_max_le_uint64_max: ‹a ≤ uint32_max + 2 ⟹ a ≤ uint64_max›
by (auto simp: uint32_max_def uint64_max_def)
lemma nat_of_uint64_ge_minus:
‹ai ≥ bi ⟹
nat_of_uint64 (ai - bi) = nat_of_uint64 ai - nat_of_uint64 bi›
apply transfer
unfolding unat_def
by (subst uint_sub_lem[THEN iffD1])
(auto simp: unat_def uint_nonnegative nat_diff_distrib word_le_def[symmetric] intro: leI)
definition sum_mod_uint64_max where
‹sum_mod_uint64_max a b = (a + b) mod (uint64_max + 1)›
definition uint32_max_uint32 :: uint32 where
‹uint32_max_uint32 = - 1›
lemma nat_of_uint32_uint32_max_uint32[simp]:
‹nat_of_uint32 (uint32_max_uint32) = uint32_max›
proof -
have ‹unat (Rep_uint32 (-1) :: 32 Word.word) = unat (- Numeral1 :: 32 Word.word)›
unfolding numeral.numeral_One uminus_uint32.rep_eq one_uint32.rep_eq ..
also have ‹… = uint32_max›
unfolding unat_bintrunc_neg
apply (simp add: uint32_max_def)
apply (subst numeral_eq_Suc; subst bintrunc.Suc; simp)+
done
finally show ?thesis by (simp add: nat_of_uint32_def uint32_max_uint32_def)
qed
lemma sum_mod_uint64_max_le_uint64_max[simp]: ‹sum_mod_uint64_max a b ≤ uint64_max›
unfolding sum_mod_uint64_max_def
by auto
definition uint64_of_uint32 where
‹uint64_of_uint32 n = uint64_of_nat (nat_of_uint32 n)›
export_code uint64_of_uint32 in SML
text ‹We do not want to follow the definition in the generated code (that would be crazy).
›
definition uint64_of_uint32' where
[symmetric, code]: ‹uint64_of_uint32' = uint64_of_uint32›
code_printing constant uint64_of_uint32' ⇀
(SML) "(Uint64.fromLarge (Word32.toLarge (_)))"
export_code uint64_of_uint32 checking SML_imp
export_code uint64_of_uint32 in SML_imp
lemma
assumes n[simp]: ‹n ≤ uint32_max_uint32›
shows ‹nat_of_uint64 (uint64_of_uint32 n) = nat_of_uint32 n›
proof -
have H: ‹nat_of_uint32 n ≤ uint32_max› if ‹n ≤ uint32_max_uint32› for n
apply (subst nat_of_uint32_uint32_max_uint32[symmetric])
apply (subst nat_of_uint32_le_iff)
by (auto simp: that)
have [simp]: ‹nat_of_uint32 n ≤ uint64_max› if ‹n ≤ uint32_max_uint32› for n
using H[of n] by (auto simp: that uint64_max_def uint32_max_def)
show ?thesis
apply (auto simp: uint64_of_uint32_def
nat_of_uint64_uint64_of_nat_id uint64_max_def)
by (subst nat_of_uint64_uint64_of_nat_id) auto
qed
definition zero_uint64 where
‹zero_uint64 ≡ (0 :: uint64)›
definition zero_uint32 where
‹zero_uint32 ≡ (0 :: uint32)›
definition two_uint64 where ‹two_uint64 = (2 :: uint64)›
lemma nat_of_uint64_ao:
‹nat_of_uint64 m AND nat_of_uint64 n = nat_of_uint64 (m AND n)›
‹nat_of_uint64 m OR nat_of_uint64 n = nat_of_uint64 (m OR n)›
by (simp_all add: nat_of_uint64_and nat_of_uint64_or nat_of_uint64_le_uint64_max)
subsubsection ‹Conversions›
paragraph ‹From nat to 64 bits›
definition uint64_of_nat_conv :: ‹nat ⇒ nat› where
‹uint64_of_nat_conv i = i›
paragraph ‹From nat to 32 bits›
definition nat_of_uint32_spec :: ‹nat ⇒ nat› where
[simp]: ‹nat_of_uint32_spec n = n›
paragraph ‹From 64 to nat bits›
definition nat_of_uint64_conv :: ‹nat ⇒ nat› where
[simp]: ‹nat_of_uint64_conv i = i›
paragraph ‹From 32 to nat bits›
definition nat_of_uint32_conv :: ‹nat ⇒ nat› where
[simp]: ‹nat_of_uint32_conv i = i›
definition convert_to_uint32 :: ‹nat ⇒ nat› where
[simp]: ‹convert_to_uint32 = id›
paragraph ‹From 32 to 64 bits›
definition uint64_of_uint32_conv :: ‹nat ⇒ nat› where
[simp]: ‹uint64_of_uint32_conv x = x›
lemma nat_of_uint32_le_uint32_max: ‹nat_of_uint32 n ≤ uint32_max›
using nat_of_uint32_plus[of n 0]
pos_mod_bound[of ‹uint32_max + 1› ‹nat_of_uint32 n›]
by auto
lemma nat_of_uint32_le_uint64_max: ‹nat_of_uint32 n ≤ uint64_max›
using nat_of_uint32_le_uint32_max[of n] unfolding uint64_max_def uint32_max_def
by auto
lemma nat_of_uint64_uint64_of_uint32: ‹nat_of_uint64 (uint64_of_uint32 n) = nat_of_uint32 n›
unfolding uint64_of_uint32_def
by (auto simp: nat_of_uint64_uint64_of_nat_id nat_of_uint32_le_uint64_max)
paragraph ‹From 64 to 32 bits›
definition uint32_of_uint64 where
‹uint32_of_uint64 n = uint32_of_nat (nat_of_uint64 n)›
definition uint32_of_uint64_conv where
[simp]: ‹uint32_of_uint64_conv n = n›
lemma (in -) uint64_neq0_gt: ‹j ≠ (0::uint64) ⟷ j > 0›
by transfer (auto simp: word_neq_0_conv)
lemma uint64_gt0_ge1: ‹j > 0 ⟷ j ≥ (1::uint64)›
apply (subst nat_of_uint64_less_iff[symmetric])
apply (subst nat_of_uint64_le_iff[symmetric])
by auto
definition three_uint32 where ‹three_uint32 = (3 :: uint32)›
definition nat_of_uint64_id_conv :: ‹uint64 ⇒ nat› where
‹nat_of_uint64_id_conv = nat_of_uint64›
definition op_map :: "('b ⇒ 'a) ⇒ 'a ⇒ 'b list ⇒ 'a list nres" where
‹op_map R e xs = do {
let zs = replicate (length xs) e;
(_, zs) ← WHILE⇩T⇗λ(i,zs). i ≤ length xs ∧ take i zs = map R (take i xs) ∧
length zs = length xs ∧ (∀k≥i. k < length xs ⟶ zs ! k = e)⇖
(λ(i, zs). i < length zs)
(λ(i, zs). do {ASSERT(i < length zs); RETURN (i+1, zs[i := R (xs!i)])})
(0, zs);
RETURN zs
}›
lemma op_map_map: ‹op_map R e xs ≤ RETURN (map R xs)›
unfolding op_map_def Let_def
by (refine_vcg WHILEIT_rule[where R=‹measure (λ(i,_). length xs - i)›])
(auto simp: last_conv_nth take_Suc_conv_app_nth list_update_append split: nat.splits)
lemma op_map_map_rel:
‹(op_map R e, RETURN o (map R)) ∈ ⟨Id⟩list_rel →⇩f ⟨⟨Id⟩list_rel⟩nres_rel›
by (intro frefI nres_relI) (auto simp: op_map_map)
definition array_nat_of_uint64_conv :: ‹nat list ⇒ nat list› where
‹array_nat_of_uint64_conv = id›
definition array_nat_of_uint64 :: "nat list ⇒ nat list nres" where
‹array_nat_of_uint64 xs = op_map nat_of_uint64_conv 0 xs›
lemma array_nat_of_uint64_conv_alt_def:
‹array_nat_of_uint64_conv = map nat_of_uint64_conv›
unfolding nat_of_uint64_conv_def array_nat_of_uint64_conv_def by auto
definition array_uint64_of_nat_conv :: ‹nat list ⇒ nat list› where
‹array_uint64_of_nat_conv = id›
definition array_uint64_of_nat :: "nat list ⇒ nat list nres" where
‹array_uint64_of_nat xs = op_map uint64_of_nat_conv zero_uint64_nat xs›
end