theory Bitwise

lemma word_rbl_mul_induct:
  "length xs \<le> size y \<Longrightarrow>
    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 ((\<and>) 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: push_bit_eq_mult shiftl_def) have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> 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) apply (simp add: zip_take_triv) apply (simp only: mult.commute [of _ 2] to_bl_double_eq) apply (simp flip: butlast_rev add: take_butlast) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))) proof (state)
goal (2 subgoals):
 1. length [] \<le> size y \<Longrightarrow> rbl_mul [] (rev (to_bl y)) = take (length []) (rev (to_bl (of_bl (rev []) * y)))
 2. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (state)
this:
length [] \<le> size y

goal (2 subgoals):
 1. length [] \<le> size y \<Longrightarrow> rbl_mul [] (rev (to_bl y)) = take (length []) (rev (to_bl (of_bl (rev []) * y)))
 2. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (prove)
goal (1 subgoal):
 1. rbl_mul [] (rev (to_bl y)) = take (length []) (rev (to_bl (of_bl (rev []) * y))) proof (state)
this:
rbl_mul [] (rev (to_bl y)) = take (length []) (rev (to_bl (of_bl (rev []) * y)))

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (state)
this:
length zs \<le> size y \<Longrightarrow> rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y)))
length (z # zs) \<le> size y

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (prove)
goal (1 subgoal):
 1. to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y))) proof (state)
this:
to_bl (?x + ?y) = rev (rbl_plus False (rev (to_bl ?x)) (rev (to_bl ?y)))

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (prove)
goal (1 subgoal):
 1. to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y) proof (state)
this:
to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (prove)
goal (1 subgoal):
 1. of_bl xs * 2 * y = of_bl xs * y << 1 proof (state)
this:
of_bl ?xs * 2 * y = of_bl ?xs * y << 1

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (prove)
goal (1 subgoal):
 1. \<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys proof (state)
this:
?n = length ?ys \<Longrightarrow> zip (take ?n ?xs) ?ys = zip ?xs ?ys

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>length xs \<le> size y \<Longrightarrow> rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y))); length (a # xs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_mul (a # xs) (rev (to_bl y)) = take (length (a # xs)) (rev (to_bl (of_bl (rev (a # xs)) * y))) proof (chain)
picking this:
length zs \<le> size y \<Longrightarrow> rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y)))
length (z # zs) \<le> size y proof (prove)
using this:
length zs \<le> size y \<Longrightarrow> rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y)))
length (z # zs) \<le> size y

goal (1 subgoal):
 1. rbl_mul (z # zs) (rev (to_bl y)) = take (length (z # zs)) (rev (to_bl (of_bl (rev (z # zs)) * y))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y))); Suc (length zs) \<le> size y\<rbrakk> \<Longrightarrow> rbl_plus False (map ((\<and>) z) (rev (to_bl y))) (False # take (length zs) (rev (to_bl (of_bl (rev zs) * y)))) = take (Suc (length zs)) (rbl_plus False (rev (map ((\<and>) z) (to_bl y))) (rev (to_bl (of_bl (rev zs) * y * 2)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y))); Suc (length zs) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> rbl_plus False (map ((\<and>) z) (rev (to_bl y))) (False # take (length zs) (rev (to_bl (of_bl (rev zs) * y)))) = rbl_plus False (take (Suc (length zs)) (map ((\<and>) z) (rev (to_bl y)))) (take (Suc (length zs)) (rev (to_bl (of_bl (rev zs) * y * 2)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y))); Suc (length zs) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (map ((\<and>) z) (rev (to_bl y))) (False # take (length zs) (rev (to_bl (of_bl (rev zs) * y))))) (\<lambda>_. []) False = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (take (Suc (length zs)) (map ((\<and>) z) (rev (to_bl y)))) (take (Suc (length zs)) (rev (to_bl (of_bl (rev zs) * y * 2))))) (\<lambda>_. []) False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y))); Suc (length zs) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (map ((\<and>) z) (rev (to_bl y))) (False # take (length zs) (rev (to_bl (of_bl (rev zs) * y))))) (\<lambda>_. []) False = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (map ((\<and>) z) (rev (to_bl y))) (take (Suc (length zs)) (rev (to_bl (of_bl (rev zs) * y * 2))))) (\<lambda>_. []) False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rbl_mul zs (rev (to_bl y)) = take (length zs) (rev (to_bl (of_bl (rev zs) * y))); Suc (length zs) \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (map ((\<and>) z) (rev (to_bl y))) (False # take (length zs) (rev (to_bl (of_bl (rev zs) * y))))) (\<lambda>_. []) False = foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip (map ((\<and>) z) (rev (to_bl y))) (take (Suc (length zs)) (rev (tl (to_bl (of_bl (rev zs) * y)) @ [False])))) (\<lambda>_. []) False proof (prove)
goal:
No subgoals! proof (state)
this:
rbl_mul (z # zs) (rev (to_bl y)) = take (length (z # zs)) (rev (to_bl (of_bl (rev (z # zs)) * y)))

goal:
No subgoals!