Theory LLVM_More_Word
section ‹Entry-Point to Word Library and additional lemmas for Isabelle-LLVM›
theory LLVM_More_Word
imports LLVM_More_Word_Lemmas Bits_Natural "Word_Lib.Word_Lib_Sumo"
begin
declare [[coercion_enabled = false]]
subsection ‹Additional Lemmas›
lemmas [simp] = word_sbin.norm_Rep[simplified]
lemma to_bl_scast_down: "is_down SCAST('a::len → 'b::len) ⟹ to_bl (SCAST('a → 'b) w) = drop (LENGTH('a)-LENGTH('b)) (to_bl w)"
by (simp add: is_down scast_down_drop source_size target_size)
lemma [simp]: "from_bool Φ = 0 ⟷ ¬Φ" by (rule from_bool_0)
declare word_unat.Rep_inject[simp del]
declare word_uint.Rep_inject[simp del]
lemma msb_uint_big: "msb (w::'a::len word) ⟷ uint w ≥ 2^(LENGTH('a)-1)"
apply (simp add: msb_big)
by (metis One_nat_def Suc_pred' diff_le_self le_antisym len_gt_0 n_not_Suc_n p2_eq_0 uint_2p word_le_def word_neq_0_conv)
lemma msb_unat_big: "msb (w::'a::len word) ⟷ unat w ≥ 2^(LENGTH('a)-1)"
by (simp add: msb_big word_le_nat_alt)
lemma word1_neqZ_is_one: "(a::1 word) ≠ 0 ⟷ a=1"
apply transfer
subgoal for a
apply (cases "bin_last a")
by auto
done
lemma word1_cases[cases type]:
fixes a :: "1 word" obtains (zero) "a=0" | (one) "a=1"
apply (cases "a=0")
by (auto simp: word1_neqZ_is_one)
lemma word1_NOT_eq: "~~(x::1 word) = x+1"
by (auto simp: NOT_eq)
lemma upcast_no_msb[simp]: "LENGTH('small::len) < LENGTH('big::len) ⟹ ¬msb (UCAST('small → 'big) x)"
by (simp add: bit_word_ucast_iff msb_word_eq)
lemma word_split_0[simp]: "word_split 0 = (0,0)"
by (auto simp: word_split_def)
subsection ‹Integer Division with Rounding Towards Zero›
text ‹Division with rounding towards zero›
lemma int_sgn_cases: fixes a::int obtains (negative) "a<0" | (zero) "a=0" | (positive) "a>0"
by (rule linorder_cases)
text ‹Lemmas to match original definitions from this development to
definitions from Word-Library, to which we switched at some point.›
lemma sdiv_int_original_def: "(a::int) sdiv b = (if a≥0 ⟷ b≥0 then ¦a¦ div ¦b¦ else - ( ¦a¦ div ¦b¦))"
apply (cases a rule: int_sgn_cases; cases b rule: int_sgn_cases)
apply (auto simp: sdiv_int_def sgn_mult)
done
lemma srem_int_original_def: "(a::int) smod b = (if a≥0 then ¦a¦ mod ¦b¦ else - (¦a¦ mod ¦b¦))"
apply (cases a rule: int_sgn_cases; cases b rule: int_sgn_cases)
apply (auto
simp: smod_int_def sdiv_int_def sgn_mult algebra_simps
simp flip: minus_mod_eq_mult_div mult_minus_left)
done
text ‹Standard properties of remainders›
lemma div_rem_rtz_id: "(a::int) sdiv b * b + a smod b = a"
by (rule signed_division_class.sdiv_mult_smod_eq)
lemma abs_rem_rtz_lt: "b≠0 ⟹ ¦a smod b¦ < ¦b::int¦"
using srem_int_original_def by auto
text ‹LLVM documentation: The remainder is either zero, or has the same sign as the dividend›
lemma rem_rtz_sign: "(a::int) smod b = 0 ∨ sgn ((a::int) smod b) = sgn a"
apply (clarsimp simp: srem_int_original_def)
by (metis (no_types) Euclidean_Division.pos_mod_sign abs_le_zero_iff abs_of_nonneg add.inverse_neutral mod_0 mod_by_0 neg_le_0_iff_le not_le sgn_pos)
lemma sdiv_positive[simp]: "(a::int)≥0 ⟹ b≥0 ⟹ a sdiv b = a div b"
by (simp add: sdiv_int_original_def)
lemma smod_positive[simp]: "(a::int)≥0 ⟹ b≥0 ⟹ a smod b = a mod b"
by (auto simp: srem_int_original_def)
subsection ‹Additions to Bits-Int›
declare bin_to_bl_def[simp del]
lemma map2_eq_Nil_conv[simp]: "map2 f a b = [] ⟷ a=[] ∨ b=[]"
by (cases a; cases b; auto)
lemma bin_to_bl_eq_Nil_conv[simp]: "bin_to_bl w i = [] ⟷ w=0"
by (metis bin_to_bl_aux.Z bin_to_bl_def size_bin_to_bl)
lemma bin_to_bl_aux_eq_Nil_conv[simp]: "bin_to_bl_aux w i acc = [] ⟷ w=0 ∧ acc=[]"
by (metis bin_to_bl_aux.Z bin_to_bl_eq_Nil_conv take.simps(1) take_bin2bl_lem1)
lemma "bl_to_bin_aux bl (1+n) = bl_to_bin_aux bl n + 2 ^ length bl"
apply (induction bl arbitrary: n)
apply (simp_all add: algebra_simps)
by smt
lemma bl_to_bin_True [simp]: "bl_to_bin (True # bl) = bl_to_bin bl + 2^length bl"
proof -
have "bl_to_bin_aux bl (1+n) = bl_to_bin_aux bl n + 2 ^ length bl" for n
apply (induction bl arbitrary: n)
apply (simp_all add: algebra_simps)
by smt
from this[of 0] show ?thesis
unfolding bl_to_bin_def
by simp
qed
lemma bl_to_bin_append_num: "bl_to_bin (a@b) = 2^length b * bl_to_bin a + bl_to_bin b"
by (simp add: bin_cat_num bl_to_bin_app_cat)
lemma bl_to_bin_rep_True: "bl_to_bin (replicate n True) = 2 ^ n - 1"
by (metis bin_bl_bin bin_to_bl_minus1 bintr_Min)
lemma bl_to_bin_rep_T: "bl_to_bin (replicate n True @ bl) = 2 ^ length bl * (2 ^ n - 1) + bl_to_bin bl"
by (simp add: bl_to_bin_append_num bl_to_bin_rep_True algebra_simps)
lemma bin_to_bl_strunc[simp]:
"w⇩1 ≤ w⇩2 + 1 ⟹ bin_to_bl w⇩1 (sbintrunc w⇩2 i) = bin_to_bl w⇩1 i"
by (simp add: bintrunc_sbintrunc_le bl_to_bin_inj)
lemma bin_last_x2[simp]: "bin_last (2*n) = False" by (auto)
lemma bin_rest_x2[simp]: "bin_rest (2*n) = n" by simp
lemma bin_to_bl_x2[simp]: "w≠0 ⟹ bin_to_bl w (2*n) = bin_to_bl (w-1) n @ [False]"
by (cases w) (auto simp: bin_to_bl_def bin_to_bl_aux_append)
lemma bin_to_bl_xp2[simp]:
assumes "n≤w"
shows "bin_to_bl w (x * 2^n) = bin_to_bl (w-n) x @ replicate n False"
proof -
have [simp]: "x * (2 * 2 ^ n) = 2 * (x*2^n)" for n by auto
show ?thesis using assms
by (induction n) (auto simp: drop_bin2bl[symmetric] replicate_append_same)
qed
lemma bintrunc_eq_if_in_range: "bintrunc w i = i ⟷ i∈uints w"
by (simp add: bintrunc_mod2p int_mod_lem uints_num)
lemma sbintrunc_eq_if_in_range: "sbintrunc (w-Suc 0) i = i ⟷ i∈sints w"
by (clarsimp simp: sints_def sbintrunc_eq_in_range)
lemma bl_to_bin_in_uints: "bl_to_bin x ∈ uints (length x)"
using bl_to_bin_def bintrunc_eq_if_in_range by fastforce
method_setup pull_mods = ‹Scan.succeed (fn ctxt => SIMPLE_METHOD' (
CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv @{thms pull_mods}))) ctxt)
))›
method_setup pull_push_mods = ‹Scan.succeed (fn ctxt => SIMPLE_METHOD' (
CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv @{thms pull_mods}))) ctxt)
THEN' (full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms mod_mod_trivial push_mods}))
))› ‹Pull in, then push out modulos›
subsection ‹Signed integers in Two's Complement Representation›
definition bl_to_sbin :: "bool list ⇒ int"
where "bl_to_sbin bl = sbintrunc (length bl - 1) (bl_to_bin bl)"
lemma bl_to_sbin_alt:
"bl_to_sbin bl = (case bl of [] ⇒ 0 | b#bl ⇒ (if b then -(2^length bl) else 0) + bl_to_bin bl)"
apply (auto simp: bl_to_sbin_def sbintrunc_mod2p bl_to_bin_ge0 bl_to_bin_lt2p split: list.splits)
by (smt bl_to_bin_ge0 bl_to_bin_lt2p int_mod_eq')
lemma bl_sbin_bl[simp]: "bin_to_bl (length bs) (bl_to_sbin bs) = bs"
unfolding bl_to_sbin_def by auto
lemma sbin_bl_bin[simp]:
"0<w ⟹ bl_to_sbin (bin_to_bl w i) = sbintrunc (w-1) i"
unfolding bl_to_sbin_def by auto
lemma bl_to_sbin_in_sints: "bl_to_sbin x ∈ sints (length x)"
using bl_to_sbin_def sbintrunc_eq_if_in_range by fastforce
end