# HG changeset patch # User haftmann # Date 1593624731 0 # Node ID a1cf296a7786f5b3f5a26fa683af12cecdd21194 # Parent 10a8d943a8d8d611c33572467b0be61c410a669f moved to Word_Lib diff -r 10a8d943a8d8 -r a1cf296a7786 NEWS --- a/NEWS Wed Jul 01 17:32:10 2020 +0000 +++ b/NEWS Wed Jul 01 17:32:11 2020 +0000 @@ -57,6 +57,9 @@ generic algebraic bit operations from HOL-Library.Bit_Operations. INCOMPATIBILITY. +* Session HOL-Word: Theory "Word_Bitwise" has been moved to AFP entry +Word_Lib as theory "Bitwise". INCOMPATIBILITY. + * Session HOL-Word: Compound operation "bin_split" simplifies by default into its components "drop_bit" and "take_bit". INCOMPATIBILITY. diff -r 10a8d943a8d8 -r a1cf296a7786 src/HOL/Word/More_Word.thy --- a/src/HOL/Word/More_Word.thy Wed Jul 01 17:32:10 2020 +0000 +++ b/src/HOL/Word/More_Word.thy Wed Jul 01 17:32:11 2020 +0000 @@ -1,12 +1,11 @@ (* Title: HOL/Word/More_Word.thy *) -section \Comprehensive Word Library\ +section \Ancient comprehensive Word Library\ theory More_Word imports Word - Word_Bitwise begin end diff -r 10a8d943a8d8 -r a1cf296a7786 src/HOL/Word/Word_Bitwise.thy --- a/src/HOL/Word/Word_Bitwise.thy Wed Jul 01 17:32:10 2020 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,526 +0,0 @@ -(* Title: HOL/Word/Word_Bitwise.thy - Authors: Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen -*) - -theory Word_Bitwise - imports Word -begin - -text \Helper constants used in defining addition\ - -definition xor3 :: "bool \ bool \ bool \ bool" - where "xor3 a b c = (a = (b = c))" - -definition carry :: "bool \ bool \ bool \ bool" - where "carry a b c = ((a \ (b \ c)) \ (b \ c))" - -lemma carry_simps: - "carry True a b = (a \ b)" - "carry a True b = (a \ b)" - "carry a b True = (a \ b)" - "carry False a b = (a \ b)" - "carry a False b = (a \ b)" - "carry a b False = (a \ b)" - by (auto simp add: carry_def) - -lemma xor3_simps: - "xor3 True a b = (a = b)" - "xor3 a True b = (a = b)" - "xor3 a b True = (a = b)" - "xor3 False a b = (a \ b)" - "xor3 a False b = (a \ b)" - "xor3 a b False = (a \ b)" - by (simp_all add: xor3_def) - -text \Breaking up word equalities into equalities on their - bit lists. Equalities are generated and manipulated in the - reverse order to \<^const>\to_bl\.\ - -lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))" - by simp - -lemma rbl_word_1: "rev (to_bl (1 :: 'a::len word)) = takefill False (LENGTH('a)) [True]" - apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans) - apply simp - apply (simp only: rtb_rbl_ariths(1)[OF refl]) - apply simp - apply (case_tac "LENGTH('a)") - apply simp - apply (simp add: takefill_alt) - done - -lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))" - by (simp add: split_def) - -lemma rbl_add_carry_Cons: - "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) = - xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)" - by (simp add: carry_def xor3_def) - -lemma rbl_add_suc_carry_fold: - "length xs = length ys \ - \car. (if car then rbl_succ else id) (rbl_add xs ys) = - (foldr (\(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\_. [])) car" - apply (erule list_induct2) - apply simp - apply (simp only: rbl_add_carry_Cons) - apply simp - done - -lemma to_bl_plus_carry: - "to_bl (x + y) = - rev (foldr (\(x, y) res car. xor3 x y car # res (carry x y car)) - (rev (zip (to_bl x) (to_bl y))) (\_. []) False)" - using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"] - apply (simp add: word_add_rbl[OF refl refl]) - apply (drule_tac x=False in spec) - apply (simp add: zip_rev) - done - -definition "rbl_plus cin xs ys = - foldr (\(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\_. []) cin" - -lemma rbl_plus_simps: - "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys" - "rbl_plus cin [] ys = []" - "rbl_plus cin xs [] = []" - by (simp_all add: rbl_plus_def) - -lemma rbl_word_plus: "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))" - by (simp add: rbl_plus_def to_bl_plus_carry zip_rev) - -definition "rbl_succ2 b xs = (if b then rbl_succ xs else xs)" - -lemma rbl_succ2_simps: - "rbl_succ2 b [] = []" - "rbl_succ2 b (x # xs) = (b \ x) # rbl_succ2 (x \ b) xs" - by (simp_all add: rbl_succ2_def) - -lemma twos_complement: "- x = word_succ (NOT x)" - using arg_cong[OF word_add_not[where x=x], where f="\a. a - x + 1"] - by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not) - -lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))" - for x :: \'a::len word\ - by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def) - -lemma rbl_word_cat: - "rev (to_bl (word_cat x y :: 'a::len word)) = - takefill False (LENGTH('a)) (rev (to_bl y) @ rev (to_bl x))" - by (simp add: word_cat_bl word_rev_tf) - -lemma rbl_word_slice: - "rev (to_bl (slice n w :: 'a::len word)) = - takefill False (LENGTH('a)) (drop n (rev (to_bl w)))" - apply (simp add: slice_take word_rev_tf rev_take) - apply (cases "n < LENGTH('b)", simp_all) - done - -lemma rbl_word_ucast: - "rev (to_bl (ucast x :: 'a::len word)) = takefill False (LENGTH('a)) (rev (to_bl x))" - apply (simp add: to_bl_ucast takefill_alt) - apply (simp add: rev_drop) - apply (cases "LENGTH('a) < LENGTH('b)") - apply simp_all - done - -lemma rbl_shiftl: - "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))" - by (simp add: bl_shiftl takefill_alt word_size rev_drop) - -lemma rbl_shiftr: - "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))" - by (simp add: shiftr_slice rbl_word_slice word_size) - -definition "drop_nonempty v n xs = (if n < length xs then drop n xs else [last (v # xs)])" - -lemma drop_nonempty_simps: - "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs" - "drop_nonempty v 0 (x # xs) = (x # xs)" - "drop_nonempty v n [] = [v]" - by (simp_all add: drop_nonempty_def) - -definition "takefill_last x n xs = takefill (last (x # xs)) n xs" - -lemma takefill_last_simps: - "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs" - "takefill_last z 0 xs = []" - "takefill_last z n [] = replicate n z" - by (simp_all add: takefill_last_def) (simp_all add: takefill_alt) - -lemma rbl_sshiftr: - "rev (to_bl (w >>> n)) = takefill_last False (size w) (drop_nonempty False n (rev (to_bl w)))" - apply (cases "n < size w") - apply (simp add: bl_sshiftr takefill_last_def word_size - takefill_alt rev_take last_rev - drop_nonempty_def) - apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))") - apply (simp add: word_size takefill_last_def takefill_alt - last_rev word_msb_alt word_rev_tf - drop_nonempty_def take_Cons') - apply (case_tac "LENGTH('a)", simp_all) - apply (rule word_eqI) - apply (simp add: nth_sshiftr word_size test_bit_of_bl - msb_nth) - done - -lemma nth_word_of_int: - "(word_of_int x :: 'a::len word) !! n = (n < LENGTH('a) \ bin_nth x n)" - apply (simp add: test_bit_bl word_size to_bl_of_bin) - apply (subst conj_cong[OF refl], erule bin_nth_bl) - apply auto - done - -lemma nth_scast: - "(scast (x :: 'a::len word) :: 'b::len word) !! n = - (n < LENGTH('b) \ - (if n < LENGTH('a) - 1 then x !! n - else x !! (LENGTH('a) - 1)))" - by (simp add: scast_def nth_sint) - -lemma rbl_word_scast: - "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (LENGTH('a)) (rev (to_bl x))" - apply (rule nth_equalityI) - apply (simp add: word_size takefill_last_def) - apply (clarsimp simp: nth_scast takefill_last_def - nth_takefill word_size nth_rev to_bl_nth) - apply (cases "LENGTH('b)") - apply simp - apply (clarsimp simp: less_Suc_eq_le linorder_not_less - last_rev word_msb_alt[symmetric] - msb_nth) - done - -definition rbl_mul :: "bool list \ bool list \ bool list" - where "rbl_mul xs ys = foldr (\x sm. rbl_plus False (map ((\) x) ys) (False # sm)) xs []" - -lemma rbl_mul_simps: - "rbl_mul (x # xs) ys = rbl_plus False (map ((\) x) ys) (False # rbl_mul xs ys)" - "rbl_mul [] ys = []" - by (simp_all add: rbl_mul_def) - -lemma takefill_le2: "length xs \ n \ takefill x m (takefill x n xs) = takefill x m xs" - by (simp add: takefill_alt replicate_add[symmetric]) - -lemma take_rbl_plus: "\n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)" - apply (simp add: rbl_plus_def take_zip[symmetric]) - apply (rule_tac list="zip xs ys" in list.induct) - apply simp - apply (clarsimp simp: split_def) - apply (case_tac n, simp_all) - done - -lemma word_rbl_mul_induct: - "length xs \ size y \ - rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))" - for y :: "'a::len word" -proof (induct xs) - case Nil - show ?case by (simp add: rbl_mul_simps) -next - case (Cons z zs) - - have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))" - for x y :: "'a word" - by (simp add: rbl_word_plus[symmetric]) - - have mult_bit: "to_bl (of_bl [z] * y) = map ((\) z) (to_bl y)" - by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong) - - have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs - by (simp add: shiftl_t2n) - - have zip_take_triv: "\xs ys n. n = length ys \ zip (take n xs) ys = zip xs ys" - by (rule nth_equalityI) simp_all - - from Cons show ?case - apply (simp add: trans [OF of_bl_append add.commute] - rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl) - apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def) - apply (simp add: rbl_plus_def zip_take_triv) - done -qed - -lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))" - for x :: "'a::len word" - using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size) - -text \Breaking up inequalities into bitlist properties.\ - -definition - "rev_bl_order F xs ys = - (length xs = length ys \ - ((xs = ys \ F) - \ (\n < length xs. drop (Suc n) xs = drop (Suc n) ys - \ \ xs ! n \ ys ! n)))" - -lemma rev_bl_order_simps: - "rev_bl_order F [] [] = F" - "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \ \ x) \ ((y \ \ x) \ F)) xs ys" - apply (simp_all add: rev_bl_order_def) - apply (rule conj_cong[OF refl]) - apply (cases "xs = ys") - apply (simp add: nth_Cons') - apply blast - apply (simp add: nth_Cons') - apply safe - apply (rule_tac x="n - 1" in exI) - apply simp - apply (rule_tac x="Suc n" in exI) - apply simp - done - -lemma rev_bl_order_rev_simp: - "length xs = length ys \ - rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \ \ x) \ ((y \ \ x) \ rev_bl_order F xs ys))" - by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps) - -lemma rev_bl_order_bl_to_bin: - "length xs = length ys \ - rev_bl_order True xs ys = (bl_to_bin (rev xs) \ bl_to_bin (rev ys)) \ - rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))" - apply (induct xs ys rule: list_induct2) - apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat) - apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def) - done - -lemma word_le_rbl: "x \ y \ rev_bl_order True (rev (to_bl x)) (rev (to_bl y))" - for x y :: "'a::len word" - by (simp add: rev_bl_order_bl_to_bin word_le_def) - -lemma word_less_rbl: "x < y \ rev_bl_order False (rev (to_bl x)) (rev (to_bl y))" - for x y :: "'a::len word" - by (simp add: word_less_alt rev_bl_order_bl_to_bin) - -lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)" - apply (cases "msb x") - apply (rule word_sint.Abs_eqD[where 'a='a], simp_all) - apply (simp add: word_size wi_hom_syms word_of_int_2p_len) - apply (simp add: sints_num word_size) - apply (rule conjI) - apply (simp add: le_diff_eq') - apply (rule order_trans[where y="2 ^ (LENGTH('a) - 1)"]) - apply (simp add: power_Suc[symmetric]) - apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric]) - apply (rule notI, drule word_eqD[where x="size x - 1"]) - apply (simp add: msb_nth word_ops_nth_size word_size) - apply (simp add: order_less_le_trans[where y=0]) - apply (rule word_uint.Abs_eqD[where 'a='a], simp_all) - apply (simp add: linorder_not_less uints_num word_msb_sint) - apply (rule order_less_le_trans[OF sint_lt]) - apply simp - done - -lemma word_sle_msb_le: "x <=s y \ (msb y \ msb x) \ ((msb x \ \ msb y) \ x \ y)" - apply (simp add: word_sle_def 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_def word_sle_msb_le) - -definition "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])" - -lemma map_last_simps: - "map_last f [] = []" - "map_last f [x] = [f x]" - "map_last f (x # y # zs) = x # map_last f (y # zs)" - by (simp_all add: map_last_def) - -lemma word_sle_rbl: - "x <=s y \ rev_bl_order True (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))" - using word_msb_alt[where w=x] word_msb_alt[where w=y] - apply (simp add: word_sle_msb_le word_le_rbl) - apply (subgoal_tac "length (to_bl x) = length (to_bl y)") - apply (cases "to_bl x", simp) - apply (cases "to_bl y", simp) - apply (clarsimp simp: map_last_def rev_bl_order_rev_simp) - apply auto - done - -lemma word_sless_rbl: - "x rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))" - using word_msb_alt[where w=x] word_msb_alt[where w=y] - apply (simp add: word_sless_msb_less word_less_rbl) - apply (subgoal_tac "length (to_bl x) = length (to_bl y)") - apply (cases "to_bl x", simp) - apply (cases "to_bl y", simp) - apply (clarsimp simp: map_last_def rev_bl_order_rev_simp) - apply auto - done - -text \Lemmas for unpacking \<^term>\rev (to_bl n)\ for numerals n and also - for irreducible values and expressions.\ - -lemma rev_bin_to_bl_simps: - "rev (bin_to_bl 0 x) = []" - "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))" - "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))" - "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False" - "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))" - "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) = - True # rev (bin_to_bl n (- numeral (nm + num.One)))" - "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True" - "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) = - True # rev (bin_to_bl n (- numeral (nm + num.One)))" - "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) = - False # rev (bin_to_bl n (- numeral (nm + num.One)))" - "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) = - False # rev (bin_to_bl n (- numeral num.One))" - by (simp_all add: bin_to_bl_aux_append bin_to_bl_zero_aux bin_to_bl_minus1_aux replicate_append_same) - -lemma to_bl_upt: "to_bl x = rev (map ((!!) x) [0 ..< size x])" - apply (rule nth_equalityI) - apply (simp add: word_size) - apply (auto simp: to_bl_nth word_size nth_rev) - done - -lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]" - by (simp add: to_bl_upt) - -lemma upt_eq_list_intros: - "j \ i \ [i ..< j] = []" - "i = x \ x < j \ [x + 1 ..< j] = xs \ [i ..< j] = (x # xs)" - by (simp_all add: upt_eq_Cons_conv) - - -subsection \Tactic definition\ - -ML \ -structure Word_Bitwise_Tac = -struct - -val word_ss = simpset_of \<^theory_context>\Word\; - -fun mk_nat_clist ns = - fold_rev (Thm.mk_binop \<^cterm>\Cons :: nat \ _\) - ns \<^cterm>\[] :: nat list\; - -fun upt_conv ctxt ct = - case Thm.term_of ct of - (\<^const>\upt\ $ n $ m) => - let - val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m); - val ns = map (Numeral.mk_cnumber \<^ctyp>\nat\) (i upto (j - 1)) - |> mk_nat_clist; - val prop = - Thm.mk_binop \<^cterm>\(=) :: nat list \ _\ ct ns - |> Thm.apply \<^cterm>\Trueprop\; - in - try (fn () => - Goal.prove_internal ctxt [] prop - (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1 - ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) () - end - | _ => NONE; - -val expand_upt_simproc = - Simplifier.make_simproc \<^context> "expand_upt" - {lhss = [\<^term>\upt x y\], proc = K upt_conv}; - -fun word_len_simproc_fn ctxt ct = - (case Thm.term_of ct of - Const (\<^const_name>\len_of\, _) $ t => - (let - val T = fastype_of t |> dest_Type |> snd |> the_single - val n = Numeral.mk_cnumber \<^ctyp>\nat\ (Word_Lib.dest_binT T); - val prop = - Thm.mk_binop \<^cterm>\(=) :: nat \ _\ ct n - |> Thm.apply \<^cterm>\Trueprop\; - in - Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1)) - |> mk_meta_eq |> SOME - end handle TERM _ => NONE | TYPE _ => NONE) - | _ => NONE); - -val word_len_simproc = - Simplifier.make_simproc \<^context> "word_len" - {lhss = [\<^term>\len_of x\], proc = K word_len_simproc_fn}; - -(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2, - or just 5 (discarding nat) when n_sucs = 0 *) - -fun nat_get_Suc_simproc_fn n_sucs ctxt ct = - let - val (f $ arg) = Thm.term_of ct; - val n = - (case arg of \<^term>\nat\ $ n => n | n => n) - |> HOLogic.dest_number |> snd; - val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) else (n, 0); - val arg' = funpow i HOLogic.mk_Suc (HOLogic.mk_number \<^typ>\nat\ j); - val _ = if arg = arg' then raise TERM ("", []) else (); - fun propfn g = - HOLogic.mk_eq (g arg, g arg') - |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt; - val eq1 = - Goal.prove_internal ctxt [] (propfn I) - (K (simp_tac (put_simpset word_ss ctxt) 1)); - in - Goal.prove_internal ctxt [] (propfn (curry (op $) f)) - (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1)) - |> mk_meta_eq |> SOME - end handle TERM _ => NONE; - -fun nat_get_Suc_simproc n_sucs ts = - Simplifier.make_simproc \<^context> "nat_get_Suc" - {lhss = map (fn t => t $ \<^term>\n :: nat\) ts, - proc = K (nat_get_Suc_simproc_fn n_sucs)}; - -val no_split_ss = - simpset_of (put_simpset HOL_ss \<^context> - |> Splitter.del_split @{thm if_split}); - -val expand_word_eq_sss = - (simpset_of (put_simpset HOL_basic_ss \<^context> addsimps - @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}), - map simpset_of [ - put_simpset no_split_ss \<^context> addsimps - @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not - rbl_word_neg bl_word_sub rbl_word_xor - rbl_word_cat rbl_word_slice rbl_word_scast - rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr - rbl_word_if}, - put_simpset no_split_ss \<^context> addsimps - @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1}, - put_simpset no_split_ss \<^context> addsimps - @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size} - addsimprocs [word_len_simproc], - put_simpset no_split_ss \<^context> addsimps - @{thms list.simps split_conv replicate.simps list.map - zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil - foldr.simps list.map zip.simps(1) zip_Nil zip_Cons_Cons takefill_Suc_Cons - takefill_Suc_Nil takefill.Z rbl_succ2_simps - rbl_plus_simps rev_bin_to_bl_simps append.simps - takefill_last_simps drop_nonempty_simps - rev_bl_order_simps} - addsimprocs [expand_upt_simproc, - nat_get_Suc_simproc 4 - [\<^term>\replicate\, \<^term>\takefill x\, - \<^term>\drop\, \<^term>\bin_to_bl\, - \<^term>\takefill_last x\, - \<^term>\drop_nonempty x\]], - put_simpset no_split_ss \<^context> addsimps @{thms xor3_simps carry_simps if_bool_simps} - ]) - -fun tac ctxt = - let - val (ss, sss) = expand_word_eq_sss; - in - foldr1 (op THEN_ALL_NEW) - ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) :: - map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss) - end; - -end -\ - -method_setup word_bitwise = - \Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\ - "decomposer for word equalities and inequalities into bit propositions" - -end diff -r 10a8d943a8d8 -r a1cf296a7786 src/HOL/Word/Word_Examples.thy --- a/src/HOL/Word/Word_Examples.thy Wed Jul 01 17:32:10 2020 +0000 +++ b/src/HOL/Word/Word_Examples.thy Wed Jul 01 17:32:11 2020 +0000 @@ -7,7 +7,7 @@ section "Examples of word operations" theory Word_Examples - imports Word_Bitwise + imports Word begin type_synonym word32 = "32 word" @@ -165,42 +165,4 @@ finally show ?thesis . qed -text "alternative proof using bitwise expansion" - -lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" - by word_bitwise - -text "more proofs using bitwise expansion" - -lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)" - for x :: "10 word" - by word_bitwise - -lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3" - for x :: "12 word" - by word_bitwise - -text "some problems require further reasoning after bit expansion" - -lemma "x \ 42 \ x \ 89" - for x :: "8 word" - apply word_bitwise - apply blast - done - -lemma "(x AND 1023) = 0 \ x \ -1024" - for x :: word32 - apply word_bitwise - apply clarsimp - done - -text "operations like shifts by non-numerals will expose some internal list - representations but may still be easy to solve" - -lemma shiftr_overflow: "32 \ a \ b >> a = 0" - for b :: word32 - apply word_bitwise - apply simp - done - end