theory Reversed_Bit_Lists

lemma aligned_bl_add_size [OF refl]:
  "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
    take m (to_bl y) = replicate m False \<Longrightarrow>
    to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)" for x :: \<open>'a::len word\<close> apply (subgoal_tac "x AND y = 0") prefer 2 apply (rule word_bl.Rep_eqD) apply (simp add: bl_word_and) apply (rule align_lem_and [THEN trans]) apply (simp_all add: word_size)[5] apply simp apply (subst word_plus_and_or [symmetric]) apply (simp add : bl_word_or) apply (rule align_lem_or) apply (simp_all add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> x AND y = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> x AND y = 0
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> to_bl (x AND y) = to_bl 0
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> map2 (\<and>) (to_bl x) (to_bl y) = replicate LENGTH('a) False
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> length (to_bl x) = ?n4 + ?m4
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> length (to_bl y) = ?n4 + ?m4
 3. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> drop ?m4 (to_bl x) = replicate ?n4 False
 4. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> take ?m4 (to_bl y) = replicate ?m4 False
 5. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> replicate (?n4 + ?m4) False = replicate LENGTH('a) False
 6. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>LENGTH('a) - n = m; n \<le> LENGTH('a); drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False\<rbrakk> \<Longrightarrow> n + m = LENGTH('a)
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> to_bl ((x AND y) + (x OR y)) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> map2 (\<or>) (to_bl x) (to_bl y) = take m (to_bl x) @ drop m (to_bl y) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> length (to_bl x) = ?n88 + m
 2. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> length (to_bl y) = ?n88 + m
 3. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> drop m (to_bl x) = replicate ?n88 False
 4. \<lbrakk>size x - n = m; n \<le> size x; drop m (to_bl x) = replicate n False; take m (to_bl y) = replicate m False; x AND y = 0\<rbrakk> \<Longrightarrow> take m (to_bl y) = replicate m False proof (prove)
goal:
No subgoals!