diff --git a/thys/Word_Lib/Aligned.thy b/thys/Word_Lib/Aligned.thy --- a/thys/Word_Lib/Aligned.thy +++ b/thys/Word_Lib/Aligned.thy @@ -1,1325 +1,1325 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Word Alignment" theory Aligned imports "HOL-Library.Word" More_Word Bit_Shifts_Infix_Syntax begin context includes bit_operations_syntax begin lift_definition is_aligned :: \'a::len word \ nat \ bool\ is \\k n. 2 ^ n dvd take_bit LENGTH('a) k\ by simp lemma is_aligned_iff_udvd: \is_aligned w n \ 2 ^ n udvd w\ by transfer (simp flip: take_bit_eq_0_iff add: min_def) lemma is_aligned_iff_take_bit_eq_0: \is_aligned w n \ take_bit n w = 0\ by (simp add: is_aligned_iff_udvd take_bit_eq_0_iff exp_dvd_iff_exp_udvd) lemma is_aligned_iff_dvd_int: \is_aligned ptr n \ 2 ^ n dvd uint ptr\ by transfer simp lemma is_aligned_iff_dvd_nat: \is_aligned ptr n \ 2 ^ n dvd unat ptr\ proof - have \unat ptr = nat \uint ptr\\ by transfer simp then have \2 ^ n dvd unat ptr \ 2 ^ n dvd uint ptr\ by (simp only: dvd_nat_abs_iff) simp then show ?thesis by (simp add: is_aligned_iff_dvd_int) qed lemma is_aligned_0 [simp]: \is_aligned 0 n\ by transfer simp lemma is_aligned_at_0 [simp]: \is_aligned w 0\ by transfer simp lemma is_aligned_beyond_length: \is_aligned w n \ w = 0\ if \LENGTH('a) \ n\ for w :: \'a::len word\ using that apply (simp add: is_aligned_iff_udvd) apply transfer apply auto done lemma is_alignedI [intro?]: \is_aligned x n\ if \x = 2 ^ n * k\ for x :: \'a::len word\ proof (unfold is_aligned_iff_udvd) from that show \2 ^ n udvd x\ using dvd_triv_left exp_dvd_iff_exp_udvd by blast qed lemma is_alignedE: fixes w :: \'a::len word\ assumes \is_aligned w n\ obtains q where \w = 2 ^ n * word_of_nat q\ \q < 2 ^ (LENGTH('a) - n)\ proof (cases \n < LENGTH('a)\) case False with assms have \w = 0\ by (simp add: is_aligned_beyond_length) with that [of 0] show thesis by simp next case True moreover define m where \m = LENGTH('a) - n\ ultimately have l: \LENGTH('a) = n + m\ and \m \ 0\ by simp_all from \n < LENGTH('a)\ have *: \unat (2 ^ n :: 'a word) = 2 ^ n\ by transfer simp from assms have \2 ^ n udvd w\ by (simp add: is_aligned_iff_udvd) then obtain v :: \'a word\ where \unat w = unat (2 ^ n :: 'a word) * unat v\ .. moreover define q where \q = unat v\ ultimately have unat_w: \unat w = 2 ^ n * q\ by (simp add: *) then have \word_of_nat (unat w) = (word_of_nat (2 ^ n * q) :: 'a word)\ by simp then have w: \w = 2 ^ n * word_of_nat q\ by simp moreover have \q < 2 ^ (LENGTH('a) - n)\ proof (rule ccontr) assume \\ q < 2 ^ (LENGTH('a) - n)\ then have \2 ^ (LENGTH('a) - n) \ q\ by simp then have \2 ^ LENGTH('a) \ 2 ^ n * q\ by (simp add: l power_add) with unat_w [symmetric] show False - by (metis le_antisym nat_less_le unsigned_less) + by (metis le_antisym nat_less_le unsigned_less) qed ultimately show thesis using that by blast qed lemma is_alignedE' [elim?]: fixes w :: \'a::len word\ assumes \is_aligned w n\ obtains q where \w = push_bit n (word_of_nat q)\ \q < 2 ^ (LENGTH('a) - n)\ proof - from assms obtain q where \w = 2 ^ n * word_of_nat q\ \q < 2 ^ (LENGTH('a) - n)\ by (rule is_alignedE) then have \w = push_bit n (word_of_nat q)\ by (simp add: push_bit_eq_mult) with that show thesis using \q < 2 ^ (LENGTH('a) - n)\ . qed lemma is_aligned_mask: \is_aligned w n \ w AND mask n = 0\ by (simp add: is_aligned_iff_take_bit_eq_0 take_bit_eq_mask) lemma is_aligned_imp_not_bit: \\ bit w m\ if \is_aligned w n\ and \m < n\ for w :: \'a::len word\ proof - from \is_aligned w n\ obtain q where \w = push_bit n (word_of_nat q)\ \q < 2 ^ (LENGTH('a) - n)\ .. moreover have \\ bit (push_bit n (word_of_nat q :: 'a word)) m\ using \m < n\ by (simp add: bit_simps) ultimately show ?thesis by simp qed lemma is_aligned_weaken: "\ is_aligned w x; x \ y \ \ is_aligned w y" unfolding is_aligned_iff_dvd_nat by (erule dvd_trans [rotated]) (simp add: le_imp_power_dvd) lemma is_alignedE_pre: fixes w::"'a::len word" assumes aligned: "is_aligned w n" shows rl: "\q. w = 2 ^ n * (of_nat q) \ q < 2 ^ (LENGTH('a) - n)" using aligned is_alignedE by blast lemma aligned_add_aligned: fixes x::"'a::len word" assumes aligned1: "is_aligned x n" and aligned2: "is_aligned y m" and lt: "m \ n" shows "is_aligned (x + y) m" proof cases assume nlt: "n < LENGTH('a)" show ?thesis unfolding is_aligned_iff_dvd_nat dvd_def proof - from aligned2 obtain q2 where yv: "y = 2 ^ m * of_nat q2" and q2v: "q2 < 2 ^ (LENGTH('a) - m)" by (auto elim: is_alignedE) from lt obtain k where kv: "m + k = n" by (auto simp: le_iff_add) with aligned1 obtain q1 where xv: "x = 2 ^ (m + k) * of_nat q1" and q1v: "q1 < 2 ^ (LENGTH('a) - (m + k))" by (auto elim: is_alignedE) have l1: "2 ^ (m + k) * q1 < 2 ^ LENGTH('a)" by (rule nat_less_power_trans [OF q1v]) (subst kv, rule order_less_imp_le [OF nlt]) have l2: "2 ^ m * q2 < 2 ^ LENGTH('a)" by (rule nat_less_power_trans [OF q2v], rule order_less_imp_le [OF order_le_less_trans]) fact+ have "x = of_nat (2 ^ (m + k) * q1)" using xv by simp moreover have "y = of_nat (2 ^ m * q2)" using yv by simp ultimately have upls: "unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)" proof - have f1: "unat x = 2 ^ (m + k) * q1" using q1v unat_mult_power_lem xv by blast have "unat y = 2 ^ m * q2" using q2v unat_mult_power_lem yv by blast then show ?thesis using f1 by (simp add: power_add semiring_normalization_rules(34)) qed (* (2 ^ k * q1 + q2) *) show "\d. unat (x + y) = 2 ^ m * d" proof (cases "unat x + unat y < 2 ^ LENGTH('a)") case True have "unat (x + y) = unat x + unat y" by (subst unat_plus_if', rule if_P) fact also have "\ = 2 ^ m * (2 ^ k * q1 + q2)" by (rule upls) finally show ?thesis .. next case False then have "unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)" by (subst unat_word_ariths(1)) simp also have "\ = (2 ^ m * (2 ^ k * q1 + q2)) mod 2 ^ LENGTH('a)" by (subst upls, rule refl) also have "\ = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))" proof - have "m \ len_of (TYPE('a))" by (meson le_trans less_imp_le_nat lt nlt) then show ?thesis by (metis mult_mod_right ordered_cancel_comm_monoid_diff_class.add_diff_inverse power_add) qed finally show ?thesis .. qed qed next assume "\ n < LENGTH('a)" with assms show ?thesis by (simp add: is_aligned_mask not_less take_bit_eq_mod power_overflow word_arith_nat_defs(7) flip: take_bit_eq_mask) qed corollary aligned_sub_aligned: "\is_aligned (x::'a::len word) n; is_aligned y m; m \ n\ \ is_aligned (x - y) m" apply (simp del: add_uminus_conv_diff add:diff_conv_add_uminus) apply (erule aligned_add_aligned, simp_all) apply (erule is_alignedE) apply (rule_tac k="- of_nat q" in is_alignedI) apply simp done lemma is_aligned_shift: fixes k::"'a::len word" shows "is_aligned (k << m) m" proof cases assume mv: "m < LENGTH('a)" from mv obtain q where mq: "m + q = LENGTH('a)" and "0 < q" by (auto dest: less_imp_add_positive) have "(2::nat) ^ m dvd unat (push_bit m k)" proof have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k" by (rule div_mult_mod_eq) have "unat (push_bit m k) = unat (2 ^ m * k)" by (simp add: push_bit_eq_mult ac_simps) also have "\ = (2 ^ m * unat k) mod (2 ^ LENGTH('a))" using mv by (simp add: unat_word_ariths(2)) also have "\ = 2 ^ m * (unat k mod 2 ^ q)" by (subst mq [symmetric], subst power_add, subst mod_mult2_eq) simp finally show "unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)" . qed then show ?thesis by (unfold is_aligned_iff_dvd_nat shiftl_def) next assume "\ m < LENGTH('a)" then show ?thesis by (simp add: not_less power_overflow is_aligned_mask word_size shiftl_def) qed lemma aligned_mod_eq_0: fixes p::"'a::len word" assumes al: "is_aligned p sz" shows "p mod 2 ^ sz = 0" proof cases assume szv: "sz < LENGTH('a)" with al show ?thesis unfolding is_aligned_iff_dvd_nat by (simp add: and_mask_dvd_nat p2_gt_0 word_mod_2p_is_mask) next assume "\ sz < LENGTH('a)" with al show ?thesis by (simp add: is_aligned_mask flip: take_bit_eq_mask take_bit_eq_mod) qed lemma is_aligned_triv: "is_aligned (2 ^ n ::'a::len word) n" by (rule is_alignedI [where k = 1], simp) lemma is_aligned_mult_triv1: "is_aligned (2 ^ n * x ::'a::len word) n" by (rule is_alignedI [OF refl]) lemma is_aligned_mult_triv2: "is_aligned (x * 2 ^ n ::'a::len word) n" by (subst mult.commute, simp add: is_aligned_mult_triv1) lemma word_power_less_0_is_0: fixes x :: "'a::len word" shows "x < a ^ 0 \ x = 0" by simp lemma is_aligned_no_wrap: fixes off :: "'a::len word" fixes ptr :: "'a::len word" assumes al: "is_aligned ptr sz" and off: "off < 2 ^ sz" shows "unat ptr + unat off < 2 ^ LENGTH('a)" proof - have szv: "sz < LENGTH('a)" using off p2_gt_0 word_neq_0_conv by fastforce from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and qv: "q < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) show ?thesis proof (cases "sz = 0") case True then show ?thesis using off ptrq qv by simp next case False then have sne: "0 < sz" .. show ?thesis proof - have uq: "unat (of_nat q ::'a::len word) = q" apply (subst unat_of_nat) apply (rule mod_less) apply (rule order_less_trans [OF qv]) apply (rule power_strict_increasing [OF diff_less [OF sne]]) apply (simp_all) done have uptr: "unat ptr = 2 ^ sz * q" apply (subst ptrq) apply (subst iffD1 [OF unat_mult_lem]) apply (subst unat_power_lower [OF szv]) apply (subst uq) apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]]) apply (subst uq) apply (subst unat_power_lower [OF szv]) apply simp done show "unat ptr + unat off < 2 ^ LENGTH('a)" using szv apply (subst uptr) apply (subst mult.commute, rule nat_add_offset_less [OF _ qv]) apply (rule order_less_le_trans [OF unat_mono [OF off] order_eq_refl]) apply simp_all done qed qed qed lemma is_aligned_no_wrap': fixes ptr :: "'a::len word" assumes al: "is_aligned ptr sz" and off: "off < 2 ^ sz" shows "ptr \ ptr + off" by (subst no_plus_overflow_unat_size, subst word_size, rule is_aligned_no_wrap) fact+ lemma is_aligned_no_overflow': fixes p :: "'a::len word" assumes al: "is_aligned p n" shows "p \ p + (2 ^ n - 1)" proof cases assume "n n ptr \ ptr + 2^sz - 1" by (drule is_aligned_no_overflow') (simp add: field_simps) lemma replicate_not_True: "\n. xs = replicate n False \ True \ set xs" by (induct xs) auto lemma map_zip_replicate_False_xor: "n = length xs \ map (\(x, y). x = (\ y)) (zip xs (replicate n False)) = xs" by (induct xs arbitrary: n, auto) lemma drop_minus_lem: "\ n \ length xs; 0 < n; n' = length xs \ \ drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs" proof (induct xs arbitrary: n n') case Nil then show ?case by simp next case (Cons y ys) from Cons.prems show ?case apply simp apply (cases "n = Suc (length ys)") apply (simp add: nth_append) apply (simp add: Suc_diff_le Cons.hyps nth_append) apply clarsimp apply arith done qed lemma drop_minus: "\ n < length xs; n' = length xs \ \ drop (n' - Suc n) xs = rev xs ! n # drop (n' - n) xs" apply (subst drop_minus_lem) apply simp apply simp apply simp apply simp apply (cases "length xs", simp) apply (simp add: Suc_diff_le) done lemma aligned_add_xor: \(x + 2 ^ n) XOR 2 ^ n = x\ if al: \is_aligned (x::'a::len word) n'\ and le: \n < n'\ proof - have \\ bit x n\ using that by (rule is_aligned_imp_not_bit) then have \x + 2 ^ n = x OR 2 ^ n\ by (subst disjunctive_add) (auto simp add: bit_simps disjunctive_add) moreover have \(x OR 2 ^ n) XOR 2 ^ n = x\ by (rule bit_word_eqI) (auto simp add: bit_simps \\ bit x n\) ultimately show ?thesis by simp qed lemma is_aligned_add_mult_multI: fixes p :: "'a::len word" shows "\is_aligned p m; n \ m; n' = n\ \ is_aligned (p + x * 2 ^ n * z) n'" apply (erule aligned_add_aligned) apply (auto intro: is_alignedI [where k="x*z"]) done lemma is_aligned_add_multI: fixes p :: "'a::len word" shows "\is_aligned p m; n \ m; n' = n\ \ is_aligned (p + x * 2 ^ n) n'" apply (erule aligned_add_aligned) apply (auto intro: is_alignedI [where k="x"]) done lemma is_aligned_no_wrap''': fixes ptr :: "'a::len word" shows"\ is_aligned ptr sz; sz < LENGTH('a); off < 2 ^ sz \ \ unat ptr + off < 2 ^ LENGTH('a)" apply (drule is_aligned_no_wrap[where off="of_nat off"]) apply (simp add: word_less_nat_alt) apply (erule order_le_less_trans[rotated]) apply (simp add: take_bit_eq_mod unsigned_of_nat) apply (subst(asm) unat_of_nat_len) apply (erule order_less_trans) apply (erule power_strict_increasing) apply simp apply assumption done lemma is_aligned_get_word_bits: fixes p :: "'a::len word" shows "\ is_aligned p n; \ is_aligned p n; n < LENGTH('a) \ \ P; \ p = 0; n \ LENGTH('a) \ \ P \ \ P" apply (cases "n < LENGTH('a)") apply simp apply simp apply (erule meta_mp) apply (simp add: is_aligned_mask power_add power_overflow not_less flip: take_bit_eq_mask) apply (metis take_bit_length_eq take_bit_of_0 take_bit_tightened) done lemma aligned_small_is_0: "\ is_aligned x n; x < 2 ^ n \ \ x = 0" by (simp add: is_aligned_mask less_mask_eq) corollary is_aligned_less_sz: "\is_aligned a sz; a \ 0\ \ \ a < 2 ^ sz" by (rule notI, drule(1) aligned_small_is_0, erule(1) notE) lemma aligned_at_least_t2n_diff: "\is_aligned x n; is_aligned y n; x < y\ \ x \ y - 2 ^ n" apply (erule is_aligned_get_word_bits[where p=y]) apply (rule ccontr) apply (clarsimp simp: linorder_not_le) apply (subgoal_tac "y - x = 0") apply clarsimp apply (rule aligned_small_is_0) apply (erule(1) aligned_sub_aligned) apply simp apply unat_arith apply simp done lemma is_aligned_no_overflow'': "\is_aligned x n; x + 2 ^ n \ 0\ \ x \ x + 2 ^ n" apply (frule is_aligned_no_overflow') apply (erule order_trans) apply (simp add: field_simps) apply (erule word_sub_1_le) done lemma is_aligned_bitI: \is_aligned p m\ if \\n. n < m \ \ bit p n\ apply (simp add: is_aligned_mask) apply (rule bit_word_eqI) using that apply (auto simp add: bit_simps) done lemma is_aligned_nth: "is_aligned p m = (\n < m. \ bit p n)" apply (auto intro: is_aligned_bitI simp add: is_aligned_mask bit_eq_iff) apply (auto simp: bit_simps) using bit_imp_le_length not_less apply blast done lemma range_inter: "({a..b} \ {c..d} = {}) = (\x. \(a \ x \ x \ b \ c \ x \ x \ d))" by auto lemma aligned_inter_non_empty: "\ {p..p + (2 ^ n - 1)} \ {p..p + 2 ^ m - 1} = {}; is_aligned p n; is_aligned p m\ \ False" apply (clarsimp simp only: range_inter) apply (erule_tac x=p in allE) apply simp apply (erule impE) apply (erule is_aligned_no_overflow') apply (erule notE) apply (erule is_aligned_no_overflow) done lemma not_aligned_mod_nz: assumes al: "\ is_aligned a n" shows "a mod 2 ^ n \ 0" apply (rule ccontr) using al apply (rule notE) apply simp apply (rule is_alignedI [of _ _ \a div 2 ^ n\]) apply (metis add.right_neutral mult.commute word_mod_div_equality) done lemma nat_add_offset_le: fixes x :: nat assumes yv: "y \ 2 ^ n" and xv: "x < 2 ^ m" and mn: "sz = m + n" shows "x * 2 ^ n + y \ 2 ^ sz" proof (subst mn) from yv obtain qy where "y + qy = 2 ^ n" by (auto simp: le_iff_add) have "x * 2 ^ n + y \ x * 2 ^ n + 2 ^ n" using yv xv by simp also have "\ = (x + 1) * 2 ^ n" by simp also have "\ \ 2 ^ (m + n)" using xv by (subst power_add) (rule mult_le_mono1, simp) finally show "x * 2 ^ n + y \ 2 ^ (m + n)" . qed lemma is_aligned_no_wrap_le: fixes ptr::"'a::len word" assumes al: "is_aligned ptr sz" and szv: "sz < LENGTH('a)" and off: "off \ 2 ^ sz" shows "unat ptr + off \ 2 ^ LENGTH('a)" proof - from al obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and qv: "q < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) show ?thesis proof (cases "sz = 0") case True then show ?thesis using off ptrq qv by (auto simp add: le_Suc_eq Suc_le_eq) (simp add: le_less) next case False then have sne: "0 < sz" .. show ?thesis proof - have uq: "unat (of_nat q :: 'a word) = q" apply (subst unat_of_nat) apply (rule mod_less) apply (rule order_less_trans [OF qv]) apply (rule power_strict_increasing [OF diff_less [OF sne]]) apply simp_all done have uptr: "unat ptr = 2 ^ sz * q" apply (subst ptrq) apply (subst iffD1 [OF unat_mult_lem]) apply (subst unat_power_lower [OF szv]) apply (subst uq) apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]]) apply (subst uq) apply (subst unat_power_lower [OF szv]) apply simp done show "unat ptr + off \ 2 ^ LENGTH('a)" using szv apply (subst uptr) apply (subst mult.commute, rule nat_add_offset_le [OF off qv]) apply simp done qed qed qed lemma is_aligned_neg_mask: "m \ n \ is_aligned (x AND NOT (mask n)) m" by (rule is_aligned_bitI) (simp add: bit_simps) lemma unat_minus: "unat (- (x :: 'a :: len word)) = (if x = 0 then 0 else 2 ^ size x - unat x)" using unat_sub_if_size[where x="2 ^ size x" and y=x] by (simp add: unat_eq_0 word_size) lemma is_aligned_minus: \is_aligned (- p) n\ if \is_aligned p n\ for p :: \'a::len word\ using that apply (cases \n < LENGTH('a)\) apply (simp_all add: not_less is_aligned_beyond_length) apply transfer apply (simp flip: take_bit_eq_0_iff) apply (subst take_bit_minus [symmetric]) apply simp done lemma add_mask_lower_bits: "\is_aligned (x :: 'a :: len word) n; \n' \ n. n' < LENGTH('a) \ \ bit p n'\ \ x + p AND NOT (mask n) = x" apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_size is_aligned_nth) apply (erule_tac x=na in allE)+ apply (simp add: bit_simps) apply (rule bit_word_eqI) apply (auto simp add: bit_simps not_less word_size) apply (metis is_aligned_nth not_le) done lemma is_aligned_andI1: "is_aligned x n \ is_aligned (x AND y) n" by (simp add: is_aligned_nth bit_simps) lemma is_aligned_andI2: "is_aligned y n \ is_aligned (x AND y) n" by (simp add: is_aligned_nth bit_simps) lemma is_aligned_shiftl: "is_aligned w (n - m) \ is_aligned (w << m) n" by (simp add: is_aligned_nth bit_simps) lemma is_aligned_shiftr: "is_aligned w (n + m) \ is_aligned (w >> m) n" by (simp add: is_aligned_nth bit_simps) lemma is_aligned_shiftl_self: "is_aligned (p << n) n" by (rule is_aligned_shift) lemma is_aligned_neg_mask_eq: "is_aligned p n \ p AND NOT (mask n) = p" apply (rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth) done lemma is_aligned_shiftr_shiftl: "is_aligned w n \ w >> n << n = w" apply (rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth intro: ccontr) apply (subst add_diff_inverse_nat) apply (auto intro: ccontr) done lemma aligned_shiftr_mask_shiftl: "is_aligned x n \ ((x >> n) AND mask v) << n = x AND mask (v + n)" apply (rule word_eqI) apply (simp add: word_size bit_simps) apply (subgoal_tac "\m. bit x m \ m \ n") apply auto[1] apply (clarsimp simp: is_aligned_mask) apply (drule_tac x=m in word_eqD) apply (frule test_bit_size) apply (simp add: word_size bit_simps) done lemma mask_zero: "is_aligned x a \ x AND mask a = 0" by (metis is_aligned_mask) lemma is_aligned_neg_mask_eq_concrete: "\ is_aligned p n; msk AND NOT (mask n) = NOT (mask n) \ \ p AND msk = p" by (metis word_bw_assocs(1) word_bw_comms(1) is_aligned_neg_mask_eq) lemma is_aligned_and_not_zero: "\ is_aligned n k; n \ 0 \ \ 2 ^ k \ n" using is_aligned_less_sz leI by blast lemma is_aligned_and_2_to_k: "(n AND 2 ^ k - 1) = 0 \ is_aligned (n :: 'a :: len word) k" by (simp add: is_aligned_mask mask_eq_decr_exp) lemma is_aligned_power2: "b \ a \ is_aligned (2 ^ a) b" by (metis is_aligned_triv is_aligned_weaken) lemma aligned_sub_aligned': "\ is_aligned (a :: 'a :: len word) n; is_aligned b n; n < LENGTH('a) \ \ is_aligned (a - b) n" by (simp add: aligned_sub_aligned) lemma is_aligned_neg_mask_weaken: "\ is_aligned p n; m \ n \ \ p AND NOT (mask m) = p" using is_aligned_neg_mask_eq is_aligned_weaken by blast lemma is_aligned_neg_mask2 [simp]: "is_aligned (a AND NOT (mask n)) n" by (rule is_aligned_bitI) (simp add: bit_simps) lemma is_aligned_0': "is_aligned 0 n" by (fact is_aligned_0) lemma aligned_add_offset_no_wrap: fixes off :: "('a::len) word" and x :: "'a word" assumes al: "is_aligned x sz" and offv: "off < 2 ^ sz" shows "unat x + unat off < 2 ^ LENGTH('a)" proof cases assume szv: "sz < LENGTH('a)" from al obtain k where xv: "x = 2 ^ sz * (of_nat k)" and kl: "k < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) show ?thesis using szv apply (subst xv) apply (subst unat_mult_power_lem[OF kl]) apply (subst mult.commute, rule nat_add_offset_less) apply (rule less_le_trans[OF unat_mono[OF offv, simplified]]) apply (erule eq_imp_le[OF unat_power_lower]) apply (rule kl) apply simp done next assume "\ sz < LENGTH('a)" with offv show ?thesis by (simp add: not_less power_overflow ) qed lemma aligned_add_offset_mod: fixes x :: "('a::len) word" assumes al: "is_aligned x sz" and kv: "k < 2 ^ sz" shows "(x + k) mod 2 ^ sz = k" proof cases assume szv: "sz < LENGTH('a)" have ux: "unat x + unat k < 2 ^ LENGTH('a)" by (rule aligned_add_offset_no_wrap) fact+ show ?thesis using al szv apply (simp flip: take_bit_eq_mod) apply (rule bit_word_eqI) apply (auto simp add: bit_simps) apply (metis assms(2) bit_or_iff is_aligned_mask is_aligned_nth leD less_mask_eq word_and_le1 word_bw_lcs(1) word_neq_0_conv word_plus_and_or_coroll) apply (meson assms(2) leI less_2p_is_upper_bits_unset) apply (metis assms(2) bit_disjunctive_add_iff bit_imp_le_length bit_push_bit_iff is_alignedE' less_2p_is_upper_bits_unset) done next assume "\ sz < LENGTH('a)" with al show ?thesis by (simp add: not_less power_overflow is_aligned_mask mask_eq_decr_exp word_mod_by_0) qed lemma aligned_neq_into_no_overlap: fixes x :: "'a::len word" assumes neq: "x \ y" and alx: "is_aligned x sz" and aly: "is_aligned y sz" shows "{x .. x + (2 ^ sz - 1)} \ {y .. y + (2 ^ sz - 1)} = {}" proof cases assume szv: "sz < LENGTH('a)" show ?thesis proof (rule equals0I, clarsimp) fix z assume xb: "x \ z" and xt: "z \ x + (2 ^ sz - 1)" and yb: "y \ z" and yt: "z \ y + (2 ^ sz - 1)" have rl: "\(p::'a word) k w. \uint p + uint k < 2 ^ LENGTH('a); w = p + k; w \ p + (2 ^ sz - 1) \ \ k < 2 ^ sz" apply - apply simp apply (subst (asm) add.commute, subst (asm) add.commute, drule word_plus_mcs_4) apply (subst add.commute, subst no_plus_overflow_uint_size) apply transfer apply simp apply (auto simp add: le_less power_2_ge_iff szv) apply (metis le_less_trans mask_eq_decr_exp mask_lt_2pn order_less_imp_le szv) done from xb obtain kx where kx: "z = x + kx" and kxl: "uint x + uint kx < 2 ^ LENGTH('a)" by (clarsimp dest!: word_le_exists') from yb obtain ky where ky: "z = y + ky" and kyl: "uint y + uint ky < 2 ^ LENGTH('a)" by (clarsimp dest!: word_le_exists') have "x = y" proof - have "kx = z mod 2 ^ sz" proof (subst kx, rule sym, rule aligned_add_offset_mod) show "kx < 2 ^ sz" by (rule rl) fact+ qed fact+ also have "\ = ky" proof (subst ky, rule aligned_add_offset_mod) show "ky < 2 ^ sz" using kyl ky yt by (rule rl) qed fact+ finally have kxky: "kx = ky" . moreover have "x + kx = y + ky" by (simp add: kx [symmetric] ky [symmetric]) ultimately show ?thesis by simp qed then show False using neq by simp qed next assume "\ sz < LENGTH('a)" with neq alx aly have False by (simp add: is_aligned_mask mask_eq_decr_exp power_overflow) then show ?thesis .. qed lemma is_aligned_add_helper: "\ is_aligned p n; d < 2 ^ n \ \ (p + d AND mask n = d) \ (p + d AND (NOT (mask n)) = p)" apply (subst (asm) is_aligned_mask) apply (drule less_mask_eq) apply (rule context_conjI) apply (subst word_plus_and_or_coroll) apply (simp_all flip: take_bit_eq_mask) apply (metis take_bit_eq_mask word_bw_lcs(1) word_log_esimps(1)) apply (metis add.commute add_left_imp_eq take_bit_eq_mask word_plus_and_or_coroll2) done lemmas mask_inner_mask = mask_eqs(1) lemma mask_add_aligned: "is_aligned p n \ (p + q) AND mask n = q AND mask n" apply (simp add: is_aligned_mask) apply (subst mask_inner_mask [symmetric]) apply simp done lemma mask_out_add_aligned: assumes al: "is_aligned p n" shows "p + (q AND NOT (mask n)) = (p + q) AND NOT (mask n)" using mask_add_aligned [OF al] by (simp add: mask_out_sub_mask) lemma is_aligned_add_or: "\is_aligned p n; d < 2 ^ n\ \ p + d = p OR d" apply (subst disjunctive_add, simp_all) apply (clarsimp simp: is_aligned_nth less_2p_is_upper_bits_unset) subgoal for m apply (cases \m < n\) apply (auto simp add: not_less dest: bit_imp_possible_bit) done done lemma not_greatest_aligned: "\ x < y; is_aligned x n; is_aligned y n \ \ x + 2 ^ n \ 0" by (metis NOT_mask add_diff_cancel_right' diff_0 is_aligned_neg_mask_eq not_le word_and_le1) lemma neg_mask_mono_le: "x \ y \ x AND NOT(mask n) \ y AND NOT(mask n)" for x :: "'a :: len word" proof (rule ccontr, simp add: linorder_not_le, cases "n < LENGTH('a)") case False then show "y AND NOT(mask n) < x AND NOT(mask n) \ False" by (simp add: mask_eq_decr_exp linorder_not_less power_overflow) next case True assume a: "x \ y" and b: "y AND NOT(mask n) < x AND NOT(mask n)" have word_bits: "n < LENGTH('a)" by fact have "y \ (y AND NOT(mask n)) + (y AND mask n)" by (simp add: word_plus_and_or_coroll2 add.commute) also have "\ \ (y AND NOT(mask n)) + 2 ^ n" apply (rule word_plus_mono_right) apply (rule order_less_imp_le, rule and_mask_less_size) apply (simp add: word_size word_bits) apply (rule is_aligned_no_overflow'', simp add: is_aligned_neg_mask word_bits) apply (rule not_greatest_aligned, rule b; simp add: is_aligned_neg_mask) done also have "\ \ x AND NOT(mask n)" using b apply (subst add.commute) apply (rule le_plus) apply (rule aligned_at_least_t2n_diff; simp add: is_aligned_neg_mask) apply (rule ccontr, simp add: linorder_not_le) apply (drule aligned_small_is_0[rotated]; simp add: is_aligned_neg_mask) done also have "\ \ x" by (rule word_and_le2) also have "x \ y" by fact finally show "False" using b by simp qed lemma and_neg_mask_eq_iff_not_mask_le: "w AND NOT(mask n) = NOT(mask n) \ NOT(mask n) \ w" for w :: \'a::len word\ by (metis eq_iff neg_mask_mono_le word_and_le1 word_and_le2 word_bw_same(1)) lemma neg_mask_le_high_bits: \NOT (mask n) \ w \ (\i \ {n ..< size w}. bit w i)\ (is \?P \ ?Q\) for w :: \'a::len word\ proof assume ?Q then have \w AND NOT (mask n) = NOT (mask n)\ by (auto simp add: bit_simps word_size intro: bit_word_eqI) then show ?P by (simp add: and_neg_mask_eq_iff_not_mask_le) next assume ?P then have *: \w AND NOT (mask n) = NOT (mask n)\ by (simp add: and_neg_mask_eq_iff_not_mask_le) show \?Q\ proof (rule ccontr) assume \\ (\i\{n.. then obtain m where m: \\ bit w m\ \n \ m\ \m < LENGTH('a)\ by (auto simp add: word_size) from * have \bit (w AND NOT (mask n)) m \ bit (NOT (mask n :: 'a word)) m\ by auto with m show False by (auto simp add: bit_simps) qed qed lemma is_aligned_add_less_t2n: "\is_aligned (p::'a::len word) n; d < 2^n; n \ m; p < 2^m\ \ p + d < 2^m" apply (case_tac "m < LENGTH('a)") apply (subst mask_eq_iff_w2p[symmetric]) apply (simp add: word_size) apply (simp add: is_aligned_add_or word_ao_dist less_mask_eq) apply (subst less_mask_eq) apply (erule order_less_le_trans) apply (erule(1) two_power_increasing) apply simp apply (simp add: power_overflow) done lemma aligned_offset_non_zero: "\ is_aligned x n; y < 2 ^ n; x \ 0 \ \ x + y \ 0" apply (cases "y = 0") apply simp apply (subst word_neq_0_conv) apply (subst gt0_iff_gem1) apply (erule is_aligned_get_word_bits) apply (subst field_simps[symmetric], subst plus_le_left_cancel_nowrap) apply (rule is_aligned_no_wrap') apply simp apply (rule word_leq_le_minus_one) apply simp apply assumption apply (erule (1) is_aligned_no_wrap') apply (simp add: gt0_iff_gem1 [symmetric] word_neq_0_conv) apply simp done lemma is_aligned_over_length: "\ is_aligned p n; LENGTH('a) \ n \ \ (p::'a::len word) = 0" by (simp add: is_aligned_mask mask_over_length) lemma is_aligned_no_overflow_mask: "is_aligned x n \ x \ x + mask n" by (simp add: mask_eq_decr_exp) (erule is_aligned_no_overflow') lemma aligned_mask_step: "\ n' \ n; p' \ p + mask n; is_aligned p n; is_aligned p' n' \ \ (p'::'a::len word) + mask n' \ p + mask n" apply (cases "LENGTH('a) \ n") apply (frule (1) is_aligned_over_length) apply (drule mask_over_length) apply clarsimp apply (simp add: not_le) apply (simp add: word_le_nat_alt unat_plus_simple) apply (subst unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask)+ apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) apply (clarsimp simp: dvd_def is_aligned_iff_dvd_nat) apply (rename_tac k k') apply (thin_tac "unat p = x" for p x)+ apply (subst Suc_le_mono[symmetric]) apply (simp only: Suc_2p_unat_mask) apply (drule le_imp_less_Suc, subst (asm) Suc_2p_unat_mask, assumption) apply (erule (1) power_2_mult_step_le) done lemma is_aligned_mask_offset_unat: fixes off :: "('a::len) word" and x :: "'a word" assumes al: "is_aligned x sz" and offv: "off \ mask sz" shows "unat x + unat off < 2 ^ LENGTH('a)" proof cases assume szv: "sz < LENGTH('a)" from al obtain k where xv: "x = 2 ^ sz * (of_nat k)" and kl: "k < 2 ^ (LENGTH('a) - sz)" by (auto elim: is_alignedE) from offv szv have offv': "unat off < 2 ^ sz" by (simp add: mask_2pm1 unat_less_power) show ?thesis using szv using al is_aligned_no_wrap''' offv' by blast next assume "\ sz < LENGTH('a)" with al have "x = 0" - by (meson is_aligned_get_word_bits) + by (meson is_aligned_get_word_bits) thus ?thesis by simp qed lemma aligned_less_plus_1: "\ is_aligned x n; n > 0 \ \ x < x + 1" apply (rule plus_one_helper2) apply (rule order_refl) apply (clarsimp simp: field_simps) apply (drule arg_cong[where f="\x. x - 1"]) apply (clarsimp simp: is_aligned_mask) done lemma aligned_add_offset_less: "\is_aligned x n; is_aligned y n; x < y; z < 2 ^ n\ \ x + z < y" apply (cases "y = 0") apply simp apply (erule is_aligned_get_word_bits[where p=y], simp_all) apply (cases "z = 0", simp_all) apply (drule(2) aligned_at_least_t2n_diff[rotated -1]) apply (drule plus_one_helper2) apply (rule less_is_non_zero_p1) apply (rule aligned_less_plus_1) apply (erule aligned_sub_aligned[OF _ _ order_refl], simp_all add: is_aligned_triv)[1] apply (cases n, simp_all)[1] apply (simp only: trans[OF diff_add_eq diff_diff_eq2[symmetric]]) apply (drule word_less_add_right) apply (rule ccontr, simp add: linorder_not_le) apply (drule aligned_small_is_0, erule order_less_trans) apply (clarsimp simp: power_overflow) apply simp apply (erule order_le_less_trans[rotated], rule word_plus_mono_right) apply (erule word_le_minus_one_leq) apply (simp add: is_aligned_no_wrap' is_aligned_no_overflow field_simps) done lemma gap_between_aligned: "\a < (b :: 'a ::len word); is_aligned a n; is_aligned b n; n < LENGTH('a) \ \ a + (2^n - 1) < b" by (simp add: aligned_add_offset_less) lemma is_aligned_add_step_le: "\ is_aligned (a::'a::len word) n; is_aligned b n; a < b; b \ a + mask n \ \ False" apply (simp flip: not_le) apply (erule notE) apply (cases "LENGTH('a) \ n") apply (drule (1) is_aligned_over_length)+ apply (drule mask_over_length) apply clarsimp apply (clarsimp simp: word_le_nat_alt not_less not_le) apply (subst (asm) unat_plus_simple[THEN iffD1], erule is_aligned_no_overflow_mask) apply (subst (asm) unat_add_lem' [symmetric]) apply (simp add: is_aligned_mask_offset_unat) apply (metis gap_between_aligned linorder_not_less mask_eq_decr_exp unat_arith_simps(2)) done lemma aligned_add_mask_lessD: "\ x + mask n < y; is_aligned x n \ \ x < y" for y::"'a::len word" by (metis is_aligned_no_overflow' mask_2pm1 order_le_less_trans) lemma aligned_add_mask_less_eq: "\ is_aligned x n; is_aligned y n; n < LENGTH('a) \ \ (x + mask n < y) = (x < y)" for y::"'a::len word" using aligned_add_mask_lessD is_aligned_add_step_le word_le_not_less by blast lemma is_aligned_diff: fixes m :: "'a::len word" assumes alm: "is_aligned m s1" and aln: "is_aligned n s2" and s2wb: "s2 < LENGTH('a)" and nm: "m \ {n .. n + (2 ^ s2 - 1)}" and s1s2: "s1 \ s2" and s10: "0 < s1" (* Probably can be folded into the proof \ *) shows "\q. m - n = of_nat q * 2 ^ s1 \ q < 2 ^ (s2 - s1)" proof - have rl: "\m s. \ m < 2 ^ (LENGTH('a) - s); s < LENGTH('a) \ \ unat ((2::'a word) ^ s * of_nat m) = 2 ^ s * m" proof - fix m :: nat and s assume m: "m < 2 ^ (LENGTH('a) - s)" and s: "s < LENGTH('a)" then have "unat ((of_nat m) :: 'a word) = m" apply (subst unat_of_nat) apply (subst mod_less) apply (erule order_less_le_trans) apply (rule power_increasing) apply simp_all done then show "?thesis m s" using s m apply (subst iffD1 [OF unat_mult_lem]) apply (simp add: nat_less_power_trans)+ done qed have s1wb: "s1 < LENGTH('a)" using s2wb s1s2 by simp from alm obtain mq where mmq: "m = 2 ^ s1 * of_nat mq" and mq: "mq < 2 ^ (LENGTH('a) - s1)" by (auto elim: is_alignedE simp: field_simps) from aln obtain nq where nnq: "n = 2 ^ s2 * of_nat nq" and nq: "nq < 2 ^ (LENGTH('a) - s2)" by (auto elim: is_alignedE simp: field_simps) from s1s2 obtain sq where sq: "s2 = s1 + sq" by (auto simp: le_iff_add) note us1 = rl [OF mq s1wb] note us2 = rl [OF nq s2wb] from nm have "n \ m" by clarsimp then have "(2::'a word) ^ s2 * of_nat nq \ 2 ^ s1 * of_nat mq" using nnq mmq by simp then have "2 ^ s2 * nq \ 2 ^ s1 * mq" using s1wb s2wb by (simp add: word_le_nat_alt us1 us2) then have nqmq: "2 ^ sq * nq \ mq" using sq by (simp add: power_add) have "m - n = 2 ^ s1 * of_nat mq - 2 ^ s2 * of_nat nq" using mmq nnq by simp also have "\ = 2 ^ s1 * of_nat mq - 2 ^ s1 * 2 ^ sq * of_nat nq" using sq by (simp add: power_add) also have "\ = 2 ^ s1 * (of_nat mq - 2 ^ sq * of_nat nq)" by (simp add: field_simps) also have "\ = 2 ^ s1 * of_nat (mq - 2 ^ sq * nq)" using s1wb s2wb us1 us2 nqmq by (simp add: of_nat_diff) finally have mn: "m - n = of_nat (mq - 2 ^ sq * nq) * 2 ^ s1" by simp moreover from nm have "m - n \ 2 ^ s2 - 1" by - (rule word_diff_ls', (simp add: field_simps)+) then have "(2::'a word) ^ s1 * of_nat (mq - 2 ^ sq * nq) < 2 ^ s2" using mn s2wb by (simp add: field_simps) then have "of_nat (mq - 2 ^ sq * nq) < (2::'a word) ^ (s2 - s1)" proof (rule word_power_less_diff) have mm: "mq - 2 ^ sq * nq < 2 ^ (LENGTH('a) - s1)" using mq by simp moreover from s10 have "LENGTH('a) - s1 < LENGTH('a)" by (rule diff_less, simp) ultimately show "of_nat (mq - 2 ^ sq * nq) < (2::'a word) ^ (LENGTH('a) - s1)" using take_bit_nat_less_self_iff [of \LENGTH('a)\ \mq - 2 ^ sq * nq\] apply (auto simp add: word_less_nat_alt not_le not_less unsigned_of_nat) apply (metis take_bit_nat_eq_self_iff) done qed then have "mq - 2 ^ sq * nq < 2 ^ (s2 - s1)" using mq s2wb apply (simp add: word_less_nat_alt take_bit_eq_mod unsigned_of_nat) apply (subst (asm) mod_less) apply auto apply (rule order_le_less_trans) apply (rule diff_le_self) apply (erule order_less_le_trans) apply simp done ultimately show ?thesis by auto qed lemma is_aligned_addD1: assumes al1: "is_aligned (x + y) n" and al2: "is_aligned (x::'a::len word) n" shows "is_aligned y n" using al2 proof (rule is_aligned_get_word_bits) assume "x = 0" then show ?thesis using al1 by simp next assume nv: "n < LENGTH('a)" from al1 obtain q1 where xy: "x + y = 2 ^ n * of_nat q1" and "q1 < 2 ^ (LENGTH('a) - n)" by (rule is_alignedE) moreover from al2 obtain q2 where x: "x = 2 ^ n * of_nat q2" and "q2 < 2 ^ (LENGTH('a) - n)" by (rule is_alignedE) ultimately have "y = 2 ^ n * (of_nat q1 - of_nat q2)" by (simp add: field_simps) then show ?thesis using nv by (simp add: is_aligned_mult_triv1) qed lemmas is_aligned_addD2 = is_aligned_addD1[OF subst[OF add.commute, of "%x. is_aligned x n" for n]] lemma is_aligned_add: "\is_aligned p n; is_aligned q n\ \ is_aligned (p + q) n" by (simp add: is_aligned_mask mask_add_aligned) lemma aligned_shift: "\x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \ LENGTH('a)\ \ (x + y) >> n = y >> n" apply (subst word_plus_and_or_coroll; rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth) apply (metis less_2p_is_upper_bits_unset not_le) apply (metis le_add1 less_2p_is_upper_bits_unset test_bit_bin) done lemma aligned_shift': "\x < 2 ^ n; is_aligned (y :: 'a :: len word) n;n \ LENGTH('a)\ \ (y + x) >> n = y >> n" apply (subst word_plus_and_or_coroll; rule bit_word_eqI) apply (auto simp add: bit_simps is_aligned_nth) apply (metis less_2p_is_upper_bits_unset not_le) apply (metis bit_imp_le_length le_add1 less_2p_is_upper_bits_unset) done lemma and_neg_mask_plus_mask_mono: "(p AND NOT (mask n)) + mask n \ p" for p :: \'a::len word\ apply (rule word_le_minus_cancel[where x = "p AND NOT (mask n)"]) apply (clarsimp simp: subtract_mask) using word_and_le1[where a = "mask n" and y = p] apply (clarsimp simp: mask_eq_decr_exp word_le_less_eq) apply (rule is_aligned_no_overflow'[folded mask_2pm1]) apply (clarsimp simp: is_aligned_neg_mask) done lemma word_neg_and_le: "ptr \ (ptr AND NOT (mask n)) + (2 ^ n - 1)" for ptr :: \'a::len word\ by (simp add: and_neg_mask_plus_mask_mono mask_2pm1[symmetric]) lemma is_aligned_sub_helper: "\ is_aligned (p - d) n; d < 2 ^ n \ \ (p AND mask n = d) \ (p AND (NOT (mask n)) = p - d)" by (drule(1) is_aligned_add_helper, simp) lemma is_aligned_after_mask: "\is_aligned k m;m\ n\ \ is_aligned (k AND mask n) m" by (rule is_aligned_andI1) lemma and_mask_plus: "\is_aligned ptr m; m \ n; a < 2 ^ m\ \ ptr + a AND mask n = (ptr AND mask n) + a" apply (rule mask_eqI[where n = m]) apply (simp add:mask_twice min_def) apply (simp add:is_aligned_add_helper) apply (subst is_aligned_add_helper[THEN conjunct1]) apply (erule is_aligned_after_mask) apply simp apply simp apply simp apply (subgoal_tac "(ptr + a AND mask n) AND NOT (mask m) = (ptr + a AND NOT (mask m) ) AND mask n") apply (simp add:is_aligned_add_helper) apply (subst is_aligned_add_helper[THEN conjunct2]) apply (simp add:is_aligned_after_mask) apply simp apply simp apply (simp add:word_bw_comms word_bw_lcs) done lemma is_aligned_add_not_aligned: "\is_aligned (p::'a::len word) n; \ is_aligned (q::'a::len word) n\ \ \ is_aligned (p + q) n" by (metis is_aligned_addD1) lemma neg_mask_add_aligned: "\ is_aligned p n; q < 2 ^ n \ \ (p + q) AND NOT (mask n) = p AND NOT (mask n)" by (metis is_aligned_add_helper is_aligned_neg_mask_eq) lemma word_add_power_off: fixes a :: "'a :: len word" assumes ak: "a < k" and kw: "k < 2 ^ (LENGTH('a) - m)" and mw: "m < LENGTH('a)" and off: "off < 2 ^ m" shows "(a * 2 ^ m) + off < k * 2 ^ m" proof (cases "m = 0") case True then show ?thesis using off ak by simp next case False from ak have ak1: "a + 1 \ k" by (rule inc_le) then have "(a + 1) * 2 ^ m \ 0" apply - apply (rule word_power_nonzero) apply (erule order_le_less_trans [OF _ kw]) apply (rule mw) apply (rule less_is_non_zero_p1 [OF ak]) done then have "(a * 2 ^ m) + off < ((a + 1) * 2 ^ m)" using kw mw apply - apply (simp add: distrib_right) apply (rule word_plus_strict_mono_right [OF off]) apply (rule is_aligned_no_overflow'') apply (rule is_aligned_mult_triv2) apply assumption done also have "\ \ k * 2 ^ m" using ak1 mw kw False apply - apply (erule word_mult_le_mono1) apply (simp add: p2_gt_0) apply (simp add: word_less_nat_alt) apply (meson nat_mult_power_less_eq zero_less_numeral) done finally show ?thesis . qed lemma offset_not_aligned: "\ is_aligned (p::'a::len word) n; i > 0; i < 2 ^ n; n < LENGTH('a)\ \ \ is_aligned (p + of_nat i) n" apply (erule is_aligned_add_not_aligned) apply transfer apply (auto simp add: is_aligned_iff_udvd) apply (metis (no_types, lifting) le_less_trans less_not_refl2 less_or_eq_imp_le of_nat_eq_0_iff take_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_of_nat unat_lt2p unat_power_lower) done lemma le_or_mask: "w \ w' \ w OR mask x \ w' OR mask x" for w w' :: \'a::len word\ by (metis neg_mask_add_mask add.commute le_word_or1 mask_2pm1 neg_mask_mono_le word_plus_mono_left) end end diff --git a/thys/Word_Lib/Bits_Int.thy b/thys/Word_Lib/Bits_Int.thy --- a/thys/Word_Lib/Bits_Int.thy +++ b/thys/Word_Lib/Bits_Int.thy @@ -1,1573 +1,1577 @@ (* * Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA * * SPDX-License-Identifier: BSD-2-Clause *) section \Bitwise Operations on integers\ theory Bits_Int imports "Word_Lib.Most_significant_bit" "Word_Lib.Least_significant_bit" "Word_Lib.Generic_set_bit" "Word_Lib.Bit_Comprehension" begin subsection \Implicit bit representation of \<^typ>\int\\ lemma bin_last_def: "(odd :: int \ bool) w \ w mod 2 = 1" by (fact odd_iff_mod_2_eq_one) lemma bin_last_numeral_simps [simp]: "\ odd (0 :: int)" "odd (1 :: int)" "odd (- 1 :: int)" "odd (Numeral1 :: int)" "\ odd (numeral (Num.Bit0 w) :: int)" "odd (numeral (Num.Bit1 w) :: int)" "\ odd (- numeral (Num.Bit0 w) :: int)" "odd (- numeral (Num.Bit1 w) :: int)" by simp_all lemma bin_rest_numeral_simps [simp]: "(\k::int. k div 2) 0 = 0" "(\k::int. k div 2) 1 = 0" "(\k::int. k div 2) (- 1) = - 1" "(\k::int. k div 2) Numeral1 = 0" "(\k::int. k div 2) (numeral (Num.Bit0 w)) = numeral w" "(\k::int. k div 2) (numeral (Num.Bit1 w)) = numeral w" "(\k::int. k div 2) (- numeral (Num.Bit0 w)) = - numeral w" "(\k::int. k div 2) (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)" by simp_all lemma bin_rl_eqI: "\(\k::int. k div 2) x = (\k::int. k div 2) y; odd x = odd y\ \ x = y" by (auto elim: oddE) lemma [simp]: shows bin_rest_lt0: "(\k::int. k div 2) i < 0 \ i < 0" and bin_rest_ge_0: "(\k::int. k div 2) i \ 0 \ i \ 0" by auto lemma bin_rest_gt_0 [simp]: "(\k::int. k div 2) x > 0 \ x > 1" by auto subsection \Bit projection\ lemma bin_nth_eq_iff: "(bit :: int \ nat \ bool) x = (bit :: int \ nat \ bool) y \ x = y" by (simp add: bit_eq_iff fun_eq_iff) lemma bin_eqI: "x = y" if "\n. (bit :: int \ nat \ bool) x n \ (bit :: int \ nat \ bool) y n" using that by (rule bit_eqI) lemma bin_eq_iff: "x = y \ (\n. (bit :: int \ nat \ bool) x n = (bit :: int \ nat \ bool) y n)" by (metis bit_eq_iff) lemma bin_nth_zero [simp]: "\ (bit :: int \ nat \ bool) 0 n" by simp lemma bin_nth_1 [simp]: "(bit :: int \ nat \ bool) 1 n \ n = 0" by (cases n) (simp_all add: bit_Suc) lemma bin_nth_minus1 [simp]: "(bit :: int \ nat \ bool) (- 1) n" by simp lemma bin_nth_numeral: "(\k::int. k div 2) x = y \ (bit :: int \ nat \ bool) x (numeral n) = (bit :: int \ nat \ bool) y (pred_numeral n)" by (simp add: numeral_eq_Suc bit_Suc) lemmas bin_nth_numeral_simps [simp] = bin_nth_numeral [OF bin_rest_numeral_simps(8)] lemmas bin_nth_simps = bit_0 bit_Suc bin_nth_zero bin_nth_minus1 bin_nth_numeral_simps lemma nth_2p_bin: "(bit :: int \ nat \ bool) (2 ^ n) m = (m = n)" \ \for use when simplifying with \bin_nth_Bit\\ by (auto simp add: bit_exp_iff) lemma nth_rest_power_bin: "(bit :: int \ nat \ bool) (((\k::int. k div 2) ^^ k) w) n = (bit :: int \ nat \ bool) w (n + k)" apply (induct k arbitrary: n) apply clarsimp apply clarsimp apply (simp only: bit_Suc [symmetric] add_Suc) done lemma bin_nth_numeral_unfold: "(bit :: int \ nat \ bool) (numeral (num.Bit0 x)) n \ n > 0 \ (bit :: int \ nat \ bool) (numeral x) (n - 1)" "(bit :: int \ nat \ bool) (numeral (num.Bit1 x)) n \ (n > 0 \ (bit :: int \ nat \ bool) (numeral x) (n - 1))" by (cases n; simp)+ subsection \Truncating\ definition bin_sign :: "int \ int" where "bin_sign k = (if k \ 0 then 0 else - 1)" lemma bin_sign_simps [simp]: "bin_sign 0 = 0" "bin_sign 1 = 0" "bin_sign (- 1) = - 1" "bin_sign (numeral k) = 0" "bin_sign (- numeral k) = -1" by (simp_all add: bin_sign_def) lemma bin_sign_rest [simp]: "bin_sign ((\k::int. k div 2) w) = bin_sign w" by (simp add: bin_sign_def) lemma bintrunc_mod2p: "(take_bit :: nat \ int \ int) n w = w mod 2 ^ n" by (fact take_bit_eq_mod) lemma sbintrunc_mod2p: "(signed_take_bit :: nat \ int \ int) n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n" by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift) lemma sbintrunc_eq_take_bit: \(signed_take_bit :: nat \ int \ int) n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\ by (fact signed_take_bit_eq_take_bit_shift) lemma sign_bintr: "bin_sign ((take_bit :: nat \ int \ int) n w) = 0" by (simp add: bin_sign_def) lemma bintrunc_n_0: "(take_bit :: nat \ int \ int) n 0 = 0" by (fact take_bit_of_0) lemma sbintrunc_n_0: "(signed_take_bit :: nat \ int \ int) n 0 = 0" by (fact signed_take_bit_of_0) lemma sbintrunc_n_minus1: "(signed_take_bit :: nat \ int \ int) n (- 1) = -1" by (fact signed_take_bit_of_minus_1) lemma bintrunc_Suc_numeral: "(take_bit :: nat \ int \ int) (Suc n) 1 = 1" "(take_bit :: nat \ int \ int) (Suc n) (- 1) = 1 + 2 * (take_bit :: nat \ int \ int) n (- 1)" "(take_bit :: nat \ int \ int) (Suc n) (numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \ int \ int) n (numeral w)" "(take_bit :: nat \ int \ int) (Suc n) (numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \ int \ int) n (numeral w)" "(take_bit :: nat \ int \ int) (Suc n) (- numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \ int \ int) n (- numeral w)" "(take_bit :: nat \ int \ int) (Suc n) (- numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \ int \ int) n (- numeral (w + Num.One))" by (simp_all add: take_bit_Suc del: take_bit_minus_one_eq_mask) lemma sbintrunc_0_numeral [simp]: "(signed_take_bit :: nat \ int \ int) 0 1 = -1" "(signed_take_bit :: nat \ int \ int) 0 (numeral (Num.Bit0 w)) = 0" "(signed_take_bit :: nat \ int \ int) 0 (numeral (Num.Bit1 w)) = -1" "(signed_take_bit :: nat \ int \ int) 0 (- numeral (Num.Bit0 w)) = 0" "(signed_take_bit :: nat \ int \ int) 0 (- numeral (Num.Bit1 w)) = -1" by simp_all lemma sbintrunc_Suc_numeral: "(signed_take_bit :: nat \ int \ int) (Suc n) 1 = 1" "(signed_take_bit :: nat \ int \ int) (Suc n) (numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \ int \ int) n (numeral w)" "(signed_take_bit :: nat \ int \ int) (Suc n) (numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \ int \ int) n (numeral w)" "(signed_take_bit :: nat \ int \ int) (Suc n) (- numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \ int \ int) n (- numeral w)" "(signed_take_bit :: nat \ int \ int) (Suc n) (- numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \ int \ int) n (- numeral (w + Num.One))" by (simp_all add: signed_take_bit_Suc) lemma bin_sign_lem: "(bin_sign ((signed_take_bit :: nat \ int \ int) n bin) = -1) = bit bin n" by (simp add: bin_sign_def) lemma nth_bintr: "(bit :: int \ nat \ bool) ((take_bit :: nat \ int \ int) m w) n \ n < m \ (bit :: int \ nat \ bool) w n" by (fact bit_take_bit_iff) lemma nth_sbintr: "(bit :: int \ nat \ bool) ((signed_take_bit :: nat \ int \ int) m w) n = (if n < m then (bit :: int \ nat \ bool) w n else (bit :: int \ nat \ bool) w m)" by (simp add: bit_signed_take_bit_iff min_def) lemma bin_nth_Bit0: "(bit :: int \ nat \ bool) (numeral (Num.Bit0 w)) n \ (\m. n = Suc m \ (bit :: int \ nat \ bool) (numeral w) m)" using bit_double_iff [of \numeral w :: int\ n] by (auto intro: exI [of _ \n - 1\]) lemma bin_nth_Bit1: "(bit :: int \ nat \ bool) (numeral (Num.Bit1 w)) n \ n = 0 \ (\m. n = Suc m \ (bit :: int \ nat \ bool) (numeral w) m)" using even_bit_succ_iff [of \2 * numeral w :: int\ n] bit_double_iff [of \numeral w :: int\ n] by auto lemma bintrunc_bintrunc_l: "n \ m \ (take_bit :: nat \ int \ int) m ((take_bit :: nat \ int \ int) n w) = (take_bit :: nat \ int \ int) n w" by simp lemma sbintrunc_sbintrunc_l: "n \ m \ (signed_take_bit :: nat \ int \ int) m ((signed_take_bit :: nat \ int \ int) n w) = (signed_take_bit :: nat \ int \ int) n w" by simp lemma bintrunc_bintrunc_ge: "n \ m \ (take_bit :: nat \ int \ int) n ((take_bit :: nat \ int \ int) m w) = (take_bit :: nat \ int \ int) n w" by (rule bin_eqI) (auto simp: nth_bintr) lemma bintrunc_bintrunc_min [simp]: "(take_bit :: nat \ int \ int) m ((take_bit :: nat \ int \ int) n w) = (take_bit :: nat \ int \ int) (min m n) w" by (rule take_bit_take_bit) lemma sbintrunc_sbintrunc_min [simp]: "(signed_take_bit :: nat \ int \ int) m ((signed_take_bit :: nat \ int \ int) n w) = (signed_take_bit :: nat \ int \ int) (min m n) w" by (rule signed_take_bit_signed_take_bit) lemmas sbintrunc_Suc_Pls = signed_take_bit_Suc [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps] lemmas sbintrunc_Suc_Min = signed_take_bit_Suc [where a="-1::int", simplified bin_last_numeral_simps bin_rest_numeral_simps] lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_numeral lemmas sbintrunc_Pls = signed_take_bit_0 [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps] lemmas sbintrunc_Min = signed_take_bit_0 [where a="-1::int", simplified bin_last_numeral_simps bin_rest_numeral_simps] lemmas sbintrunc_0_simps = sbintrunc_Pls sbintrunc_Min lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs lemma bintrunc_minus: "0 < n \ (take_bit :: nat \ int \ int) (Suc (n - 1)) w = (take_bit :: nat \ int \ int) n w" by auto lemma sbintrunc_minus: "0 < n \ (signed_take_bit :: nat \ int \ int) (Suc (n - 1)) w = (signed_take_bit :: nat \ int \ int) n w" by auto lemmas sbintrunc_minus_simps = sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] lemma sbintrunc_BIT_I: \0 < n \ (signed_take_bit :: nat \ int \ int) (n - 1) 0 = y \ (signed_take_bit :: nat \ int \ int) n 0 = 2 * y\ by simp lemma sbintrunc_Suc_Is: \(signed_take_bit :: nat \ int \ int) n (- 1) = y \ (signed_take_bit :: nat \ int \ int) (Suc n) (- 1) = 1 + 2 * y\ by auto lemma sbintrunc_Suc_lem: "(signed_take_bit :: nat \ int \ int) (Suc n) x = y \ m = Suc n \ (signed_take_bit :: nat \ int \ int) m x = y" by (rule ssubst) lemmas sbintrunc_Suc_Ialts = sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] lemma sbintrunc_bintrunc_lt: "m > n \ (signed_take_bit :: nat \ int \ int) n ((take_bit :: nat \ int \ int) m w) = (signed_take_bit :: nat \ int \ int) n w" by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr) lemma bintrunc_sbintrunc_le: "m \ Suc n \ (take_bit :: nat \ int \ int) m ((signed_take_bit :: nat \ int \ int) n w) = (take_bit :: nat \ int \ int) m w" by (rule take_bit_signed_take_bit) lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le] lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt] lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l] lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] lemma bintrunc_sbintrunc' [simp]: "0 < n \ (take_bit :: nat \ int \ int) n ((signed_take_bit :: nat \ int \ int) (n - 1) w) = (take_bit :: nat \ int \ int) n w" by (cases n) simp_all lemma sbintrunc_bintrunc' [simp]: "0 < n \ (signed_take_bit :: nat \ int \ int) (n - 1) ((take_bit :: nat \ int \ int) n w) = (signed_take_bit :: nat \ int \ int) (n - 1) w" by (cases n) simp_all lemma bin_sbin_eq_iff: "(take_bit :: nat \ int \ int) (Suc n) x = (take_bit :: nat \ int \ int) (Suc n) y \ (signed_take_bit :: nat \ int \ int) n x = (signed_take_bit :: nat \ int \ int) n y" apply (rule iffI) apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc]) apply simp apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc]) apply simp done lemma bin_sbin_eq_iff': "0 < n \ (take_bit :: nat \ int \ int) n x = (take_bit :: nat \ int \ int) n y \ (signed_take_bit :: nat \ int \ int) (n - 1) x = (signed_take_bit :: nat \ int \ int) (n - 1) y" by (cases n) (simp_all add: bin_sbin_eq_iff) lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def] lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def] lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l] lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l] (* although bintrunc_minus_simps, if added to default simpset, tends to get applied where it's not wanted in developing the theories, we get a version for when the word length is given literally *) lemmas nat_non0_gr = trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] lemma bintrunc_numeral: "(take_bit :: nat \ int \ int) (numeral k) x = of_bool (odd x) + 2 * (take_bit :: nat \ int \ int) (pred_numeral k) (x div 2)" by (simp add: numeral_eq_Suc take_bit_Suc mod_2_eq_odd) lemma sbintrunc_numeral: "(signed_take_bit :: nat \ int \ int) (numeral k) x = of_bool (odd x) + 2 * (signed_take_bit :: nat \ int \ int) (pred_numeral k) (x div 2)" by (simp add: numeral_eq_Suc signed_take_bit_Suc mod2_eq_if) lemma bintrunc_numeral_simps [simp]: "(take_bit :: nat \ int \ int) (numeral k) (numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \ int \ int) (pred_numeral k) (numeral w)" "(take_bit :: nat \ int \ int) (numeral k) (numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \ int \ int) (pred_numeral k) (numeral w)" "(take_bit :: nat \ int \ int) (numeral k) (- numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \ int \ int) (pred_numeral k) (- numeral w)" "(take_bit :: nat \ int \ int) (numeral k) (- numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \ int \ int) (pred_numeral k) (- numeral (w + Num.One))" "(take_bit :: nat \ int \ int) (numeral k) 1 = 1" by (simp_all add: bintrunc_numeral) lemma sbintrunc_numeral_simps [simp]: "(signed_take_bit :: nat \ int \ int) (numeral k) (numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \ int \ int) (pred_numeral k) (numeral w)" "(signed_take_bit :: nat \ int \ int) (numeral k) (numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \ int \ int) (pred_numeral k) (numeral w)" "(signed_take_bit :: nat \ int \ int) (numeral k) (- numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \ int \ int) (pred_numeral k) (- numeral w)" "(signed_take_bit :: nat \ int \ int) (numeral k) (- numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \ int \ int) (pred_numeral k) (- numeral (w + Num.One))" "(signed_take_bit :: nat \ int \ int) (numeral k) 1 = 1" by (simp_all add: sbintrunc_numeral) lemma no_bintr_alt1: "(take_bit :: nat \ int \ int) n = (\w. w mod 2 ^ n :: int)" by (rule ext) (rule bintrunc_mod2p) lemma range_bintrunc: "range ((take_bit :: nat \ int \ int) n) = {i. 0 \ i \ i < 2 ^ n}" by (auto simp add: take_bit_eq_mod image_iff) (metis mod_pos_pos_trivial) lemma no_sbintr_alt2: "(signed_take_bit :: nat \ int \ int) n = (\w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)" by (rule ext) (simp add : sbintrunc_mod2p) lemma range_sbintrunc: "range ((signed_take_bit :: nat \ int \ int) n) = {i. - (2 ^ n) \ i \ i < 2 ^ n}" proof - have \surj (\k::int. k + 2 ^ n)\ by (rule surjI [of _ \(\k. k - 2 ^ n)\]) simp moreover have \(signed_take_bit :: nat \ int \ int) n = ((\k. k - 2 ^ n) \ take_bit (Suc n) \ (\k. k + 2 ^ n))\ by (simp add: sbintrunc_eq_take_bit fun_eq_iff) ultimately show ?thesis apply (simp only: fun.set_map range_bintrunc) apply (auto simp add: image_iff) apply presburger done qed lemma sbintrunc_inc: \k + 2 ^ Suc n \ (signed_take_bit :: nat \ int \ int) n k\ if \k < - (2 ^ n)\ using that by (fact signed_take_bit_int_greater_eq) lemma sbintrunc_dec: \(signed_take_bit :: nat \ int \ int) n k \ k - 2 ^ (Suc n)\ if \k \ 2 ^ n\ using that by (fact signed_take_bit_int_less_eq) lemma bintr_ge0: "0 \ (take_bit :: nat \ int \ int) n w" by (simp add: bintrunc_mod2p) lemma bintr_lt2p: "(take_bit :: nat \ int \ int) n w < 2 ^ n" by (simp add: bintrunc_mod2p) lemma bintr_Min: "(take_bit :: nat \ int \ int) n (- 1) = 2 ^ n - 1" by (simp add: stable_imp_take_bit_eq mask_eq_exp_minus_1) lemma sbintr_ge: "- (2 ^ n) \ (signed_take_bit :: nat \ int \ int) n w" by (fact signed_take_bit_int_greater_eq_minus_exp) lemma sbintr_lt: "(signed_take_bit :: nat \ int \ int) n w < 2 ^ n" by (fact signed_take_bit_int_less_exp) lemma sign_Pls_ge_0: "bin_sign bin = 0 \ bin \ 0" for bin :: int by (simp add: bin_sign_def) lemma sign_Min_lt_0: "bin_sign bin = -1 \ bin < 0" for bin :: int by (simp add: bin_sign_def) lemma bin_rest_trunc: "(\k::int. k div 2) ((take_bit :: nat \ int \ int) n bin) = (take_bit :: nat \ int \ int) (n - 1) ((\k::int. k div 2) bin)" by (simp add: take_bit_rec [of n bin]) lemma bin_rest_power_trunc: "((\k::int. k div 2) ^^ k) ((take_bit :: nat \ int \ int) n bin) = (take_bit :: nat \ int \ int) (n - k) (((\k::int. k div 2) ^^ k) bin)" by (induct k) (auto simp: bin_rest_trunc) lemma bin_rest_trunc_i: "(take_bit :: nat \ int \ int) n ((\k::int. k div 2) bin) = (\k::int. k div 2) ((take_bit :: nat \ int \ int) (Suc n) bin)" by (auto simp add: take_bit_Suc) lemma bin_rest_strunc: "(\k::int. k div 2) ((signed_take_bit :: nat \ int \ int) (Suc n) bin) = (signed_take_bit :: nat \ int \ int) n ((\k::int. k div 2) bin)" by (simp add: signed_take_bit_Suc) lemma bintrunc_rest [simp]: "(take_bit :: nat \ int \ int) n ((\k::int. k div 2) ((take_bit :: nat \ int \ int) n bin)) = (\k::int. k div 2) ((take_bit :: nat \ int \ int) n bin)" by (induct n arbitrary: bin) (simp_all add: take_bit_Suc) lemma sbintrunc_rest [simp]: "(signed_take_bit :: nat \ int \ int) n ((\k::int. k div 2) ((signed_take_bit :: nat \ int \ int) n bin)) = (\k::int. k div 2) ((signed_take_bit :: nat \ int \ int) n bin)" by (induct n arbitrary: bin) (simp_all add: signed_take_bit_Suc mod2_eq_if) lemma bintrunc_rest': "(take_bit :: nat \ int \ int) n \ (\k::int. k div 2) \ (take_bit :: nat \ int \ int) n = (\k::int. k div 2) \ (take_bit :: nat \ int \ int) n" by (rule ext) auto lemma sbintrunc_rest': "(signed_take_bit :: nat \ int \ int) n \ (\k::int. k div 2) \ (signed_take_bit :: nat \ int \ int) n = (\k::int. k div 2) \ (signed_take_bit :: nat \ int \ int) n" by (rule ext) auto lemma rco_lem: "f \ g \ f = g \ f \ f \ (g \ f) ^^ n = g ^^ n \ f" apply (rule ext) apply (induct_tac n) apply (simp_all (no_asm)) apply (drule fun_cong) apply (unfold o_def) apply (erule trans) apply simp done lemmas rco_bintr = bintrunc_rest' [THEN rco_lem [THEN fun_cong], unfolded o_def] lemmas rco_sbintr = sbintrunc_rest' [THEN rco_lem [THEN fun_cong], unfolded o_def] subsection \Splitting and concatenation\ definition bin_split :: \nat \ int \ int \ int\ where [simp]: \bin_split n k = (drop_bit n k, take_bit n k)\ lemma [code]: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (w div 2) in (w1, of_bool (odd w) + 2 * w2))" "bin_split 0 w = (w, 0)" by (simp_all add: drop_bit_Suc take_bit_Suc mod_2_eq_odd) lemma bin_cat_eq_push_bit_add_take_bit: \concat_bit n l k = push_bit n k + take_bit n l\ by (simp add: concat_bit_eq) lemma bin_sign_cat: "bin_sign ((\k n l. concat_bit n l k) x n y) = bin_sign x" proof - have \0 \ x\ if \0 \ x * 2 ^ n + y mod 2 ^ n\ proof - have \y mod 2 ^ n < 2 ^ n\ using pos_mod_bound [of \2 ^ n\ y] by simp then have \\ y mod 2 ^ n \ 2 ^ n\ by (simp add: less_le) with that have \x \ - 1\ by auto have *: \- 1 \ (- (y mod 2 ^ n)) div 2 ^ n\ by (simp add: zdiv_zminus1_eq_if) from that have \- (y mod 2 ^ n) \ x * 2 ^ n\ by simp then have \(- (y mod 2 ^ n)) div 2 ^ n \ (x * 2 ^ n) div 2 ^ n\ using zdiv_mono1 zero_less_numeral zero_less_power by blast with * have \- 1 \ x * 2 ^ n div 2 ^ n\ by simp with \x \ - 1\ show ?thesis by simp qed then show ?thesis by (simp add: bin_sign_def not_le not_less bin_cat_eq_push_bit_add_take_bit push_bit_eq_mult take_bit_eq_mod) qed lemma bin_cat_assoc: "(\k n l. concat_bit n l k) ((\k n l. concat_bit n l k) x m y) n z = (\k n l. concat_bit n l k) x (m + n) ((\k n l. concat_bit n l k) y n z)" by (fact concat_bit_assoc) lemma bin_cat_assoc_sym: "(\k n l. concat_bit n l k) x m ((\k n l. concat_bit n l k) y n z) = (\k n l. concat_bit n l k) ((\k n l. concat_bit n l k) x (m - n) y) (min m n) z" by (fact concat_bit_assoc_sym) definition bin_rcat :: \nat \ int list \ int\ where \bin_rcat n = horner_sum (take_bit n) (2 ^ n) \ rev\ lemma bin_rcat_eq_foldl: \bin_rcat n = foldl (\u v. (\k n l. concat_bit n l k) u n v) 0\ proof fix ks :: \int list\ show \bin_rcat n ks = foldl (\u v. (\k n l. concat_bit n l k) u n v) 0 ks\ by (induction ks rule: rev_induct) (simp_all add: bin_rcat_def concat_bit_eq push_bit_eq_mult) qed fun bin_rsplit_aux :: "nat \ nat \ int \ int list \ int list" where "bin_rsplit_aux n m c bs = (if m = 0 \ n = 0 then bs else let (a, b) = bin_split n c in bin_rsplit_aux n (m - n) a (b # bs))" definition bin_rsplit :: "nat \ nat \ int \ int list" where "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []" fun bin_rsplitl_aux :: "nat \ nat \ int \ int list \ int list" where "bin_rsplitl_aux n m c bs = (if m = 0 \ n = 0 then bs else let (a, b) = bin_split (min m n) c in bin_rsplitl_aux n (m - n) a (b # bs))" definition bin_rsplitl :: "nat \ nat \ int \ int list" where "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []" declare bin_rsplit_aux.simps [simp del] declare bin_rsplitl_aux.simps [simp del] lemma bin_nth_cat: "(bit :: int \ nat \ bool) ((\k n l. concat_bit n l k) x k y) n = (if n < k then (bit :: int \ nat \ bool) y n else (bit :: int \ nat \ bool) x (n - k))" by (simp add: bit_concat_bit_iff) lemma bin_nth_drop_bit_iff: \(bit :: int \ nat \ bool) (drop_bit n c) k \ (bit :: int \ nat \ bool) c (n + k)\ by (simp add: bit_drop_bit_eq) lemma bin_nth_take_bit_iff: \(bit :: int \ nat \ bool) (take_bit n c) k \ k < n \ (bit :: int \ nat \ bool) c k\ by (fact bit_take_bit_iff) lemma bin_nth_split: "bin_split n c = (a, b) \ (\k. (bit :: int \ nat \ bool) a k = (bit :: int \ nat \ bool) c (n + k)) \ (\k. (bit :: int \ nat \ bool) b k = (k < n \ (bit :: int \ nat \ bool) c k))" by (auto simp add: bin_nth_drop_bit_iff bin_nth_take_bit_iff) lemma bin_cat_zero [simp]: "(\k n l. concat_bit n l k) 0 n w = (take_bit :: nat \ int \ int) n w" by (simp add: bin_cat_eq_push_bit_add_take_bit) lemma bintr_cat1: "(take_bit :: nat \ int \ int) (k + n) ((\k n l. concat_bit n l k) a n b) = (\k n l. concat_bit n l k) ((take_bit :: nat \ int \ int) k a) n b" by (metis bin_cat_assoc bin_cat_zero) lemma bintr_cat: "(take_bit :: nat \ int \ int) m ((\k n l. concat_bit n l k) a n b) = (\k n l. concat_bit n l k) ((take_bit :: nat \ int \ int) (m - n) a) n ((take_bit :: nat \ int \ int) (min m n) b)" by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr) lemma bintr_cat_same [simp]: "(take_bit :: nat \ int \ int) n ((\k n l. concat_bit n l k) a n b) = (take_bit :: nat \ int \ int) n b" by (auto simp add : bintr_cat) lemma cat_bintr [simp]: "(\k n l. concat_bit n l k) a n ((take_bit :: nat \ int \ int) n b) = (\k n l. concat_bit n l k) a n b" by (simp add: bin_cat_eq_push_bit_add_take_bit) lemma split_bintrunc: "bin_split n c = (a, b) \ b = (take_bit :: nat \ int \ int) n c" by simp lemma bin_cat_split: "bin_split n w = (u, v) \ w = (\k n l. concat_bit n l k) u n v" by (auto simp add: bin_cat_eq_push_bit_add_take_bit bits_ident) lemma drop_bit_bin_cat_eq: \drop_bit n ((\k n l. concat_bit n l k) v n w) = v\ by (rule bit_eqI) (simp add: bit_drop_bit_eq bit_concat_bit_iff) lemma take_bit_bin_cat_eq: \take_bit n ((\k n l. concat_bit n l k) v n w) = take_bit n w\ by (rule bit_eqI) (simp add: bit_concat_bit_iff) lemma bin_split_cat: "bin_split n ((\k n l. concat_bit n l k) v n w) = (v, (take_bit :: nat \ int \ int) n w)" by (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq) lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)" by simp lemma bin_split_minus1 [simp]: "bin_split n (- 1) = (- 1, (take_bit :: nat \ int \ int) n (- 1))" by simp lemma bin_split_trunc: "bin_split (min m n) c = (a, b) \ bin_split n ((take_bit :: nat \ int \ int) m c) = ((take_bit :: nat \ int \ int) (m - n) a, b)" apply (induct n arbitrary: m b c, clarsimp) apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) apply (case_tac m) apply (auto simp: Let_def drop_bit_Suc take_bit_Suc mod_2_eq_odd split: prod.split_asm) done lemma bin_split_trunc1: "bin_split n c = (a, b) \ bin_split n ((take_bit :: nat \ int \ int) m c) = ((take_bit :: nat \ int \ int) (m - n) a, (take_bit :: nat \ int \ int) m b)" apply (induct n arbitrary: m b c, clarsimp) apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) apply (case_tac m) apply (auto simp: Let_def drop_bit_Suc take_bit_Suc mod_2_eq_odd split: prod.split_asm) done lemma bin_cat_num: "(\k n l. concat_bit n l k) a n b = a * 2 ^ n + (take_bit :: nat \ int \ int) n b" by (simp add: bin_cat_eq_push_bit_add_take_bit push_bit_eq_mult) lemma bin_split_num: "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" by (simp add: drop_bit_eq_div take_bit_eq_mod) lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps lemmas rsplit_aux_simps = bin_rsplit_aux_simps lemmas th_if_simp1 = if_split [where P = "(=) l", THEN iffD1, THEN conjunct1, THEN mp] for l lemmas th_if_simp2 = if_split [where P = "(=) l", THEN iffD1, THEN conjunct2, THEN mp] for l lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1] lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2] \ \these safe to \[simp add]\ as require calculating \m - n\\ lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def] lemmas rbscl = bin_rsplit_aux_simp2s (2) lemmas rsplit_aux_0_simps [simp] = rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2] lemma bin_rsplit_aux_append: "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs" apply (induct n m c bs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) apply (subst bin_rsplit_aux.simps) apply (clarsimp split: prod.split) done lemma bin_rsplitl_aux_append: "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs" apply (induct n m c bs rule: bin_rsplitl_aux.induct) apply (subst bin_rsplitl_aux.simps) apply (subst bin_rsplitl_aux.simps) apply (clarsimp split: prod.split) done lemmas rsplit_aux_apps [where bs = "[]"] = bin_rsplit_aux_append bin_rsplitl_aux_append lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def lemmas rsplit_aux_alts = rsplit_aux_apps [unfolded append_Nil rsplit_def_auxs [symmetric]] lemma bin_split_minus: "0 < n \ bin_split (Suc (n - 1)) w = bin_split n w" by auto lemma bin_split_pred_simp [simp]: "(0::nat) < numeral bin \ bin_split (numeral bin) w = (let (w1, w2) = bin_split (numeral bin - 1) ((\k::int. k div 2) w) in (w1, of_bool (odd w) + 2 * w2))" by (simp add: take_bit_rec drop_bit_rec mod_2_eq_odd) lemma bin_rsplit_aux_simp_alt: "bin_rsplit_aux n m c bs = (if m = 0 \ n = 0 then bs else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)" apply (simp add: bin_rsplit_aux.simps [of n m c bs]) apply (subst rsplit_aux_alts) apply (simp add: bin_rsplit_def) done lemmas bin_rsplit_simp_alt = trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt] lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans] lemma bin_rsplit_size_sign' [rule_format]: "n > 0 \ rev sw = bin_rsplit n (nw, w) \ \v\set sw. (take_bit :: nat \ int \ int) n v = v" apply (induct sw arbitrary: nw w) apply clarsimp apply clarsimp apply (drule bthrs) apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) apply clarify apply simp done lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]] lemma bin_nth_rsplit [rule_format] : "n > 0 \ m < n \ \w k nw. rev sw = bin_rsplit n (nw, w) \ k < size sw \ (bit :: int \ nat \ bool) (sw ! k) m = (bit :: int \ nat \ bool) w (k * n + m)" apply (induct sw) apply clarsimp apply clarsimp apply (drule bthrs) apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) apply (erule allE, erule impE, erule exI) apply (case_tac k) apply clarsimp prefer 2 apply clarsimp apply (erule allE) apply (erule (1) impE) apply (simp add: bit_drop_bit_eq ac_simps) apply (simp add: bit_take_bit_iff ac_simps) done lemma bin_rsplit_all: "0 < nw \ nw \ n \ bin_rsplit n (nw, w) = [(take_bit :: nat \ int \ int) n w]" by (auto simp: bin_rsplit_def rsplit_aux_simp2ls split: prod.split dest!: split_bintrunc) lemma bin_rsplit_l [rule_format]: "\bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, (take_bit :: nat \ int \ int) m bin)" apply (rule_tac a = "m" in wf_less_than [THEN wf_induct]) apply (simp (no_asm) add: bin_rsplitl_def bin_rsplit_def) apply (rule allI) apply (subst bin_rsplitl_aux.simps) apply (subst bin_rsplit_aux.simps) apply (clarsimp simp: Let_def split: prod.split) apply (simp add: ac_simps) apply (subst rsplit_aux_alts(1)) apply (subst rsplit_aux_alts(2)) apply clarsimp unfolding bin_rsplit_def bin_rsplitl_def apply (simp add: drop_bit_take_bit) apply (case_tac \x < n\) apply (simp_all add: not_less min_def) done lemma bin_rsplit_rcat [rule_format]: "n > 0 \ bin_rsplit n (n * size ws, bin_rcat n ws) = map ((take_bit :: nat \ int \ int) n) ws" apply (unfold bin_rsplit_def bin_rcat_eq_foldl) apply (rule_tac xs = ws in rev_induct) apply clarsimp apply clarsimp apply (subst rsplit_aux_alts) apply (simp add: drop_bit_bin_cat_eq take_bit_bin_cat_eq) done lemma bin_rsplit_aux_len_le [rule_format] : "\ws m. n \ 0 \ ws = bin_rsplit_aux n nw w bs \ length ws \ m \ nw + length bs * n \ m * n" proof - have *: R if d: "i \ j \ m < j'" and R1: "i * k \ j * k \ R" and R2: "Suc m * k' \ j' * k' \ R" for i j j' k k' m :: nat and R using d apply safe apply (rule R1, erule mult_le_mono1) apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) done have **: "0 < sc \ sc - n + (n + lb * n) \ m * n \ sc + lb * n \ m * n" for sc m n lb :: nat apply safe apply arith apply (case_tac "sc \ n") apply arith apply (insert linorder_le_less_linear [of m lb]) apply (erule_tac k=n and k'=n in *) apply arith apply simp done show ?thesis apply (induct n nw w bs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) apply (simp add: ** Let_def split: prod.split) done qed lemma bin_rsplit_len_le: "n \ 0 \ ws = bin_rsplit n (nw, w) \ length ws \ m \ nw \ m * n" by (auto simp: bin_rsplit_def bin_rsplit_aux_len_le) lemma bin_rsplit_aux_len: "n \ 0 \ length (bin_rsplit_aux n nw w cs) = (nw + n - 1) div n + length cs" apply (induct n nw w cs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) apply (clarsimp simp: Let_def split: prod.split) apply (erule thin_rl) apply (case_tac m) apply simp apply (case_tac "m \ n") apply (auto simp add: div_add_self2) done lemma bin_rsplit_len: "n \ 0 \ length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" by (auto simp: bin_rsplit_def bin_rsplit_aux_len) lemma bin_rsplit_aux_len_indep: "n \ 0 \ length bs = length cs \ length (bin_rsplit_aux n nw v bs) = length (bin_rsplit_aux n nw w cs)" proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) case (1 n m w cs v bs) show ?case proof (cases "m = 0") case True with \length bs = length cs\ show ?thesis by simp next case False from "1.hyps" [of \bin_split n w\ \drop_bit n w\ \take_bit n w\] \m \ 0\ \n \ 0\ have hyp: "\v bs. length bs = Suc (length cs) \ length (bin_rsplit_aux n (m - n) v bs) = length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs))" using bin_rsplit_aux_len by fastforce from \length bs = length cs\ \n \ 0\ show ?thesis by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split) qed qed lemma bin_rsplit_len_indep: "n \ 0 \ length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" apply (unfold bin_rsplit_def) apply (simp (no_asm)) apply (erule bin_rsplit_aux_len_indep) apply (rule refl) done subsection \Logical operations\ abbreviation (input) bin_sc :: \nat \ bool \ int \ int\ where \bin_sc n b i \ set_bit i n b\ lemma bin_sc_0 [simp]: "bin_sc 0 b w = of_bool b + 2 * (\k::int. k div 2) w" by (simp add: set_bit_int_def) lemma bin_sc_Suc [simp]: "bin_sc (Suc n) b w = of_bool (odd w) + 2 * bin_sc n b (w div 2)" by (simp add: set_bit_int_def set_bit_Suc unset_bit_Suc bin_last_def) lemma bin_nth_sc [bit_simps]: "bit (bin_sc n b w) n \ b" by (simp add: bit_simps) lemma bin_sc_sc_same [simp]: "bin_sc n c (bin_sc n b w) = bin_sc n c w" by (induction n arbitrary: w) (simp_all add: bit_Suc) lemma bin_sc_sc_diff: "m \ n \ bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" apply (induct n arbitrary: w m) apply (case_tac [!] m) apply auto done lemma bin_nth_sc_gen: "(bit :: int \ nat \ bool) (bin_sc n b w) m = (if m = n then b else (bit :: int \ nat \ bool) w m)" apply (induct n arbitrary: w m) apply (case_tac m; simp add: bit_Suc) apply (case_tac m; simp add: bit_Suc) done lemma bin_sc_eq: \bin_sc n False = unset_bit n\ \bin_sc n True = Bit_Operations.set_bit n\ apply (simp_all add: fun_eq_iff bit_eq_iff) apply (simp_all add: bit_simps bin_nth_sc_gen) done lemma bin_sc_nth [simp]: "bin_sc n ((bit :: int \ nat \ bool) w n) w = w" by (rule bit_eqI) (simp add: bin_nth_sc_gen) lemma bin_sign_sc [simp]: "bin_sign (bin_sc n b w) = bin_sign w" proof (induction n arbitrary: w) case 0 then show ?case by (auto simp add: bin_sign_def) (use bin_rest_ge_0 in fastforce) next case (Suc n) from Suc [of \w div 2\] show ?case by (auto simp add: bin_sign_def split: if_splits) qed lemma bin_sc_bintr [simp]: "(take_bit :: nat \ int \ int) m (bin_sc n x ((take_bit :: nat \ int \ int) m w)) = (take_bit :: nat \ int \ int) m (bin_sc n x w)" apply (rule bit_eqI) apply (cases x) apply (auto simp add: bit_simps bin_sc_eq) done lemma bin_clr_le: "bin_sc n False w \ w" by (simp add: set_bit_int_def unset_bit_less_eq) lemma bin_set_ge: "bin_sc n True w \ w" by (simp add: set_bit_int_def set_bit_greater_eq) lemma bintr_bin_clr_le: "(take_bit :: nat \ int \ int) n (bin_sc m False w) \ (take_bit :: nat \ int \ int) n w" by (simp add: set_bit_int_def take_bit_unset_bit_eq unset_bit_less_eq) lemma bintr_bin_set_ge: "(take_bit :: nat \ int \ int) n (bin_sc m True w) \ (take_bit :: nat \ int \ int) n w" by (simp add: set_bit_int_def take_bit_set_bit_eq set_bit_greater_eq) lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0" by (induct n) auto lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1" by (induct n) auto lemmas bin_sc_simps = bin_sc_0 bin_sc_Suc bin_sc_TM bin_sc_FP lemma bin_sc_minus: "0 < n \ bin_sc (Suc (n - 1)) b w = bin_sc n b w" by auto lemmas bin_sc_Suc_minus = trans [OF bin_sc_minus [symmetric] bin_sc_Suc] lemma bin_sc_numeral [simp]: "bin_sc (numeral k) b w = of_bool (odd w) + 2 * bin_sc (pred_numeral k) b (w div 2)" by (simp add: numeral_eq_Suc) lemmas bin_sc_minus_simps = bin_sc_simps (2,3,4) [THEN [2] trans, OF bin_sc_minus [THEN sym]] lemma int_set_bit_0 [simp]: fixes x :: int shows "set_bit x 0 b = of_bool b + 2 * (x div 2)" by (fact bin_sc_0) lemma int_set_bit_Suc: fixes x :: int shows "set_bit x (Suc n) b = of_bool (odd x) + 2 * set_bit (x div 2) n b" by (fact bin_sc_Suc) lemma bin_last_set_bit: "odd (set_bit x n b :: int) = (if n > 0 then odd x else b)" by (cases n) (simp_all add: int_set_bit_Suc) lemma bin_rest_set_bit: "(set_bit x n b :: int) div 2 = (if n > 0 then set_bit (x div 2) (n - 1) b else x div 2)" by (cases n) (simp_all add: int_set_bit_Suc) lemma int_set_bit_numeral: fixes x :: int shows "set_bit x (numeral w) b = of_bool (odd x) + 2 * set_bit (x div 2) (pred_numeral w) b" by (fact bin_sc_numeral) lemmas int_set_bit_numerals [simp] = int_set_bit_numeral[where x="numeral w'"] int_set_bit_numeral[where x="- numeral w'"] int_set_bit_numeral[where x="Numeral1"] int_set_bit_numeral[where x="1"] int_set_bit_numeral[where x="0"] int_set_bit_Suc[where x="numeral w'"] int_set_bit_Suc[where x="- numeral w'"] int_set_bit_Suc[where x="Numeral1"] int_set_bit_Suc[where x="1"] int_set_bit_Suc[where x="0"] for w' lemma msb_set_bit [simp]: "msb (set_bit (x :: int) n b) \ msb x" by (simp add: msb_int_def set_bit_int_def) lemma word_set_bit_def: \set_bit a n x = word_of_int (bin_sc n x (uint a))\ apply (rule bit_word_eqI) apply (cases x) apply (simp_all add: bit_simps bin_sc_eq) done lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)" unfolding word_set_bit_def by (rule word_eqI) (simp add: word_size bin_nth_sc_gen nth_bintr bit_simps) lemma word_set_numeral [simp]: "set_bit (numeral bin::'a::len word) n b = word_of_int (bin_sc n b (numeral bin))" unfolding word_numeral_alt by (rule set_bit_word_of_int) lemma word_set_neg_numeral [simp]: "set_bit (- numeral bin::'a::len word) n b = word_of_int (bin_sc n b (- numeral bin))" unfolding word_neg_numeral_alt by (rule set_bit_word_of_int) lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)" unfolding word_0_wi by (rule set_bit_word_of_int) lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)" unfolding word_1_wi by (rule set_bit_word_of_int) lemma shiftl_int_def: "push_bit n x = x * 2 ^ n" for x :: int by (fact push_bit_eq_mult) lemma shiftr_int_def: "drop_bit n x = x div 2 ^ n" for x :: int by (fact drop_bit_eq_div) subsubsection \Basic simplification rules\ context includes bit_operations_syntax begin lemmas int_not_def = not_int_def lemma int_not_simps: "NOT (0::int) = -1" "NOT (1::int) = -2" "NOT (- 1::int) = 0" "NOT (numeral w::int) = - numeral (w + Num.One)" "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)" "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)" by (simp_all add: not_int_def) lemma int_not_not: "NOT (NOT x) = x" for x :: int by (fact bit.double_compl) lemma int_and_0 [simp]: "0 AND x = 0" for x :: int by (fact bit.conj_zero_left) lemma int_and_m1 [simp]: "-1 AND x = x" for x :: int by (fact and.left_neutral) lemma int_or_zero [simp]: "0 OR x = x" for x :: int by (fact or.left_neutral) lemma int_or_minus1 [simp]: "-1 OR x = -1" for x :: int by (fact bit.disj_one_left) lemma int_xor_zero [simp]: "0 XOR x = x" for x :: int by (fact xor.left_neutral) subsubsection \Binary destructors\ lemma bin_rest_NOT [simp]: "(\k::int. k div 2) (NOT x) = NOT ((\k::int. k div 2) x)" by (fact not_int_div_2) lemma bin_last_NOT [simp]: "(odd :: int \ bool) (NOT x) \ \ (odd :: int \ bool) x" by simp lemma bin_rest_AND [simp]: "(\k::int. k div 2) (x AND y) = (\k::int. k div 2) x AND (\k::int. k div 2) y" by (subst and_int_rec) auto lemma bin_last_AND [simp]: "(odd :: int \ bool) (x AND y) \ (odd :: int \ bool) x \ (odd :: int \ bool) y" by (subst and_int_rec) auto lemma bin_rest_OR [simp]: "(\k::int. k div 2) (x OR y) = (\k::int. k div 2) x OR (\k::int. k div 2) y" by (subst or_int_rec) auto lemma bin_last_OR [simp]: "(odd :: int \ bool) (x OR y) \ (odd :: int \ bool) x \ (odd :: int \ bool) y" by (subst or_int_rec) auto lemma bin_rest_XOR [simp]: "(\k::int. k div 2) (x XOR y) = (\k::int. k div 2) x XOR (\k::int. k div 2) y" by (subst xor_int_rec) auto lemma bin_last_XOR [simp]: "(odd :: int \ bool) (x XOR y) \ ((odd :: int \ bool) x \ (odd :: int \ bool) y) \ \ ((odd :: int \ bool) x \ (odd :: int \ bool) y)" by (subst xor_int_rec) auto lemma bin_nth_ops: "\x y. (bit :: int \ nat \ bool) (x AND y) n \ (bit :: int \ nat \ bool) x n \ (bit :: int \ nat \ bool) y n" "\x y. (bit :: int \ nat \ bool) (x OR y) n \ (bit :: int \ nat \ bool) x n \ (bit :: int \ nat \ bool) y n" "\x y. (bit :: int \ nat \ bool) (x XOR y) n \ (bit :: int \ nat \ bool) x n \ (bit :: int \ nat \ bool) y n" "\x. (bit :: int \ nat \ bool) (NOT x) n \ \ (bit :: int \ nat \ bool) x n" by (simp_all add: bit_and_iff bit_or_iff bit_xor_iff bit_not_iff) subsubsection \Derived properties\ lemma int_xor_minus1 [simp]: "-1 XOR x = NOT x" for x :: int by (fact bit.xor_one_left) lemma int_xor_extra_simps [simp]: "w XOR 0 = w" "w XOR -1 = NOT w" for w :: int by simp_all lemma int_or_extra_simps [simp]: "w OR 0 = w" "w OR -1 = -1" for w :: int by simp_all lemma int_and_extra_simps [simp]: "w AND 0 = 0" "w AND -1 = w" for w :: int by simp_all text \Commutativity of the above.\ lemma bin_ops_comm: fixes x y :: int shows int_and_comm: "x AND y = y AND x" and int_or_comm: "x OR y = y OR x" and int_xor_comm: "x XOR y = y XOR x" by (simp_all add: ac_simps) lemma bin_ops_same [simp]: "x AND x = x" "x OR x = x" "x XOR x = 0" for x :: int by simp_all lemmas bin_log_esimps = int_and_extra_simps int_or_extra_simps int_xor_extra_simps int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1 subsubsection \Basic properties of logical (bit-wise) operations\ lemma bbw_ao_absorb: "x AND (y OR x) = x \ x OR (y AND x) = x" for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemma bbw_ao_absorbs_other: "x AND (x OR y) = x \ (y AND x) OR x = x" "(y OR x) AND x = x \ x OR (x AND y) = x" "(x OR y) AND x = x \ (x AND y) OR x = x" for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other lemma int_xor_not: "(NOT x) XOR y = NOT (x XOR y) \ x XOR (NOT y) = NOT (x XOR y)" for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemma int_and_assoc: "(x AND y) AND z = x AND (y AND z)" for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemma int_or_assoc: "(x OR y) OR z = x OR (y OR z)" for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemma int_xor_assoc: "(x XOR y) XOR z = x XOR (y XOR z)" for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc (* BH: Why are these declared as simp rules??? *) lemma bbw_lcs [simp]: "y AND (x AND z) = x AND (y AND z)" "y OR (x OR z) = x OR (y OR z)" "y XOR (x XOR z) = x XOR (y XOR z)" for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemma bbw_not_dist: "NOT (x OR y) = (NOT x) AND (NOT y)" "NOT (x AND y) = (NOT x) OR (NOT y)" for x y :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemma bbw_oa_dist: "(x AND y) OR z = (x OR z) AND (y OR z)" for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops) lemma bbw_ao_dist: "(x OR y) AND z = (x AND z) OR (y AND z)" for x y z :: int by (auto simp add: bin_eq_iff bin_nth_ops) subsubsection \Simplification with numerals\ text \Cases for \0\ and \-1\ are already covered by other simp rules.\ lemma bin_rest_neg_numeral_BitM [simp]: "(\k::int. k div 2) (- numeral (Num.BitM w)) = - numeral w" by simp lemma bin_last_neg_numeral_BitM [simp]: "(odd :: int \ bool) (- numeral (Num.BitM w))" by simp subsubsection \Interactions with arithmetic\ lemma le_int_or: "bin_sign y = 0 \ x \ x OR y" for x y :: int by (simp add: bin_sign_def or_greater_eq split: if_splits) lemmas int_and_le = xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] text \Interaction between bit-wise and arithmetic: good example of \bin_induction\.\ lemma bin_add_not: "x + NOT x = (-1::int)" by (simp add: not_int_def) lemma AND_mod: "x AND (2 ^ n - 1) = x mod 2 ^ n" for x :: int by (simp flip: take_bit_eq_mod add: take_bit_eq_mask mask_eq_exp_minus_1) subsubsection \Truncating results of bit-wise operations\ lemma bin_trunc_ao: "(take_bit :: nat \ int \ int) n x AND (take_bit :: nat \ int \ int) n y = (take_bit :: nat \ int \ int) n (x AND y)" "(take_bit :: nat \ int \ int) n x OR (take_bit :: nat \ int \ int) n y = (take_bit :: nat \ int \ int) n (x OR y)" by simp_all lemma bin_trunc_xor: "(take_bit :: nat \ int \ int) n ((take_bit :: nat \ int \ int) n x XOR (take_bit :: nat \ int \ int) n y) = (take_bit :: nat \ int \ int) n (x XOR y)" by simp lemma bin_trunc_not: "(take_bit :: nat \ int \ int) n (NOT ((take_bit :: nat \ int \ int) n x)) = (take_bit :: nat \ int \ int) n (NOT x)" by (fact take_bit_not_take_bit) text \Want theorems of the form of \bin_trunc_xor\.\ lemma bintr_bintr_i: "x = (take_bit :: nat \ int \ int) n y \ (take_bit :: nat \ int \ int) n x = (take_bit :: nat \ int \ int) n y" by auto lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i] lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i] subsubsection \More lemmas\ lemma not_int_cmp_0 [simp]: fixes i :: int shows "0 < NOT i \ i < -1" "0 \ NOT i \ i < 0" "NOT i < 0 \ i \ 0" "NOT i \ 0 \ i \ -1" by(simp_all add: int_not_def) arith+ lemma bbw_ao_dist2: "(x :: int) AND (y OR z) = x AND y OR x AND z" by (fact bit.conj_disj_distrib) lemmas int_and_ac = bbw_lcs(1) int_and_comm int_and_assoc lemma int_nand_same [simp]: fixes x :: int shows "x AND NOT x = 0" by simp lemma int_nand_same_middle: fixes x :: int shows "x AND y AND NOT x = 0" by (simp add: bit_eq_iff bit_and_iff bit_not_iff) lemma and_xor_dist: fixes x :: int shows "x AND (y XOR z) = (x AND y) XOR (x AND z)" by (fact bit.conj_xor_distrib) lemma int_and_lt0 [simp]: \x AND y < 0 \ x < 0 \ y < 0\ for x y :: int by (fact and_negative_int_iff) lemma int_and_ge0 [simp]: \x AND y \ 0 \ x \ 0 \ y \ 0\ for x y :: int by (fact and_nonnegative_int_iff) lemma int_and_1: fixes x :: int shows "x AND 1 = x mod 2" by (fact and_one_eq) lemma int_1_and: fixes x :: int shows "1 AND x = x mod 2" by (fact one_and_eq) lemma int_or_lt0 [simp]: \x OR y < 0 \ x < 0 \ y < 0\ for x y :: int by (fact or_negative_int_iff) lemma int_or_ge0 [simp]: \x OR y \ 0 \ x \ 0 \ y \ 0\ for x y :: int by (fact or_nonnegative_int_iff) lemma int_xor_lt0 [simp]: \x XOR y < 0 \ (x < 0) \ (y < 0)\ for x y :: int by (fact xor_negative_int_iff) lemma int_xor_ge0 [simp]: \x XOR y \ 0 \ (x \ 0 \ y \ 0)\ for x y :: int by (fact xor_nonnegative_int_iff) lemma even_conv_AND: \even i \ i AND 1 = 0\ for i :: int by (simp add: and_one_eq mod2_eq_if) lemma bin_last_conv_AND: "(odd :: int \ bool) i \ i AND 1 \ 0" by (simp add: and_one_eq mod2_eq_if) lemma bitval_bin_last: "of_bool ((odd :: int \ bool) i) = i AND 1" by (simp add: and_one_eq mod2_eq_if) lemma bin_sign_and: "bin_sign (i AND j) = - (bin_sign i * bin_sign j)" by(simp add: bin_sign_def) lemma int_not_neg_numeral: "NOT (- numeral n) = (Num.sub n num.One :: int)" by(simp add: int_not_def) lemma int_neg_numeral_pOne_conv_not: "- numeral (n + num.One) = (NOT (numeral n) :: int)" by(simp add: int_not_def) subsection \Setting and clearing bits\ lemma int_shiftl_BIT: fixes x :: int shows int_shiftl0: "push_bit 0 x = x" and int_shiftl_Suc: "push_bit (Suc n) x = 2 * push_bit n x" by (auto simp add: shiftl_int_def) lemma int_0_shiftl: "push_bit n 0 = (0 :: int)" by (fact push_bit_of_0) lemma bin_last_shiftl: "odd (push_bit n x) \ n = 0 \ (odd :: int \ bool) x" by simp lemma bin_rest_shiftl: "(\k::int. k div 2) (push_bit n x) = (if n > 0 then push_bit (n - 1) x else (\k::int. k div 2) x)" by (cases n) (simp_all add: push_bit_eq_mult) lemma bin_nth_shiftl: "(bit :: int \ nat \ bool) (push_bit n x) m \ n \ m \ (bit :: int \ nat \ bool) x (m - n)" by (fact bit_push_bit_iff_int) lemma bin_last_shiftr: "odd (drop_bit n x) \ bit x n" for x :: int by (simp add: bit_iff_odd_drop_bit) lemma bin_rest_shiftr: "(\k::int. k div 2) (drop_bit n x) = drop_bit (Suc n) x" by (simp add: drop_bit_Suc drop_bit_half) lemma bin_nth_shiftr: "(bit :: int \ nat \ bool) (drop_bit n x) m = (bit :: int \ nat \ bool) x (n + m)" by (simp add: bit_simps) lemma bin_nth_conv_AND: fixes x :: int shows "(bit :: int \ nat \ bool) x n \ x AND (push_bit n 1) \ 0" by (fact bit_iff_and_push_bit_not_eq_0) lemma int_shiftl_numeral [simp]: "push_bit (numeral w') (numeral w :: int) = push_bit (pred_numeral w') (numeral (num.Bit0 w))" "push_bit (numeral w') (- numeral w :: int) = push_bit (pred_numeral w') (- numeral (num.Bit0 w))" by(simp_all add: numeral_eq_Suc shiftl_int_def) (metis add_One mult_inc semiring_norm(11) semiring_norm(13) semiring_norm(2) semiring_norm(6) semiring_norm(87))+ lemma int_shiftl_One_numeral [simp]: "push_bit (numeral w) (1::int) = push_bit (pred_numeral w) 2" using int_shiftl_numeral [of Num.One w] by (simp only: numeral_eq_Suc push_bit_Suc) simp lemma shiftl_ge_0: fixes i :: int shows "push_bit n i \ 0 \ i \ 0" by (fact push_bit_nonnegative_int_iff) lemma shiftl_lt_0: fixes i :: int shows "push_bit n i < 0 \ i < 0" by (fact push_bit_negative_int_iff) lemma int_shiftl_test_bit: "bit (push_bit i n :: int) m \ m \ i \ bit n (m - i)" by (fact bit_push_bit_iff_int) lemma int_0shiftr: "drop_bit x (0 :: int) = 0" by (fact drop_bit_of_0) lemma int_minus1_shiftr: "drop_bit x (-1 :: int) = -1" by (fact drop_bit_minus_one) lemma int_shiftr_ge_0: fixes i :: int shows "drop_bit n i \ 0 \ i \ 0" by (fact drop_bit_nonnegative_int_iff) lemma int_shiftr_lt_0 [simp]: fixes i :: int shows "drop_bit n i < 0 \ i < 0" by (fact drop_bit_negative_int_iff) lemma int_shiftr_numeral [simp]: "drop_bit (numeral w') (1 :: int) = 0" "drop_bit (numeral w') (numeral num.One :: int) = 0" "drop_bit (numeral w') (numeral (num.Bit0 w) :: int) = drop_bit (pred_numeral w') (numeral w)" "drop_bit (numeral w') (numeral (num.Bit1 w) :: int) = drop_bit (pred_numeral w') (numeral w)" "drop_bit (numeral w') (- numeral (num.Bit0 w) :: int) = drop_bit (pred_numeral w') (- numeral w)" "drop_bit (numeral w') (- numeral (num.Bit1 w) :: int) = drop_bit (pred_numeral w') (- numeral (Num.inc w))" by (simp_all add: numeral_eq_Suc add_One drop_bit_Suc) lemma int_shiftr_numeral_Suc0 [simp]: "drop_bit (Suc 0) (1 :: int) = 0" "drop_bit (Suc 0) (numeral num.One :: int) = 0" "drop_bit (Suc 0) (numeral (num.Bit0 w) :: int) = numeral w" "drop_bit (Suc 0) (numeral (num.Bit1 w) :: int) = numeral w" "drop_bit (Suc 0) (- numeral (num.Bit0 w) :: int) = - numeral w" "drop_bit (Suc 0) (- numeral (num.Bit1 w) :: int) = - numeral (Num.inc w)" by (simp_all add: drop_bit_Suc add_One) lemma bin_nth_minus_p2: assumes sign: "bin_sign x = 0" and y: "y = push_bit n 1" and m: "m < n" and x: "x < y" shows "bit (x - y) m = bit x m" proof - from sign y x have \x \ 0\ and \y = 2 ^ n\ and \x < 2 ^ n\ by (simp_all add: bin_sign_def push_bit_eq_mult split: if_splits) from \0 \ x\ \x < 2 ^ n\ \m < n\ have \bit x m \ bit (x - 2 ^ n) m\ proof (induction m arbitrary: x n) case 0 then show ?case by simp next case (Suc m) moreover define q where \q = n - 1\ ultimately have n: \n = Suc q\ by simp have \(x - 2 ^ Suc q) div 2 = x div 2 - 2 ^ q\ by simp moreover from Suc.IH [of \x div 2\ q] Suc.prems have \bit (x div 2) m \ bit (x div 2 - 2 ^ q) m\ by (simp add: n) ultimately show ?case by (simp add: bit_Suc n) qed with \y = 2 ^ n\ show ?thesis by simp qed lemma bin_clr_conv_NAND: "bin_sc n False i = i AND NOT (push_bit n 1)" by (rule bit_eqI) (auto simp add: bin_sc_eq bit_simps) lemma bin_set_conv_OR: "bin_sc n True i = i OR (push_bit n 1)" by (rule bit_eqI) (auto simp add: bin_sc_eq bit_simps) end subsection \More lemmas on words\ lemma msb_conv_bin_sign: "msb x \ bin_sign x = -1" by (simp add: bin_sign_def not_le msb_int_def) lemma msb_bin_sc: "msb (bin_sc n b x) \ msb x" by (simp add: msb_conv_bin_sign) lemma msb_word_def: \msb a \ bin_sign (signed_take_bit (LENGTH('a) - 1) (uint a)) = - 1\ for a :: \'a::len word\ by (simp add: bin_sign_def bit_simps msb_word_iff_bit) lemma word_msb_def: "msb a \ bin_sign (sint a) = - 1" by (simp add: msb_word_def sint_uint) lemma word_rcat_eq: \word_rcat ws = word_of_int (bin_rcat (LENGTH('a::len)) (map uint ws))\ for ws :: \'a::len word list\ apply (simp add: word_rcat_def bin_rcat_def rev_map) apply transfer apply (simp add: horner_sum_foldr foldr_map comp_def) done lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0" by (simp add: sign_Pls_ge_0) lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or \ \following definitions require both arithmetic and bit-wise word operations\ \ \to get \word_no_log_defs\ from \word_log_defs\, using \bin_log_bintrs\\ lemmas wils1 = bin_log_bintrs [THEN word_of_int_eq_iff [THEN iffD2], folded uint_word_of_int_eq, THEN eq_reflection] \ \the binary operations only\ (* BH: why is this needed? *) lemmas word_log_binary_defs = word_and_def word_or_def word_xor_def lemma setBit_no: "Bit_Operations.set_bit n (numeral bin) = word_of_int (bin_sc n True (numeral bin))" by (rule bit_word_eqI) (simp add: bit_simps) lemma clearBit_no: "unset_bit n (numeral bin) = word_of_int (bin_sc n False (numeral bin))" by (rule bit_word_eqI) (simp add: bit_simps) lemma eq_mod_iff: "0 < n \ b = b mod n \ 0 \ b \ b < n" for b n :: int by auto (metis pos_mod_conj)+ lemma split_uint_lem: "bin_split n (uint w) = (a, b) \ a = take_bit (LENGTH('a) - n) a \ b = take_bit (LENGTH('a)) b" for w :: "'a::len word" by transfer (simp add: drop_bit_take_bit ac_simps) \ \limited hom result\ lemma word_cat_hom: "LENGTH('a::len) \ LENGTH('b::len) + LENGTH('c::len) \ (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = word_of_int ((\k n l. concat_bit n l k) w (size b) (uint b))" by transfer (simp add: take_bit_concat_bit_eq) lemma bintrunc_shiftl: "take_bit n (push_bit i m) = push_bit i (take_bit (n - i) m)" for m :: int by (fact take_bit_push_bit) lemma uint_shiftl: "uint (push_bit i n) = take_bit (size n) (push_bit i (uint n))" by (simp add: unsigned_push_bit_eq word_size) lemma bin_mask_conv_pow2: "mask n = 2 ^ n - (1 :: int)" by (fact mask_eq_exp_minus_1) lemma bin_mask_ge0: "mask n \ (0 :: int)" by (fact mask_nonnegative_int) context includes bit_operations_syntax begin lemma and_bin_mask_conv_mod: "x AND mask n = x mod 2 ^ n" for x :: int by (simp flip: take_bit_eq_mod add: take_bit_eq_mask) end lemma bin_mask_numeral: "mask (numeral n) = (1 :: int) + 2 * mask (pred_numeral n)" by (fact mask_numeral) lemma bin_nth_mask: "bit (mask n :: int) i \ i < n" by (simp add: bit_mask_iff) lemma bin_sign_mask [simp]: "bin_sign (mask n) = 0" by (simp add: bin_sign_def bin_mask_conv_pow2) lemma bin_mask_p1_conv_shift: "mask n + 1 = push_bit n (1 :: int)" by (simp add: bin_mask_conv_pow2 shiftl_int_def) lemma sbintrunc_eq_in_range: "((signed_take_bit :: nat \ int \ int) n x = x) = (x \ range ((signed_take_bit :: nat \ int \ int) n))" "(x = (signed_take_bit :: nat \ int \ int) n x) = (x \ range ((signed_take_bit :: nat \ int \ int) n))" apply (simp_all add: image_def) apply (metis sbintrunc_sbintrunc)+ done lemma sbintrunc_If: "- 3 * (2 ^ n) \ x \ x < 3 * (2 ^ n) \ (signed_take_bit :: nat \ int \ int) n x = (if x < - (2 ^ n) then x + 2 * (2 ^ n) else if x \ 2 ^ n then x - 2 * (2 ^ n) else x)" apply (simp add: no_sbintr_alt2, safe) apply (simp add: mod_pos_geq) apply (subst mod_add_self1[symmetric], simp) done lemma sint_range': \- (2 ^ (LENGTH('a) - Suc 0)) \ sint x \ sint x < 2 ^ (LENGTH('a) - Suc 0)\ for x :: \'a::len word\ apply transfer using sbintr_ge sbintr_lt apply auto done lemma signed_arith_eq_checks_to_ord: "(sint a + sint b = sint (a + b )) = ((a <=s a + b) = (0 <=s b))" "(sint a - sint b = sint (a - b )) = ((0 <=s a - b) = (b <=s a))" "(- sint a = sint (- a)) = (0 <=s (- a) = (a <=s 0))" using sint_range'[where x=a] sint_range'[where x=b] by (simp_all add: sint_word_ariths word_sle_eq word_sless_alt sbintrunc_If) lemma signed_mult_eq_checks_double_size: assumes mult_le: "(2 ^ (len_of TYPE ('a) - 1) + 1) ^ 2 \ (2 :: int) ^ (len_of TYPE ('b) - 1)" and le: "2 ^ (LENGTH('a) - 1) \ (2 :: int) ^ (len_of TYPE ('b) - 1)" shows "(sint (a :: 'a :: len word) * sint b = sint (a * b)) = (scast a * scast b = (scast (a * b) :: 'b :: len word))" proof - have P: "(signed_take_bit :: nat \ int \ int) (size a - 1) (sint a * sint b) \ range ((signed_take_bit :: nat \ int \ int) (size a - 1))" by simp have abs: "!! x :: 'a word. abs (sint x) < 2 ^ (size a - 1) + 1" apply (cut_tac x=x in sint_range') apply (simp add: abs_le_iff word_size) done have abs_ab: "abs (sint a * sint b) < 2 ^ (LENGTH('b) - 1)" using abs_mult_less[OF abs[where x=a] abs[where x=b]] mult_le by (simp add: abs_mult power2_eq_square word_size) define r s where \r = LENGTH('a) - 1\ \s = LENGTH('b) - 1\ then have \LENGTH('a) = Suc r\ \LENGTH('b) = Suc s\ \size a = Suc r\ \size b = Suc r\ by (simp_all add: word_size) then show ?thesis using P[unfolded range_sbintrunc] abs_ab le apply clarsimp apply (transfer fixing: r s) apply (auto simp add: signed_take_bit_int_eq_self simp flip: signed_take_bit_eq_iff_take_bit_eq) done qed lemma bintrunc_id: "\m \ int n; 0 < m\ \ take_bit n m = m" by (simp add: take_bit_int_eq_self_iff le_less_trans) lemma bin_cat_cong: "concat_bit n b a = concat_bit m d c" if "n = m" "a = c" "take_bit m b = take_bit m d" using that(3) unfolding that(1,2) by (simp add: bin_cat_eq_push_bit_add_take_bit) lemma bin_cat_eqD1: "concat_bit n b a = concat_bit n d c \ a = c" by (metis drop_bit_bin_cat_eq) lemma bin_cat_eqD2: "concat_bit n b a = concat_bit n d c \ take_bit n b = take_bit n d" by (metis take_bit_bin_cat_eq) lemma bin_cat_inj: "(concat_bit n b a) = concat_bit n d c \ a = c \ take_bit n b = take_bit n d" by (auto intro: bin_cat_cong bin_cat_eqD1 bin_cat_eqD2) +lemma bin_sc_pos: + "0 \ i \ 0 \ bin_sc n b i" + by (metis bin_sign_sc sign_Pls_ge_0) + code_identifier code_module Bits_Int \ (SML) Bit_Operations and (OCaml) Bit_Operations and (Haskell) Bit_Operations and (Scala) Bit_Operations end diff --git a/thys/Word_Lib/Guide.thy b/thys/Word_Lib/Guide.thy --- a/thys/Word_Lib/Guide.thy +++ b/thys/Word_Lib/Guide.thy @@ -1,418 +1,420 @@ (* * Copyright Florian Haftmann * * SPDX-License-Identifier: BSD-2-Clause *) (*<*) theory Guide imports Word_Lib_Sumo Machine_Word_32 Machine_Word_64 Ancient_Numeral begin context semiring_bit_operations begin lemma bit_eq_iff: \a = b \ (\n. 2 ^ n \ 0 \ bit a n \ bit b n)\ using bit_eq_iff [of a b] by (simp add: possible_bit_def) end notation (output) Generic_set_bit.set_bit (\Generic'_set'_bit.set'_bit\) hide_const (open) Generic_set_bit.set_bit no_notation bit (infixl \!!\ 100) (*>*) section \A short overview over bit operations and word types\ subsection \Key principles\ text \ When formalizing bit operations, it is tempting to represent bit values as explicit lists over a binary type. This however is a bad idea, mainly due to the inherent ambiguities in representation concerning repeating leading bits. Hence this approach avoids such explicit lists altogether following an algebraic path: \<^item> Bit values are represented by numeric types: idealized unbounded bit values can be represented by type \<^typ>\int\, bounded bit values by quotient types over \<^typ>\int\, aka \<^typ>\'a word\. \<^item> (A special case are idealized unbounded bit values ending in @{term [source] 0} which can be represented by type \<^typ>\nat\ but only support a restricted set of operations). The fundamental principles are developed in theory \<^theory>\HOL.Bit_Operations\ (which is part of \<^theory>\Main\): \<^item> Multiplication by \<^term>\2 :: int\ is a bit shift to the left and \<^item> Division by \<^term>\2 :: int\ is a bit shift to the right. \<^item> Concerning bounded bit values, iterated shifts to the left may result in eliminating all bits by shifting them all beyond the boundary. The property \<^prop>\(2 :: int) ^ n \ 0\ represents that \<^term>\n\ is \<^emph>\not\ beyond that boundary. \<^item> The projection on a single bit is then @{thm [mode=iff] bit_iff_odd [where ?'a = int, no_vars]}. \<^item> This leads to the most fundamental properties of bit values: \<^item> Equality rule: @{thm [display, mode=iff] bit_eq_iff [where ?'a = int, no_vars]} \<^item> Induction rule: @{thm [display, mode=iff] bits_induct [where ?'a = int, no_vars]} \<^item> Characteristic properties @{prop [source] \bit (f x) n \ P x n\} are available in fact collection \<^text>\bit_simps\. On top of this, the following generic operations are provided: \<^item> Singleton \<^term>\n\th bit: \<^term>\(2 :: int) ^ n\ \<^item> Bit mask upto bit \<^term>\n\: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]} \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]} \<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]} \<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]} \<^item> Bitwise negation: @{thm [mode=iff] bit_not_iff_eq [where ?'a = int, no_vars]} \<^item> Bitwise conjunction: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]} \<^item> Bitwise disjunction: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]} \<^item> Bitwise exclusive disjunction: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]} \<^item> Setting a single bit: @{thm set_bit_def [where ?'a = int, no_vars]} \<^item> Unsetting a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]} \<^item> Flipping a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]} \<^item> Signed truncation, or modulus centered around \<^term>\0::int\: @{thm [display] signed_take_bit_def [where ?'a = int, no_vars]} \<^item> (Bounded) conversion from and to a list of bits: @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} - Bit concatenation on \<^typ>\int\ as given by + Bit concatenation on \<^typ>\int\ as given by @{thm [display] concat_bit_def [no_vars]} appears quite technical but is the logical foundation for the quite natural bit concatenation on \<^typ>\'a word\ (see below). \ subsection \Core word theory\ text \ Proper word types are introduced in theory \<^theory>\HOL-Library.Word\, with the following specific operations: \<^item> Standard arithmetic: @{term \(+) :: 'a::len word \ 'a word \ 'a word\}, @{term \uminus :: 'a::len word \ 'a word\}, @{term \(-) :: 'a::len word \ 'a word \ 'a word\}, @{term \(*) :: 'a::len word \ 'a word \ 'a word\}, @{term \0 :: 'a::len word\}, @{term \1 :: 'a::len word\}, numerals etc. \<^item> Standard bit operations: see above. \<^item> Conversion with unsigned interpretation of words: \<^item> @{term [source] \unsigned :: 'a::len word \ 'b::semiring_1\} \<^item> Important special cases as abbreviations: \<^item> @{term [source] \unat :: 'a::len word \ nat\} \<^item> @{term [source] \uint :: 'a::len word \ int\} \<^item> @{term [source] \ucast :: 'a::len word \ 'b::len word\} \<^item> Conversion with signed interpretation of words: \<^item> @{term [source] \signed :: 'a::len word \ 'b::ring_1\} \<^item> Important special cases as abbreviations: \<^item> @{term [source] \sint :: 'a::len word \ int\} \<^item> @{term [source] \scast :: 'a::len word \ 'b::len word\} \<^item> Operations with unsigned interpretation of words: \<^item> @{thm [mode=iff] word_le_nat_alt [no_vars]} \<^item> @{thm [mode=iff] word_less_nat_alt [no_vars]} \<^item> @{thm unat_div_distrib [no_vars]} \<^item> @{thm unat_drop_bit_eq [no_vars]} \<^item> @{thm unat_mod_distrib [no_vars]} \<^item> @{thm [mode=iff] udvd_iff_dvd [no_vars]} \<^item> Operations with signed interpretation of words: \<^item> @{thm [mode=iff] word_sle_eq [no_vars]} \<^item> @{thm [mode=iff] word_sless_alt [no_vars]} \<^item> @{thm sint_signed_drop_bit_eq [no_vars]} \<^item> Rotation and reversal: \<^item> @{term [source] \word_rotl :: nat \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_rotr :: nat \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_roti :: int \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_reverse :: 'a::len word \ 'a word\} \<^item> Concatenation: @{term [source, display] \word_cat :: 'a::len word \ 'b::len word \ 'c::len word\} For proofs about words the following default strategies are applicable: \<^item> Using bit extensionality (facts \<^text>\bit_eq_iff\, \<^text>\bit_word_eqI\; fact collection \<^text>\bit_simps\). \<^item> Using the @{method transfer} method. \ subsection \More library theories\ text \ Note: currently, most theories listed here are hardly separate entities since they import each other in various ways. Always inspect them to understand what you pull in if you want to import one. \<^descr>[Syntax] \<^descr>[\<^theory>\Word_Lib.Syntax_Bundles\] Bundles to provide alternative syntax for various bit operations. \<^descr>[\<^theory>\Word_Lib.Hex_Words\] Printing word numerals as hexadecimal numerals. \<^descr>[\<^theory>\Word_Lib.Type_Syntax\] Pretty type-sensitive syntax for cast operations. \<^descr>[\<^theory>\Word_Lib.Word_Syntax\] Specific ASCII syntax for prominent bit operations on word. \<^descr>[Proof tools] \<^descr>[\<^theory>\Word_Lib.Norm_Words\] Rewriting word numerals to normal forms. \<^descr>[\<^theory>\Word_Lib.Bitwise\] Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions. \<^descr>[\<^theory>\Word_Lib.Bitwise_Signed\] Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions. \<^descr>[\<^theory>\Word_Lib.Word_EqI\] Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions. \<^descr>[Operations] \<^descr>[\<^theory>\Word_Lib.Signed_Division_Word\] Signed division on word: \<^item> @{term [source] \(sdiv) :: 'a::len word \ 'a word \ 'a word\} \<^item> @{term [source] \(smod) :: 'a::len word \ 'a word \ 'a word\} \<^descr>[\<^theory>\Word_Lib.Aligned\] \ \<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]} \<^descr>[\<^theory>\Word_Lib.Least_significant_bit\] The least significant bit as an alias: @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]} \<^descr>[\<^theory>\Word_Lib.Most_significant_bit\] The most significant bit: \<^item> @{thm [mode=iff] msb_int_def [of k]} \<^item> @{thm [mode=iff] word_msb_sint [no_vars]} \<^item> @{thm [mode=iff] msb_word_iff_sless_0 [no_vars]} \<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]} \<^descr>[\<^theory>\Word_Lib.Bit_Shifts_Infix_Syntax\] Bit shifts decorated with infix syntax: \<^item> @{thm Bit_Shifts_Infix_Syntax.shiftl_def [no_vars]} \<^item> @{thm Bit_Shifts_Infix_Syntax.shiftr_def [no_vars]} \<^item> @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]} \<^descr>[\<^theory>\Word_Lib.Next_and_Prev\] \ \<^item> @{thm word_next_unfold [no_vars]} \<^item> @{thm word_prev_unfold [no_vars]} \<^descr>[\<^theory>\Word_Lib.Enumeration_Word\] More on explicit enumeration of word types. \<^descr>[\<^theory>\Word_Lib.More_Word_Operations\] Even more operations on word. \<^descr>[Types] \<^descr>[\<^theory>\Word_Lib.Signed_Words\] Formal tagging of word types with a \<^text>\signed\ marker. \<^descr>[Lemmas] \<^descr>[\<^theory>\Word_Lib.More_Word\] More lemmas on words. \<^descr>[\<^theory>\Word_Lib.Word_Lemmas\] More lemmas on words, covering many other theories mentioned here. \<^descr>[Words of popular lengths]. \<^descr>[\<^theory>\Word_Lib.Word_8\] for 8-bit words. \<^descr>[\<^theory>\Word_Lib.Word_16\] for 16-bit words. \<^descr>[\<^theory>\Word_Lib.Word_32\] for 32-bit words. \<^descr>[\<^theory>\Word_Lib.Word_64\] - for 64-bit words. + for 64-bit words. This theory is not part of \<^text>\Word_Lib_Sumo\, because it shadows + names from \<^theory>\Word_Lib.Word_32\. They can be used together, but then will have + to use qualified names in applications. \<^descr>[\<^theory>\Word_Lib.Machine_Word_32\ and \<^theory>\Word_Lib.Machine_Word_64\] provide lemmas for 32-bit words and 64-bit words under the same name, which can help to organize applications relying on some form of genericity. \ subsection \More library sessions\ text \ \<^descr>[\<^text>\Native_Word\] Makes machine words and machine arithmetic available for code generation. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. \ subsection \Legacy theories\ text \ The following theories contain material which has been factored out since it is not recommended to use it in new applications, mostly because matters can be expressed succinctly using already existing operations. This section gives some indication how to migrate away from those theories. However theorem coverage may still be terse in some cases. \<^descr>[\<^theory>\Word_Lib.Word_Lib_Sumo\] An entry point importing any relevant theory in that session. Intended for backward compatibility: start importing this theory when migrating applications to Isabelle2021, and later sort out what you really need. You may need to include \<^theory>\Word_Lib.Word_64\ separately. \<^descr>[\<^theory>\Word_Lib.Generic_set_bit\] Kind of an alias: @{thm set_bit_eq [no_vars]} \<^descr>[\<^theory>\Word_Lib.Typedef_Morphisms\] A low-level extension to HOL typedef providing conversions along type morphisms. The @{method transfer} method seems to be sufficient for most applications though. \<^descr>[\<^theory>\Word_Lib.Bit_Comprehension\] Comprehension syntax for bit values over predicates \<^typ>\nat \ bool\. For \<^typ>\'a::len word\, straightforward alternatives exist; difficult to handle for \<^typ>\int\. \<^descr>[\<^theory>\Word_Lib.Reversed_Bit_Lists\] Representation of bit values as explicit list in \<^emph>\reversed\ order. This should rarely be necessary: the \<^const>\bit\ projection should be sufficient in most cases. In case explicit lists are needed, existing operations can be used: @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} \<^descr>[\<^theory>\Word_Lib.Many_More\] Collection of operations and theorems which are kept for backward compatibility and not used in other theories in session \<^text>\Word_Lib\. They are used in applications of \<^text>\Word_Lib\, but should be migrated to there. \ section \Changelog\ text \ \<^descr>[Changes since AFP 2021] ~ - \<^item> Theory \<^theory>\Word_Lib.Ancient_Numeral\ is no part of \<^theory>\Word_Lib.Word_Lib_Sumo\ + \<^item> Theory \<^theory>\Word_Lib.Ancient_Numeral\ is not part of \<^theory>\Word_Lib.Word_Lib_Sumo\ any longer. \<^item> Infix syntax for \<^term>\(AND)\, \<^term>\(OR)\, \<^term>\(XOR)\ organized in syntax bundle \<^bundle>\bit_operations_syntax\. \<^item> Abbreviation \<^abbrev>\max_word\ moved from distribution into theory \<^theory>\Word_Lib.Legacy_Aliases\. \<^item> Operation \<^const>\test_bit\ replaced by input abbreviation \<^abbrev>\test_bit\. \<^item> Abbreviations \<^abbrev>\bin_nth\, \<^abbrev>\bin_last\, \<^abbrev>\bin_rest\, \<^abbrev>\bintrunc\, \<^abbrev>\sbintrunc\, \<^abbrev>\norm_sint\, \<^abbrev>\bin_cat\ moved into theory \<^theory>\Word_Lib.Legacy_Aliases\. \<^item> Operations \<^abbrev>\bshiftr1\, \<^abbrev>\setBit\, \<^abbrev>\clearBit\ moved from distribution into theory \<^theory>\Word_Lib.Legacy_Aliases\ and replaced by input abbreviations. \<^item> Operations \<^const>\shiftl1\, \<^const>\shiftr1\, \<^const>\sshiftr1\ moved here from distribution. \<^item> Operation \<^const>\complement\ replaced by input abbreviation \<^abbrev>\complement\. \ (*<*) end (*>*) diff --git a/thys/Word_Lib/Machine_Word_32.thy b/thys/Word_Lib/Machine_Word_32.thy --- a/thys/Word_Lib/Machine_Word_32.thy +++ b/thys/Word_Lib/Machine_Word_32.thy @@ -1,136 +1,136 @@ (* * Copyright 2014, NICTA * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. * See "LICENSE_BSD2.txt" for details. * * @TAG(NICTA_BSD) *) section "32-Bit Machine Word Setup" theory Machine_Word_32 imports Machine_Word_32_Basics More_Word Bit_Shifts_Infix_Syntax Rsplit begin context includes bit_operations_syntax begin type_synonym machine_word = \machine_word_len word\ lemma word_bits_len_of: \LENGTH(machine_word_len) = word_bits\ - by (simp add: word_bits_conv) + by (simp add: word_bits_conv) lemma word_bits_size: "size (w :: machine_word) = word_bits" by (simp add: word_bits_def word_size) lemma word_bits_word_size_conv: \word_bits = word_size * 8\ by (simp add: word_bits_def word_size_def) lemma word_size_word_size_bits: \word_size = (2 :: 'a :: semiring_1) ^ word_size_bits\ by (simp add: word_size_def word_size_bits_def) lemma lt_word_bits_lt_pow: "sz < word_bits \ sz < 2 ^ word_bits" by (simp add: word_bits_conv) lemma if_then_1_else_0: "((if P then 1 else 0) = (0 :: machine_word)) = (\ P)" by simp lemma if_then_0_else_1: "((if P then 0 else 1) = (0 :: machine_word)) = (P)" by simp lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0 lemma bool_mask [simp]: \0 < x AND 1 \ x AND 1 = 1\ for x :: machine_word by (rule bool_mask') auto lemma in_16_range: "0 \ S \ r \ (\x. r + x * (16 :: machine_word)) ` S" "n - 1 \ S \ (r + (16 * n - 16)) \ (\x :: machine_word. r + x * 16) ` S" by (clarsimp simp: image_def elim!: bexI[rotated])+ lemma le_step_down_word_3: fixes x :: machine_word shows "\x \ y; x \ y\ \ x \ y - 1" by (fact le_step_down_word_2) lemma shiftr_1: "(x::machine_word) >> 1 = 0 \ x < 2" apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_Suc) done lemma Suc_unat_mask_div: "Suc (unat (mask sz div word_size :: machine_word)) = 2 ^ (min sz word_bits - word_size_bits)" by (simp add: word_size_word_size_bits unat_drop_bit_eq unat_mask_eq drop_bit_mask_eq Suc_mask_eq_exp flip: drop_bit_eq_div word_bits_conv) lemma ucast_not_helper: fixes a::"8 word" assumes a: "a \ 0xFF" shows "ucast a \ (0xFF::machine_word)" proof assume "ucast a = (0xFF::machine_word)" also have "(0xFF::machine_word) = ucast (0xFF::8 word)" by simp finally show False using a apply - apply (drule up_ucast_inj, simp) apply simp done qed lemma unat_less_2p_word_bits: "unat (x :: machine_word) < 2 ^ word_bits" apply (simp only: word_bits_def) apply (rule unat_lt2p) done lemma unat_less_word_bits: fixes y :: machine_word shows "x < unat y \ x < 2 ^ word_bits" unfolding word_bits_def by (rule order_less_trans [OF _ unat_lt2p]) lemma unat_mask_2_less_4: "unat (p AND mask 2 :: machine_word) < 4" by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor) lemma unat_mult_simple: \unat (x * y) = unat x * unat y\ if \unat x * unat y < 2 ^ LENGTH(machine_word_len)\ for x y :: machine_word using that by (simp flip: unat_mult_lem) lemma upto_2_helper: "{0..<2 :: machine_word} = {0, 1}" by (safe; simp) unat_arith lemma word_ge_min: \- (2 ^ (word_bits - 1)) \ sint x\ for x :: machine_word using sint_ge [of x] by (simp add: word_bits_def) lemma word_rsplit_0: "word_rsplit (0 :: machine_word) = replicate (word_bits div 8) (0 :: 8 word)" by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq) lemma x_less_2_0_1: fixes x :: machine_word shows "x < 2 \ x = 0 \ x = 1" by (rule x_less_2_0_1') auto end end diff --git a/thys/Word_Lib/Most_significant_bit.thy b/thys/Word_Lib/Most_significant_bit.thy --- a/thys/Word_Lib/Most_significant_bit.thy +++ b/thys/Word_Lib/Most_significant_bit.thy @@ -1,194 +1,194 @@ (* * Copyright Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) (* Author: Jeremy Dawson, NICTA *) section \Dedicated operation for the most significant bit\ theory Most_significant_bit imports "HOL-Library.Word" Bit_Shifts_Infix_Syntax More_Word More_Arithmetic begin class msb = fixes msb :: \'a \ bool\ instantiation int :: msb begin definition \msb x \ x < 0\ for x :: int instance .. end lemma msb_bin_rest [simp]: "msb (x div 2) = msb x" for x :: int by (simp add: msb_int_def) context includes bit_operations_syntax begin lemma int_msb_and [simp]: "msb ((x :: int) AND y) \ msb x \ msb y" by(simp add: msb_int_def) lemma int_msb_or [simp]: "msb ((x :: int) OR y) \ msb x \ msb y" by(simp add: msb_int_def) lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) \ msb x \ msb y" by(simp add: msb_int_def) lemma int_msb_not [simp]: "msb (NOT (x :: int)) \ \ msb x" by(simp add: msb_int_def not_less) end lemma msb_shiftl [simp]: "msb ((x :: int) << n) \ msb x" by (simp add: msb_int_def shiftl_def) lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \ msb x" by (simp add: msb_int_def shiftr_def) lemma msb_0 [simp]: "msb (0 :: int) = False" by(simp add: msb_int_def) lemma msb_1 [simp]: "msb (1 :: int) = False" by(simp add: msb_int_def) lemma msb_numeral [simp]: "msb (numeral n :: int) = False" "msb (- numeral n :: int) = True" by(simp_all add: msb_int_def) instantiation word :: (len) msb begin definition msb_word :: \'a word \ bool\ where msb_word_iff_bit: \msb w \ bit w (LENGTH('a) - Suc 0)\ for w :: \'a::len word\ instance .. end lemma msb_word_eq: \msb w \ bit w (LENGTH('a) - 1)\ for w :: \'a::len word\ by (simp add: msb_word_iff_bit) lemma word_msb_sint: "msb w \ sint w < 0" by (simp add: msb_word_eq bit_last_iff) lemma msb_word_iff_sless_0: \msb w \ w by (simp add: word_msb_sint word_sless_alt) lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bit x (LENGTH('a) - 1)" by (simp add: msb_word_iff_bit bit_simps) lemma word_msb_numeral [simp]: "msb (numeral w::'a::len word) = bit (numeral w :: int) (LENGTH('a) - 1)" unfolding word_numeral_alt by (rule msb_word_of_int) lemma word_msb_neg_numeral [simp]: "msb (- numeral w::'a::len word) = bit (- numeral w :: int) (LENGTH('a) - 1)" unfolding word_neg_numeral_alt by (rule msb_word_of_int) lemma word_msb_0 [simp]: "\ msb (0::'a::len word)" by (simp add: msb_word_iff_bit) lemma word_msb_1 [simp]: "msb (1::'a::len word) \ LENGTH('a) = 1" by (simp add: msb_word_iff_bit le_Suc_eq) lemma word_msb_nth: "msb w = bit (uint w) (LENGTH('a) - 1)" for w :: "'a::len word" by (simp add: msb_word_iff_bit bit_simps) lemma msb_nth: "msb w = bit w (LENGTH('a) - 1)" for w :: "'a::len word" by (fact msb_word_eq) - + lemma word_msb_n1 [simp]: "msb (-1::'a::len word)" by (simp add: msb_word_eq not_le) lemma msb_shift: "msb w \ w >> LENGTH('a) - 1 \ 0" for w :: "'a::len word" by (simp add: drop_bit_eq_zero_iff_not_bit_last msb_word_eq shiftr_def) lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]] lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)" apply (cases \LENGTH('a)\) apply (simp_all add: msb_word_iff_bit word_size) apply transfer apply (simp add: signed_take_bit_eq_take_bit_minus) done lemma word_sle_msb_le: "x <=s y \ (msb y \ msb x) \ ((msb x \ \ msb y) \ x \ y)" apply (simp add: word_sle_eq word_sint_msb_eq word_size word_le_def) apply safe apply (rule order_trans[OF _ uint_ge_0]) apply (simp add: order_less_imp_le) apply (erule notE[OF leD]) apply (rule order_less_le_trans[OF _ uint_ge_0]) apply simp done lemma word_sless_msb_less: "x (msb y \ msb x) \ ((msb x \ \ msb y) \ x < y)" by (auto simp add: word_sless_eq word_sle_msb_le) lemma not_msb_from_less: "(v :: 'a word) < 2 ^ (LENGTH('a :: len) - 1) \ \ msb v" apply (clarsimp simp add: msb_nth) apply (drule less_mask_eq) apply (drule word_eqD, drule(1) iffD2) apply (simp add: bit_simps) done lemma sint_eq_uint: "\ msb x \ sint x = uint x" apply (cases \LENGTH('a)\) apply (simp_all add: msb_word_iff_bit) apply transfer apply (simp add: signed_take_bit_eq_take_bit_minus) done lemma scast_eq_ucast: "\ msb x \ scast x = ucast x" apply (cases \LENGTH('a)\) apply simp apply (rule bit_word_eqI) apply (auto simp add: bit_signed_iff bit_unsigned_iff min_def msb_word_eq) apply (erule notE) apply (metis le_less_Suc_eq test_bit_bin) done lemma msb_ucast_eq: "LENGTH('a) = LENGTH('b) \ msb (ucast x :: ('a::len) word) = msb (x :: ('b::len) word)" by (simp add: msb_word_eq bit_simps) lemma msb_big: \msb a \ 2 ^ (LENGTH('a) - Suc 0) \ a\ for a :: \'a::len word\ using bang_is_le [of a \LENGTH('a) - Suc 0\] apply (auto simp add: msb_nth word_le_not_less) apply (rule ccontr) apply (erule notE) apply (rule ccontr) apply (clarsimp simp: not_less) apply (subgoal_tac "a = take_bit (LENGTH('a) - Suc 0) a") apply (cut_tac and_mask_less' [where w=a and n="LENGTH('a) - Suc 0"]) apply auto apply (simp flip: take_bit_eq_mask) apply (rule sym) apply (simp add: take_bit_eq_self_iff_drop_bit_eq_0 drop_bit_eq_zero_iff_not_bit_last) done end diff --git a/thys/Word_Lib/Signed_Words.thy b/thys/Word_Lib/Signed_Words.thy --- a/thys/Word_Lib/Signed_Words.thy +++ b/thys/Word_Lib/Signed_Words.thy @@ -1,113 +1,113 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Signed Words" theory Signed_Words imports "HOL-Library.Word" begin text \Signed words as separate (isomorphic) word length class. Useful for tagging words in C.\ typedef ('a::len0) signed = "UNIV :: 'a set" .. lemma card_signed [simp]: "CARD (('a::len0) signed) = CARD('a)" unfolding type_definition.card [OF type_definition_signed] by simp instantiation signed :: (len0) len0 begin definition len_signed [simp]: "len_of (x::'a::len0 signed itself) = LENGTH('a)" instance .. end instance signed :: (len) len by (intro_classes, simp) lemma scast_scast_id [simp]: "scast (scast x :: ('a::len) signed word) = (x :: 'a word)" "scast (scast y :: ('a::len) word) = (y :: 'a signed word)" by (auto simp: is_up scast_up_scast_id) lemma ucast_scast_id [simp]: "ucast (scast (x :: 'a::len signed word) :: 'a word) = x" by transfer (simp add: take_bit_signed_take_bit) lemma scast_of_nat [simp]: "scast (of_nat x :: 'a::len signed word) = (of_nat x :: 'a word)" by transfer (simp add: take_bit_signed_take_bit) lemma scast_ucast_id [simp]: "scast (ucast (x :: 'a::len word) :: 'a signed word) = x" - by transfer (simp add: take_bit_signed_take_bit) + by transfer (simp add: take_bit_signed_take_bit) lemma scast_eq_scast_id [simp]: "((scast (a :: 'a::len signed word) :: 'a word) = scast b) = (a = b)" by (metis ucast_scast_id) lemma ucast_eq_ucast_id [simp]: "((ucast (a :: 'a::len word) :: 'a signed word) = ucast b) = (a = b)" by (metis scast_ucast_id) lemma scast_ucast_norm [simp]: "(ucast (a :: 'a::len word) = (b :: 'a signed word)) = (a = scast b)" "((b :: 'a signed word) = ucast (a :: 'a::len word)) = (a = scast b)" by (metis scast_ucast_id ucast_scast_id)+ lemma scast_2_power [simp]: "scast ((2 :: 'a::len signed word) ^ x) = ((2 :: 'a word) ^ x)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma ucast_nat_def': "of_nat (unat x) = (ucast :: 'a :: len word \ ('b :: len) signed word) x" by (fact of_nat_unat) lemma zero_sle_ucast_up: "\ is_down (ucast :: 'a word \ 'b signed word) \ (0 <=s ((ucast (b::('a::len) word)) :: ('b::len) signed word))" by transfer (simp add: bit_simps) lemma word_le_ucast_sless: "\ x \ y; y \ -1; LENGTH('a) < LENGTH('b) \ \ (ucast x :: ('b :: len) signed word) 'a::len word\ apply (cases \LENGTH('b)\) apply simp_all apply transfer apply (simp add: signed_take_bit_take_bit) - apply (metis add.commute mask_eq_exp_minus_1 mask_eq_take_bit_minus_one take_bit_incr_eq zle_add1_eq_le) + apply (metis add.commute mask_eq_exp_minus_1 take_bit_incr_eq zle_add1_eq_le) done lemma zero_sle_ucast: "(0 <=s ((ucast (b::('a::len) word)) :: ('a::len) signed word)) = (uint b < 2 ^ (LENGTH('a) - 1))" apply transfer apply (cases \LENGTH('a)\) apply (simp_all add: take_bit_Suc_from_most bit_simps) apply (simp_all add: bit_simps disjunctive_add) done lemma nth_w2p_scast: "(bit (scast ((2::'a::len signed word) ^ n) :: 'a word) m) \ (bit (((2::'a::len word) ^ n) :: 'a word) m)" by (simp add: bit_simps) lemma scast_nop1 [simp]: "((scast ((of_int x)::('a::len) word))::'a signed word) = of_int x" - by transfer (simp add: take_bit_signed_take_bit) + by transfer (simp add: take_bit_signed_take_bit) lemma scast_nop2 [simp]: "((scast ((of_int x)::('a::len) signed word))::'a word) = of_int x" by transfer (simp add: take_bit_signed_take_bit) lemmas scast_nop = scast_nop1 scast_nop2 scast_id type_synonym 'a sword = "'a signed word" end diff --git a/thys/Word_Lib/Word_EqI.thy b/thys/Word_Lib/Word_EqI.thy --- a/thys/Word_Lib/Word_EqI.thy +++ b/thys/Word_Lib/Word_EqI.thy @@ -1,72 +1,73 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Solving Word Equalities" theory Word_EqI imports More_Word Aligned "HOL-Eisbach.Eisbach_Tools" begin text \ Some word equalities can be solved by considering the problem bitwise for all @{prop "n < LENGTH('a::len)"}, which is different to running @{text word_bitwise} and expanding into an explicit list of bits. \ named_theorems word_eqI_simps lemmas [word_eqI_simps] = word_ops_nth_size + word_ao_nth bit_mask_iff word_size word_or_zero neg_mask_test_bit nth_ucast nth_w2p bit_push_bit_iff bit_drop_bit_eq less_2p_is_upper_bits_unset le_mask_high_bits bang_eq neg_test_bit is_up is_down is_aligned_nth neg_mask_le_high_bits lemmas word_eqI_rule = word_eqI [rule_format] lemma test_bit_lenD: "bit x n \ n < LENGTH('a) \ bit x n" for x :: "'a :: len word" by (fastforce dest: test_bit_size simp: word_size) method word_eqI uses simp simp_del split split_del cong flip = ((* reduce conclusion to test_bit: *) rule word_eqI_rule, (* make sure we're in clarsimp normal form: *) (clarsimp simp: simp simp del: simp_del simp flip: flip split: split split del: split_del cong: cong)?, (* turn x < 2^n assumptions into mask equations: *) ((drule less_mask_eq)+)?, (* expand and distribute test_bit everywhere: *) (clarsimp simp: word_eqI_simps simp simp del: simp_del simp flip: flip split: split split del: split_del cong: cong)?, (* add any additional word size constraints to new indices: *) ((drule test_bit_lenD)+)?, (* try to make progress (can't use +, would loop): *) (clarsimp simp: word_eqI_simps simp simp del: simp_del simp flip: flip split: split split del: split_del cong: cong)?, (* helps sometimes, rarely: *) (simp add: simp test_bit_conj_lt del: simp_del flip: flip split: split split del: split_del cong: cong)?) method word_eqI_solve uses simp simp_del split split_del cong flip = solves \word_eqI simp: simp simp_del: simp_del split: split split_del: split_del cong: cong simp flip: flip; (fastforce dest: test_bit_size simp: word_eqI_simps simp flip: flip simp: simp simp del: simp_del split: split split del: split_del cong: cong)?\ end diff --git a/thys/Word_Lib/Word_Lemmas.thy b/thys/Word_Lib/Word_Lemmas.thy --- a/thys/Word_Lib/Word_Lemmas.thy +++ b/thys/Word_Lib/Word_Lemmas.thy @@ -1,1961 +1,1970 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Lemmas with Generic Word Length" theory Word_Lemmas imports Type_Syntax Signed_Division_Word Signed_Words More_Word Most_significant_bit Enumeration_Word Aligned Bit_Shifts_Infix_Syntax + Word_EqI begin context includes bit_operations_syntax begin lemma ucast_le_ucast_eq: fixes x y :: "'a::len word" assumes x: "x < 2 ^ n" assumes y: "y < 2 ^ n" assumes n: "n = LENGTH('b::len)" shows "(UCAST('a \ 'b) x \ UCAST('a \ 'b) y) = (x \ y)" apply (rule iffI) apply (cases "LENGTH('b) < LENGTH('a)") apply (subst less_mask_eq[OF x, symmetric]) apply (subst less_mask_eq[OF y, symmetric]) apply (unfold n) apply (subst ucast_ucast_mask[symmetric])+ apply (simp add: ucast_le_ucast)+ apply (erule ucast_mono_le[OF _ y[unfolded n]]) done lemma ucast_zero_is_aligned: \is_aligned w n\ if \UCAST('a::len \ 'b::len) w = 0\ \n \ LENGTH('b)\ proof (rule is_aligned_bitI) fix q assume \q < n\ moreover have \bit (UCAST('a::len \ 'b::len) w) q = bit 0 q\ using that by simp with \q < n\ \n \ LENGTH('b)\ show \\ bit w q\ by (simp add: bit_simps) qed lemma unat_ucast_eq_unat_and_mask: "unat (UCAST('b::len \ 'a::len) w) = unat (w AND mask LENGTH('a))" apply (simp flip: take_bit_eq_mask) apply transfer apply (simp add: ac_simps) done lemma le_max_word_ucast_id: \UCAST('b \ 'a) (UCAST('a \ 'b) x) = x\ if \x \ UCAST('b::len \ 'a) (- 1)\ for x :: \'a::len word\ proof - from that have a1: \x \ word_of_int (uint (word_of_int (2 ^ LENGTH('b) - 1) :: 'b word))\ by (simp add: of_int_mask_eq) have f2: "((\i ia. (0::int) \ i \ \ 0 \ i + - 1 * ia \ i mod ia \ i) \ \ (0::int) \ - 1 + 2 ^ LENGTH('b) \ (0::int) \ - 1 + 2 ^ LENGTH('b) + - 1 * 2 ^ LENGTH('b) \ (- (1::int) + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b) = - 1 + 2 ^ LENGTH('b)) = ((\i ia. (0::int) \ i \ \ 0 \ i + - 1 * ia \ i mod ia \ i) \ \ (1::int) \ 2 ^ LENGTH('b) \ 2 ^ LENGTH('b) + - (1::int) * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)) = 1)" by force have f3: "\i ia. \ (0::int) \ i \ 0 \ i + - 1 * ia \ i mod ia = i" using mod_pos_pos_trivial by force have "(1::int) \ 2 ^ LENGTH('b)" by simp then have "2 ^ LENGTH('b) + - (1::int) * ((- 1 + 2 ^ LENGTH('b)) mod 2 ^ len_of TYPE ('b)) = 1" using f3 f2 by blast then have f4: "- (1::int) + 2 ^ LENGTH('b) = (- 1 + 2 ^ LENGTH('b)) mod 2 ^ LENGTH('b)" by linarith have f5: "x \ word_of_int (uint (word_of_int (- 1 + 2 ^ LENGTH('b))::'b word))" using a1 by force have f6: "2 ^ LENGTH('b) + - (1::int) = - 1 + 2 ^ LENGTH('b)" by force have f7: "- (1::int) * 1 = - 1" by auto have "\x0 x1. (x1::int) - x0 = x1 + - 1 * x0" by force then have "x \ 2 ^ LENGTH('b) - 1" using f7 f6 f5 f4 by (metis uint_word_of_int wi_homs(2) word_arith_wis(8) word_of_int_2p) then have \uint x \ uint (2 ^ LENGTH('b) - (1 :: 'a word))\ by (simp add: word_le_def) then have \uint x \ 2 ^ LENGTH('b) - 1\ by (simp add: uint_word_ariths) (metis \1 \ 2 ^ LENGTH('b)\ \uint x \ uint (2 ^ LENGTH('b) - 1)\ linorder_not_less lt2p_lem uint_1 uint_minus_simple_alt uint_power_lower word_le_def zle_diff1_eq) then show ?thesis apply (simp add: unsigned_ucast_eq take_bit_word_eq_self_iff) apply (meson \x \ 2 ^ LENGTH('b) - 1\ not_le word_less_sub_le) done qed lemma uint_shiftr_eq: \uint (w >> n) = uint w div 2 ^ n\ by (rule bit_eqI) (simp flip: drop_bit_eq_div add: bit_simps) lemma bit_shiftl_word_iff [bit_simps]: \bit (w << m) n \ m \ n \ n < LENGTH('a) \ bit w (n - m)\ for w :: \'a::len word\ by (simp add: bit_simps) lemma bit_shiftr_word_iff: \bit (w >> m) n \ bit w (m + n)\ for w :: \'a::len word\ by (simp add: bit_simps) lemma uint_sshiftr_eq: \uint (w >>> n) = take_bit LENGTH('a) (sint w div 2 ^ n)\ for w :: \'a::len word\ by (rule bit_eqI) (auto simp add: bit_simps not_less simp flip: drop_bit_eq_div dest: bit_imp_le_length) lemma sshiftr_0: "0 >>> n = 0" by (simp add: sshiftr_def) - + lemma sshiftr_n1: "-1 >>> n = -1" by (simp add: sshiftr_def) lemma bit_sshiftr_word_iff: \bit (w >>> m) n \ bit w (if LENGTH('a) - m \ n \ n < LENGTH('a) then LENGTH('a) - 1 else (m + n))\ for w :: \'a::len word\ by (fact bit_sshiftr_iff) lemma nth_sshiftr : "bit (w >>> m) n = (n < size w \ (if n + m \ size w then bit w (size w - 1) else bit w (n + m)))" apply (auto simp add: bit_simps word_size ac_simps not_less) apply (meson bit_imp_le_length bit_shiftr_word_iff leD) done lemma sshiftr_numeral: \(numeral k >>> numeral n :: 'a::len word) = word_of_int (signed_take_bit (LENGTH('a) - 1) (numeral k) >> numeral n)\ using signed_drop_bit_word_numeral [of n k] by (simp add: sshiftr_def shiftr_def) lemma sshiftr_div_2n: "sint (w >>> n) = sint w div 2 ^ n" apply (rule bit_eqI) apply (cases \n < LENGTH('a)\) apply (auto simp add: bit_simps not_less le_diff_conv2 simp flip: drop_bit_eq_div) done lemma mask_eq: \mask n = (1 << n) - (1 :: 'a::len word)\ by (simp add: mask_eq_exp_minus_1 shiftl_def) lemma nth_shiftl': "bit (w << m) n \ n < size w \ n >= m \ bit w (n - m)" for w :: "'a::len word" by (simp add: bit_simps word_size ac_simps) lemmas nth_shiftl = nth_shiftl' [unfolded word_size] lemma nth_shiftr: "bit (w >> m) n = bit w (n + m)" for w :: "'a::len word" by (simp add: bit_simps ac_simps) lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n" by (fact uint_shiftr_eq) lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)" by (simp add: shiftl_rev) lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)" by (simp add: rev_shiftl) lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)" by (simp add: shiftr_rev) lemmas ucast_up = rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]] lemmas ucast_down = rc2 [simplified rev_shiftr revcast_ucast [symmetric]] lemma shiftl_zero_size: "size x \ n \ x << n = 0" for x :: "'a::len word" by (simp add: shiftl_def word_size) lemma shiftl_t2n: "shiftl w n = 2 ^ n * w" for w :: "'a::len word" by (simp add: shiftl_def push_bit_eq_mult) lemma word_shift_by_2: "x * 4 = (x::'a::len word) << 2" by (simp add: shiftl_t2n) +lemma word_shift_by_3: + "x * 8 = (x::'a::len word) << 3" + by (simp add: shiftl_t2n) + lemma slice_shiftr: "slice n w = ucast (w >> n)" apply (rule bit_word_eqI) apply (cases \n \ LENGTH('b)\) apply (auto simp add: bit_slice_iff bit_ucast_iff bit_shiftr_word_iff ac_simps dest: bit_imp_le_length) done lemma shiftr_zero_size: "size x \ n \ x >> n = 0" for x :: "'a :: len word" by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size) lemma shiftr_x_0 [simp]: "x >> 0 = x" for x :: "'a::len word" by (simp add: shiftr_def) lemma shiftl_x_0 [simp]: "x << 0 = x" for x :: "'a::len word" by (simp add: shiftl_def) lemma shiftl_1: "(1::'a::len word) << n = 2^n" by (simp add: shiftl_def) lemma shiftr_1 [simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)" by (simp add: shiftr_def) lemma shiftl0: "x << 0 = (x :: 'a :: len word)" by (fact shiftl_x_0) lemma and_not_mask: "w AND NOT (mask n) = (w >> n) << n" for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps) lemma and_mask: "w AND mask n = (w << (size w - n)) >> (size w - n)" for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps word_size) lemma shiftr_div_2n_w: "n < size w \ w >> n = w div (2^n :: 'a :: len word)" apply (unfold word_div_def) apply (simp add: uint_2p_alt word_size) apply (metis uint_shiftr_eq word_of_int_uint) done lemma le_shiftr: "u \ v \ u >> (n :: nat) \ (v :: 'a :: len word) >> n" apply (unfold shiftr_def) apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_eq_div zdiv_mono1) done lemma le_shiftr': "\ u >> n \ v >> n ; u >> n \ v >> n \ \ (u::'a::len word) \ v" apply (metis le_cases le_shiftr verit_la_disequality) done lemma shiftr_mask_le: "n <= m \ mask n >> m = (0 :: 'a::len word)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma shiftr_mask [simp]: \mask m >> m = (0::'a::len word)\ by (rule shiftr_mask_le) simp lemma le_mask_iff: "(w \ mask n) = (w >> n = 0)" for w :: \'a::len word\ apply safe apply (rule word_le_0_iff [THEN iffD1]) apply (rule xtrans(3)) apply (erule_tac [2] le_shiftr) apply simp apply (rule word_leI) apply (rename_tac n') apply (drule_tac x = "n' - n" in word_eqD) apply (simp add : nth_shiftr word_size bit_simps) apply (case_tac "n <= n'") by auto lemma and_mask_eq_iff_shiftr_0: "(w AND mask n = w) = (w >> n = 0)" for w :: \'a::len word\ by (simp flip: take_bit_eq_mask add: shiftr_def take_bit_eq_self_iff_drop_bit_eq_0) lemma mask_shiftl_decompose: "mask m << n = mask (m + n) AND NOT (mask n :: 'a::len word)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma shiftl_over_and_dist: fixes a::"'a::len word" shows "(a AND b) << c = (a << c) AND (b << c)" by (unfold shiftl_def) (fact push_bit_and) lemma shiftr_over_and_dist: fixes a::"'a::len word" shows "a AND b >> c = (a >> c) AND (b >> c)" by (unfold shiftr_def) (fact drop_bit_and) lemma sshiftr_over_and_dist: fixes a::"'a::len word" shows "a AND b >>> c = (a >>> c) AND (b >>> c)" apply(rule word_eqI) apply(simp add:nth_sshiftr word_ao_nth word_size) done lemma shiftl_over_or_dist: fixes a::"'a::len word" shows "a OR b << c = (a << c) OR (b << c)" by (unfold shiftl_def) (fact push_bit_or) lemma shiftr_over_or_dist: fixes a::"'a::len word" shows "a OR b >> c = (a >> c) OR (b >> c)" by (unfold shiftr_def) (fact drop_bit_or) lemma sshiftr_over_or_dist: fixes a::"'a::len word" shows "a OR b >>> c = (a >>> c) OR (b >>> c)" by (rule bit_word_eqI) (simp add: bit_simps) lemmas shift_over_ao_dists = shiftl_over_or_dist shiftr_over_or_dist sshiftr_over_or_dist shiftl_over_and_dist shiftr_over_and_dist sshiftr_over_and_dist lemma shiftl_shiftl: fixes a::"'a::len word" shows "a << b << c = a << (b + c)" apply(rule word_eqI) apply(auto simp:word_size nth_shiftl add.commute add.left_commute) done lemma shiftr_shiftr: fixes a::"'a::len word" shows "a >> b >> c = a >> (b + c)" apply(rule word_eqI) apply(simp add:word_size nth_shiftr add.left_commute add.commute) done lemma shiftl_shiftr1: fixes a::"'a::len word" shows "c \ b \ a << b >> c = a AND (mask (size a - b)) << (b - c)" apply (rule word_eqI) apply (auto simp add: bit_simps not_le word_size ac_simps) done lemma shiftl_shiftr2: fixes a::"'a::len word" shows "b < c \ a << b >> c = (a >> (c - b)) AND (mask (size a - c))" apply(rule word_eqI) apply(auto simp:nth_shiftr nth_shiftl word_size word_ao_nth bit_simps) done lemma shiftr_shiftl1: fixes a::"'a::len word" shows "c \ b \ a >> b << c = (a >> (b - c)) AND (NOT (mask c))" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma shiftr_shiftl2: fixes a::"'a::len word" shows "b < c \ a >> b << c = (a << (c - b)) AND (NOT (mask c))" apply (rule word_eqI) apply (auto simp add: bit_simps not_le word_size ac_simps) done lemmas multi_shift_simps = shiftl_shiftl shiftr_shiftr shiftl_shiftr1 shiftl_shiftr2 shiftr_shiftl1 shiftr_shiftl2 lemma shiftr_mask2: "n \ LENGTH('a) \ (mask n >> m :: ('a :: len) word) = mask (n - m)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma word_shiftl_add_distrib: fixes x :: "'a :: len word" shows "(x + y) << n = (x << n) + (y << n)" by (simp add: shiftl_t2n ring_distribs) lemma mask_shift: "(x AND NOT (mask y)) >> y = x >> y" for x :: \'a::len word\ apply (rule bit_eqI) apply (simp add: bit_and_iff bit_not_iff bit_shiftr_word_iff bit_mask_iff not_le) using bit_imp_le_length apply auto done lemma shiftr_div_2n': "unat (w >> n) = unat w div 2 ^ n" apply (unfold unat_eq_nat_uint) apply (subst shiftr_div_2n) apply (subst nat_div_distrib) apply simp apply (simp add: nat_power_eq) done lemma shiftl_shiftr_id: assumes nv: "n < LENGTH('a)" and xv: "x < 2 ^ (LENGTH('a) - n)" shows "x << n >> n = (x::'a::len word)" apply (simp add: shiftl_t2n) apply (rule word_eq_unatI) apply (subst shiftr_div_2n') apply (cases n) apply simp apply (subst iffD1 [OF unat_mult_lem])+ apply (subst unat_power_lower[OF nv]) apply (rule nat_less_power_trans [OF _ order_less_imp_le [OF nv]]) apply (rule order_less_le_trans [OF unat_mono [OF xv] order_eq_refl]) apply (rule unat_power_lower) apply simp apply (subst unat_power_lower[OF nv]) apply simp done lemma ucast_shiftl_eq_0: fixes w :: "'a :: len word" shows "\ n \ LENGTH('b) \ \ ucast (w << n) = (0 :: 'b :: len word)" by (transfer fixing: n) (simp add: take_bit_push_bit) lemma word_shift_nonzero: "\ (x::'a::len word) \ 2 ^ m; m + n < LENGTH('a::len); x \ 0\ \ x << n \ 0" apply (simp only: word_neq_0_conv word_less_nat_alt shiftl_t2n mod_0 unat_word_ariths unat_power_lower word_le_nat_alt) apply (subst mod_less) apply (rule order_le_less_trans) apply (erule mult_le_mono2) apply (subst power_add[symmetric]) apply (rule power_strict_increasing) apply simp apply simp apply simp done lemma word_shiftr_lt: fixes w :: "'a::len word" shows "unat (w >> n) < (2 ^ (LENGTH('a) - n))" apply (subst shiftr_div_2n') apply transfer apply (simp flip: drop_bit_eq_div add: drop_bit_nat_eq drop_bit_take_bit) done lemma shiftr_less_t2n': "\ x AND mask (n + m) = x; m < LENGTH('a) \ \ x >> n < 2 ^ m" for x :: "'a :: len word" apply (simp add: word_size mask_eq_iff_w2p [symmetric] flip: take_bit_eq_mask) apply transfer apply (simp add: take_bit_drop_bit ac_simps) done lemma shiftr_less_t2n: "x < 2 ^ (n + m) \ x >> n < 2 ^ m" for x :: "'a :: len word" apply (rule shiftr_less_t2n') apply (erule less_mask_eq) apply (rule ccontr) apply (simp add: not_less) apply (subst (asm) p2_eq_0[symmetric]) apply (simp add: power_add) done lemma shiftr_eq_0: "n \ LENGTH('a) \ ((w::'a::len word) >> n) = 0" apply (cut_tac shiftr_less_t2n'[of w n 0], simp) apply (simp add: mask_eq_iff) apply (simp add: lt2p_lem) apply simp done lemma shiftl_less_t2n: fixes x :: "'a :: len word" shows "\ x < (2 ^ (m - n)); m < LENGTH('a) \ \ (x << n) < 2 ^ m" apply (simp add: word_size mask_eq_iff_w2p [symmetric] flip: take_bit_eq_mask) apply transfer apply (simp add: take_bit_push_bit) done lemma shiftl_less_t2n': "(x::'a::len word) < 2 ^ m \ m+n < LENGTH('a) \ x << n < 2 ^ (m + n)" by (rule shiftl_less_t2n) simp_all lemma scast_bit_test [simp]: "scast ((1 :: 'a::len signed word) << n) = (1 :: 'a word) << n" by (rule bit_word_eqI) (simp add: bit_simps) lemma signed_shift_guard_to_word: \unat x * 2 ^ y < 2 ^ n \ x = 0 \ x < 1 << n >> y\ if \n < LENGTH('a)\ \0 < n\ for x :: \'a::len word\ proof (cases \x = 0\) case True then show ?thesis by simp next case False then have \unat x \ 0\ by (simp add: unat_eq_0) then have \unat x \ 1\ by simp show ?thesis proof (cases \y < n\) case False then have \n \ y\ by simp then obtain q where \y = n + q\ using le_Suc_ex by blast moreover have \(2 :: nat) ^ n >> n + q \ 1\ by (simp add: drop_bit_eq_div power_add shiftr_def) ultimately show ?thesis using \x \ 0\ \unat x \ 1\ \n < LENGTH('a)\ by (simp add: power_add not_less word_le_nat_alt unat_drop_bit_eq shiftr_def shiftl_def) next case True with that have \y < LENGTH('a)\ by simp show ?thesis proof (cases \2 ^ n = unat x * 2 ^ y\) case True moreover have \unat x * 2 ^ y < 2 ^ LENGTH('a)\ using \n < LENGTH('a)\ by (simp flip: True) moreover have \(word_of_nat (2 ^ n) :: 'a word) = word_of_nat (unat x * 2 ^ y)\ using True by simp then have \2 ^ n = x * 2 ^ y\ by simp ultimately show ?thesis using \y < LENGTH('a)\ by (auto simp add: drop_bit_eq_div word_less_nat_alt unat_div unat_word_ariths shiftr_def shiftl_def) next case False with \y < n\ have *: \unat x \ 2 ^ n div 2 ^ y\ by (auto simp flip: power_sub power_add) have \unat x * 2 ^ y < 2 ^ n \ unat x * 2 ^ y \ 2 ^ n\ using False by (simp add: less_le) also have \\ \ unat x \ 2 ^ n div 2 ^ y\ by (simp add: less_eq_div_iff_mult_less_eq) also have \\ \ unat x < 2 ^ n div 2 ^ y\ using * by (simp add: less_le) finally show ?thesis using that \x \ 0\ by (simp flip: push_bit_eq_mult drop_bit_eq_div add: shiftr_def shiftl_def unat_drop_bit_eq word_less_iff_unsigned [where ?'a = nat]) qed qed qed lemma shiftr_not_mask_0: "n+m \ LENGTH('a :: len) \ ((w::'a::len word) >> n) AND NOT (mask m) = 0" by (rule bit_word_eqI) (auto simp add: bit_simps word_size dest: bit_imp_le_length) lemma shiftl_mask_is_0[simp]: "(x << n) AND mask n = 0" for x :: \'a::len word\ by (simp flip: take_bit_eq_mask add: take_bit_push_bit shiftl_def) lemma rshift_sub_mask_eq: "(a >> (size a - b)) AND mask b = a >> (size a - b)" for a :: \'a::len word\ using shiftl_shiftr2[where a=a and b=0 and c="size a - b"] apply (cases "b < size a") apply simp apply (simp add: linorder_not_less mask_eq_decr_exp word_size p2_eq_0[THEN iffD2]) done lemma shiftl_shiftr3: "b \ c \ a << b >> c = (a >> c - b) AND mask (size a - c)" for a :: \'a::len word\ apply (cases "b = c") apply (simp add: shiftl_shiftr1) apply (simp add: shiftl_shiftr2) done lemma and_mask_shiftr_comm: "m \ size w \ (w AND mask m) >> n = (w >> n) AND mask (m-n)" for w :: \'a::len word\ by (simp add: and_mask shiftr_shiftr) (simp add: word_size shiftl_shiftr3) lemma and_mask_shiftl_comm: "m+n \ size w \ (w AND mask m) << n = (w << n) AND mask (m+n)" for w :: \'a::len word\ by (simp add: and_mask word_size shiftl_shiftl) (simp add: shiftl_shiftr1) lemma le_mask_shiftl_le_mask: "s = m + n \ x \ mask n \ x << m \ mask s" for x :: \'a::len word\ by (simp add: le_mask_iff shiftl_shiftr3) lemma word_and_1_shiftl: "x AND (1 << n) = (if bit x n then (1 << n) else 0)" for x :: "'a :: len word" apply (rule bit_word_eqI; transfer) apply (auto simp add: bit_simps not_le ac_simps) done lemmas word_and_1_shiftls' = word_and_1_shiftl[where n=0] word_and_1_shiftl[where n=1] word_and_1_shiftl[where n=2] lemmas word_and_1_shiftls = word_and_1_shiftls' [simplified] lemma word_and_mask_shiftl: "x AND (mask n << m) = ((x >> m) AND mask n) << m" for x :: \'a::len word\ apply (rule bit_word_eqI; transfer) apply (auto simp add: bit_simps not_le ac_simps) done lemma shift_times_fold: "(x :: 'a :: len word) * (2 ^ n) << m = x << (m + n)" by (simp add: shiftl_t2n ac_simps power_add) lemma of_bool_nth: "of_bool (bit x v) = (x >> v) AND 1" for x :: \'a::len word\ by (simp add: bit_iff_odd_drop_bit word_and_1 shiftr_def) lemma shiftr_mask_eq: "(x >> n) AND mask (size x - n) = x >> n" for x :: "'a :: len word" apply (simp flip: take_bit_eq_mask) apply transfer apply (simp add: take_bit_drop_bit) done lemma shiftr_mask_eq': "m = (size x - n) \ (x >> n) AND mask m = x >> n" for x :: "'a :: len word" by (simp add: shiftr_mask_eq) lemma and_eq_0_is_nth: fixes x :: "'a :: len word" shows "y = 1 << n \ ((x AND y) = 0) = (\ (bit x n))" by (simp add: and_exp_eq_0_iff_not_bit shiftl_def) lemma word_shift_zero: "\ x << n = 0; x \ 2^m; m + n < LENGTH('a)\ \ (x::'a::len word) = 0" apply (rule ccontr) apply (drule (2) word_shift_nonzero) apply simp done lemma mask_shift_and_negate[simp]:"(w AND mask n << m) AND NOT (mask n << m) = 0" for w :: \'a::len word\ by (rule bit_word_eqI) (simp add: bit_simps) (* The seL4 bitfield generator produces functions containing mask and shift operations, such that * invoking two of them consecutively can produce something like the following. *) lemma bitfield_op_twice: "(x AND NOT (mask n << m) OR ((y AND mask n) << m)) AND NOT (mask n << m) = x AND NOT (mask n << m)" for x :: \'a::len word\ by (induct n arbitrary: m) (auto simp: word_ao_dist) lemma bitfield_op_twice'': "\NOT a = b << c; \x. b = mask x\ \ (x AND a OR (y AND b << c)) AND a = x AND a" for a b :: \'a::len word\ apply clarsimp apply (cut_tac n=xa and m=c and x=x and y=y in bitfield_op_twice) apply (clarsimp simp:mask_eq_decr_exp) apply (drule not_switch) apply clarsimp done lemma shiftr1_unfold: "x div 2 = x >> 1" by (simp add: drop_bit_eq_div shiftr_def) lemma shiftr1_is_div_2: "(x::('a::len) word) >> 1 = x div 2" by (simp add: drop_bit_eq_div shiftr_def) lemma shiftl1_is_mult: "(x << 1) = (x :: 'a::len word) * 2" by (metis One_nat_def mult_2 mult_2_right one_add_one power_0 power_Suc shiftl_t2n) lemma shiftr1_lt:"x \ 0 \ (x::('a::len) word) >> 1 < x" apply (subst shiftr1_is_div_2) apply (rule div_less_dividend_word) apply simp+ done lemma shiftr1_0_or_1:"(x::('a::len) word) >> 1 = 0 \ x = 0 \ x = 1" apply (subst (asm) shiftr1_is_div_2) apply (drule word_less_div) apply (case_tac "LENGTH('a) = 1") apply (simp add:degenerate_word) apply (erule disjE) apply (subgoal_tac "(2::'a word) \ 0") apply simp apply (rule not_degenerate_imp_2_neq_0) apply (subgoal_tac "LENGTH('a) \ 0") apply arith apply simp apply (rule x_less_2_0_1', simp+) done lemma shiftr1_irrelevant_lsb: "bit (x::('a::len) word) 0 \ x >> 1 = (x + 1) >> 1" apply (cases \LENGTH('a)\; transfer) apply (simp_all add: take_bit_drop_bit) apply (simp add: drop_bit_take_bit drop_bit_Suc) done lemma shiftr1_0_imp_only_lsb:"((x::('a::len) word) + 1) >> 1 = 0 \ x = 0 \ x + 1 = 0" by (metis One_nat_def shiftr1_0_or_1 word_less_1 word_overflow) lemma shiftr1_irrelevant_lsb': "\ (bit (x::('a::len) word) 0) \ x >> 1 = (x + 1) >> 1" by (metis shiftr1_irrelevant_lsb) (* Perhaps this one should be a simp lemma, but it seems a little dangerous. *) lemma cast_chunk_assemble_id: "\n = LENGTH('a::len); m = LENGTH('b::len); n * 2 = m\ \ (((ucast ((ucast (x::'b word))::'a word))::'b word) OR (((ucast ((ucast (x >> n))::'a word))::'b word) << n)) = x" apply (subgoal_tac "((ucast ((ucast (x >> n))::'a word))::'b word) = x >> n") apply clarsimp apply (subst and_not_mask[symmetric]) apply (subst ucast_ucast_mask) apply (subst word_ao_dist2[symmetric]) apply clarsimp apply (rule ucast_ucast_len) apply (rule shiftr_less_t2n') apply (subst and_mask_eq_iff_le_mask) apply (simp_all add: mask_eq_decr_exp flip: mult_2_right) apply (metis add_diff_cancel_left' len_gt_0 mult_2_right zero_less_diff) done lemma cast_chunk_scast_assemble_id: "\n = LENGTH('a::len); m = LENGTH('b::len); n * 2 = m\ \ (((ucast ((scast (x::'b word))::'a word))::'b word) OR (((ucast ((scast (x >> n))::'a word))::'b word) << n)) = x" apply (subgoal_tac "((scast x)::'a word) = ((ucast x)::'a word)") apply (subgoal_tac "((scast (x >> n))::'a word) = ((ucast (x >> n))::'a word)") apply (simp add:cast_chunk_assemble_id) apply (subst down_cast_same[symmetric], subst is_down, arith, simp)+ done lemma unat_shiftr_less_t2n: fixes x :: "'a :: len word" shows "unat x < 2 ^ (n + m) \ unat (x >> n) < 2 ^ m" by (simp add: shiftr_div_2n' power_add mult.commute less_mult_imp_div_less) lemma ucast_less_shiftl_helper: "\ LENGTH('b) + 2 < LENGTH('a); 2 ^ (LENGTH('b) + 2) \ n\ \ (ucast (x :: 'b::len word) << 2) < (n :: 'a::len word)" apply (erule order_less_le_trans[rotated]) using ucast_less[where x=x and 'a='a] apply (simp only: shiftl_t2n field_simps) apply (rule word_less_power_trans2; simp) done (* negating a mask which has been shifted to the very left *) lemma NOT_mask_shifted_lenword: "NOT (mask len << (LENGTH('a) - len) ::'a::len word) = mask (LENGTH('a) - len)" by (rule bit_word_eqI) (auto simp add: word_size bit_not_iff bit_push_bit_iff bit_mask_iff shiftl_def) (* Comparisons between different word sizes. *) lemma shiftr_less: "(w::'a::len word) < k \ w >> n < k" by (metis div_le_dividend le_less_trans shiftr_div_2n' unat_arith_simps(2)) lemma word_and_notzeroD: "w AND w' \ 0 \ w \ 0 \ w' \ 0" by auto lemma shiftr_le_0: "unat (w::'a::len word) < 2 ^ n \ w >> n = (0::'a::len word)" by (auto simp add: take_bit_word_eq_self_iff word_less_nat_alt shiftr_def simp flip: take_bit_eq_self_iff_drop_bit_eq_0 intro: ccontr) lemma of_nat_shiftl: "(of_nat x << n) = (of_nat (x * 2 ^ n) :: ('a::len) word)" proof - have "(of_nat x::'a word) << n = of_nat (2 ^ n) * of_nat x" using shiftl_t2n by (metis word_unat_power) thus ?thesis by simp qed lemma shiftl_1_not_0: "n < LENGTH('a) \ (1::'a::len word) << n \ 0" by (simp add: shiftl_t2n) (* continue sorting out from here *) (* usually: x,y = (len_of TYPE ('a)) *) lemma bitmagic_zeroLast_leq_or1Last: "(a::('a::len) word) AND (mask len << x - len) \ a OR mask (y - len)" by (meson le_word_or2 order_trans word_and_le2) lemma zero_base_lsb_imp_set_eq_as_bit_operation: fixes base ::"'a::len word" assumes valid_prefix: "mask (LENGTH('a) - len) AND base = 0" shows "(base = NOT (mask (LENGTH('a) - len)) AND a) \ (a \ {base .. base OR mask (LENGTH('a) - len)})" proof have helper3: "x OR y = x OR y AND NOT x" for x y ::"'a::len word" by (simp add: word_oa_dist2) from assms show "base = NOT (mask (LENGTH('a) - len)) AND a \ a \ {base..base OR mask (LENGTH('a) - len)}" apply(simp add: word_and_le1) apply(metis helper3 le_word_or2 word_bw_comms(1) word_bw_comms(2)) done next assume "a \ {base..base OR mask (LENGTH('a) - len)}" hence a: "base \ a \ a \ base OR mask (LENGTH('a) - len)" by simp show "base = NOT (mask (LENGTH('a) - len)) AND a" proof - have f2: "\x\<^sub>0. base AND NOT (mask x\<^sub>0) \ a AND NOT (mask x\<^sub>0)" using a neg_mask_mono_le by blast have f3: "\x\<^sub>0. a AND NOT (mask x\<^sub>0) \ (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>0)" using a neg_mask_mono_le by blast have f4: "base = base AND NOT (mask (LENGTH('a) - len))" using valid_prefix by (metis mask_eq_0_eq_x word_bw_comms(1)) hence f5: "\x\<^sub>6. (base OR x\<^sub>6) AND NOT (mask (LENGTH('a) - len)) = base OR x\<^sub>6 AND NOT (mask (LENGTH('a) - len))" using word_ao_dist by (metis) have f6: "\x\<^sub>2 x\<^sub>3. a AND NOT (mask x\<^sub>2) \ x\<^sub>3 \ \ (base OR mask (LENGTH('a) - len)) AND NOT (mask x\<^sub>2) \ x\<^sub>3" using f3 dual_order.trans by auto have "base = (base OR mask (LENGTH('a) - len)) AND NOT (mask (LENGTH('a) - len))" using f5 by auto hence "base = a AND NOT (mask (LENGTH('a) - len))" using f2 f4 f6 by (metis eq_iff) thus "base = NOT (mask (LENGTH('a) - len)) AND a" by (metis word_bw_comms(1)) qed qed lemma of_nat_eq_signed_scast: "(of_nat x = (y :: ('a::len) signed word)) = (of_nat x = (scast y :: 'a word))" by (metis scast_of_nat scast_scast_id(2)) lemma word_aligned_add_no_wrap_bounded: "\ w + 2^n \ x; w + 2^n \ 0; is_aligned w n \ \ (w::'a::len word) < x" by (blast dest: is_aligned_no_overflow le_less_trans word_leq_le_minus_one) lemma mask_Suc: "mask (Suc n) = (2 :: 'a::len word) ^ n + mask n" by (simp add: mask_eq_decr_exp) lemma mask_mono: "sz' \ sz \ mask sz' \ (mask sz :: 'a::len word)" by (simp add: le_mask_iff shiftr_mask_le) lemma aligned_mask_disjoint: "\ is_aligned (a :: 'a :: len word) n; b \ mask n \ \ a AND b = 0" by (metis and_zero_eq is_aligned_mask le_mask_imp_and_mask word_bw_lcs(1)) lemma word_and_or_mask_aligned: "\ is_aligned a n; b \ mask n \ \ a + b = a OR b" by (simp add: aligned_mask_disjoint word_plus_and_or_coroll) lemma word_and_or_mask_aligned2: \is_aligned b n \ a \ mask n \ a + b = a OR b\ using word_and_or_mask_aligned [of b n a] by (simp add: ac_simps) lemma is_aligned_ucastI: "is_aligned w n \ is_aligned (ucast w) n" by (simp add: bit_ucast_iff is_aligned_nth) lemma ucast_le_maskI: "a \ mask n \ UCAST('a::len \ 'b::len) a \ mask n" by (metis and_mask_eq_iff_le_mask ucast_and_mask) lemma ucast_add_mask_aligned: "\ a \ mask n; is_aligned b n \ \ UCAST ('a::len \ 'b::len) (a + b) = ucast a + ucast b" by (metis add.commute is_aligned_ucastI ucast_le_maskI ucast_or_distrib word_and_or_mask_aligned) lemma ucast_shiftl: "LENGTH('b) \ LENGTH ('a) \ UCAST ('a::len \ 'b::len) x << n = ucast (x << n)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma ucast_leq_mask: "LENGTH('a) \ n \ ucast (x::'a::len word) \ mask n" apply (simp add: less_eq_mask_iff_take_bit_eq_self) apply transfer apply (simp add: ac_simps) done lemma shiftl_inj: \x = y\ if \x << n = y << n\ \x \ mask (LENGTH('a) - n)\ \y \ mask (LENGTH('a) - n)\ for x y :: \'a::len word\ proof (cases \n < LENGTH('a)\) case False with that show ?thesis by simp next case True moreover from that have \take_bit (LENGTH('a) - n) x = x\ \take_bit (LENGTH('a) - n) y = y\ by (simp_all add: less_eq_mask_iff_take_bit_eq_self) ultimately show ?thesis using \x << n = y << n\ by (metis diff_less gr_implies_not0 linorder_cases linorder_not_le shiftl_shiftr_id shiftl_x_0 take_bit_word_eq_self_iff) qed lemma distinct_word_add_ucast_shift_inj: \p' = p \ off' = off\ if *: \p + (UCAST('a::len \ 'b::len) off << n) = p' + (ucast off' << n)\ and \is_aligned p n'\ \is_aligned p' n'\ \n' = n + LENGTH('a)\ \n' < LENGTH('b)\ proof - from \n' = n + LENGTH('a)\ have [simp]: \n' - n = LENGTH('a)\ \n + LENGTH('a) = n'\ by simp_all from \is_aligned p n'\ obtain q where p: \p = push_bit n' (word_of_nat q)\ \q < 2 ^ (LENGTH('b) - n')\ by (rule is_alignedE') from \is_aligned p' n'\ obtain q' where p': \p' = push_bit n' (word_of_nat q')\ \q' < 2 ^ (LENGTH('b) - n')\ by (rule is_alignedE') define m :: nat where \m = unat off\ then have off: \off = word_of_nat m\ by simp define m' :: nat where \m' = unat off'\ then have off': \off' = word_of_nat m'\ by simp have \push_bit n' q + take_bit n' (push_bit n m) < 2 ^ LENGTH('b)\ by (metis id_apply is_aligned_no_wrap''' of_nat_eq_id of_nat_push_bit p(1) p(2) take_bit_nat_eq_self_iff take_bit_nat_less_exp take_bit_push_bit that(2) that(5) unsigned_of_nat) moreover have \push_bit n' q' + take_bit n' (push_bit n m') < 2 ^ LENGTH('b)\ by (metis \n' - n = LENGTH('a)\ id_apply is_aligned_no_wrap''' m'_def of_nat_eq_id of_nat_push_bit off' p'(1) p'(2) take_bit_nat_eq_self_iff take_bit_push_bit that(3) that(5) unsigned_of_nat) ultimately have \push_bit n' q + take_bit n' (push_bit n m) = push_bit n' q' + take_bit n' (push_bit n m')\ using * by (simp add: p p' off off' push_bit_of_nat push_bit_take_bit word_of_nat_inj unsigned_of_nat shiftl_def flip: of_nat_add) then have \int (push_bit n' q + take_bit n' (push_bit n m)) = int (push_bit n' q' + take_bit n' (push_bit n m'))\ by simp then have \concat_bit n' (int (push_bit n m)) (int q) = concat_bit n' (int (push_bit n m')) (int q')\ by (simp add: of_nat_push_bit of_nat_take_bit concat_bit_eq) then show ?thesis by (simp add: p p' off off' take_bit_of_nat take_bit_push_bit word_of_nat_eq_iff concat_bit_eq_iff) (simp add: push_bit_eq_mult) qed lemma word_upto_Nil: "y < x \ [x .e. y ::'a::len word] = []" by (simp add: upto_enum_red not_le word_less_nat_alt) lemma word_enum_decomp_elem: assumes "[x .e. (y ::'a::len word)] = as @ a # bs" shows "x \ a \ a \ y" proof - have "set as \ set [x .e. y] \ a \ set [x .e. y]" using assms by (auto dest: arg_cong[where f=set]) then show ?thesis by auto qed lemma word_enum_prefix: "[x .e. (y ::'a::len word)] = as @ a # bs \ as = (if x < a then [x .e. a - 1] else [])" apply (induct as arbitrary: x; clarsimp) apply (case_tac "x < y") prefer 2 apply (case_tac "x = y", simp) apply (simp add: not_less) apply (drule (1) dual_order.not_eq_order_implies_strict) apply (simp add: word_upto_Nil) apply (simp add: word_upto_Cons_eq) apply (case_tac "x < y") prefer 2 apply (case_tac "x = y", simp) apply (simp add: not_less) apply (drule (1) dual_order.not_eq_order_implies_strict) apply (simp add: word_upto_Nil) apply (clarsimp simp: word_upto_Cons_eq) apply (frule word_enum_decomp_elem) apply clarsimp apply (rule conjI) prefer 2 apply (subst word_Suc_le[symmetric]; clarsimp) apply (drule meta_spec) apply (drule (1) meta_mp) apply clarsimp apply (rule conjI; clarsimp) apply (subst (2) word_upto_Cons_eq) apply unat_arith apply simp done lemma word_enum_decomp_set: "[x .e. (y ::'a::len word)] = as @ a # bs \ a \ set as" by (metis distinct_append distinct_enum_upto' not_distinct_conv_prefix) lemma word_enum_decomp: assumes "[x .e. (y ::'a::len word)] = as @ a # bs" shows "x \ a \ a \ y \ a \ set as \ (\z \ set as. x \ z \ z \ y)" proof - from assms have "set as \ set [x .e. y] \ a \ set [x .e. y]" by (auto dest: arg_cong[where f=set]) with word_enum_decomp_set[OF assms] show ?thesis by auto qed lemma of_nat_unat_le_mask_ucast: "\of_nat (unat t) = w; t \ mask LENGTH('a)\ \ t = UCAST('a::len \ 'b::len) w" by (clarsimp simp: ucast_nat_def ucast_ucast_mask simp flip: and_mask_eq_iff_le_mask) lemma less_diff_gt0: "a < b \ (0 :: 'a :: len word) < b - a" by unat_arith lemma unat_plus_gt: "unat ((a :: 'a :: len word) + b) \ unat a + unat b" by (clarsimp simp: unat_plus_if_size) lemma const_less: "\ (a :: 'a :: len word) - 1 < b; a \ b \ \ a < b" by (metis less_1_simp word_le_less_eq) lemma add_mult_aligned_neg_mask: \(x + y * m) AND NOT(mask n) = (x AND NOT(mask n)) + y * m\ if \m AND (2 ^ n - 1) = 0\ for x y m :: \'a::len word\ by (metis (no_types, opaque_lifting) add.assoc add.commute add.right_neutral add_uminus_conv_diff mask_eq_decr_exp mask_eqs(2) mask_eqs(6) mult.commute mult_zero_left subtract_mask(1) that) lemma unat_of_nat_minus_1: "\ n < 2 ^ LENGTH('a); n \ 0 \ \ unat ((of_nat n:: 'a :: len word) - 1) = n - 1" by (simp add: of_nat_diff unat_eq_of_nat) lemma word_eq_zeroI: "a \ a - 1 \ a = 0" for a :: "'a :: len word" by (simp add: word_must_wrap) lemma word_add_format: "(-1 :: 'a :: len word) + b + c = b + (c - 1)" by simp lemma upto_enum_word_nth: "\ i \ j; k \ unat (j - i) \ \ [i .e. j] ! k = i + of_nat k" apply (clarsimp simp: upto_enum_def nth_append) apply (clarsimp simp: word_le_nat_alt[symmetric]) apply (rule conjI, clarsimp) apply (subst toEnum_of_nat, unat_arith) apply unat_arith apply (clarsimp simp: not_less unat_sub[symmetric]) apply unat_arith done lemma upto_enum_step_nth: "\ a \ c; n \ unat ((c - a) div (b - a)) \ \ [a, b .e. c] ! n = a + of_nat n * (b - a)" by (clarsimp simp: upto_enum_step_def not_less[symmetric] upto_enum_word_nth) lemma upto_enum_inc_1_len: "a < - 1 \ [(0 :: 'a :: len word) .e. 1 + a] = [0 .e. a] @ [1 + a]" apply (simp add: upto_enum_word) apply (subgoal_tac "unat (1+a) = 1 + unat a") apply simp apply (subst unat_plus_simple[THEN iffD1]) apply (metis add.commute no_plus_overflow_neg olen_add_eqv) apply unat_arith done lemma neg_mask_add: "y AND mask n = 0 \ x + y AND NOT(mask n) = (x AND NOT(mask n)) + y" for x y :: \'a::len word\ by (clarsimp simp: mask_out_sub_mask mask_eqs(7)[symmetric] mask_twice) lemma shiftr_shiftl_shiftr[simp]: "(x :: 'a :: len word) >> a << a >> a = x >> a" by (rule bit_word_eqI) (auto simp add: bit_simps dest: bit_imp_le_length) lemma add_right_shift: "\ x AND mask n = 0; y AND mask n = 0; x \ x + y \ \ (x + y :: ('a :: len) word) >> n = (x >> n) + (y >> n)" apply (simp add: no_olen_add_nat is_aligned_mask[symmetric]) apply (simp add: unat_arith_simps shiftr_div_2n' split del: if_split) apply (subst if_P) apply (erule order_le_less_trans[rotated]) apply (simp add: add_mono) apply (simp add: shiftr_div_2n' is_aligned_iff_dvd_nat) done lemma sub_right_shift: "\ x AND mask n = 0; y AND mask n = 0; y \ x \ \ (x - y) >> n = (x >> n :: 'a :: len word) - (y >> n)" using add_right_shift[where x="x - y" and y=y and n=n] by (simp add: aligned_sub_aligned is_aligned_mask[symmetric] word_sub_le) lemma and_and_mask_simple: "y AND mask n = mask n \ (x AND y) AND mask n = x AND mask n" by (simp add: ac_simps) lemma and_and_mask_simple_not: "y AND mask n = 0 \ (x AND y) AND mask n = 0" by (simp add: ac_simps) lemma word_and_le': "b \ c \ (a :: 'a :: len word) AND b \ c" by (metis word_and_le1 order_trans) lemma word_and_less': "b < c \ (a :: 'a :: len word) AND b < c" by transfer simp lemma shiftr_w2p: "x < LENGTH('a) \ 2 ^ x = (2 ^ (LENGTH('a) - 1) >> (LENGTH('a) - 1 - x) :: 'a :: len word)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma t2p_shiftr: "\ b \ a; a < LENGTH('a) \ \ (2 :: 'a :: len word) ^ a >> b = 2 ^ (a - b)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma scast_1[simp]: "scast (1 :: 'a :: len signed word) = (1 :: 'a word)" by simp lemma unsigned_uminus1 [simp]: \(unsigned (-1::'b::len word)::'c::len word) = mask LENGTH('b)\ by (fact unsigned_minus_1_eq_mask) lemma ucast_ucast_mask_eq: "\ UCAST('a::len \ 'b::len) x = y; x AND mask LENGTH('b) = x \ \ x = ucast y" by (drule sym) (simp flip: take_bit_eq_mask add: unsigned_ucast_eq) lemma ucast_up_eq: "\ ucast x = (ucast y::'b::len word); LENGTH('a) \ LENGTH ('b) \ \ ucast x = (ucast y::'a::len word)" by (simp add: word_eq_iff bit_simps) lemma ucast_up_neq: "\ ucast x \ (ucast y::'b::len word); LENGTH('b) \ LENGTH ('a) \ \ ucast x \ (ucast y::'a::len word)" by (fastforce dest: ucast_up_eq) lemma mask_AND_less_0: "\ x AND mask n = 0; m \ n \ \ x AND mask m = 0" for x :: \'a::len word\ by (metis mask_twice2 word_and_notzeroD) lemma mask_len_id [simp]: "(x :: 'a :: len word) AND mask LENGTH('a) = x" using uint_lt2p [of x] by (simp add: mask_eq_iff) lemma scast_ucast_down_same: "LENGTH('b) \ LENGTH('a) \ SCAST('a \ 'b) = UCAST('a::len \ 'b::len)" by (simp add: down_cast_same is_down) lemma word_aligned_0_sum: "\ a + b = 0; is_aligned (a :: 'a :: len word) n; b \ mask n; n < LENGTH('a) \ \ a = 0 \ b = 0" by (simp add: word_plus_and_or_coroll aligned_mask_disjoint word_or_zero) lemma mask_eq1_nochoice: "\ LENGTH('a) > 1; (x :: 'a :: len word) AND 1 = x \ \ x = 0 \ x = 1" by (metis word_and_1) lemma shiftr_and_eq_shiftl: "(w >> n) AND x = y \ w AND (x << n) = (y << n)" for y :: "'a:: len word" apply (drule sym) apply simp apply (rule bit_word_eqI) apply (auto simp add: bit_simps) done lemma add_mask_lower_bits': "\ len = LENGTH('a); is_aligned (x :: 'a :: len word) n; \n' \ n. n' < len \ \ bit p n' \ \ x + p AND NOT(mask n) = x" using add_mask_lower_bits by auto lemma leq_mask_shift: "(x :: 'a :: len word) \ mask (low_bits + high_bits) \ (x >> low_bits) \ mask high_bits" by (simp add: le_mask_iff shiftr_shiftr ac_simps) lemma ucast_ucast_eq_mask_shift: "(x :: 'a :: len word) \ mask (low_bits + LENGTH('b)) \ ucast((ucast (x >> low_bits)) :: 'b :: len word) = x >> low_bits" by (meson and_mask_eq_iff_le_mask eq_ucast_ucast_eq not_le_imp_less shiftr_less_t2n' ucast_ucast_len) lemma const_le_unat: "\ b < 2 ^ LENGTH('a); of_nat b \ a \ \ b \ unat (a :: 'a :: len word)" by (simp add: word_le_nat_alt unsigned_of_nat take_bit_nat_eq_self) lemma upt_enum_offset_trivial: "\ x < 2 ^ LENGTH('a) - 1 ; n \ unat x \ \ ([(0 :: 'a :: len word) .e. x] ! n) = of_nat n" apply (induct x arbitrary: n) apply simp by (simp add: upto_enum_word_nth) lemma word_le_mask_out_plus_2sz: "x \ (x AND NOT(mask sz)) + 2 ^ sz - 1" for x :: \'a::len word\ by (metis add_diff_eq word_neg_and_le) lemma ucast_add: "ucast (a + (b :: 'a :: len word)) = ucast a + (ucast b :: ('a signed word))" by transfer (simp add: take_bit_add) lemma ucast_minus: "ucast (a - (b :: 'a :: len word)) = ucast a - (ucast b :: ('a signed word))" apply (insert ucast_add[where a=a and b="-b"]) apply (metis (no_types, opaque_lifting) add_diff_eq diff_add_cancel ucast_add) done lemma scast_ucast_add_one [simp]: "scast (ucast (x :: 'a::len word) + (1 :: 'a signed word)) = x + 1" apply (subst ucast_1[symmetric]) apply (subst ucast_add[symmetric]) apply clarsimp done lemma word_and_le_plus_one: "a > 0 \ (x :: 'a :: len word) AND (a - 1) < a" by (simp add: gt0_iff_gem1 word_and_less') lemma unat_of_ucast_then_shift_eq_unat_of_shift[simp]: "LENGTH('b) \ LENGTH('a) \ unat ((ucast (x :: 'a :: len word) :: 'b :: len word) >> n) = unat (x >> n)" by (simp add: shiftr_div_2n' unat_ucast_up_simp) lemma unat_of_ucast_then_mask_eq_unat_of_mask[simp]: "LENGTH('b) \ LENGTH('a) \ unat ((ucast (x :: 'a :: len word) :: 'b :: len word) AND mask m) = unat (x AND mask m)" by (metis ucast_and_mask unat_ucast_up_simp) lemma shiftr_less_t2n3: "\ (2 :: 'a word) ^ (n + m) = 0; m < LENGTH('a) \ \ (x :: 'a :: len word) >> n < 2 ^ m" by (fastforce intro: shiftr_less_t2n' simp: mask_eq_decr_exp power_overflow) lemma unat_shiftr_le_bound: "\ 2 ^ (LENGTH('a :: len) - n) - 1 \ bnd; 0 < n \ \ unat ((x :: 'a word) >> n) \ bnd" apply transfer apply (simp add: take_bit_drop_bit) apply (simp add: drop_bit_take_bit) apply (rule order_trans) defer apply assumption apply (simp add: nat_le_iff of_nat_diff) done lemma shiftr_eqD: "\ x >> n = y >> n; is_aligned x n; is_aligned y n \ \ x = y" by (metis is_aligned_shiftr_shiftl) lemma word_shiftr_shiftl_shiftr_eq_shiftr: "a \ b \ (x :: 'a :: len word) >> a << b >> b = x >> a" apply (rule bit_word_eqI) apply (auto simp add: bit_simps dest: bit_imp_le_length) done lemma of_int_uint_ucast: "of_int (uint (x :: 'a::len word)) = (ucast x :: 'b::len word)" by (fact Word.of_int_uint) lemma mod_mask_drop: "\ m = 2 ^ n; 0 < m; mask n AND msk = mask n \ \ (x mod m) AND msk = x mod m" for x :: \'a::len word\ by (simp add: word_mod_2p_is_mask word_bw_assocs) lemma mask_eq_ucast_eq: "\ x AND mask LENGTH('a) = (x :: ('c :: len word)); LENGTH('a) \ LENGTH('b)\ \ ucast (ucast x :: ('a :: len word)) = (ucast x :: ('b :: len word))" by (metis ucast_and_mask ucast_id ucast_ucast_mask ucast_up_eq) lemma of_nat_less_t2n: "of_nat i < (2 :: ('a :: len) word) ^ n \ n < LENGTH('a) \ unat (of_nat i :: 'a word) < 2 ^ n" by (metis order_less_trans p2_gt_0 unat_less_power word_neq_0_conv) lemma two_power_increasing_less_1: "\ n \ m; m \ LENGTH('a) \ \ (2 :: 'a :: len word) ^ n - 1 \ 2 ^ m - 1" by (metis diff_diff_cancel le_m1_iff_lt less_imp_diff_less p2_gt_0 two_power_increasing word_1_le_power word_le_minus_mono_left word_less_sub_1) lemma word_sub_mono4: "\ y + x \ z + x; y \ y + x; z \ z + x \ \ y \ z" for y :: "'a :: len word" by (simp add: word_add_le_iff2) lemma eq_or_less_helperD: "\ n = unat (2 ^ m - 1 :: 'a :: len word) \ n < unat (2 ^ m - 1 :: 'a word); m < LENGTH('a) \ \ n < 2 ^ m" by (meson le_less_trans nat_less_le unat_less_power word_power_less_1) lemma mask_sub: "n \ m \ mask m - mask n = mask m AND NOT(mask n :: 'a::len word)" by (metis (full_types) and_mask_eq_iff_shiftr_0 mask_out_sub_mask shiftr_mask_le word_bw_comms(1)) lemma neg_mask_diff_bound: "sz'\ sz \ (ptr AND NOT(mask sz')) - (ptr AND NOT(mask sz)) \ 2 ^ sz - 2 ^ sz'" (is "_ \ ?lhs \ ?rhs") for ptr :: \'a::len word\ proof - assume lt: "sz' \ sz" hence "?lhs = ptr AND (mask sz AND NOT(mask sz'))" by (metis add_diff_cancel_left' multiple_mask_trivia) also have "\ \ ?rhs" using lt by (metis (mono_tags) add_diff_eq diff_eq_eq eq_iff mask_2pm1 mask_sub word_and_le') finally show ?thesis by simp qed lemma mask_out_eq_0: "\ idx < 2 ^ sz; sz < LENGTH('a) \ \ (of_nat idx :: 'a :: len word) AND NOT(mask sz) = 0" by (simp add: of_nat_power less_mask_eq mask_eq_0_eq_x) lemma is_aligned_neg_mask_eq': "is_aligned ptr sz = (ptr AND NOT(mask sz) = ptr)" using is_aligned_mask mask_eq_0_eq_x by blast lemma neg_mask_mask_unat: "sz < LENGTH('a) \ unat ((ptr :: 'a :: len word) AND NOT(mask sz)) + unat (ptr AND mask sz) = unat ptr" by (metis AND_NOT_mask_plus_AND_mask_eq unat_plus_simple word_and_le2) lemma unat_pow_le_intro: "LENGTH('a) \ n \ unat (x :: 'a :: len word) < 2 ^ n" by (metis lt2p_lem not_le of_nat_le_iff of_nat_numeral semiring_1_class.of_nat_power uint_nat) lemma unat_shiftl_less_t2n: \unat (x << n) < 2 ^ m\ if \unat (x :: 'a :: len word) < 2 ^ (m - n)\ \m < LENGTH('a)\ proof (cases \n \ m\) case False with that show ?thesis apply (transfer fixing: m n) apply (simp add: not_le take_bit_push_bit) - apply (metis diff_le_self order_le_less_trans push_bit_of_0 take_bit_0 take_bit_int_eq_self - take_bit_int_less_exp take_bit_nonnegative take_bit_tightened) + apply (metis diff_le_self order_le_less_trans push_bit_of_0 take_bit_0 take_bit_int_eq_self + take_bit_int_less_exp take_bit_nonnegative take_bit_tightened) done next case True moreover define q r where \q = m - n\ and \r = LENGTH('a) - n - q\ ultimately have \m - n = q\ \m = n + q\ \LENGTH('a) = r + q + n\ using that by simp_all with that show ?thesis apply (transfer fixing: m n q r) apply (simp add: not_le take_bit_push_bit) apply (simp add: push_bit_eq_mult power_add) using take_bit_tightened_less_eq_int [of \r + q\ \r + q + n\] apply (rule le_less_trans) apply simp_all done qed lemma unat_is_aligned_add: "\ is_aligned p n; unat d < 2 ^ n \ \ unat (p + d AND mask n) = unat d \ unat (p + d AND NOT(mask n)) = unat p" by (metis add.right_neutral and_mask_eq_iff_le_mask and_not_mask le_mask_iff mask_add_aligned mask_out_add_aligned mult_zero_right shiftl_t2n shiftr_le_0) lemma unat_shiftr_shiftl_mask_zero: "\ c + a \ LENGTH('a) + b ; c < LENGTH('a) \ \ unat (((q :: 'a :: len word) >> a << b) AND NOT(mask c)) = 0" by (fastforce intro: unat_is_aligned_add[where p=0 and n=c, simplified, THEN conjunct2] unat_shiftl_less_t2n unat_shiftr_less_t2n unat_pow_le_intro) lemmas of_nat_ucast = ucast_of_nat[symmetric] lemma shift_then_mask_eq_shift_low_bits: "x \ mask (low_bits + high_bits) \ (x >> low_bits) AND mask high_bits = x >> low_bits" for x :: \'a::len word\ by (simp add: leq_mask_shift le_mask_imp_and_mask) lemma leq_low_bits_iff_zero: "\ x \ mask (low bits + high bits); x >> low_bits = 0 \ \ (x AND mask low_bits = 0) = (x = 0)" for x :: \'a::len word\ using and_mask_eq_iff_shiftr_0 by force lemma unat_less_iff: "\ unat (a :: 'a :: len word) = b; c < 2 ^ LENGTH('a) \ \ (a < of_nat c) = (b < c)" using unat_ucast_less_no_overflow_simp by blast lemma is_aligned_no_overflow3: "\ is_aligned (a :: 'a :: len word) n; n < LENGTH('a); b < 2 ^ n; c \ 2 ^ n; b < c \ \ a + b \ a + (c - 1)" by (meson is_aligned_no_wrap' le_m1_iff_lt not_le word_less_sub_1 word_plus_mono_right) lemma mask_add_aligned_right: "is_aligned p n \ (q + p) AND mask n = q AND mask n" by (simp add: mask_add_aligned add.commute) lemma leq_high_bits_shiftr_low_bits_leq_bits_mask: "x \ mask high_bits \ (x :: 'a :: len word) << low_bits \ mask (low_bits + high_bits)" by (metis le_mask_shiftl_le_mask) lemma word_two_power_neg_ineq: "2 ^ m \ (0 :: 'a word) \ 2 ^ n \ - (2 ^ m :: 'a :: len word)" apply (cases "n < LENGTH('a)"; simp add: power_overflow) apply (cases "m < LENGTH('a)"; simp add: power_overflow) apply (simp add: word_le_nat_alt unat_minus word_size) apply (cases "LENGTH('a)"; simp) apply (simp add: less_Suc_eq_le) apply (drule power_increasing[where a=2 and n=n] power_increasing[where a=2 and n=m], simp)+ apply (drule(1) add_le_mono) apply simp done lemma unat_shiftl_absorb: "\ x \ 2 ^ p; p + k < LENGTH('a) \ \ unat (x :: 'a :: len word) * 2 ^ k = unat (x * 2 ^ k)" by (smt add_diff_cancel_right' add_lessD1 le_add2 le_less_trans mult.commute nat_le_power_trans unat_lt2p unat_mult_lem unat_power_lower word_le_nat_alt) lemma word_plus_mono_right_split: "\ unat ((x :: 'a :: len word) AND mask sz) + unat z < 2 ^ sz; sz < LENGTH('a) \ \ x \ x + z" apply (subgoal_tac "(x AND NOT(mask sz)) + (x AND mask sz) \ (x AND NOT(mask sz)) + ((x AND mask sz) + z)") apply (simp add:word_plus_and_or_coroll2 field_simps) apply (rule word_plus_mono_right) apply (simp add: less_le_trans no_olen_add_nat) using of_nat_power is_aligned_no_wrap' by force lemma mul_not_mask_eq_neg_shiftl: "NOT(mask n :: 'a::len word) = -1 << n" by (simp add: NOT_mask shiftl_t2n) lemma shiftr_mul_not_mask_eq_and_not_mask: "(x >> n) * NOT(mask n) = - (x AND NOT(mask n))" for x :: \'a::len word\ by (metis NOT_mask and_not_mask mult_minus_left semiring_normalization_rules(7) shiftl_t2n) lemma mask_eq_n1_shiftr: "n \ LENGTH('a) \ (mask n :: 'a :: len word) = -1 >> (LENGTH('a) - n)" by (metis diff_diff_cancel eq_refl mask_full shiftr_mask2) lemma is_aligned_mask_out_add_eq: "is_aligned p n \ (p + x) AND NOT(mask n) = p + (x AND NOT(mask n))" by (simp add: mask_out_sub_mask mask_add_aligned) lemmas is_aligned_mask_out_add_eq_sub = is_aligned_mask_out_add_eq[where x="a - b" for a b, simplified field_simps] lemma aligned_bump_down: "is_aligned x n \ (x - 1) AND NOT(mask n) = x - 2 ^ n" by (drule is_aligned_mask_out_add_eq[where x="-1"]) (simp add: NOT_mask) lemma unat_2tp_if: "unat (2 ^ n :: ('a :: len) word) = (if n < LENGTH ('a) then 2 ^ n else 0)" by (split if_split, simp_all add: power_overflow) lemma mask_of_mask: "mask (n::nat) AND mask (m::nat) = (mask (min m n) :: 'a::len word)" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma unat_signed_ucast_less_ucast: "LENGTH('a) \ LENGTH('b) \ unat (ucast (x :: 'a :: len word) :: 'b :: len signed word) = unat x" by (simp add: unat_ucast_up_simp) lemma toEnum_of_ucast: "LENGTH('b) \ LENGTH('a) \ (toEnum (unat (b::'b :: len word))::'a :: len word) = of_nat (unat b)" by (simp add: unat_pow_le_intro) +lemma plus_mask_AND_NOT_mask_eq: + "x AND NOT(mask n) = x \ (x + mask n) AND NOT(mask n) = x" for x::\'a::len word\ + by (subst word_plus_and_or_coroll; word_eqI_solve) + lemmas unat_ucast_mask = unat_ucast_eq_unat_and_mask[where w=a for a] lemma t2n_mask_eq_if: "2 ^ n AND mask m = (if n < m then 2 ^ n else (0 :: 'a::len word))" by (rule word_eqI) (auto simp add: bit_simps) lemma unat_ucast_le: "unat (ucast (x :: 'a :: len word) :: 'b :: len word) \ unat x" by (simp add: ucast_nat_def word_unat_less_le) lemma ucast_le_up_down_iff: "\ LENGTH('a) \ LENGTH('b); (x :: 'b :: len word) \ ucast (- 1 :: 'a :: len word) \ \ (ucast x \ (y :: 'a word)) = (x \ ucast y)" using le_max_word_ucast_id ucast_le_ucast by metis lemma ucast_ucast_mask_shift: "a \ LENGTH('a) + b \ ucast (ucast (p AND mask a >> b) :: 'a :: len word) = p AND mask a >> b" by (metis add.commute le_mask_iff shiftr_mask_le ucast_ucast_eq_mask_shift word_and_le') lemma unat_ucast_mask_shift: "a \ LENGTH('a) + b \ unat (ucast (p AND mask a >> b) :: 'a :: len word) = unat (p AND mask a >> b)" by (metis linear ucast_ucast_mask_shift unat_ucast_up_simp) lemma mask_overlap_zero: "a \ b \ (p AND mask a) AND NOT(mask b) = 0" for p :: \'a::len word\ by (metis NOT_mask_AND_mask mask_lower_twice2 max_def) lemma mask_shifl_overlap_zero: "a + c \ b \ (p AND mask a << c) AND NOT(mask b) = 0" for p :: \'a::len word\ by (metis and_mask_0_iff_le_mask mask_mono mask_shiftl_decompose order_trans shiftl_over_and_dist word_and_le' word_and_le2) lemma mask_overlap_zero': "a \ b \ (p AND NOT(mask a)) AND mask b = 0" for p :: \'a::len word\ using mask_AND_NOT_mask mask_AND_less_0 by blast lemma mask_rshift_mult_eq_rshift_lshift: "((a :: 'a :: len word) >> b) * (1 << c) = (a >> b << c)" by (simp add: shiftl_t2n) lemma shift_alignment: "a \ b \ is_aligned (p >> a << a) b" using is_aligned_shift is_aligned_weaken by blast lemma mask_split_sum_twice: "a \ b \ (p AND NOT(mask a)) + ((p AND mask a) AND NOT(mask b)) + (p AND mask b) = p" for p :: \'a::len word\ by (simp add: add.commute multiple_mask_trivia word_bw_comms(1) word_bw_lcs(1) word_plus_and_or_coroll2) lemma mask_shift_eq_mask_mask: "(p AND mask a >> b << b) = (p AND mask a) AND NOT(mask b)" for p :: \'a::len word\ by (simp add: and_not_mask) lemma mask_shift_sum: "\ a \ b; unat n = unat (p AND mask b) \ \ (p AND NOT(mask a)) + (p AND mask a >> b) * (1 << b) + n = (p :: 'a :: len word)" apply (simp add: shiftl_def shiftr_def flip: push_bit_eq_mult take_bit_eq_mask word_unat_eq_iff) apply (subst disjunctive_add) apply (auto simp add: bit_simps) apply (subst disjunctive_add) apply (auto simp add: bit_simps) apply (rule bit_word_eqI) apply (auto simp add: bit_simps) done lemma is_up_compose: "\ is_up uc; is_up uc' \ \ is_up (uc' \ uc)" unfolding is_up_def by (simp add: Word.target_size Word.source_size) lemma of_int_sint_scast: "of_int (sint (x :: 'a :: len word)) = (scast x :: 'b :: len word)" by (fact Word.of_int_sint) lemma scast_of_nat_to_signed [simp]: "scast (of_nat x :: 'a :: len word) = (of_nat x :: 'a signed word)" by (rule bit_word_eqI) (simp add: bit_simps) lemma scast_of_nat_signed_to_unsigned_add: "scast (of_nat x + of_nat y :: 'a :: len signed word) = (of_nat x + of_nat y :: 'a :: len word)" by (metis of_nat_add scast_of_nat) lemma scast_of_nat_unsigned_to_signed_add: "(scast (of_nat x + of_nat y :: 'a :: len word)) = (of_nat x + of_nat y :: 'a :: len signed word)" by (metis Abs_fnat_hom_add scast_of_nat_to_signed) lemma and_mask_cases: fixes x :: "'a :: len word" assumes len: "n < LENGTH('a)" shows "x AND mask n \ of_nat ` set [0 ..< 2 ^ n]" apply (simp flip: take_bit_eq_mask) apply (rule image_eqI [of _ _ \unat (take_bit n x)\]) using len apply simp_all apply transfer apply simp done lemma sint_eq_uint_2pl: "\ (a :: 'a :: len word) < 2 ^ (LENGTH('a) - 1) \ \ sint a = uint a" by (simp add: not_msb_from_less sint_eq_uint word_2p_lem word_size) lemma pow_sub_less: "\ a + b \ LENGTH('a); unat (x :: 'a :: len word) = 2 ^ a \ \ unat (x * 2 ^ b - 1) < 2 ^ (a + b)" by (smt (z3) eq_or_less_helperD le_add2 le_eq_less_or_eq le_trans power_add unat_mult_lem unat_pow_le_intro unat_power_lower word_eq_unatI) lemma sle_le_2pl: "\ (b :: 'a :: len word) < 2 ^ (LENGTH('a) - 1); a \ b \ \ a <=s b" by (simp add: not_msb_from_less word_sle_msb_le) lemma sless_less_2pl: "\ (b :: 'a :: len word) < 2 ^ (LENGTH('a) - 1); a < b \ \ a > n = w AND mask (size w - n)" for w :: \'a::len word\ by (rule bit_word_eqI) (auto simp add: bit_simps word_size) lemma aligned_sub_aligned_simple: "\ is_aligned a n; is_aligned b n \ \ is_aligned (a - b) n" by (simp add: aligned_sub_aligned) lemma minus_one_shift: "- (1 << n) = (-1 << n :: 'a::len word)" - by (simp add: shiftl_def minus_exp_eq_not_mask push_bit_minus_one_eq_not_mask) + by (simp add: shiftl_def minus_exp_eq_not_mask) lemma ucast_eq_mask: "(UCAST('a::len \ 'b::len) x = UCAST('a \ 'b) y) = (x AND mask LENGTH('b) = y AND mask LENGTH('b))" by transfer (simp flip: take_bit_eq_mask add: ac_simps) context fixes w :: "'a::len word" begin private lemma sbintrunc_uint_ucast: assumes "Suc n = LENGTH('b::len)" shows "signed_take_bit n (uint (ucast w :: 'b word)) = signed_take_bit n (uint w)" by (rule bit_eqI) (use assms in \simp add: bit_simps\) private lemma test_bit_sbintrunc: assumes "i < LENGTH('a)" shows "bit (word_of_int (signed_take_bit n (uint w)) :: 'a word) i = (if n < i then bit w n else bit w i)" using assms by (simp add: bit_simps) private lemma test_bit_sbintrunc_ucast: assumes len_a: "i < LENGTH('a)" shows "bit (word_of_int (signed_take_bit (LENGTH('b) - 1) (uint (ucast w :: 'b word))) :: 'a word) i = (if LENGTH('b::len) \ i then bit w (LENGTH('b) - 1) else bit w i)" using len_a by (auto simp add: sbintrunc_uint_ucast bit_simps) lemma scast_ucast_high_bits: \scast (ucast w :: 'b::len word) = w \ (\ i \ {LENGTH('b) ..< size w}. bit w i = bit w (LENGTH('b) - 1))\ proof (cases \LENGTH('a) \ LENGTH('b)\) case True moreover define m where \m = LENGTH('b) - LENGTH('a)\ ultimately have \LENGTH('b) = m + LENGTH('a)\ by simp then show ?thesis apply (simp_all add: signed_ucast_eq word_size) apply (rule bit_word_eqI) apply (simp add: bit_signed_take_bit_iff) done next case False define q where \q = LENGTH('b) - 1\ then have \LENGTH('b) = Suc q\ by simp moreover define m where \m = Suc LENGTH('a) - LENGTH('b)\ with False \LENGTH('b) = Suc q\ have \LENGTH('a) = m + q\ by (simp add: not_le) ultimately show ?thesis apply (simp_all add: signed_ucast_eq word_size) apply (transfer fixing: m q) apply (simp add: signed_take_bit_take_bit) apply rule apply (subst bit_eq_iff) apply (simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def) apply (auto simp add: Suc_le_eq) using less_imp_le_nat apply blast using less_imp_le_nat apply blast done qed lemma scast_ucast_mask_compare: "scast (ucast w :: 'b::len word) = w \ (w \ mask (LENGTH('b) - 1) \ NOT(mask (LENGTH('b) - 1)) \ w)" apply (clarsimp simp: le_mask_high_bits neg_mask_le_high_bits scast_ucast_high_bits word_size) apply (rule iffI; clarsimp) apply (rename_tac i j; case_tac "i = LENGTH('b) - 1"; case_tac "j = LENGTH('b) - 1") by auto lemma ucast_less_shiftl_helper': "\ LENGTH('b) + (a::nat) < LENGTH('a); 2 ^ (LENGTH('b) + a) \ n\ \ (ucast (x :: 'b::len word) << a) < (n :: 'a::len word)" apply (erule order_less_le_trans[rotated]) using ucast_less[where x=x and 'a='a] apply (simp only: shiftl_t2n field_simps) apply (rule word_less_power_trans2; simp) done end lemma ucast_ucast_mask2: "is_down (UCAST ('a \ 'b)) \ UCAST ('b::len \ 'c::len) (UCAST ('a::len \ 'b::len) x) = UCAST ('a \ 'c) (x AND mask LENGTH('b))" apply (simp flip: take_bit_eq_mask) apply transfer apply simp done lemma ucast_NOT: "ucast (NOT x) = NOT(ucast x) AND mask (LENGTH('a))" for x::"'a::len word" by (rule bit_word_eqI) (auto simp add: bit_simps) lemma ucast_NOT_down: "is_down UCAST('a::len \ 'b::len) \ UCAST('a \ 'b) (NOT x) = NOT(UCAST('a \ 'b) x)" by (rule bit_word_eqI) (auto simp add: bit_simps is_down.rep_eq) lemma upto_enum_step_shift: "\ is_aligned p n \ \ ([p , p + 2 ^ m .e. p + 2 ^ n - 1]) = map ((+) p) [0, 2 ^ m .e. 2 ^ n - 1]" apply (erule is_aligned_get_word_bits) prefer 2 apply (simp add: map_idI) apply (clarsimp simp: upto_enum_step_def) apply (frule is_aligned_no_overflow) apply (simp add: linorder_not_le [symmetric]) done lemma upto_enum_step_shift_red: "\ is_aligned p sz; sz < LENGTH('a); us \ sz \ \ [p :: 'a :: len word, p + 2 ^ us .e. p + 2 ^ sz - 1] = map (\x. p + of_nat x * 2 ^ us) [0 ..< 2 ^ (sz - us)]" apply (subst upto_enum_step_shift, assumption) apply (simp add: upto_enum_step_red) done lemma upto_enum_step_subset: "set [x, y .e. z] \ {x .. z}" apply (clarsimp simp: upto_enum_step_def linorder_not_less) apply (drule div_to_mult_word_lt) apply (rule conjI) apply (erule word_random[rotated]) apply simp apply (rule order_trans) apply (erule word_plus_mono_right) apply simp apply simp done lemma ucast_distrib: fixes M :: "'a::len word \ 'a::len word \ 'a::len word" fixes M' :: "'b::len word \ 'b::len word \ 'b::len word" fixes L :: "int \ int \ int" assumes lift_M: "\x y. uint (M x y) = L (uint x) (uint y) mod 2 ^ LENGTH('a)" assumes lift_M': "\x y. uint (M' x y) = L (uint x) (uint y) mod 2 ^ LENGTH('b)" assumes distrib: "\x y. (L (x mod (2 ^ LENGTH('b))) (y mod (2 ^ LENGTH('b)))) mod (2 ^ LENGTH('b)) = (L x y) mod (2 ^ LENGTH('b))" assumes is_down: "is_down (ucast :: 'a word \ 'b word)" shows "ucast (M a b) = M' (ucast a) (ucast b)" apply (simp only: ucast_eq) apply (subst lift_M) apply (subst of_int_uint [symmetric], subst lift_M') apply (metis local.distrib local.is_down take_bit_eq_mod ucast_down_wi uint_word_of_int_eq word_of_int_uint) done lemma ucast_down_add: "is_down (ucast:: 'a word \ 'b word) \ ucast ((a :: 'a::len word) + b) = (ucast a + ucast b :: 'b::len word)" by (rule ucast_distrib [where L="(+)"], (clarsimp simp: uint_word_ariths)+, presburger, simp) lemma ucast_down_minus: "is_down (ucast:: 'a word \ 'b word) \ ucast ((a :: 'a::len word) - b) = (ucast a - ucast b :: 'b::len word)" apply (rule ucast_distrib [where L="(-)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_diff_left_eq mod_diff_right_eq) apply simp done lemma ucast_down_mult: "is_down (ucast:: 'a word \ 'b word) \ ucast ((a :: 'a::len word) * b) = (ucast a * ucast b :: 'b::len word)" apply (rule ucast_distrib [where L="(*)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_mult_eq) apply simp done lemma scast_distrib: fixes M :: "'a::len word \ 'a::len word \ 'a::len word" fixes M' :: "'b::len word \ 'b::len word \ 'b::len word" fixes L :: "int \ int \ int" assumes lift_M: "\x y. uint (M x y) = L (uint x) (uint y) mod 2 ^ LENGTH('a)" assumes lift_M': "\x y. uint (M' x y) = L (uint x) (uint y) mod 2 ^ LENGTH('b)" assumes distrib: "\x y. (L (x mod (2 ^ LENGTH('b))) (y mod (2 ^ LENGTH('b)))) mod (2 ^ LENGTH('b)) = (L x y) mod (2 ^ LENGTH('b))" assumes is_down: "is_down (scast :: 'a word \ 'b word)" shows "scast (M a b) = M' (scast a) (scast b)" apply (subst (1 2 3) down_cast_same [symmetric]) apply (insert is_down) apply (clarsimp simp: is_down_def target_size source_size is_down) apply (rule ucast_distrib [where L=L, OF lift_M lift_M' distrib]) apply (insert is_down) apply (clarsimp simp: is_down_def target_size source_size is_down) done lemma scast_down_add: "is_down (scast:: 'a word \ 'b word) \ scast ((a :: 'a::len word) + b) = (scast a + scast b :: 'b::len word)" by (rule scast_distrib [where L="(+)"], (clarsimp simp: uint_word_ariths)+, presburger, simp) lemma scast_down_minus: "is_down (scast:: 'a word \ 'b word) \ scast ((a :: 'a::len word) - b) = (scast a - scast b :: 'b::len word)" apply (rule scast_distrib [where L="(-)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_diff_left_eq mod_diff_right_eq) apply simp done lemma scast_down_mult: "is_down (scast:: 'a word \ 'b word) \ scast ((a :: 'a::len word) * b) = (scast a * scast b :: 'b::len word)" apply (rule scast_distrib [where L="(*)"], (clarsimp simp: uint_word_ariths)+) apply (metis mod_mult_eq) apply simp done lemma scast_ucast_1: "\ is_down (ucast :: 'a word \ 'b word); is_down (ucast :: 'b word \ 'c word) \ \ (scast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi) lemma scast_ucast_3: "\ is_down (ucast :: 'a word \ 'c word); is_down (ucast :: 'b word \ 'c word) \ \ (scast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi) lemma scast_ucast_4: "\ is_up (ucast :: 'a word \ 'b word); is_down (ucast :: 'b word \ 'c word) \ \ (scast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi) lemma scast_scast_b: "\ is_up (scast :: 'a word \ 'b word) \ \ (scast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" by (metis scast_eq sint_up_scast) lemma ucast_scast_1: "\ is_down (scast :: 'a word \ 'b word); is_down (ucast :: 'b word \ 'c word) \ \ (ucast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" by (metis scast_eq ucast_down_wi) lemma ucast_scast_3: "\ is_down (scast :: 'a word \ 'c word); is_down (ucast :: 'b word \ 'c word) \ \ (ucast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" by (metis scast_eq ucast_down_wi) lemma ucast_scast_4: "\ is_up (scast :: 'a word \ 'b word); is_down (ucast :: 'b word \ 'c word) \ \ (ucast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" by (metis down_cast_same scast_eq sint_up_scast) lemma ucast_ucast_a: "\ is_down (ucast :: 'b word \ 'c word) \ \ (ucast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis down_cast_same ucast_eq ucast_down_wi) lemma ucast_ucast_b: "\ is_up (ucast :: 'a word \ 'b word) \ \ (ucast (ucast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = ucast a" by (metis ucast_up_ucast) lemma scast_scast_a: "\ is_down (scast :: 'b word \ 'c word) \ \ (scast (scast (a :: 'a::len word) :: 'b::len word) :: 'c::len word) = scast a" apply (simp only: scast_eq) apply (metis down_cast_same is_up_down scast_eq ucast_down_wi) done lemma scast_down_wi [OF refl]: "uc = scast \ is_down uc \ uc (word_of_int x) = word_of_int x" by (metis down_cast_same is_up_down ucast_down_wi) lemmas cast_simps = is_down is_up scast_down_add scast_down_minus scast_down_mult ucast_down_add ucast_down_minus ucast_down_mult scast_ucast_1 scast_ucast_3 scast_ucast_4 ucast_scast_1 ucast_scast_3 ucast_scast_4 ucast_ucast_a ucast_ucast_b scast_scast_a scast_scast_b ucast_down_wi scast_down_wi ucast_of_nat scast_of_nat uint_up_ucast sint_up_scast up_scast_surj up_ucast_surj lemma sdiv_word_max: "(sint (a :: ('a::len) word) sdiv sint (b :: ('a::len) word) < (2 ^ (size a - 1))) = ((a \ - (2 ^ (size a - 1)) \ (b \ -1)))" (is "?lhs = (\ ?a_int_min \ \ ?b_minus1)") proof (rule classical) assume not_thesis: "\ ?thesis" have not_zero: "b \ 0" using not_thesis by (clarsimp) let ?range = \{- (2 ^ (size a - 1))..<2 ^ (size a - 1)} :: int set\ have result_range: "sint a sdiv sint b \ ?range \ {2 ^ (size a - 1)}" using sdiv_word_min [of a b] sdiv_word_max [of a b] by auto have result_range_overflow: "(sint a sdiv sint b = 2 ^ (size a - 1)) = (?a_int_min \ ?b_minus1)" apply (rule iffI [rotated]) apply (clarsimp simp: signed_divide_int_def sgn_if word_size sint_int_min) apply (rule classical) apply (case_tac "?a_int_min") apply (clarsimp simp: word_size sint_int_min) apply (metis diff_0_right int_sdiv_negated_is_minus1 minus_diff_eq minus_int_code(2) power_eq_0_iff sint_minus1 zero_neq_numeral) apply (subgoal_tac "abs (sint a) < 2 ^ (size a - 1)") apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1] apply (clarsimp simp: word_size) apply (insert sdiv_int_range [where a="sint a" and b="sint b"])[1] apply auto apply (cases \size a\) apply simp_all apply (smt (z3) One_nat_def diff_Suc_1 signed_word_eqI sint_int_min sint_range_size wsst_TYs(3)) done have result_range_simple: "(sint a sdiv sint b \ ?range) \ ?thesis" apply (insert sdiv_int_range [where a="sint a" and b="sint b"]) apply (clarsimp simp: word_size sint_int_min) done show ?thesis apply (rule UnE [OF result_range result_range_simple]) apply simp apply (clarsimp simp: word_size) using result_range_overflow apply (clarsimp simp: word_size) done qed lemmas sdiv_word_min' = sdiv_word_min [simplified word_size, simplified] lemmas sdiv_word_max' = sdiv_word_max [simplified word_size, simplified] lemma signed_arith_ineq_checks_to_eq: "((- (2 ^ (size a - 1)) \ (sint a + sint b)) \ (sint a + sint b \ (2 ^ (size a - 1) - 1))) = (sint a + sint b = sint (a + b ))" "((- (2 ^ (size a - 1)) \ (sint a - sint b)) \ (sint a - sint b \ (2 ^ (size a - 1) - 1))) = (sint a - sint b = sint (a - b))" "((- (2 ^ (size a - 1)) \ (- sint a)) \ (- sint a) \ (2 ^ (size a - 1) - 1)) = ((- sint a) = sint (- a))" "((- (2 ^ (size a - 1)) \ (sint a * sint b)) \ (sint a * sint b \ (2 ^ (size a - 1) - 1))) = (sint a * sint b = sint (a * b))" "((- (2 ^ (size a - 1)) \ (sint a sdiv sint b)) \ (sint a sdiv sint b \ (2 ^ (size a - 1) - 1))) = (sint a sdiv sint b = sint (a sdiv b))" "((- (2 ^ (size a - 1)) \ (sint a smod sint b)) \ (sint a smod sint b \ (2 ^ (size a - 1) - 1))) = (sint a smod sint b = sint (a smod b))" by (auto simp: sint_word_ariths word_size signed_div_arith signed_mod_arith signed_take_bit_int_eq_self_iff intro: sym dest: sym) lemma signed_arith_sint: "((- (2 ^ (size a - 1)) \ (sint a + sint b)) \ (sint a + sint b \ (2 ^ (size a - 1) - 1))) \ sint (a + b) = (sint a + sint b)" "((- (2 ^ (size a - 1)) \ (sint a - sint b)) \ (sint a - sint b \ (2 ^ (size a - 1) - 1))) \ sint (a - b) = (sint a - sint b)" "((- (2 ^ (size a - 1)) \ (- sint a)) \ (- sint a) \ (2 ^ (size a - 1) - 1)) \ sint (- a) = (- sint a)" "((- (2 ^ (size a - 1)) \ (sint a * sint b)) \ (sint a * sint b \ (2 ^ (size a - 1) - 1))) \ sint (a * b) = (sint a * sint b)" "((- (2 ^ (size a - 1)) \ (sint a sdiv sint b)) \ (sint a sdiv sint b \ (2 ^ (size a - 1) - 1))) \ sint (a sdiv b) = (sint a sdiv sint b)" "((- (2 ^ (size a - 1)) \ (sint a smod sint b)) \ (sint a smod sint b \ (2 ^ (size a - 1) - 1))) \ sint (a smod b) = (sint a smod sint b)" by (subst (asm) signed_arith_ineq_checks_to_eq; simp)+ lemma nasty_split_lt: \x * 2 ^ n + (2 ^ n - 1) \ 2 ^ m - 1\ if \x < 2 ^ (m - n)\ \n \ m\ \m < LENGTH('a::len)\ for x :: \'a::len word\ proof - define q where \q = m - n\ with \n \ m\ have \m = q + n\ by simp with \x < 2 ^ (m - n)\ have *: \i < q\ if \bit x i\ for i using that by simp (metis bit_take_bit_iff take_bit_word_eq_self_iff) from \m = q + n\ have \push_bit n x OR mask n \ mask m\ by (auto simp add: le_mask_high_bits word_size bit_simps dest!: *) then have \push_bit n x + mask n \ mask m\ by (simp add: disjunctive_add bit_simps) then show ?thesis by (simp add: mask_eq_exp_minus_1 push_bit_eq_mult) qed lemma nasty_split_less: "\m \ n; n \ nm; nm < LENGTH('a::len); x < 2 ^ (nm - n)\ \ (x :: 'a word) * 2 ^ n + (2 ^ m - 1) < 2 ^ nm" apply (simp only: word_less_sub_le[symmetric]) apply (rule order_trans [OF _ nasty_split_lt]) apply (rule word_plus_mono_right) apply (rule word_sub_mono) apply (simp add: word_le_nat_alt) apply simp apply (simp add: word_sub_1_le[OF power_not_zero]) apply (simp add: word_sub_1_le[OF power_not_zero]) apply (rule is_aligned_no_wrap') apply (rule is_aligned_mult_triv2) apply simp apply (erule order_le_less_trans, simp) apply simp+ done end end diff --git a/thys/Word_Lib/Word_Lib_Sumo.thy b/thys/Word_Lib/Word_Lib_Sumo.thy --- a/thys/Word_Lib/Word_Lib_Sumo.thy +++ b/thys/Word_Lib/Word_Lib_Sumo.thy @@ -1,137 +1,136 @@ (* * Copyright Florian Haftmann * * SPDX-License-Identifier: BSD-2-Clause *) section \Ancient comprehensive Word Library\ theory Word_Lib_Sumo imports "HOL-Library.Word" Aligned Bit_Comprehension Bit_Shifts_Infix_Syntax Bits_Int Bitwise_Signed Bitwise Enumeration_Word Generic_set_bit Hex_Words Least_significant_bit More_Arithmetic More_Divides More_Sublist Even_More_List More_Misc Strict_part_mono Legacy_Aliases Most_significant_bit Next_and_Prev Norm_Words Reversed_Bit_Lists Rsplit Signed_Words Syntax_Bundles Typedef_Morphisms Type_Syntax Word_EqI Word_Lemmas Word_8 Word_16 Word_32 - Word_64 Word_Syntax Signed_Division_Word Singleton_Bit_Shifts More_Word_Operations Many_More begin unbundle bit_operations_syntax unbundle bit_projection_infix_syntax declare word_induct2[induct type] declare word_nat_cases[cases type] declare signed_take_bit_Suc [simp] (* these generate take_bit terms, which we often don't want for concrete lengths *) lemmas of_int_and_nat = unsigned_of_nat unsigned_of_int signed_of_int signed_of_nat bundle no_take_bit begin declare of_int_and_nat[simp del] end lemmas bshiftr1_def = bshiftr1_eq lemmas is_down_def = is_down_eq lemmas is_up_def = is_up_eq lemmas mask_def = mask_eq lemmas scast_def = scast_eq lemmas shiftl1_def = shiftl1_eq lemmas shiftr1_def = shiftr1_eq lemmas sshiftr1_def = sshiftr1_eq lemmas sshiftr_def = sshiftr_eq_funpow_sshiftr1 lemmas to_bl_def = to_bl_eq lemmas ucast_def = ucast_eq lemmas unat_def = unat_eq_nat_uint lemmas word_cat_def = word_cat_eq lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl lemmas word_rotl_def = word_rotl_eq lemmas word_rotr_def = word_rotr_eq lemmas word_sle_def = word_sle_eq lemmas word_sless_def = word_sless_eq lemmas uint_0 = uint_nonnegative lemmas uint_lt = uint_bounded lemmas uint_mod_same = uint_idem lemmas of_nth_def = word_set_bits_def lemmas of_nat_word_eq_iff = word_of_nat_eq_iff lemmas of_nat_word_eq_0_iff = word_of_nat_eq_0_iff lemmas of_int_word_eq_iff = word_of_int_eq_iff lemmas of_int_word_eq_0_iff = word_of_int_eq_0_iff lemmas word_next_def = word_next_unfold lemmas word_prev_def = word_prev_unfold lemmas is_aligned_def = is_aligned_iff_dvd_nat lemmas word_and_max_simps = word8_and_max_simp word16_and_max_simp word32_and_max_simp lemma distinct_lemma: "f x \ f y \ x \ y" by auto lemmas and_bang = word_and_nth lemmas sdiv_int_def = signed_divide_int_def lemmas smod_int_def = signed_modulo_int_def (* shortcut for some specific lengths *) lemma word_fixed_sint_1[simp]: "sint (1::8 word) = 1" "sint (1::16 word) = 1" "sint (1::32 word) = 1" "sint (1::64 word) = 1" by (auto simp: sint_word_ariths) declare of_nat_diff [simp] (* Haskellish names/syntax *) notation (input) bit ("testBit") lemmas cast_simps = cast_simps ucast_down_bl (* shadows the slightly weaker Word.nth_ucast *) lemma nth_ucast: "(ucast (w::'a::len word)::'b::len word) !! n = (w !! n \ n < min LENGTH('a) LENGTH('b))" by (auto simp add: bit_simps not_le dest: bit_imp_le_length) end