# Theory WordBitwise

theory WordBitwise
imports Word
```(*  Title:      HOL/Word/WordBitwise.thy
Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
*)

theory WordBitwise
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)"

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)"

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 word_eq_rbl_eq: "x = y ⟷ rev (to_bl x) = rev (to_bl y)"
by simp

lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (∨) (rev (to_bl x)) (rev (to_bl y))"
by (simp add: map2_def zip_rev bl_word_or rev_map)

lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (∧) (rev (to_bl x)) (rev (to_bl y))"
by (simp add: map2_def zip_rev bl_word_and rev_map)

lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (≠) (rev (to_bl x)) (rev (to_bl y))"
by (simp add: map2_def zip_rev bl_word_xor rev_map)

lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"

lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))"
by simp

lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (len_of TYPE('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 "len_of TYPE('a)")
apply simp
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))"

"(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)"

"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
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 (drule_tac x=False in spec)
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 [] = []"

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"

lemma twos_complement: "- x = word_succ (NOT x)"
using arg_cong[OF word_add_not[where x=x], where f="λa. a - x + 1"]

lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
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::len0 word)) =
takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"

lemma rbl_word_slice:
"rev (to_bl (slice n w :: 'a::len0 word)) =
takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
apply (simp add: slice_take word_rev_tf rev_take)
apply (cases "n < len_of TYPE('b)", simp_all)
done

lemma rbl_word_ucast:
"rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (len_of TYPE('a)) (rev (to_bl x))"
apply (cases "len_of TYPE('a) < len_of TYPE('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]"

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"

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 "len_of TYPE('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::len0 word) !! n = (n < len_of TYPE('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 < len_of TYPE('b) ∧
(if n < len_of TYPE('a) - 1 then x !! n
else x !! (len_of TYPE('a) - 1)))"

lemma rbl_word_scast:
"rev (to_bl (scast x :: 'a::len word)) = takefill_last False (len_of TYPE('a)) (rev (to_bl x))"
apply (rule nth_equalityI)
apply (clarsimp simp: nth_scast takefill_last_def
nth_takefill word_size nth_rev to_bl_nth)
apply (cases "len_of TYPE('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 = []"

lemma takefill_le2: "length xs ≤ n ⟹ takefill x m (takefill x n xs) = takefill x m xs"

lemma take_rbl_plus: "∀n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)"
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"

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

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
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)
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 (rule conj_cong[OF refl])
apply (cases "xs = ys")
apply blast
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)
done

lemma word_le_rbl: "x ≤ y ⟷ rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
for x y :: "'a::len0 word"

lemma word_less_rbl: "x < y ⟷ rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
for x y :: "'a::len0 word"

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 (rule conjI)
apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
apply (rule notI, drule word_eqD[where x="size x - 1"])
apply (simp add: msb_nth word_ops_nth_size word_size)
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 (erule notE[OF leD])
apply (rule order_less_le_trans[OF _ uint_ge_0])
apply simp
done

lemma word_sless_msb_less: "x <s y ⟷ (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)"

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 (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 <s y ⟷ 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 (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))"
apply simp_all
apply (simp_all only: bin_to_bl_aux_alt)
apply (simp_all)
done

lemma to_bl_upt: "to_bl x = rev (map ((!!) x) [0 ..< size x])"
apply (rule nth_equalityI)
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]"

lemma upt_eq_list_intros:
"j ≤ i ⟹ [i ..< j] = []"
"i = x ⟹ x < j ⟹ [x + 1 ..< j] = xs ⟹ [i ..< j] = (x # xs)"

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 =
@{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
map simpset_of [
@{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},
@{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
@{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
@{thms list.simps split_conv replicate.simps list.map
zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
foldr.simps map2_Cons map2_Nil 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}
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
```