Theory LLVM_Integer
section ‹LLVM like Integer Types with Flexible Bit-Width›
theory LLVM_Integer
imports LLVM_More_Word "HOL-Library.Signed_Division"
begin
subsection ‹Lifting of Operations›
definition "cnv_uop1 f a ≡ bin_to_bl (length a) (f (bl_to_bin a))"
definition "cnv_uop2 nel f a b ≡
if length a = length b then
bin_to_bl (length a) (f (bl_to_bin a) (bl_to_bin b))
else nel ()"
definition "cnv_uop2b nel f a b ≡ if length a = length b then
f (bl_to_bin a) (bl_to_bin b)
else nel ()"
lemma cnv_uop1_correct[simp]:
"bl_to_bin (cnv_uop1 f a) = bintrunc (length a) (f (bl_to_bin a))
∧ length (cnv_uop1 f a) = length a"
by (auto simp: cnv_uop1_def)
lemma cnv_uop2_correct[simp]:
"length a = length b
⟹ bl_to_bin (cnv_uop2 nel f a b) = bintrunc (length a) (f (bl_to_bin a) (bl_to_bin b))
∧ length (cnv_uop2 nel f a b) = length b"
by (auto simp: cnv_uop2_def)
lemma cnv_uop2b_correct[simp]:
"length a = length b ⟹ cnv_uop2b nel f a b = f (bl_to_bin a) (bl_to_bin b)"
by (auto simp: cnv_uop2b_def)
definition "cnv_sop1 f a ≡ bin_to_bl (length a) (f (bl_to_sbin a))"
definition "cnv_sop2 nel f a b ≡
if length a = length b then
bin_to_bl (length a) (f (bl_to_sbin a) (bl_to_sbin b))
else
nel ()"
definition "cnv_sop2b nel f a b ≡ if length a = length b then
f (bl_to_sbin a) (bl_to_sbin b)
else nel ()"
lemma length_cnv_sop1[simp]: "length (cnv_sop1 f a) = length a"
unfolding cnv_sop1_def by auto
lemma cnv_sop1_correct[simp]: "a≠[]
⟹ bl_to_sbin (cnv_sop1 f a) = sbintrunc (length a - 1) (f (bl_to_sbin a))
∧ length (cnv_sop1 f a) = length a"
by (auto simp: cnv_sop1_def)
lemma cnv_sop2_correct[simp]: "a≠[] ⟹ length a = length b
⟹ bl_to_sbin (cnv_sop2 nel f a b) = sbintrunc (length a - 1) (f (bl_to_sbin a) (bl_to_sbin b))
∧ length (cnv_sop2 nel f a b) = length b"
apply (auto simp: cnv_sop2_def)
using sbin_bl_bin by fastforce
lemma cnv_sop2_correct'[simp]: "b≠[] ⟹ length a = length b
⟹ bl_to_sbin (cnv_sop2 nel f a b) = sbintrunc (length a - 1) (f (bl_to_sbin a) (bl_to_sbin b))
∧ length (cnv_sop2 nel f a b) = length b"
by (metis cnv_sop2_correct length_0_conv)
lemma cnv_sop2b_correct[simp]:
"length a = length b ⟹ cnv_sop2b nel f a b = f (bl_to_sbin a) (bl_to_sbin b)"
by (auto simp: cnv_sop2b_def)
lemma cnv_uop1_empty_iff[simp]: "cnv_uop1 f a = [] ⟷ a=[]"
by (auto simp: cnv_uop1_def)
lemma cnv_uop2_empty_iff[simp]: "cnv_uop2 nel f a b = [] ⟷ (if length a = length b then a=[] else nel () = [])"
by (auto simp: cnv_uop2_def)
lemma cnv_sop2_empty_iff[simp]: "cnv_sop2 nel f a b = [] ⟷ (if length a = length b then a=[] else nel () = [])"
by (auto simp: cnv_sop2_def)
lemma cnv_sop1_empty_iff[simp]: "cnv_sop1 f a = [] ⟷ a=[]"
by (auto simp: cnv_sop1_def)
subsubsection ‹Operations Independent of Signed/Unsigned Interpretation ›
definition "signed_unsigned_compat1 f ≡ ∀w a. sbintrunc w (f (sbintrunc w a)) = sbintrunc w (f a)"
definition "signed_unsigned_compat2 f ≡ ∀w a b. sbintrunc w (f (sbintrunc w a) (sbintrunc w b)) = sbintrunc w (f a b)"
lemma cnv_uop1_to_sop1:
assumes "signed_unsigned_compat1 f"
shows "cnv_uop1 f a = cnv_sop1 f a"
apply (auto simp: cnv_uop1_def cnv_sop1_def bl_to_sbin_def)
using assms unfolding signed_unsigned_compat1_def
by (metis (no_types, lifting) bin_bl_bin bintrunc_sbintruncS0 bl_bin_bl length_greater_0_conv size_bin_to_bl)
lemma cnv_uop2_to_sop2:
assumes [simp]: "length a = length b"
assumes "signed_unsigned_compat2 f"
shows "cnv_uop2 nel f a b = cnv_sop2 nel f a b"
apply (auto simp: cnv_uop2_def cnv_sop2_def bl_to_sbin_def)
using assms(2) unfolding signed_unsigned_compat2_def
by (metis (no_types, lifting) bin_bl_bin bintrunc_sbintruncS0 bl_bin_bl length_greater_0_conv size_bin_to_bl)
lemma cnv_uop1_compat_correct:
assumes [simp]: "signed_unsigned_compat1 f"
assumes [simp]: "a≠[]"
shows "bl_to_sbin (cnv_uop1 f a) = sbintrunc (length a - 1) (f (bl_to_sbin a))"
by (auto simp: cnv_uop1_to_sop1)
lemma cnv_uop2_compat_correct:
assumes [simp]: "length a = length b"
assumes [simp]: "signed_unsigned_compat2 f"
assumes [simp]: "a≠[]"
shows "bl_to_sbin (cnv_uop2 nel f a b) = sbintrunc (length a - 1) (f (bl_to_sbin a) (bl_to_sbin b))"
by (auto simp: cnv_uop2_to_sop2)
lemma cnv_uop2_compat_correct':
assumes [simp]: "length a = length b"
assumes [simp]: "signed_unsigned_compat2 f"
assumes [simp]: "b≠[]"
shows "bl_to_sbin (cnv_uop2 nel f a b) = sbintrunc (length a - 1) (f (bl_to_sbin a) (bl_to_sbin b))"
by (metis assms cnv_uop2_compat_correct length_0_conv)
lemma signed_unsigned_compat2_plus[simp]: "signed_unsigned_compat2 (+)"
apply (auto simp: signed_unsigned_compat2_def sbintrunc_mod2p)
apply (pull_push_mods)
by (simp add: algebra_simps)
lemma signed_unsigned_compat2_minus[simp]: "signed_unsigned_compat2 (-)"
apply (clarsimp simp: signed_unsigned_compat2_def sbintrunc_mod2p)
apply (pull_push_mods)
by (simp add: algebra_simps)
lemma signed_unsigned_compat2_mult[simp]: "signed_unsigned_compat2 (*)"
apply (auto simp: signed_unsigned_compat2_def sbintrunc_mod2p)
apply pull_push_mods
by (simp add: algebra_simps)
subsection ‹Bitwise Interpretation of Operations›
text ‹Provides an additional sanity check, by equating our definitions with the definitions found in
"OLD:HOL-Word.Bits_Int". Unfortunately, they do not define minus there.›
lemma cnv_plus_rbl_conv: "length a = length b ⟹ cnv_uop2 nel (+) a b = rev (rbl_add (rev a) (rev b))"
apply (rule sym)
apply (subst bl_bin_bl[symmetric, of a])
apply (subst bl_bin_bl[symmetric, of b])
by (auto simp: cnv_uop2_def rbl_add simp del: bl_bin_bl)
lemma cnv_mult_rbl_conv: "length a = length b ⟹ cnv_uop2 nel (*) a b = rev (rbl_mult (rev a) (rev b))"
apply (rule sym)
apply (subst bl_bin_bl[symmetric, of a])
apply (subst bl_bin_bl[symmetric, of b])
by (auto simp: cnv_uop2_def rbl_mult simp del: bl_bin_bl)
lemma cnv_AND_bl_conv: "length a = length b ⟹ cnv_uop2 nel (AND) a b = map2 (∧) a b"
apply (rule sym)
apply (subst bl_bin_bl[symmetric, of a])
apply (subst bl_bin_bl[symmetric, of b])
by (auto simp: cnv_uop2_def bl_and_bin simp del: bl_bin_bl)
lemma cnv_OR_bl_conv: "length a = length b ⟹ cnv_uop2 nel (OR) a b = map2 (∨) a b"
apply (rule sym)
apply (subst bl_bin_bl[symmetric, of a])
apply (subst bl_bin_bl[symmetric, of b])
by (auto simp: cnv_uop2_def bl_or_bin simp del: bl_bin_bl)
lemma cnv_XOR_bl_conv: "length a = length b ⟹ cnv_uop2 nel (XOR) a b = map2 (≠) a b"
apply (rule sym)
apply (subst bl_bin_bl[symmetric, of a])
apply (subst bl_bin_bl[symmetric, of b])
by (auto simp: bl_xor_bin[simplified] cnv_uop2_def simp del: bl_bin_bl)
lemma cnv_NOT_bl_conv: "cnv_uop1 (NOT) a = map Not a"
apply (rule sym)
apply (subst bl_bin_bl[symmetric, of a])
apply (simp only: bl_not_bin)
by (auto simp: cnv_uop1_def)
lemma cnv_SHL_bl_conv: "n≤length a ⟹ cnv_uop1 (λx. x * 2^n) a = drop n a @ replicate n False"
by (auto simp: cnv_uop1_def bl_bin_bl_rep_drop)
lemma butlast_bin_to_bl_aux: "acc≠[] ⟹ butlast (bin_to_bl_aux w i acc) = bin_to_bl_aux w i (butlast acc)"
by (simp add: bin_to_bl_aux_alt butlast_append)
find_theorems bin_to_bl_aux "(@)"
lemma bin_to_bl_Suc: "bin_to_bl (Suc w) i = bin_to_bl w (bin_rest i) @ [bin_last i]"
by (simp add: bin_to_bl_aux_append bin_to_bl_def)
lemma "butlast (bin_to_bl w n) = bin_to_bl (w-1) (bin_rest n)" oops
thm butlast_rest_bin
find_theorems "bin_to_bl _ _ ! _"
lemma bin_to_bl_div2_shift: "⟦w≠0; n≥0; n<2^w⟧ ⟹ bin_to_bl w (n div 2) = False # butlast (bin_to_bl w n)"
apply (cases w; simp)
apply (rule nth_equalityI)
apply (auto simp: butlast_rest_bin nth_Cons nth_bin_to_bl bit_iff_odd split: nat.splits)
done
lemma div_div_p2_eq_div_p2s:
"w div (2^a) div (2^b) = (w::int) div 2^(a+b)"
"w div 2 div (2^b) = (w::int) div 2^(Suc b)"
by (simp_all add: div_mult2_eq power_add zdiv_zmult2_eq)
lemma bin_to_bl_div2p_shift: "⟦n≥0; n<2^w; k≤w⟧ ⟹ bin_to_bl w (n div 2^k) = replicate k False @ take (w-k) (bin_to_bl w n)"
apply (rule nth_equalityI)
apply simp
apply clarsimp
apply auto
apply (auto simp: butlast_rest_bin nth_Cons nth_append nth_bin_to_bl split: nat.splits if_splits)
subgoal apply (auto simp: bit_int_def algebra_simps div_div_p2_eq_div_p2s)
by (metis Nat.add_diff_assoc2 Suc_leI add.commute bits_div_0 div_div_p2_eq_div_p2s(1) div_pos_pos_trivial dvd_0_right)
subgoal
by (simp add: add.commute bit_int_def div_exp_eq)
subgoal
by (simp add: add.commute bit_iff_odd div_div_p2_eq_div_p2s(1))
done
lemma cnv_LSHR_bl_conv: "n≤length a ⟹ cnv_uop1 (λx. x div 2^n) a = replicate n False @ take (length a - n) a"
apply (cases "length a")
apply (auto simp: cnv_uop1_def bin_to_bl_div2p_shift)
by (metis bin_to_bl_div2p_shift bl_bin_bl bl_to_bin_ge0 bl_to_bin_lt2p)
text ‹Note: This division is with rounding down!›
lemma bin_to_bl_sdiv2_shift:
assumes ran: "-(2^w)≤i" "i<2^w"
shows "bin_to_bl (Suc w) (i div 2) = hd (bin_to_bl (Suc w) i) # butlast (bin_to_bl (Suc w) i)"
proof -
have "⟦ ¬ 0 ≤ (i::int)⟧ ⟹ i div (2*2^w) = -1" using ran
by (smt cancel_div_mod_rules(2) div_pos_pos_trivial mod_add_self2 mult_cancel_left1 mult_minus_right)
then show ?thesis using ran
apply (rule_tac nth_equalityI)
apply (auto
simp: butlast_rest_bin nth_Cons bl_sbin_sign nth_bin_to_bl bin_sign_def sbintrunc_mod2p div_div_p2_eq_div_p2s bit_int_def
split: nat.splits)
done
qed
lemma bin_to_bl_sdiv2p_shift:
assumes ran: "-(2^w)≤i" "i<2^w" and K: "k<Suc w"
shows "bin_to_bl (Suc w) (i div 2^k) = replicate k (hd (bin_to_bl (Suc w) i)) @ take (Suc w - k) (bin_to_bl (Suc w) i)"
proof -
have "⟦¬0≤i; x≥w⟧ ⟹ i div (2^x) = -1" for x using ran
apply auto
by (smt cancel_div_mod_rules(2) int_mod_eq' linorder_not_le mod_add_self2 mult_cancel_left1 mult_minus_right power_strict_increasing_iff)
with ran K show ?thesis
apply (rule_tac nth_equalityI)
apply (auto
simp: butlast_rest_bin nth_Cons bl_sbin_sign nth_bin_to_bl bit_int_def bin_sign_def sbintrunc_mod2p div_div_p2_eq_div_p2s
simp: nth_append algebra_simps
split: nat.splits)
by (smt (verit, ccfv_SIG) Nat.add_diff_assoc2 div_pos_pos_trivial even_add le_add2 le_eq_less_or_eq power_increasing_iff)
qed
lemma cnv_ASHR_bl_conv: "n<length a ⟹ cnv_sop1 (λx. x div 2^n) a = replicate n (hd a) @ take (length a - n) a"
apply (cases "length a")
apply (auto simp: cnv_sop1_def)
by (metis bin_to_bl_sdiv2p_shift bl_sbin_bl bl_to_sbin_def diff_Suc_1 sbintr_ge sbintr_lt)
subsection ‹Signed and Unsigned Extension and Truncation›
definition bl_trunc :: "nat ⇒ bool list ⇒ bool list" where "bl_trunc w bl ≡ drop (length bl - w) bl"
lemma bl_trunc_ge[simp]: "length bl < w ⟹ bl_trunc w bl = bl"
by (simp add: bl_trunc_def)
lemma trunc_bl_to_bin[simp]: "bl_to_bin (bl_trunc w bl) = bintrunc w (bl_to_bin bl)"
by (simp add: bl_trunc_def trunc_bl2bin)
lemma trunc_bl_to_sbin[simp]:
"w>0 ⟹ bl_to_sbin (bl_trunc w bl) = sbintrunc (w-1) (bl_to_sbin bl)"
apply (cases "w ≤ length bl")
apply (auto simp: bl_trunc_def bl_to_sbin_def bl2bin_drop min_def)
done
lemma bl_trunc_len[simp]: "length (bl_trunc w bl) = min w (length bl)"
by (auto simp: bl_trunc_def)
lemma bl_trunc_eq_Nil_conv[simp]: "bl_trunc w l = [] ⟷ w=0 ∨ l=[]"
by (cases l) (auto simp: bl_trunc_def)
definition bl_zext :: "nat ⇒ bool list ⇒ bool list" where "bl_zext w bl ≡ replicate (w - length bl) False @ bl"
lemma bl_zext_le[simp]: "w≤length bl ⟹ bl_zext w bl = bl"
by (auto simp: bl_zext_def)
lemma bl_zext_to_bin[simp]: "bl_to_bin (bl_zext w bl) = bl_to_bin bl"
by (auto simp: bl_zext_def bl_to_bin_rep_F)
lemma bl_zext_len[simp]: "length (bl_zext w bl) = max w (length bl)"
by (auto simp: bl_zext_def)
lemma bl_zext_Nil_conv[simp]: "bl_zext w bl = [] ⟷ w=0 ∧ bl = []"
by (auto simp: bl_zext_def)
definition bl_sext :: "nat ⇒ bool list ⇒ bool list" where "bl_sext w bl ≡ replicate (w - length bl) (hd bl) @ bl"
lemma bl_sext_le[simp]: "w≤length bl ⟹ bl_sext w bl = bl"
by (auto simp: bl_sext_def)
lemma bl_to_sbin_pos_conv_bin: "¬hd bl ⟹ bl_to_sbin bl = bl_to_bin bl"
by (auto simp: bl_to_sbin_alt split: list.split)
lemma bl_to_sbin_neg_conv_bin: "bl≠[] ⟹ hd bl ⟹ bl_to_sbin bl = bl_to_bin bl - 2^(length bl)"
by (auto simp: bl_to_sbin_alt split: list.split)
lemma bl_sext_to_sbin[simp]:
assumes [simp]: "bl≠[]"
shows "bl_to_sbin (bl_sext w bl) = bl_to_sbin bl"
apply (cases "w>length bl"; simp?)
proof (cases "hd bl")
case True
assume "length bl < w"
with True show ?thesis
apply (auto simp: bl_to_sbin_neg_conv_bin bl_sext_def bl_to_bin_rep_T algebra_simps)
by (metis diff_add_inverse less_imp_add_positive power_add)
next
case False
assume "length bl < w"
with False show ?thesis by (auto simp: bl_to_sbin_pos_conv_bin bl_sext_def bl_to_bin_rep_F)
qed
lemma bl_sext_len[simp]: "length (bl_sext w bl) = max w (length bl)"
by (auto simp: bl_sext_def)
lemma bl_sext_Nil_conv[simp]: "bl_sext w bl = [] ⟷ w=0 ∧ bl = []"
by (auto simp: bl_sext_def)
subsection ‹LLVM Integer Datatype›
typedef lint = "{l::bool list. True }"
morphisms lint_to_bits bits_to_lint
by auto
setup_lifting type_definition_lint
instantiation lint :: equal
begin
lift_definition equal_lint :: "lint ⇒ lint ⇒ bool" is "equal_class.equal" .
instance
apply intro_classes
apply transfer
apply (rule equal_eq)
done
end
lift_definition width :: "lint ⇒ nat" is length .
lift_definition lint_to_uint :: "lint ⇒ int" is bl_to_bin .
lift_definition lint_to_sint :: "lint ⇒ int" is bl_to_sbin .
lemma uint_lower_bound[simp]: "0≤lint_to_uint a"
apply transfer using bl_to_bin_ge0 by auto
lemma uint_upper_bound[simp]: "lint_to_uint a < 2^width a"
apply transfer by (simp add: bl_to_bin_lt2p)
lemma sint_lower_bound[simp]: "-(2^(width a - 1))≤lint_to_sint a"
apply transfer by (simp add: bl_to_sbin_def sbintr_ge)
lemma sint_upper_bound[simp]: "lint_to_sint a < 2^(width a - 1)"
apply transfer by (simp add: bl_to_sbin_def sbintr_lt)
subsubsection ‹Overflows›
definition "uovf1 f a ≡ f (lint_to_uint a) ∉ uints (width a)"
definition "sovf1 f a ≡ f (lint_to_sint a) ∉ sints (width a)"
definition "uovf2 f a b ≡ f (lint_to_uint a) (lint_to_uint b) ∉ uints (width a)"
definition "sovf2 f a b ≡ f (lint_to_sint a) (lint_to_sint b) ∉ sints (width a)"
subsubsection ‹Operations›
lift_definition lconst :: "nat ⇒ int ⇒ lint" is "λw i. bin_to_bl w i" by simp
lemma width_lconst[simp]: "width (lconst w i) = w"
by transfer auto
lemma uint_const[simp]: "lint_to_uint (lconst w c) = bintrunc w c"
by transfer auto
lemma sint_const[simp]: "w≠0 ⟹ lint_to_sint (lconst w c) = sbintrunc (w-1) c"
by transfer (auto)
lemma bits_zero[simp]: "lint_to_bits (lconst w 0) = replicate w False"
by transfer (auto simp: bin_to_bl_zero)
lemma bits_minus1[simp]: "lint_to_bits (lconst w (-1)) = replicate w True"
by transfer (auto simp: bin_to_bl_minus1)
lemma lconst_eq_iff[simp]:
"lconst w c = lconst w' c' ⟷ w'=w ∧ (c' mod 2^w = c mod 2^w)"
apply safe
subgoal
apply transfer
by (metis len_bin_to_bl)
subgoal
apply transfer
by (metis bin_bl_bin bintrunc_mod2p len_bin_to_bl)
subgoal
apply transfer
by (auto simp: max_def bintrunc_mod2p bl_to_bin_inj)
done
definition "lint_abort (_::unit) ≡ lint_to_bits undefined"
definition "lint_abort_bool (_::unit) ≡ undefined::bool"
declare [[ code abort: lint_abort lint_abort_bool]]
instantiation lint :: "{plus,minus,times,divide,modulo,uminus}"
begin
lift_definition plus_lint :: "lint ⇒ lint ⇒ lint" is "cnv_uop2 (lint_abort) (+)" by simp
lift_definition minus_lint :: "lint ⇒ lint ⇒ lint" is "cnv_uop2 (lint_abort) (-)" by simp
lift_definition times_lint :: "lint ⇒ lint ⇒ lint" is "cnv_uop2 (lint_abort) (*)" by simp
lift_definition divide_lint :: "lint ⇒ lint ⇒ lint" is "cnv_uop2 (lint_abort) (div)" by simp
lift_definition modulo_lint :: "lint ⇒ lint ⇒ lint" is "cnv_uop2 (lint_abort) (mod)" by simp
lift_definition uminus_lint :: "lint ⇒ lint" is "cnv_sop1 uminus" by simp
definition sdivrem_ovf :: "lint ⇒ lint ⇒ bool" where
"sdivrem_ovf a b ≡ lint_to_sint a sdiv lint_to_sint b ∉ sints (width a)"
instance ..
end
instantiation lint :: "{signed_divide, signed_modulo}"
begin
lift_definition signed_divide_lint :: "lint ⇒ lint ⇒ lint"
is "λa b. if bl_to_sbin a sdiv bl_to_sbin b ∈ sints (length a) then cnv_sop2 lint_abort (sdiv) a b else lint_abort ()"
by simp
lift_definition signed_modulo_lint :: "lint ⇒ lint ⇒ lint"
is "λa b. if bl_to_sbin a sdiv bl_to_sbin b ∈ sints (length a) then cnv_sop2 lint_abort (smod) a b else lint_abort ()"
by simp
instance by standard
end
lemma width_plus[simp]:
assumes "width a = width b"
shows "width (a+b) = width b"
using assms by transfer auto
lemma uint_plus[simp]:
assumes "width a = width b"
shows "lint_to_uint (a+b) = bintrunc (width b) (lint_to_uint a + lint_to_uint b)"
using assms by transfer auto
lemma sint_plus[simp]:
assumes "width a = width b" "width b ≠ 0"
shows "lint_to_sint (a+b) = sbintrunc (width b - 1) (lint_to_sint a + lint_to_sint b)"
using assms by transfer (auto simp: cnv_uop2_compat_correct')
lemma width_minus[simp]:
assumes "width a = width b"
shows "width (a-b) = width b"
using assms by transfer auto
lemma uint_minus[simp]:
assumes "width a = width b"
shows "lint_to_uint (a-b) = bintrunc (width b) (lint_to_uint a - lint_to_uint b)"
using assms
by transfer auto
lemma sint_minus[simp]:
assumes "width a = width b" "width b ≠ 0"
shows "lint_to_sint (a-b) = sbintrunc (width b - 1) (lint_to_sint a - lint_to_sint b)"
using assms
by transfer (auto simp: cnv_uop2_compat_correct')
lemma width_times[simp]:
assumes "width a = width b"
shows "width (a*b) = width b"
using assms by transfer auto
lemma uint_times[simp]:
assumes "width a = width b"
shows "lint_to_uint (a*b) = bintrunc (width b) (lint_to_uint a * lint_to_uint b)"
using assms
by transfer auto
lemma sint_times[simp]:
assumes "width a = width b" "width b ≠ 0"
shows "lint_to_sint (a*b) = sbintrunc (width b - 1) (lint_to_sint a * lint_to_sint b)"
using assms
by transfer (auto simp: cnv_uop2_compat_correct')
lemma width_divide[simp]:
assumes "width a = width b"
shows "width (a div b) = width b"
using assms by transfer auto
lemma uint_divide[simp]:
assumes "width a = width b"
shows "lint_to_uint (a div b) = bintrunc (width b) (lint_to_uint a div lint_to_uint b)"
using assms
by transfer auto
lemma width_sdivide[simp]:
assumes "width a = width b" "width b ≠ 0"
assumes "¬sdivrem_ovf a b"
shows "width (a sdiv b) = width b"
using assms unfolding sdivrem_ovf_def
by transfer auto
lemma sint_sdivide[simp]:
assumes "width a = width b" "width b ≠ 0"
assumes "¬sdivrem_ovf a b"
shows "lint_to_sint (a sdiv b) = sbintrunc (width b - 1) ((lint_to_sint a) sdiv (lint_to_sint b))"
using assms unfolding sdivrem_ovf_def
by transfer auto
lemma width_modulo[simp]:
assumes "width a = width b"
shows "width (a mod b) = width b"
using assms by transfer auto
lemma uint_modulo[simp]:
assumes "width a = width b"
shows "lint_to_uint (a mod b) = bintrunc (width b) (lint_to_uint a mod lint_to_uint b)"
using assms
by transfer auto
lemma width_srem[simp]:
assumes "width a = width b" "width b ≠ 0"
assumes "¬sdivrem_ovf a b"
shows "width (a smod b) = width b"
using assms unfolding sdivrem_ovf_def
by transfer auto
lemma sint_remainder[simp]:
assumes "width a = width b" "width b ≠ 0"
assumes "¬sdivrem_ovf a b"
shows "lint_to_sint (a smod b) = sbintrunc (width b - 1) ((lint_to_sint a) smod (lint_to_sint b))"
using assms unfolding sdivrem_ovf_def
by transfer auto
lemma width_uminus[simp]:
"width (- a) = width a"
by transfer auto
lemma sint_uminus[simp]:
"width a ≠ 0 ⟹ lint_to_sint (- a) = sbintrunc (width a - 1) (- lint_to_sint a)"
by transfer auto
instantiation lint :: "{ord}"
begin
lift_definition less_lint :: "lint ⇒ lint ⇒ bool" is "cnv_uop2b lint_abort_bool (<)" .
lift_definition less_eq_lint :: "lint ⇒ lint ⇒ bool" is "cnv_uop2b lint_abort_bool (≤)" .
instance ..
end
lift_definition sless_lint :: "lint ⇒ lint ⇒ bool" (infix "<⇩s" 50) is "cnv_sop2b lint_abort_bool (<)" .
lift_definition sless_eq_lint :: "lint ⇒ lint ⇒ bool" (infix "≤⇩s" 50) is "cnv_sop2b lint_abort_bool (≤)" .
lemma uint_less[simp]:
assumes "width a = width b"
shows "a < b ⟷ lint_to_uint a < lint_to_uint b"
using assms by transfer auto
lemma uint_less_eq[simp]:
assumes "width a = width b"
shows "a ≤ b ⟷ lint_to_uint a ≤ lint_to_uint b"
using assms by transfer auto
lemma sint_less[simp]:
assumes "width a = width b"
shows "a <⇩s b ⟷ lint_to_sint a < lint_to_sint b"
using assms by transfer auto
lemma sint_less_eq[simp]:
assumes "width a = width b"
shows "a ≤⇩s b ⟷ lint_to_sint a ≤ lint_to_sint b"
using assms by transfer auto
text ‹Yields ‹0⇩1› on attempt to truncate to zero›
lift_definition trunc :: "nat ⇒ lint ⇒ lint" is "λw a. if w=0 then [False] else bl_trunc w a"
by auto
lemma width_trunc[simp]: "w≠0 ⟹ width (trunc w a) = min w (width a)" by transfer auto
lemma uint_trunc[simp]: "w≠0 ⟹ lint_to_uint (trunc w a) = bintrunc w (lint_to_uint a)"
by transfer auto
lemma sint_trunc[simp]: "w≠0 ⟹ lint_to_sint (trunc w a) = sbintrunc (w-1) (lint_to_sint a)"
by transfer auto
lift_definition zext :: "nat ⇒ lint ⇒ lint" is "bl_zext" by simp
lift_definition sext :: "nat ⇒ lint ⇒ lint" is "bl_sext" by simp
lemma width_zext[simp]: "width (zext w a) = max w (width a)"
by transfer auto
lemma width_sext[simp]: "width (sext w a) = max w (width a)"
by transfer auto
lemma uint_zext[simp]: "lint_to_uint (zext w a) = lint_to_uint a"
by transfer auto
lemma sint_sext[simp]: "width a ≠ 0 ⟹ lint_to_sint (sext w a) = lint_to_sint a"
by transfer auto
lift_definition and_lint :: "lint ⇒ lint ⇒ lint" (infixr ‹lliAND› 64) is "cnv_uop2 lint_abort (AND)" by simp
lift_definition or_lint :: "lint ⇒ lint ⇒ lint" (infixr ‹lliOR› 59) is "cnv_uop2 lint_abort (OR)" by simp
lift_definition xor_lint :: "lint ⇒ lint ⇒ lint" (infixr ‹lliXOR› 59) is "cnv_uop2 lint_abort (XOR)" by simp
lift_definition not_lint :: "lint ⇒ lint" (‹lliNOT›) is "cnv_uop1 (NOT)" by simp
lemma width_AND[simp]:
assumes "width a = width b"
shows "width (a lliAND b) = width b"
using assms by transfer auto
lemma uint_AND[simp]:
assumes "width a = width b"
shows "lint_to_uint (a lliAND b) = lint_to_uint a AND lint_to_uint b"
using assms apply (transfer)
apply (auto simp: )
by (metis trunc_bl2bin_len)
lemma width_OR[simp]:
assumes "width a = width b"
shows "width (a lliOR b) = width b"
using assms by transfer auto
lemma uint_OR[simp]:
assumes "width a = width b"
shows "lint_to_uint (a lliOR b) = lint_to_uint a OR lint_to_uint b"
using assms apply (transfer)
by (metis bin_trunc_ao(2) cnv_uop2_correct trunc_bl2bin_len)
lemma width_XOR[simp]:
assumes "width a = width b"
shows "width (a lliXOR b) = width b"
using assms by transfer auto
lemma uint_XOR[simp]:
assumes "width a = width b"
shows "lint_to_uint (a lliXOR b) = lint_to_uint a XOR lint_to_uint b"
using assms apply (transfer)
by (metis cnv_uop2_correct take_bit_xor trunc_bl2bin_len)
lemma width_NOT[simp]:
"width (lliNOT a) = width a"
by transfer auto
lemma uint_NOT[simp]:
shows "lint_to_uint (lliNOT a) = bintrunc (width a) (NOT (lint_to_uint a))"
by transfer auto
lemma bits_NOT[simp]: "lint_to_bits (lliNOT a) = map Not (lint_to_bits a)"
by transfer (auto simp: cnv_NOT_bl_conv)
lemma bits_AND[simp]: "width a = width b ⟹ lint_to_bits (a lliAND b) = map2 (∧) (lint_to_bits a) (lint_to_bits b)"
by transfer (auto simp: cnv_AND_bl_conv)
lemma bits_OR[simp]: "width a = width b ⟹ lint_to_bits (a lliOR b) = map2 (∨) (lint_to_bits a) (lint_to_bits b)"
by transfer (auto simp: cnv_OR_bl_conv)
lemma bits_XOR[simp]: "width a = width b ⟹ lint_to_bits (a lliXOR b) = map2 (≠) (lint_to_bits a) (lint_to_bits b)"
by transfer (auto simp: cnv_XOR_bl_conv)
lift_definition bitSHL :: "lint ⇒ nat ⇒ lint" is "λbl n. cnv_uop1 (λx. x*2^n) bl" by simp
lift_definition bitLSHR :: "lint ⇒ nat ⇒ lint" is "λbl n. cnv_uop1 (λx. x div 2^n) bl" by simp
lift_definition bitASHR :: "lint ⇒ nat ⇒ lint" is "λbl n. cnv_sop1 (λx. x div 2^n) bl" by simp
lemma width_bitSHL[simp]: "width (bitSHL a n) = width a"
by transfer auto
lemma uint_bitSHL[simp]: "lint_to_uint (bitSHL a n) = bintrunc (width a) (2^n * lint_to_uint a)"
by transfer (auto simp: algebra_simps)
lemma sint_bitSHL[simp]: "width a ≠ 0 ⟹ lint_to_sint (bitSHL a n) = sbintrunc (width a - 1) (2^n * lint_to_sint a)"
apply transfer
apply (simp add: bl_to_sbin_def sbintrunc_mod2p bintrunc_mod2p)
apply (pull_push_mods)
apply (auto simp: algebra_simps)
done
lemma width_bitLSHR[simp]: "width (bitLSHR a n) = width a"
by transfer auto
lemma uint_bitLSHR[simp]: "lint_to_uint (bitLSHR a n) = lint_to_uint a div 2^n"
apply transfer
apply (auto
simp: bintrunc_mod2p algebra_simps pos_imp_zdiv_nonneg_iff bl_to_bin_ge0
intro!: mod_pos_pos_trivial)
by (smt bl_to_bin_ge0 bl_to_bin_lt2p div_by_1 div_pos_pos_trivial int_div_less_self zero_less_power)
lemma width_bitASHR[simp]: "width (bitASHR a n) = width a"
by transfer auto
lemma sint_bitASHR[simp]: "width a ≠ 0 ⟹ lint_to_sint (bitASHR a n) = lint_to_sint a div 2^n"
apply transfer
using bl_to_sbin_in_sints
apply (clarsimp simp: sbintrunc_eq_if_in_range sints_num)
by (smt div_by_1 pos_imp_zdiv_nonneg_iff zdiv_mono2 zdiv_mono2_neg zero_less_power)
lemma uint_eq:
"a = b ⟷ lint_to_uint a = lint_to_uint b ∧ width a = width b"
apply (transfer)
using bl_to_bin_inj
by auto
lemma sint_eq:
"a = b ⟷ lint_to_sint a = lint_to_sint b ∧ width a = width b"
apply (transfer)
apply auto
by (metis bl_sbin_bl)
lemma lconst_inj: "lconst w a = lconst w b ⟷ a mod 2^w = b mod 2^w" by auto
subsection ‹‹i1› as Boolean›
definition "ltrue ≡ lconst 1 1"
definition "lfalse ≡ lconst 1 0"
definition "bool_to_lint b ≡ if b then ltrue else lfalse"
definition "lint_to_bool a ≡ if a = ltrue then True else if a = lfalse then False else lint_abort_bool ()"
lemma lbool_cases: "width a = 1 ⟹ a=ltrue ∨ a=lfalse"
unfolding ltrue_def lfalse_def
apply transfer
apply auto
by (smt (verit, ccfv_threshold) append.simps(2) bin_to_bl_Suc bin_to_bl_eq_Nil_conv bin_to_bl_zero bl_sbin_bl div_pos_pos_trivial even_add last_snoc rbbl_Cons rev_append rev_bin_to_bl_simps(1) rev_bin_to_bl_simps(4))
lemma lint_bool_simps[simp]:
"width ltrue = 1"
"width lfalse = 1"
"lint_to_uint ltrue = 1"
"lint_to_uint lfalse = 0"
"lint_to_sint ltrue = -1"
"lint_to_sint lfalse = 0"
"width (bool_to_lint b) = 1"
"width a = 1 ⟹ lint_to_bool a ⟷ a = ltrue"
"lint_to_bool (bool_to_lint b) = b"
"width a = 1 ⟹ bool_to_lint (lint_to_bool a) = a"
using lbool_cases
unfolding ltrue_def lfalse_def bool_to_lint_def lint_to_bool_def
by (auto)
section ‹Connection to Word Datatype›
definition lint_to_word :: "lint ⇒ 'a::len word" where "lint_to_word ≡ word_of_int o lint_to_uint"
definition word_to_lint :: "'a::len word ⇒ lint" where "word_to_lint ≡ lconst (len_of TYPE('a)) o uint"
lemma lint_word_inv[simp]: "lint_to_word (word_to_lint w) = w"
by (auto simp: word_to_lint_def lint_to_word_def)
lemma word_lint_inv[simp]: "LENGTH ('a::len) = width i ⟹ word_to_lint (lint_to_word i :: 'a word) = i"
apply (auto simp: word_to_lint_def lint_to_word_def)
by (metis uint_const uint_eq uint_lower_bound uint_upper_bound width_lconst word_of_int_inverse word_ubin.norm_Rep)
lemma bin_to_bl_eq_iff: "bin_to_bl w x = bin_to_bl w y ⟷ bintrunc w x = bintrunc w y"
by (metis bin_bl_bin bl_bin_bl size_bin_to_bl)
named_theorems word_to_lint_convs
lemma word_to_lint_plus[word_to_lint_convs]: "word_to_lint (a+b) = word_to_lint a + word_to_lint b"
apply (auto simp: word_to_lint_def lint_to_word_def)
apply transfer
apply (auto simp: cnv_uop2_def bin_to_bl_eq_iff bintrunc_mod2p mod_add_eq)
done
lemma word_to_lint_minus[word_to_lint_convs]: "word_to_lint (a-b) = word_to_lint a - word_to_lint b"
apply (auto simp: word_to_lint_def lint_to_word_def)
apply transfer
apply (auto simp: cnv_uop2_def bin_to_bl_eq_iff bintrunc_mod2p mod_diff_eq)
done
lemma word_to_lint_mult[word_to_lint_convs]: "word_to_lint (a*b) = word_to_lint a * word_to_lint b"
apply (auto simp: word_to_lint_def lint_to_word_def)
apply transfer
apply (auto simp: cnv_uop2_def bin_to_bl_eq_iff bintrunc_mod2p mod_mult_eq)
done
lemma word_to_lint_eq[word_to_lint_convs]: "word_to_lint a = word_to_lint b ⟷ a=b"
by (auto simp: word_to_lint_def word_uint.Rep_inject)
lemma word_to_lint_ule[word_to_lint_convs]: "word_to_lint a ≤ word_to_lint b ⟷ a≤b"
by (auto simp: word_to_lint_def lint_to_word_def word_le_def)
lemma word_to_lint_ult[word_to_lint_convs]: "word_to_lint a < word_to_lint b ⟷ a<b"
by (auto simp: word_to_lint_def lint_to_word_def word_less_def)
lemma word_to_lint_sle[word_to_lint_convs]: "word_to_lint a ≤⇩s word_to_lint b ⟷ a <=s b"
by (auto simp: word_to_lint_def lint_to_word_def word_sle_def sint_uint)
lemma word_to_lint_slt[word_to_lint_convs]: "word_to_lint a <⇩s word_to_lint b ⟷ a <s b"
by (auto simp: word_to_lint_def lint_to_word_def word_sless_alt sint_uint)
lemma word_to_lint_div[word_to_lint_convs]: "word_to_lint (a div b) = word_to_lint a div word_to_lint b"
apply (auto simp: word_to_lint_def lint_to_word_def)
apply transfer'
apply (auto simp: cnv_uop2_def bin_to_bl_eq_iff bintrunc_mod2p uint_div_alt)
done
lemma word_to_lint_mod[word_to_lint_convs]: "word_to_lint (a mod b) = word_to_lint a mod word_to_lint b"
apply (auto simp: word_to_lint_def lint_to_word_def)
apply transfer'
apply (auto simp: cnv_uop2_def bin_to_bl_eq_iff bintrunc_mod2p uint_mod_alt)
done
lemma word_to_lint_sdiv[word_to_lint_convs]:
fixes a b :: "'a::len word"
assumes "sint a sdiv sint b ∈ sints LENGTH('a)"
shows "word_to_lint (a sdiv b) = word_to_lint a sdiv word_to_lint b"
using assms
apply (auto simp: word_to_lint_def lint_to_word_def sints_def)
apply transfer'
by (smt (z3) One_nat_def bin_to_bl_trunc bintrunc_sbintruncS0 cnv_sop2_def len_bin_to_bl len_gt_0 order_refl sbin_bl_bin sbintrunc_eq_if_in_range)
lemma word_to_lint_smod[word_to_lint_convs]:
fixes a b :: "'a::len word"
assumes "sint a sdiv sint b ∈ sints LENGTH('a)"
shows "word_to_lint (a smod b) = word_to_lint a smod word_to_lint b"
using assms
apply (auto simp: word_to_lint_def lint_to_word_def sints_def)
apply transfer'
by (smt (z3) One_nat_def bin_to_bl_trunc cnv_sop2_def len_gt_0 order_refl sbin_bl_bin sbintrunc_eq_if_in_range sbintrunc_sbintrunc size_bin_to_bl)
lemma word_to_lint_shl[word_to_lint_convs]: "word_to_lint ((a::_::len word) << n) = bitSHL (word_to_lint a) n"
apply (auto simp: word_to_lint_def)
apply transfer'
apply (auto simp: cnv_uop1_def bin_to_bl_eq_iff bintrunc_mod2p shiftl_t2n uint_word_ariths algebra_simps)
by (simp add: push_bit_eq_mult mod_mult_right_eq semiring_normalization_rules(7) shiftl_int_def)
lemma word_to_lint_lshr[word_to_lint_convs]: "word_to_lint ((a::_::len word) >> n) = bitLSHR (word_to_lint a) n"
apply (auto simp: word_to_lint_def)
apply transfer'
apply (auto simp: cnv_uop1_def bin_to_bl_eq_iff bintrunc_mod2p uint_word_ariths shiftr_div_2n algebra_simps)
by (metis drop_bit_eq_div)
lemma word_to_lint_ashr[word_to_lint_convs]: "word_to_lint (a >>> n) = bitASHR (word_to_lint (a::'a::len word)) n"
unfolding word_to_lint_def
apply transfer'
apply (auto simp: cnv_sop1_def uint_sint sshiftr_div_2n drop_bit_eq_div)
done
lemma word_to_lint_ucast_down[word_to_lint_convs]: "is_down UCAST('a → 'b) ⟹ word_to_lint (UCAST('a::len→'b::len) a) = trunc (LENGTH('b)) (word_to_lint a)"
unfolding word_to_lint_def
apply transfer'
apply (auto simp: to_bl_ucast simp flip: to_bl_bin)
apply (auto simp: bl_trunc_def)
using diff_diff_cancel drop_bin2bl by presburger
lemma word_to_lint_scast_down[word_to_lint_convs]: "is_down SCAST('a → 'b) ⟹ word_to_lint (SCAST('a::len→'b::len) a) = trunc (LENGTH('b)) (word_to_lint a)"
unfolding word_to_lint_def
apply transfer'
apply (auto simp: to_bl_scast_down simp flip: to_bl_bin)
apply (auto simp: bl_trunc_def)
using diff_diff_cancel drop_bin2bl by presburger
lemma zext_in_range: "⟦w'≠0; w'≤w; 0≤a; a<2^w'⟧ ⟹ zext w (lconst w' a) = lconst w a"
apply transfer'
apply (auto simp: bl_zext_def)
by (metis bin_bl_bin bintrunc_mod2p bl_bin_bl_rep_drop diff_is_0_eq' diff_zero drop_bin2bl len_bin_to_bl mod_pos_pos_trivial)
lemma word_to_lint_ucast_up[word_to_lint_convs]:
"is_up UCAST('a::len→'b::len) ⟹ word_to_lint (UCAST('a→'b) a) = zext LENGTH ('b) (word_to_lint a)"
unfolding word_to_lint_def
by (simp add: zext_in_range cast_simps)
lemma word_to_lint_scast_up[word_to_lint_convs]:
"is_up SCAST('a::len→'b::len) ⟹ word_to_lint (SCAST('a→'b) a) = sext LENGTH ('b) (word_to_lint a)"
unfolding word_to_lint_def
apply (simp add: is_up sint_eq uint_sint max_def)
by (simp add: is_up sint_up_scast)
lemma word_to_lint_and_simp[word_to_lint_convs]: "word_to_lint (a AND b) = word_to_lint a lliAND word_to_lint b"
apply (auto simp: uint_eq word_to_lint_def)
apply (simp add: uint_and)
done
lemma word_to_lint_or_simp[word_to_lint_convs]: "word_to_lint (a OR b) = word_to_lint a lliOR word_to_lint b"
apply (auto simp: uint_eq word_to_lint_def)
apply (simp add: uint_or)
done
lemma word_to_lint_xor_simp[word_to_lint_convs]: "word_to_lint (a XOR b) = word_to_lint a lliXOR word_to_lint b"
apply (auto simp: uint_eq word_to_lint_def)
apply (simp add: uint_xor)
done
lemma from_bool_lint_conv: "(from_bool b :: 1 word) = lint_to_word (bool_to_lint b)"
apply (cases b)
apply (auto simp: from_bool_def bool_to_lint_def ltrue_def lfalse_def lint_to_word_def)
done
lemma word_to_lint_to_uint_conv: "lint_to_uint (word_to_lint a) = uint a"
by (auto simp: word_to_lint_def)
lemma word_to_lint_to_sint_conv: "lint_to_sint (word_to_lint a) = sint a"
by (auto simp: word_to_lint_def sint_uint)
lemma word_to_lint_to_uint_0_iff: "(lint_to_uint (word_to_lint b) = 0) = (b = 0)"
by (clarsimp simp: word_to_lint_to_uint_conv uint_0_iff)
lemma word_to_lint_to_sint_0_iff: "(lint_to_sint (word_to_lint (b::_::len word)) = 0) = (b = 0)"
by (auto simp: word_to_lint_to_sint_conv)
lemma width_word_to_lint[simp]: "width (word_to_lint (w::'a::len word)) = LENGTH ('a)"
by (auto simp: word_to_lint_def)
definition is_up' :: "('a::len word ⇒ 'b::len word) ⇒ bool"
where "is_up' c ⟷ source_size c < target_size c"
definition is_down' :: "('a::len word ⇒ 'b::len word) ⇒ bool"
where "is_down' c ⟷ target_size c < source_size c"
lemma is_down': "is_down' c ⟷ len_of TYPE('b) < len_of TYPE('a)"
for c :: "'a::len word ⇒ 'b::len word"
by (simp only: is_down'_def source_size target_size)
lemma is_up': "is_up' c ⟷ len_of TYPE('a) < len_of TYPE('b)"
for c :: "'a::len word ⇒ 'b::len word"
by (simp only: is_up'_def source_size target_size)
lemmas is_down'_imp[simp, intro] = is_down'[THEN iffD1]
lemmas is_up'_imp[simp, intro] = is_up'[THEN iffD1]
lemma is_down'_imp_down[simp, intro]: "is_down' c ⟹ is_down c" by (auto simp: is_down is_down')
lemma is_up'_imp_up[simp, intro]: "is_up' c ⟹ is_up c" by (auto simp: is_up is_up')
end