[STATEMENT]
lemma bin_nth_of_bl_aux:
  "bit (bl_to_bin_aux bl w) n =
    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bit w (n - size bl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl))
[PROOF STEP]
apply (induction bl arbitrary: w)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. bit (bl_to_bin_aux [] w) n = (n < length [] \<and> rev [] ! n \<or> length [] \<le> n \<and> bit w (n - length []))
 2. \<And>a bl w. (\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl))) \<Longrightarrow> bit (bl_to_bin_aux (a # bl) w) n = (n < length (a # bl) \<and> rev (a # bl) ! n \<or> length (a # bl) \<le> n \<and> bit w (n - length (a # bl)))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bl w. (\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl))) \<Longrightarrow> (a \<longrightarrow> (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit (1 + 2 * w) (n - length bl)) = (n < Suc (length bl) \<and> (rev bl @ [True]) ! n \<or> Suc (length bl) \<le> n \<and> bit w (n - Suc (length bl)))) \<and> (\<not> a \<longrightarrow> (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit (2 * w) (n - length bl)) = (n < Suc (length bl) \<and> (rev bl @ [False]) ! n \<or> Suc (length bl) \<le> n \<and> bit w (n - Suc (length bl))))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (32 subgoals):
 1. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 2. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 3. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 4. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 5. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 6. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 7. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 8. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 9. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < Suc (length bl); (rev bl @ [True]) ! n; \<not> length bl \<le> n\<rbrakk> \<Longrightarrow> n < length bl
 10. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < Suc (length bl); (rev bl @ [True]) ! n; \<not> length bl \<le> n\<rbrakk> \<Longrightarrow> rev bl ! n
A total of 32 subgoals...
[PROOF STEP]
apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_nth_of_bl: "bit (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)
[PROOF STEP]
by (simp add: bl_to_bin_def bin_nth_of_bl_aux)


[STATEMENT]
lemma bin_nth_bl: "n < m \<Longrightarrow> bit w n = nth (rev (bin_to_bl m w)) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> bit w n = rev (bin_to_bl m w) ! n
[PROOF STEP]
by (metis bin_bl_bin bin_nth_of_bl nth_bintr size_bin_to_bl)


[STATEMENT]
lemma nth_bin_to_bl_aux:
  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
    (if n < m then bit w (m - 1 - n) else bl ! (n - m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m))
[PROOF STEP]
apply (induction bl arbitrary: w)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. n < m + length [] \<Longrightarrow> bin_to_bl_aux m w [] ! n = (if n < m then bit w (m - 1 - n) else [] ! (n - m))
 2. \<And>a bl w. \<lbrakk>\<And>w. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m)); n < m + length (a # bl)\<rbrakk> \<Longrightarrow> bin_to_bl_aux m w (a # bl) ! n = (if n < m then bit w (m - 1 - n) else (a # bl) ! (n - m))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. n < m \<Longrightarrow> bin_to_bl_aux m w [] ! n = bit w (m - Suc n)
 2. \<And>a bl w. \<lbrakk>\<And>w. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m)); n < Suc (m + length bl)\<rbrakk> \<Longrightarrow> (n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = bit w (m - Suc n)) \<and> (\<not> n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = (a # bl) ! (n - m))
[PROOF STEP]
apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bl w. \<lbrakk>\<And>w. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m)); n < Suc (m + length bl)\<rbrakk> \<Longrightarrow> (n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = bit w (m - Suc n)) \<and> (\<not> n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = (a # bl) ! (n - m))
[PROOF STEP]
apply (metis One_nat_def Suc_pred add_diff_cancel_left'
     add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
     diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
     less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bit w (m - Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> bin_to_bl m w ! n = bit w (m - Suc n)
[PROOF STEP]
by (simp add: bin_to_bl_def nth_bin_to_bl_aux)


[STATEMENT]
lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (takefill False n bl) = length (rev (bin_to_bl n (bl_to_bin (rev bl))))
 2. \<And>i. i < length (takefill False n bl) \<Longrightarrow> takefill False n bl ! i = rev (bin_to_bl n (bl_to_bin (rev bl))) ! i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (takefill False n bl) \<Longrightarrow> takefill False n bl ! i = rev (bin_to_bl n (bl_to_bin (rev bl))) ! i
[PROOF STEP]
apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))
[PROOF STEP]
by (simp add: takefill_bintrunc)


[STATEMENT]
lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs
[PROOF STEP]
proof (induction bs arbitrary: w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w. bl_to_bin_aux [] w < (w + 1) * 2 ^ length []
 2. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs) \<Longrightarrow> bl_to_bin_aux (a # bs) w < (w + 1) * 2 ^ length (a # bs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>w. bl_to_bin_aux [] w < (w + 1) * 2 ^ length []
 2. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs) \<Longrightarrow> bl_to_bin_aux (a # bs) w < (w + 1) * 2 ^ length (a # bs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux [] w < (w + 1) * 2 ^ length []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bl_to_bin_aux [] w < (w + 1) * 2 ^ length []

goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs) \<Longrightarrow> bl_to_bin_aux (a # bs) w < (w + 1) * 2 ^ length (a # bs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs) \<Longrightarrow> bl_to_bin_aux (a # bs) w < (w + 1) * 2 ^ length (a # bs)
[PROOF STEP]
case (Cons b bs)
[PROOF STATE]
proof (state)
this:
bl_to_bin_aux bs ?w < (?w + 1) * 2 ^ length bs

goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. bl_to_bin_aux bs w < (w + 1) * 2 ^ length bs) \<Longrightarrow> bl_to_bin_aux (a # bs) w < (w + 1) * 2 ^ length (a # bs)
[PROOF STEP]
from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
[PROOF STATE]
proof (chain)
picking this:
bl_to_bin_aux bs (1 + 2 * w) < (1 + 2 * w + 1) * 2 ^ length bs
bl_to_bin_aux bs (2 * w) < (2 * w + 1) * 2 ^ length bs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bl_to_bin_aux bs (1 + 2 * w) < (1 + 2 * w + 1) * 2 ^ length bs
bl_to_bin_aux bs (2 * w) < (2 * w + 1) * 2 ^ length bs

goal (1 subgoal):
 1. bl_to_bin_aux (b # bs) w < (w + 1) * 2 ^ length (b # bs)
[PROOF STEP]
apply (auto simp add: algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bl_to_bin_aux bs (1 + w * 2) < 2 * 2 ^ length bs + w * (2 * 2 ^ length bs); bl_to_bin_aux bs (w * 2) < 2 ^ length bs + w * (2 * 2 ^ length bs); \<not> b\<rbrakk> \<Longrightarrow> bl_to_bin_aux bs (w * 2) < 2 * 2 ^ length bs + w * (2 * 2 ^ length bs)
[PROOF STEP]
apply (subst mult_2 [of \<open>2 ^ length bs\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bl_to_bin_aux bs (1 + w * 2) < 2 * 2 ^ length bs + w * (2 * 2 ^ length bs); bl_to_bin_aux bs (w * 2) < 2 ^ length bs + w * (2 * 2 ^ length bs); \<not> b\<rbrakk> \<Longrightarrow> bl_to_bin_aux bs (w * 2) < 2 ^ length bs + 2 ^ length bs + w * (2 * 2 ^ length bs)
[PROOF STEP]
apply (simp only: add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bl_to_bin_aux bs (1 + w * 2) < 2 * 2 ^ length bs + w * (2 * 2 ^ length bs); bl_to_bin_aux bs (w * 2) < 2 ^ length bs + w * (2 * 2 ^ length bs); \<not> b\<rbrakk> \<Longrightarrow> bl_to_bin_aux bs (w * 2) < 2 ^ length bs + (2 ^ length bs + w * (2 * 2 ^ length bs))
[PROOF STEP]
apply (rule pos_add_strict)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bl_to_bin_aux bs (1 + w * 2) < 2 * 2 ^ length bs + w * (2 * 2 ^ length bs); bl_to_bin_aux bs (w * 2) < 2 ^ length bs + w * (2 * 2 ^ length bs); \<not> b\<rbrakk> \<Longrightarrow> 0 < 2 ^ length bs
 2. \<lbrakk>bl_to_bin_aux bs (1 + w * 2) < 2 * 2 ^ length bs + w * (2 * 2 ^ length bs); bl_to_bin_aux bs (w * 2) < 2 ^ length bs + w * (2 * 2 ^ length bs); \<not> b\<rbrakk> \<Longrightarrow> bl_to_bin_aux bs (w * 2) < 2 ^ length bs + w * (2 * 2 ^ length bs)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
bl_to_bin_aux (b # bs) w < (w + 1) * 2 ^ length (b # bs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin bs < 2 ^ length (dropWhile Not bs)
[PROOF STEP]
proof (induct bs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bl_to_bin [] < 2 ^ length (dropWhile Not [])
 2. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. bl_to_bin [] < 2 ^ length (dropWhile Not [])
 2. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin [] < 2 ^ length (dropWhile Not [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bl_to_bin [] < 2 ^ length (dropWhile Not [])

goal (1 subgoal):
 1. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs))
[PROOF STEP]
case (Cons b bs)
[PROOF STATE]
proof (state)
this:
bl_to_bin bs < 2 ^ length (dropWhile Not bs)

goal (1 subgoal):
 1. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs))
[PROOF STEP]
with bl_to_bin_lt2p_aux[where w=1]
[PROOF STATE]
proof (chain)
picking this:
bl_to_bin_aux ?bs 1 < (1 + 1) * 2 ^ length ?bs
bl_to_bin bs < 2 ^ length (dropWhile Not bs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bl_to_bin_aux ?bs 1 < (1 + 1) * 2 ^ length ?bs
bl_to_bin bs < 2 ^ length (dropWhile Not bs)

goal (1 subgoal):
 1. bl_to_bin (b # bs) < 2 ^ length (dropWhile Not (b # bs))
[PROOF STEP]
by (simp add: bl_to_bin_def)
[PROOF STATE]
proof (state)
this:
bl_to_bin (b # bs) < 2 ^ length (dropWhile Not (b # bs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin bs < 2 ^ length bs
[PROOF STEP]
by (metis bin_bl_bin bintr_lt2p bl_bin_bl)


[STATEMENT]
lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w * 2 ^ length bs \<le> bl_to_bin_aux bs w
[PROOF STEP]
proof (induction bs arbitrary: w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w. w * 2 ^ length [] \<le> bl_to_bin_aux [] w
 2. \<And>a bs w. (\<And>w. w * 2 ^ length bs \<le> bl_to_bin_aux bs w) \<Longrightarrow> w * 2 ^ length (a # bs) \<le> bl_to_bin_aux (a # bs) w
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>w. w * 2 ^ length [] \<le> bl_to_bin_aux [] w
 2. \<And>a bs w. (\<And>w. w * 2 ^ length bs \<le> bl_to_bin_aux bs w) \<Longrightarrow> w * 2 ^ length (a # bs) \<le> bl_to_bin_aux (a # bs) w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w * 2 ^ length [] \<le> bl_to_bin_aux [] w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w * 2 ^ length [] \<le> bl_to_bin_aux [] w

goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. w * 2 ^ length bs \<le> bl_to_bin_aux bs w) \<Longrightarrow> w * 2 ^ length (a # bs) \<le> bl_to_bin_aux (a # bs) w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. w * 2 ^ length bs \<le> bl_to_bin_aux bs w) \<Longrightarrow> w * 2 ^ length (a # bs) \<le> bl_to_bin_aux (a # bs) w
[PROOF STEP]
case (Cons b bs)
[PROOF STATE]
proof (state)
this:
?w * 2 ^ length bs \<le> bl_to_bin_aux bs ?w

goal (1 subgoal):
 1. \<And>a bs w. (\<And>w. w * 2 ^ length bs \<le> bl_to_bin_aux bs w) \<Longrightarrow> w * 2 ^ length (a # bs) \<le> bl_to_bin_aux (a # bs) w
[PROOF STEP]
from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>]
[PROOF STATE]
proof (chain)
picking this:
(1 + 2 * w) * 2 ^ length bs \<le> bl_to_bin_aux bs (1 + 2 * w)
2 * w * 2 ^ length bs \<le> bl_to_bin_aux bs (2 * w)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(1 + 2 * w) * 2 ^ length bs \<le> bl_to_bin_aux bs (1 + 2 * w)
2 * w * 2 ^ length bs \<le> bl_to_bin_aux bs (2 * w)

goal (1 subgoal):
 1. w * 2 ^ length (b # bs) \<le> bl_to_bin_aux (b # bs) w
[PROOF STEP]
apply (auto simp add: algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ length bs + w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (1 + w * 2); w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (w * 2); b\<rbrakk> \<Longrightarrow> w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (1 + w * 2)
[PROOF STEP]
apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ length bs + w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (1 + w * 2); w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (w * 2); b\<rbrakk> \<Longrightarrow> 2 ^ length bs + w * (2 * 2 ^ length bs) \<le> 2 ^ length bs + bl_to_bin_aux bs (1 + w * 2)
[PROOF STEP]
apply (rule add_increasing)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>2 ^ length bs + w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (1 + w * 2); w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (w * 2); b\<rbrakk> \<Longrightarrow> 0 \<le> 2 ^ length bs
 2. \<lbrakk>2 ^ length bs + w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (1 + w * 2); w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (w * 2); b\<rbrakk> \<Longrightarrow> 2 ^ length bs + w * (2 * 2 ^ length bs) \<le> bl_to_bin_aux bs (1 + w * 2)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
w * 2 ^ length (b # bs) \<le> bl_to_bin_aux (b # bs) w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> bl_to_bin bs
[PROOF STEP]
apply (unfold bl_to_bin_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> bl_to_bin_aux bs 0
[PROOF STEP]
apply (rule xtrans(4))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?b \<le> bl_to_bin_aux bs 0
 2. ?b = 0
[PROOF STEP]
apply (rule bl_to_bin_ge2p_aux)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 * 2 ^ length bs = 0
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (w div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast (bin_to_bl n w) = bin_to_bl (n - 1) (w div 2)
[PROOF STEP]
apply (unfold bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast (bin_to_bl_aux n w []) = bin_to_bl_aux (n - 1) (w div 2) []
[PROOF STEP]
apply (cases n, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> butlast (bin_to_bl_aux n w []) = bin_to_bl_aux (n - 1) (w div 2) []
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> butlast (bin_to_bl_aux nat (w div 2) [odd w]) = bin_to_bl_aux nat (w div 2) []
[PROOF STEP]
apply (auto simp add: bin_to_bl_aux_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bl_to_bin bl div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast bl = bin_to_bl (length bl - Suc 0) (bl_to_bin bl div 2)
[PROOF STEP]
using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"]
[PROOF STATE]
proof (prove)
using this:
butlast (bin_to_bl (length bl) (bl_to_bin bl)) = bin_to_bl (length bl - 1) (bl_to_bin bl div 2)

goal (1 subgoal):
 1. butlast bl = bin_to_bl (length bl - Suc 0) (bl_to_bin bl div 2)
[PROOF STEP]
by simp


[STATEMENT]
lemma butlast_rest_bl2bin_aux:
  "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bl_to_bin_aux bl w div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bl_to_bin_aux bl w div 2
[PROOF STEP]
by (induct bl arbitrary: w) auto


[STATEMENT]
lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bl_to_bin bl div 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (butlast bl) = bl_to_bin bl div 2
[PROOF STEP]
by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)


[STATEMENT]
lemma trunc_bl2bin_aux:
  "take_bit m (bl_to_bin_aux bl w) =
    bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit m (bl_to_bin_aux bl w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)
[PROOF STEP]
proof (induct bl arbitrary: w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>w. take_bit m (bl_to_bin_aux [] w) = bl_to_bin_aux (drop (length [] - m) []) (take_bit (m - length []) w)
 2. \<And>a bl w. (\<And>w. take_bit m (bl_to_bin_aux bl w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)) \<Longrightarrow> take_bit m (bl_to_bin_aux (a # bl) w) = bl_to_bin_aux (drop (length (a # bl) - m) (a # bl)) (take_bit (m - length (a # bl)) w)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>w. take_bit m (bl_to_bin_aux [] w) = bl_to_bin_aux (drop (length [] - m) []) (take_bit (m - length []) w)
 2. \<And>a bl w. (\<And>w. take_bit m (bl_to_bin_aux bl w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)) \<Longrightarrow> take_bit m (bl_to_bin_aux (a # bl) w) = bl_to_bin_aux (drop (length (a # bl) - m) (a # bl)) (take_bit (m - length (a # bl)) w)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit m (bl_to_bin_aux [] w) = bl_to_bin_aux (drop (length [] - m) []) (take_bit (m - length []) w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take_bit m (bl_to_bin_aux [] w) = bl_to_bin_aux (drop (length [] - m) []) (take_bit (m - length []) w)

goal (1 subgoal):
 1. \<And>a bl w. (\<And>w. take_bit m (bl_to_bin_aux bl w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)) \<Longrightarrow> take_bit m (bl_to_bin_aux (a # bl) w) = bl_to_bin_aux (drop (length (a # bl) - m) (a # bl)) (take_bit (m - length (a # bl)) w)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a bl w. (\<And>w. take_bit m (bl_to_bin_aux bl w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)) \<Longrightarrow> take_bit m (bl_to_bin_aux (a # bl) w) = bl_to_bin_aux (drop (length (a # bl) - m) (a # bl)) (take_bit (m - length (a # bl)) w)
[PROOF STEP]
case (Cons b bl)
[PROOF STATE]
proof (state)
this:
take_bit m (bl_to_bin_aux bl ?w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) ?w)

goal (1 subgoal):
 1. \<And>a bl w. (\<And>w. take_bit m (bl_to_bin_aux bl w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) w)) \<Longrightarrow> take_bit m (bl_to_bin_aux (a # bl) w) = bl_to_bin_aux (drop (length (a # bl) - m) (a # bl)) (take_bit (m - length (a # bl)) w)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
proof (cases "m - length bl")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m - length bl = 0 \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
 2. \<And>nat. m - length bl = Suc nat \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
m - length bl = 0

goal (2 subgoals):
 1. m - length bl = 0 \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
 2. \<And>nat. m - length bl = Suc nat \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m - length bl = 0
[PROOF STEP]
have "Suc (length bl) - m = Suc (length bl - m)"
[PROOF STATE]
proof (prove)
using this:
m - length bl = 0

goal (1 subgoal):
 1. Suc (length bl) - m = Suc (length bl - m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (length bl) - m = Suc (length bl - m)

goal (2 subgoals):
 1. m - length bl = 0 \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
 2. \<And>nat. m - length bl = Suc nat \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
take_bit m (bl_to_bin_aux bl ?w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) ?w)
Suc (length bl) - m = Suc (length bl - m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take_bit m (bl_to_bin_aux bl ?w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) ?w)
Suc (length bl) - m = Suc (length bl - m)

goal (1 subgoal):
 1. take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)

goal (1 subgoal):
 1. \<And>nat. m - length bl = Suc nat \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. m - length bl = Suc nat \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
m - length bl = Suc n

goal (1 subgoal):
 1. \<And>nat. m - length bl = Suc nat \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m - length bl = Suc n
[PROOF STEP]
have "m - Suc (length bl) = n"
[PROOF STATE]
proof (prove)
using this:
m - length bl = Suc n

goal (1 subgoal):
 1. m - Suc (length bl) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m - Suc (length bl) = n

goal (1 subgoal):
 1. \<And>nat. m - length bl = Suc nat \<Longrightarrow> take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
with Cons Suc
[PROOF STATE]
proof (chain)
picking this:
take_bit m (bl_to_bin_aux bl ?w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) ?w)
m - length bl = Suc n
m - Suc (length bl) = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
take_bit m (bl_to_bin_aux bl ?w) = bl_to_bin_aux (drop (length bl - m) bl) (take_bit (m - length bl) ?w)
m - length bl = Suc n
m - Suc (length bl) = n

goal (1 subgoal):
 1. take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)
[PROOF STEP]
by (simp add: take_bit_Suc ac_simps)
[PROOF STATE]
proof (state)
this:
take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
take_bit m (bl_to_bin_aux (b # bl) w) = bl_to_bin_aux (drop (length (b # bl) - m) (b # bl)) (take_bit (m - length (b # bl)) w)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trunc_bl2bin: "take_bit m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)
[PROOF STEP]
by (simp add: bl_to_bin_def trunc_bl2bin_aux)


[STATEMENT]
lemma trunc_bl2bin_len [simp]: "take_bit (length bl) (bl_to_bin bl) = bl_to_bin bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit (length bl) (bl_to_bin bl) = bl_to_bin bl
[PROOF STEP]
by (simp add: trunc_bl2bin)


[STATEMENT]
lemma bl2bin_drop: "bl_to_bin (drop k bl) = take_bit (length bl - k) (bl_to_bin bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (drop k bl) = take_bit (length bl - k) (bl_to_bin bl)
[PROOF STEP]
apply (rule trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bl_to_bin (drop k bl) = ?s
 2. ?s = take_bit (length bl - k) (bl_to_bin bl)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?s = take_bit (length bl - k) (bl_to_bin bl)
 2. bl_to_bin (drop k bl) = ?s
[PROOF STEP]
apply (rule trunc_bl2bin [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (drop k bl) = bl_to_bin (drop (length bl - (length bl - k)) bl)
[PROOF STEP]
apply (cases "k \<le> length bl")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. k \<le> length bl \<Longrightarrow> bl_to_bin (drop k bl) = bl_to_bin (drop (length bl - (length bl - k)) bl)
 2. \<not> k \<le> length bl \<Longrightarrow> bl_to_bin (drop k bl) = bl_to_bin (drop (length bl - (length bl - k)) bl)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w)
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m \<le> n \<Longrightarrow> length (take m (bin_to_bl n w)) = length (bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w))
 2. \<And>i. \<lbrakk>m \<le> n; i < length (take m (bin_to_bl n w))\<rbrakk> \<Longrightarrow> take m (bin_to_bl n w) ! i = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w) ! i
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>m \<le> n; i < length (take m (bin_to_bl n w))\<rbrakk> \<Longrightarrow> take m (bin_to_bl n w) ! i = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w) ! i
[PROOF STEP]
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> odd (bl_to_bin_aux xs w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length xs \<Longrightarrow> last xs = odd (bl_to_bin_aux xs w)
[PROOF STEP]
by (induct xs arbitrary: w) auto


[STATEMENT]
lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> odd (bl_to_bin xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length xs \<Longrightarrow> last xs = odd (bl_to_bin xs)
[PROOF STEP]
unfolding bl_to_bin_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length xs \<Longrightarrow> last xs = odd (bl_to_bin_aux xs 0)
[PROOF STEP]
by (erule last_bin_last')


[STATEMENT]
lemma bin_last_last: "odd w \<longleftrightarrow> last (bin_to_bl (Suc n) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd w = last (bin_to_bl (Suc n) w)
[PROOF STEP]
by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)


[STATEMENT]
lemma drop_bin2bl_aux:
  "drop m (bin_to_bl_aux n bin bs) =
    bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs)
[PROOF STEP]
apply (induction n arbitrary: m bin bs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m bin bs. drop m (bin_to_bl_aux 0 bin bs) = bin_to_bl_aux (0 - m) bin (drop (m - 0) bs)
 2. \<And>n m bin bs. (\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs)) \<Longrightarrow> drop m (bin_to_bl_aux (Suc n) bin bs) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bs. (\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs)) \<Longrightarrow> bin_to_bl_aux (n - m) (bin div 2) (drop (m - n) (odd bin # bs)) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs)
[PROOF STEP]
apply (case_tac "m \<le> n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); m \<le> n\<rbrakk> \<Longrightarrow> bin_to_bl_aux (n - m) (bin div 2) (drop (m - n) (odd bin # bs)) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs)
 2. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); \<not> m \<le> n\<rbrakk> \<Longrightarrow> bin_to_bl_aux (n - m) (bin div 2) (drop (m - n) (odd bin # bs)) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs)
[PROOF STEP]
apply (auto simp add: not_le Suc_diff_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m\<rbrakk> \<Longrightarrow> drop (m - n) (odd bin # bs) = drop (m - Suc n) bs
[PROOF STEP]
apply (case_tac "m - n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m; m - n = 0\<rbrakk> \<Longrightarrow> drop (m - n) (odd bin # bs) = drop (m - Suc n) bs
 2. \<And>n m bin bs nat. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m; m - n = Suc nat\<rbrakk> \<Longrightarrow> drop (m - n) (odd bin # bs) = drop (m - Suc n) bs
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m bs nat. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m; m - n = Suc nat\<rbrakk> \<Longrightarrow> drop nat bs = drop (m - Suc n) bs
[PROOF STEP]
apply (use Suc_diff_Suc in fastforce)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin
[PROOF STEP]
by (simp add: bin_to_bl_def drop_bin2bl_aux)


[STATEMENT]
lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take m (bin_to_bl_aux m w bs) = bin_to_bl m w
[PROOF STEP]
apply (induct m arbitrary: w bs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w bs. take 0 (bin_to_bl_aux 0 w bs) = bin_to_bl 0 w
 2. \<And>m w bs. (\<And>w bs. take m (bin_to_bl_aux m w bs) = bin_to_bl m w) \<Longrightarrow> take (Suc m) (bin_to_bl_aux (Suc m) w bs) = bin_to_bl (Suc m) w
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w bs. (\<And>w bs. take m (bin_to_bl_aux m w bs) = bin_to_bl m w) \<Longrightarrow> take (Suc m) (bin_to_bl_aux (Suc m) w bs) = bin_to_bl (Suc m) w
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w bs. (\<And>w bs. take m (bin_to_bl_aux m w bs) = bin_to_bl m w) \<Longrightarrow> take (Suc m) (bin_to_bl_aux m (w div 2) (odd w # bs)) = bin_to_bl (Suc m) w
[PROOF STEP]
apply (simp add: bin_to_bl_aux_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w. bin_to_bl m (w div 2) @ [odd w] = bin_to_bl (Suc m) w
[PROOF STEP]
apply (simp add: bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w. bin_to_bl_aux m (w div 2) [] @ [odd w] = bin_to_bl_aux m (w div 2) [odd w]
[PROOF STEP]
apply (simp add: bin_to_bl_aux_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)
[PROOF STEP]
by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)


[STATEMENT]
lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)
[PROOF STEP]
apply (induct n arbitrary: b c)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b c. bin_split 0 c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + 0) c)
 2. \<And>n b c. \<lbrakk>\<And>b c. bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c); bin_split (Suc n) c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + Suc n) c)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n b c. \<lbrakk>\<And>b c. bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c); bin_split (Suc n) c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + Suc n) c)
[PROOF STEP]
apply (clarsimp simp: Let_def split: prod.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>ca. drop_bit n ca = drop_bit (Suc n) c \<Longrightarrow> bin_to_bl m (drop_bit (Suc n) c) = take m (bin_to_bl (m + n) ca); a = drop_bit (Suc n) c\<rbrakk> \<Longrightarrow> bin_to_bl m (drop_bit (Suc n) c) = take m (bin_to_bl (Suc (m + n)) c)
[PROOF STEP]
apply (simp add: bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>ca. drop_bit n ca = drop_bit (Suc n) c \<Longrightarrow> bin_to_bl_aux m (drop_bit (Suc n) c) [] = take m (bin_to_bl_aux (m + n) ca []); a = drop_bit (Suc n) c\<rbrakk> \<Longrightarrow> bin_to_bl_aux m (drop_bit (Suc n) c) [] = take m (bin_to_bl_aux (m + n) (c div 2) [odd c])
[PROOF STEP]
apply (simp add: take_bin2bl_lem drop_bit_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_to_bl_drop_bit:
  "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)
[PROOF STEP]
using bin_split_take
[PROOF STATE]
proof (prove)
using this:
bin_split ?n ?c = (?a, ?b) \<Longrightarrow> bin_to_bl ?m ?a = take ?m (bin_to_bl (?m + ?n) ?c)

goal (1 subgoal):
 1. k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)
[PROOF STEP]
by simp


[STATEMENT]
lemma bin_split_take1:
  "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k = m + n; bin_split n c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)
[PROOF STEP]
using bin_split_take
[PROOF STATE]
proof (prove)
using this:
bin_split ?n ?c = (?a, ?b) \<Longrightarrow> bin_to_bl ?m ?a = take ?m (bin_to_bl (?m + ?n) ?c)

goal (1 subgoal):
 1. \<lbrakk>k = m + n; bin_split n c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)
[PROOF STEP]
by simp


[STATEMENT]
lemma bl_bin_bl_rep_drop:
  "bin_to_bl n (bl_to_bin bl) =
    replicate (n - length bl) False @ drop (length bl - n) bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (bl_to_bin bl) = replicate (n - length bl) False @ drop (length bl - n) bl
[PROOF STEP]
by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)


[STATEMENT]
lemma bl_to_bin_aux_cat:
  "bl_to_bin_aux bs (concat_bit nv v w) =
    concat_bit (nv + length bs) (bl_to_bin_aux bs v) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux bs (concat_bit nv v w) = concat_bit (nv + length bs) (bl_to_bin_aux bs v) w
[PROOF STEP]
by (rule bit_eqI)
    (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)


[STATEMENT]
lemma bin_to_bl_aux_cat:
  "bin_to_bl_aux (nv + nw) (concat_bit nw w v) bs =
    bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux (nv + nw) (concat_bit nw w v) bs = bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)
[PROOF STEP]
by (induction nw arbitrary: w bs) (simp_all add: concat_bit_Suc)


[STATEMENT]
lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = concat_bit (length bs) (bl_to_bin bs) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux bs w = concat_bit (length bs) (bl_to_bin bs) w
[PROOF STEP]
using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
[PROOF STATE]
proof (prove)
using this:
bl_to_bin_aux ?bs (concat_bit 0 0 ?w) = concat_bit (0 + length ?bs) (bl_to_bin_aux ?bs 0) ?w

goal (1 subgoal):
 1. bl_to_bin_aux bs w = concat_bit (length bs) (bl_to_bin bs) w
[PROOF STEP]
by (simp add: bl_to_bin_def [symmetric])


[STATEMENT]
lemma bin_to_bl_cat:
  "bin_to_bl (nv + nw) (concat_bit nw w v) =
    bin_to_bl_aux nv v (bin_to_bl nw w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (nv + nw) (concat_bit nw w v) = bin_to_bl_aux nv v (bin_to_bl nw w)
[PROOF STEP]
by (simp add: bin_to_bl_def bin_to_bl_aux_cat)


[STATEMENT]
lemma bl_to_bin_app_cat:
  "bl_to_bin (bsa @ bs) = concat_bit (length bs) (bl_to_bin bs) (bl_to_bin bsa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bsa @ bs) = concat_bit (length bs) (bl_to_bin bs) (bl_to_bin bsa)
[PROOF STEP]
by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)


[STATEMENT]
lemma bin_to_bl_cat_app:
  "bin_to_bl (n + nw) (concat_bit nw wa w) = bin_to_bl n w @ bin_to_bl nw wa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (n + nw) (concat_bit nw wa w) = bin_to_bl n w @ bin_to_bl nw wa
[PROOF STEP]
by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)


[STATEMENT]
lemma bl_to_bin_app_cat_alt: "concat_bit n w (bl_to_bin cs) = bl_to_bin (cs @ bin_to_bl n w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_bit n w (bl_to_bin cs) = bl_to_bin (cs @ bin_to_bl n w)
[PROOF STEP]
by (simp add: bl_to_bin_app_cat)


[STATEMENT]
lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (True # replicate n False) = bl_to_bin (replicate n True) + 1
[PROOF STEP]
apply (unfold bl_to_bin_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bl_to_bin_aux (True # replicate 0 False) 0 = bl_to_bin_aux (replicate 0 True) 0 + 1
 2. \<And>n. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1 \<Longrightarrow> bl_to_bin_aux (True # replicate (Suc n) False) 0 = bl_to_bin_aux (replicate (Suc n) True) 0 + 1
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1 \<Longrightarrow> bl_to_bin_aux (True # replicate (Suc n) False) 0 = bl_to_bin_aux (replicate (Suc n) True) 0 + 1
[PROOF STEP]
apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1 \<Longrightarrow> bl_to_bin_aux (replicate 1 False) (bl_to_bin_aux (replicate n True) 0 + 1) = bl_to_bin_aux (replicate 1 True) (bl_to_bin_aux (replicate n True) 0) + 1
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_exhaust:
  "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q
[PROOF STEP]
apply (cases \<open>even bin\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q; even bin\<rbrakk> \<Longrightarrow> Q
 2. \<lbrakk>\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q; odd bin\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
apply (auto elim!: evenE oddE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>\<And>x ba. 2 * b = of_bool ba + 2 * x \<Longrightarrow> Q; bin = 2 * b\<rbrakk> \<Longrightarrow> Q
 2. \<And>b. \<lbrakk>\<And>x ba. 2 * b + 1 = of_bool ba + 2 * x \<Longrightarrow> Q; bin = 2 * b + 1\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<And>x ba. 2 * b + 1 = of_bool ba + 2 * x \<Longrightarrow> Q; bin = 2 * b + 1\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rbl_pred bl) = length bl
[PROOF STEP]
by (induct bl) auto


[STATEMENT]
lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rbl_succ bl) = length bl
[PROOF STEP]
by (induct bl) auto


[STATEMENT]
lemma size_rbl_add: "length (rbl_add bl cl) = length bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rbl_add bl cl) = length bl
[PROOF STEP]
by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)


[STATEMENT]
lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rbl_mult bl cl) = length bl
[PROOF STEP]
by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)


[STATEMENT]
lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb
[PROOF STEP]
apply (induct bla arbitrary: blb)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>blb. length [] \<le> length blb \<Longrightarrow> rbl_add [] (blb @ blc) = rbl_add [] blb
 2. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_add (a # bla) (blb @ blc) = rbl_add (a # bla) blb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_add (a # bla) (blb @ blc) = rbl_add (a # bla) blb
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb; Suc (length bla) \<le> length blb\<rbrakk> \<Longrightarrow> (let ws = rbl_add bla (tl (blb @ blc)) in (a = (\<not> hd (blb @ blc))) # (if hd (blb @ blc) \<and> a then rbl_succ ws else ws)) = (let ws = rbl_add bla (tl blb) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws))
[PROOF STEP]
apply (case_tac blb, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb aa list. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb; Suc (length bla) \<le> length blb; blb = aa # list\<rbrakk> \<Longrightarrow> (let ws = rbl_add bla (tl (blb @ blc)) in (a = (\<not> hd (blb @ blc))) # (if hd (blb @ blc) \<and> a then rbl_succ ws else ws)) = (let ws = rbl_add bla (tl blb) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws))
[PROOF STEP]
apply (clarsimp simp: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_add_take2:
  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb
[PROOF STEP]
apply (induct bla arbitrary: blb)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>blb. length [] \<le> length blb \<Longrightarrow> rbl_add [] (take (length []) blb) = rbl_add [] blb
 2. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_add (a # bla) (take (length (a # bla)) blb) = rbl_add (a # bla) blb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_add (a # bla) (take (length (a # bla)) blb) = rbl_add (a # bla) blb
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; Suc (length bla) \<le> length blb\<rbrakk> \<Longrightarrow> (let ws = rbl_add bla (tl (take (Suc (length bla)) blb)) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws)) = (let ws = rbl_add bla (tl blb) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws))
[PROOF STEP]
apply (case_tac blb, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb aa list. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; Suc (length bla) \<le> length blb; blb = aa # list\<rbrakk> \<Longrightarrow> (let ws = rbl_add bla (tl (take (Suc (length bla)) blb)) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws)) = (let ws = rbl_add bla (tl blb) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws))
[PROOF STEP]
apply (clarsimp simp: Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb
[PROOF STEP]
apply (induct bla arbitrary: blb)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>blb. length [] \<le> length blb \<Longrightarrow> rbl_mult [] (blb @ blc) = rbl_mult [] blb
 2. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_mult (a # bla) (blb @ blc) = rbl_mult (a # bla) blb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_mult (a # bla) (blb @ blc) = rbl_mult (a # bla) blb
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; Suc (length bla) \<le> length blb\<rbrakk> \<Longrightarrow> (let ws = False # rbl_mult bla blb in if a then rbl_add ws (blb @ blc) else ws) = (let ws = False # rbl_mult bla blb in if a then rbl_add ws blb else ws)
[PROOF STEP]
apply (case_tac blb, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb aa list. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; Suc (length bla) \<le> length blb; blb = aa # list\<rbrakk> \<Longrightarrow> (let ws = False # rbl_mult bla blb in if a then rbl_add ws (blb @ blc) else ws) = (let ws = False # rbl_mult bla blb in if a then rbl_add ws blb else ws)
[PROOF STEP]
apply (clarsimp simp: Let_def rbl_add_app2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_mult_take2:
  "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb
[PROOF STEP]
apply (rule trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb) = ?s
 2. length bla \<le> length blb \<Longrightarrow> ?s = rbl_mult bla blb
[PROOF STEP]
apply (rule rbl_mult_app2 [symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length bla \<le> length blb \<Longrightarrow> length bla \<le> length (take (length bla) blb)
 2. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb @ ?blc3) = rbl_mult bla blb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb @ ?blc3) = rbl_mult bla blb
[PROOF STEP]
apply (rule_tac f = "rbl_mult bla" in arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> take (length bla) blb @ ?blc3 = blb
[PROOF STEP]
apply (rule append_take_drop_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_add_split:
  "P (rbl_add (y # ys) (x # xs)) =
    (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
      (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
      (\<not> y \<longrightarrow> P (x # ws)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (rbl_add (y # ys) (x # xs)) = (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow> (y \<longrightarrow> (x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws))) \<and> (\<not> y \<longrightarrow> P (x # ws)))
[PROOF STEP]
by (cases y) (auto simp: Let_def)


[STATEMENT]
lemma rbl_mult_split:
  "P (rbl_mult (y # ys) xs) =
    (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
      (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (rbl_mult (y # ys) xs) = (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow> (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))
[PROOF STEP]
proof (unfold bin_to_bl_def, induction n arbitrary: bin)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>bin. rbl_pred (rev (bin_to_bl_aux 0 bin [])) = rev (bin_to_bl_aux 0 (bin - 1) [])
 2. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>bin. rbl_pred (rev (bin_to_bl_aux 0 bin [])) = rev (bin_to_bl_aux 0 (bin - 1) [])
 2. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbl_pred (rev (bin_to_bl_aux 0 bin [])) = rev (bin_to_bl_aux 0 (bin - 1) [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rbl_pred (rev (bin_to_bl_aux 0 bin [])) = rev (bin_to_bl_aux 0 (bin - 1) [])

goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
rbl_pred (rev (bin_to_bl_aux n ?bin [])) = rev (bin_to_bl_aux n (?bin - 1) [])

goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
obtain b k where \<open>bin = of_bool b + 2 * k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>b k. bin = of_bool b + 2 * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bin_exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>x b. ?bin = of_bool b + 2 * x \<Longrightarrow> ?Q) \<Longrightarrow> ?Q

goal (1 subgoal):
 1. (\<And>b k. bin = of_bool b + 2 * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bin = of_bool b + 2 * k

goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bin = of_bool b + 2 * k

goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
have \<open>(2 * k - 1) div 2 = k - 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 * k - 1) div 2 = k - 1
[PROOF STEP]
using even_succ_div_2 [of \<open>2 * (k - 1)\<close>]
[PROOF STATE]
proof (prove)
using this:
even (2 * (k - 1)) \<Longrightarrow> (1 + 2 * (k - 1)) div 2 = 2 * (k - 1) div 2

goal (1 subgoal):
 1. (2 * k - 1) div 2 = k - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(2 * k - 1) div 2 = k - 1

goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_pred (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin - 1) [])) \<Longrightarrow> rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bin = of_bool b + 2 * k
(2 * k - 1) div 2 = k - 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bin = of_bool b + 2 * k
(2 * k - 1) div 2 = k - 1

goal (1 subgoal):
 1. rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
using Suc [of \<open>bin div 2\<close>]
[PROOF STATE]
proof (prove)
using this:
bin = of_bool b + 2 * k
(2 * k - 1) div 2 = k - 1
rbl_pred (rev (bin_to_bl_aux n (bin div 2) [])) = rev (bin_to_bl_aux n (bin div 2 - 1) [])

goal (1 subgoal):
 1. rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])
[PROOF STEP]
by simp (auto simp add: bin_to_bl_aux_alt)
[PROOF STATE]
proof (state)
this:
rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))
[PROOF STEP]
apply (unfold bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) [])
[PROOF STEP]
apply (induction n arbitrary: bin)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>bin. rbl_succ (rev (bin_to_bl_aux 0 bin [])) = rev (bin_to_bl_aux 0 (bin + 1) [])
 2. \<And>n bin. (\<And>bin. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) [])) \<Longrightarrow> rbl_succ (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin + 1) [])
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) [])) \<Longrightarrow> rbl_succ (rev (bin_to_bl_aux n (bin div 2) [odd bin])) = rev (bin_to_bl_aux n ((bin + 1) div 2) [even bin])
[PROOF STEP]
apply (case_tac bin rule: bin_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bin x b. \<lbrakk>\<And>bin. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) []); bin = of_bool b + 2 * x\<rbrakk> \<Longrightarrow> rbl_succ (rev (bin_to_bl_aux n (bin div 2) [odd bin])) = rev (bin_to_bl_aux n ((bin + 1) div 2) [even bin])
[PROOF STEP]
apply (simp_all add: bin_to_bl_aux_alt ac_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_add:
  "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
    rev (bin_to_bl n (bina + binb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina + binb))
[PROOF STEP]
apply (unfold bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) [])
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>bina binb. rbl_add (rev (bin_to_bl_aux 0 bina [])) (rev (bin_to_bl_aux 0 binb [])) = rev (bin_to_bl_aux 0 (bina + binb) [])
 2. \<And>n bina binb. (\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) [])) \<Longrightarrow> rbl_add (rev (bin_to_bl_aux (Suc n) bina [])) (rev (bin_to_bl_aux (Suc n) binb [])) = rev (bin_to_bl_aux (Suc n) (bina + binb) [])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) [])) \<Longrightarrow> rbl_add (rev (bin_to_bl_aux (Suc n) bina [])) (rev (bin_to_bl_aux (Suc n) binb [])) = rev (bin_to_bl_aux (Suc n) (bina + binb) [])
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) [])) \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
[PROOF STEP]
apply (case_tac bina rule: bin_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
[PROOF STEP]
apply (case_tac binb rule: bin_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
[PROOF STEP]
apply (case_tac b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; b\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 2. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; \<not> b\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
[PROOF STEP]
apply (case_tac [!] "ba")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; b; ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 2. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; b; \<not> ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 3. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; \<not> b; ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 4. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; \<not> b; \<not> ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
[PROOF STEP]
apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_add_long:
  "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
    rev (bin_to_bl n (bina + binb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = rev (bin_to_bl n (bina + binb))
[PROOF STEP]
apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (take (length (rev (bin_to_bl n bina))) (rev (bin_to_bl m binb))) = rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))
 2. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb))
[PROOF STEP]
apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> take (length (rev (bin_to_bl n bina))) (rev (bin_to_bl m binb)) = rev (bin_to_bl n binb)
 2. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb))
[PROOF STEP]
apply (rule rev_swap [THEN iffD1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> rev (take (length (rev (bin_to_bl n bina))) (rev (bin_to_bl m binb))) = bin_to_bl n binb
 2. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb))
[PROOF STEP]
apply (simp add: rev_take drop_bin2bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_mult_gt1:
  "m \<ge> length bl \<Longrightarrow>
    rbl_mult bl (rev (bin_to_bl m binb)) =
    rbl_mult bl (rev (bin_to_bl (length bl) binb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> rbl_mult bl (rev (bin_to_bl m binb)) = rbl_mult bl (rev (bin_to_bl (length bl) binb))
[PROOF STEP]
apply (rule trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length bl \<le> m \<Longrightarrow> rbl_mult bl (rev (bin_to_bl m binb)) = ?s
 2. length bl \<le> m \<Longrightarrow> ?s = rbl_mult bl (rev (bin_to_bl (length bl) binb))
[PROOF STEP]
apply (rule rbl_mult_take2 [symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length bl \<le> m \<Longrightarrow> length bl \<le> length (rev (bin_to_bl m binb))
 2. length bl \<le> m \<Longrightarrow> rbl_mult bl (take (length bl) (rev (bin_to_bl m binb))) = rbl_mult bl (rev (bin_to_bl (length bl) binb))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> rbl_mult bl (take (length bl) (rev (bin_to_bl m binb))) = rbl_mult bl (rev (bin_to_bl (length bl) binb))
[PROOF STEP]
apply (rule_tac f = "rbl_mult bl" in arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> take (length bl) (rev (bin_to_bl m binb)) = rev (bin_to_bl (length bl) binb)
[PROOF STEP]
apply (rule rev_swap [THEN iffD1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length bl \<le> m \<Longrightarrow> rev (take (length bl) (rev (bin_to_bl m binb))) = bin_to_bl (length bl) binb
[PROOF STEP]
apply (simp add: rev_take drop_bin2bl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rbl_mult_gt:
  "m > n \<Longrightarrow>
    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))
[PROOF STEP]
by (auto intro: trans [OF rbl_mult_gt1])


[STATEMENT]
lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (of_bool b + 2 * x))
[PROOF STEP]
by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt)


[STATEMENT]
lemma rbl_mult:
  "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
    rev (bin_to_bl n (bina * binb))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb))
[PROOF STEP]
apply (induct n arbitrary: bina binb)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>bina binb. rbl_mult (rev (bin_to_bl 0 bina)) (rev (bin_to_bl 0 binb)) = rev (bin_to_bl 0 (bina * binb))
 2. \<And>n bina binb. (\<And>bina binb. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb))) \<Longrightarrow> rbl_mult (rev (bin_to_bl (Suc n) bina)) (rev (bin_to_bl (Suc n) binb)) = rev (bin_to_bl (Suc n) (bina * binb))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb))) \<Longrightarrow> rbl_mult (rev (bin_to_bl (Suc n) bina)) (rev (bin_to_bl (Suc n) binb)) = rev (bin_to_bl (Suc n) (bina * binb))
[PROOF STEP]
apply (unfold bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_mult (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina * binb) [])) \<Longrightarrow> rbl_mult (rev (bin_to_bl_aux (Suc n) bina [])) (rev (bin_to_bl_aux (Suc n) binb [])) = rev (bin_to_bl_aux (Suc n) (bina * binb) [])
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_mult (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina * binb) [])) \<Longrightarrow> rbl_mult (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n (bina * binb div 2) [odd bina \<and> odd binb])
[PROOF STEP]
apply (case_tac bina rule: bin_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b. \<lbrakk>\<And>bina binb. rbl_mult (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina * binb) []); bina = of_bool b + 2 * x\<rbrakk> \<Longrightarrow> rbl_mult (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n (bina * binb div 2) [odd bina \<and> odd binb])
[PROOF STEP]
apply (case_tac binb rule: bin_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_mult (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina * binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa\<rbrakk> \<Longrightarrow> rbl_mult (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n (bina * binb div 2) [odd bina \<and> odd binb])
[PROOF STEP]
apply (simp_all add: bin_to_bl_aux_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb)); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa\<rbrakk> \<Longrightarrow> (b \<longrightarrow> (ba \<longrightarrow> rbl_add (rbl_mult (rev (bin_to_bl n x)) (True # rev (bin_to_bl n xa))) (rev (bin_to_bl n xa)) = rev (bin_to_bl n ((1 + 2 * x) * (1 + 2 * xa) div 2))) \<and> (\<not> ba \<longrightarrow> rbl_add (rbl_mult (rev (bin_to_bl n x)) (False # rev (bin_to_bl n xa))) (rev (bin_to_bl n xa)) = rev (bin_to_bl n ((1 + 2 * x) * xa)))) \<and> (\<not> b \<longrightarrow> (ba \<longrightarrow> rbl_mult (rev (bin_to_bl n x)) (True # rev (bin_to_bl n xa)) = rev (bin_to_bl n (x * (1 + 2 * xa)))) \<and> (\<not> ba \<longrightarrow> rbl_mult (rev (bin_to_bl n x)) (False # rev (bin_to_bl n xa)) = rev (bin_to_bl n (2 * x * xa))))
[PROOF STEP]
apply (simp_all add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sclem: "size (concat (map (bin_to_bl n) xs)) = length xs * n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat (map (bin_to_bl n) xs)) = length xs * n
[PROOF STEP]
by (simp add: length_concat comp_def sum_list_triv)


[STATEMENT]
lemma bin_cat_foldl_lem:
  "foldl (\<lambda>u k. concat_bit n k u) x xs =
    concat_bit (size xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x
[PROOF STEP]
apply (induct xs arbitrary: x)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. foldl (\<lambda>u k. concat_bit n k u) x [] = concat_bit (length [] * n) (foldl (\<lambda>u k. concat_bit n k u) y []) x
 2. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) x (a # xs) = concat_bit (length (a # xs) * n) (foldl (\<lambda>u k. concat_bit n k u) y (a # xs)) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) x (a # xs) = concat_bit (length (a # xs) * n) (foldl (\<lambda>u k. concat_bit n k u) y (a # xs)) x
[PROOF STEP]
apply (simp (no_asm))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a x) xs = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x
[PROOF STEP]
apply (frule asm_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. \<lbrakk>\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x; \<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x\<rbrakk> \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a x) xs = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x
[PROOF STEP]
apply (drule meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. \<lbrakk>\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x; foldl (\<lambda>u k. concat_bit n k u) (?x4 a xs x) xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (?x4 a xs x)\<rbrakk> \<Longrightarrow> foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a x) xs = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x
[PROOF STEP]
apply (erule trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. (\<And>x. foldl (\<lambda>u k. concat_bit n k u) x xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) x) \<Longrightarrow> concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (concat_bit n a x) = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x
[PROOF STEP]
apply (drule_tac x = "concat_bit n a y" in meta_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs = concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (concat_bit n a y) \<Longrightarrow> concat_bit (length xs * n) (foldl (\<lambda>u k. concat_bit n k u) y xs) (concat_bit n a x) = concat_bit (n + length xs * n) (foldl (\<lambda>u k. concat_bit n k u) (concat_bit n a y) xs) x
[PROOF STEP]
apply (simp add: bin_cat_assoc_sym)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))
[PROOF STEP]
apply (unfold bin_rcat_eq_foldl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>u v. concat_bit n v u) 0 wl = bl_to_bin (concat (map (bin_to_bl n) wl))
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl
[PROOF STEP]
apply (induct wl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bl_to_bin (concat (map (bin_to_bl n) [])) = foldl (\<lambda>u v. concat_bit n v u) 0 []
 2. \<And>a wl. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl \<Longrightarrow> bl_to_bin (concat (map (bin_to_bl n) (a # wl))) = foldl (\<lambda>u v. concat_bit n v u) 0 (a # wl)
[PROOF STEP]
apply (auto simp add: bl_to_bin_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a wl. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl \<Longrightarrow> bl_to_bin_aux (concat (map (bin_to_bl n) wl)) (take_bit n a) = foldl (\<lambda>u v. concat_bit n v u) (take_bit n a) wl
[PROOF STEP]
apply (simp add: bl_to_bin_aux_alt sclem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a wl. bl_to_bin (concat (map (bin_to_bl n) wl)) = foldl (\<lambda>u v. concat_bit n v u) 0 wl \<Longrightarrow> concat_bit (length wl * n) (foldl (\<lambda>u v. concat_bit n v u) 0 wl) (take_bit n a) = foldl (\<lambda>u v. concat_bit n v u) (take_bit n a) wl
[PROOF STEP]
apply (simp add: bin_cat_foldl_lem [symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_last_bl_to_bin: "odd (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd (bl_to_bin bs) = (bs \<noteq> [] \<and> last bs)
[PROOF STEP]
by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0])


[STATEMENT]
lemma bin_rest_bl_to_bin: "bl_to_bin bs div 2 = bl_to_bin (butlast bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin bs div 2 = bl_to_bin (butlast bs)
[PROOF STEP]
by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux)


[STATEMENT]
lemma bl_xor_aux_bin:
  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<noteq>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = bin_to_bl_aux n (v XOR w) (map2 (\<noteq>) bs cs)
[PROOF STEP]
apply (induction n arbitrary: v w bs cs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v w bs cs. map2 (\<noteq>) (bin_to_bl_aux 0 v bs) (bin_to_bl_aux 0 w cs) = bin_to_bl_aux 0 (v XOR w) (map2 (\<noteq>) bs cs)
 2. \<And>n v w bs cs. (\<And>v w bs cs. map2 (\<noteq>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = bin_to_bl_aux n (v XOR w) (map2 (\<noteq>) bs cs)) \<Longrightarrow> map2 (\<noteq>) (bin_to_bl_aux (Suc n) v bs) (bin_to_bl_aux (Suc n) w cs) = bin_to_bl_aux (Suc n) (v XOR w) (map2 (\<noteq>) bs cs)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n v w bs cs. (\<And>v w bs cs. map2 (\<lambda>x y. x = (\<not> y)) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x = (\<not> y)) bs cs)) \<Longrightarrow> bin_to_bl_aux n (v div 2 XOR w div 2) ((even v = odd w) # map2 (\<lambda>x y. x = (\<not> y)) bs cs) = bin_to_bl_aux n (v div 2 XOR w div 2) (((even v \<longrightarrow> odd w) \<and> (even v \<or> even w)) # map2 (\<lambda>x y. x = (\<not> y)) bs cs)
[PROOF STEP]
apply (case_tac v rule: bin_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n v w bs cs x b. \<lbrakk>\<And>v w bs cs. map2 (\<lambda>x y. x = (\<not> y)) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x = (\<not> y)) bs cs); v = of_bool b + 2 * x\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (v div 2 XOR w div 2) ((even v = odd w) # map2 (\<lambda>x y. x = (\<not> y)) bs cs) = bin_to_bl_aux n (v div 2 XOR w div 2) (((even v \<longrightarrow> odd w) \<and> (even v \<or> even w)) # map2 (\<lambda>x y. x = (\<not> y)) bs cs)
[PROOF STEP]
apply (case_tac w rule: bin_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n v w bs cs x b xa ba. \<lbrakk>\<And>v w bs cs. map2 (\<lambda>x y. x = (\<not> y)) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x = (\<not> y)) bs cs); v = of_bool b + 2 * x; w = of_bool ba + 2 * xa\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (v div 2 XOR w div 2) ((even v = odd w) # map2 (\<lambda>x y. x = (\<not> y)) bs cs) = bin_to_bl_aux n (v div 2 XOR w div 2) (((even v \<longrightarrow> odd w) \<and> (even v \<or> even w)) # map2 (\<lambda>x y. x = (\<not> y)) bs cs)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_or_aux_bin:
  "map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = bin_to_bl_aux n (v OR w) (map2 (\<or>) bs cs)
[PROOF STEP]
by (induct n arbitrary: v w bs cs) simp_all


[STATEMENT]
lemma bl_and_aux_bin:
  "map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
    bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = bin_to_bl_aux n (v AND w) (map2 (\<and>) bs cs)
[PROOF STEP]
by (induction n arbitrary: v w bs cs) simp_all


[STATEMENT]
lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)
[PROOF STEP]
by (induct n arbitrary: w cs) auto


[STATEMENT]
lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map Not (bin_to_bl n w) = bin_to_bl n (NOT w)
[PROOF STEP]
by (simp add: bin_to_bl_def bl_not_aux_bin)


[STATEMENT]
lemma bl_and_bin: "map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)
[PROOF STEP]
by (simp add: bin_to_bl_def bl_and_aux_bin)


[STATEMENT]
lemma bl_or_bin: "map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)
[PROOF STEP]
by (simp add: bin_to_bl_def bl_or_aux_bin)


[STATEMENT]
lemma bl_xor_bin: "map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)
[PROOF STEP]
using bl_xor_aux_bin
[PROOF STATE]
proof (prove)
using this:
map2 (\<noteq>) (bin_to_bl_aux ?n ?v ?bs) (bin_to_bl_aux ?n ?w ?cs) = bin_to_bl_aux ?n (?v XOR ?w) (map2 (\<noteq>) ?bs ?cs)

goal (1 subgoal):
 1. map2 (\<noteq>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)
[PROOF STEP]
by (simp add: bin_to_bl_def)


[STATEMENT]
lemma to_bl_eq:
  \<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = bin_to_bl LENGTH('a) (uint w)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma bit_of_bl_iff [bit_simps]:
  \<open>bit (of_bl bs :: 'a word) n \<longleftrightarrow> rev bs ! n \<and> n < LENGTH('a::len) \<and> n < length bs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (of_bl bs) n = (rev bs ! n \<and> n < LENGTH('a) \<and> n < length bs)
[PROOF STEP]
by transfer (simp add: bin_nth_of_bl ac_simps)


[STATEMENT]
lemma rev_to_bl_eq:
  \<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (to_bl w) = map (bit w) [0..<LENGTH('a)]
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (rev (to_bl w)) = length (map (bit w) [0..<LENGTH('a)])
 2. \<And>i. i < length (rev (to_bl w)) \<Longrightarrow> rev (to_bl w) ! i = map (bit w) [0..<LENGTH('a)] ! i
[PROOF STEP]
apply (simp add: to_bl.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (rev (to_bl w)) \<Longrightarrow> rev (to_bl w) ! i = map (bit w) [0..<LENGTH('a)] ! i
[PROOF STEP]
apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma to_bl_eq_rev:
  \<open>to_bl w = map (bit w) (rev [0..<LENGTH('a)])\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl w = map (bit w) (rev [0..<LENGTH('a)])
[PROOF STEP]
using rev_to_bl_eq [of w]
[PROOF STATE]
proof (prove)
using this:
rev (to_bl w) = map (bit w) [0..<LENGTH('a)]

goal (1 subgoal):
 1. to_bl w = map (bit w) (rev [0..<LENGTH('a)])
[PROOF STEP]
apply (subst rev_is_rev_conv [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (to_bl w) = map (bit w) [0..<LENGTH('a)] \<Longrightarrow> rev (to_bl w) = rev (map (bit w) (rev [0..<LENGTH('a)]))
[PROOF STEP]
apply (simp add: rev_map)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma of_bl_rev_eq:
  \<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl (rev bs) = horner_sum of_bool 2 bs
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (of_bl (rev bs)) n = bit (horner_sum of_bool 2 bs) n
[PROOF STEP]
apply (simp add: bit_of_bl_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> (bs ! n \<and> n < length bs) = bit (horner_sum of_bool 2 bs) n
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n bs. n < LENGTH('a) \<Longrightarrow> (bs ! n \<and> n < length bs) = (n < LENGTH('a) \<and> bit (horner_sum of_bool 2 bs) n)
[PROOF STEP]
apply (simp add: bit_horner_sum_bit_iff ac_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma of_bl_eq:
  \<open>of_bl bs = horner_sum of_bool 2 (rev bs)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_bl bs = horner_sum of_bool 2 (rev bs)
[PROOF STEP]
using of_bl_rev_eq [of \<open>rev bs\<close>]
[PROOF STATE]
proof (prove)
using this:
of_bl (rev (rev bs)) = horner_sum of_bool 2 (rev bs)

goal (1 subgoal):
 1. of_bl bs = horner_sum of_bool 2 (rev bs)
[PROOF STEP]
by simp


[STATEMENT]
lemma bshiftr1_eq:
  \<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b) = of_bl (b # butlast (to_bl w))
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (w div 2 OR push_bit (LENGTH('a) - Suc 0) (of_bool b)) n = bit (of_bl (b # butlast (to_bl w))) n
[PROOF STEP]
apply (auto simp add: bit_simps to_bl_eq_rev nth_append rev_nth nth_butlast not_less simp flip: bit_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < LENGTH('a); LENGTH('a) - Suc 0 \<le> n; bit w (Suc n)\<rbrakk> \<Longrightarrow> b
[PROOF STEP]
apply (metis Suc_pred len_gt_0 less_eq_decr_length_iff not_bit_length verit_la_disequality)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_to_bl_eq:
  \<open>length (to_bl w) = LENGTH('a)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (to_bl w) = LENGTH('a)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma word_rotr_eq:
  \<open>word_rotr n w = of_bl (rotater n (to_bl w))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotr n w = of_bl (rotater n (to_bl w))
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. na < LENGTH('a) \<Longrightarrow> bit (word_rotr n w) na = bit (of_bl (rotater n (to_bl w))) na
[PROOF STEP]
subgoal for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < LENGTH('a) \<Longrightarrow> bit (word_rotr n w) n = bit (of_bl (rotater n (to_bl w))) n
[PROOF STEP]
apply (cases \<open>n < LENGTH('a)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr n w) n = bit (of_bl (rotater n (to_bl w))) n
 2. \<lbrakk>n < LENGTH('a); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr n w) n = bit (of_bl (rotater n (to_bl w))) n
[PROOF STEP]
apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff rotater_rev length_to_bl_eq nth_rotate rev_to_bl_eq ac_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_rotl_eq:
  \<open>word_rotl n w = of_bl (rotate n (to_bl w))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w))
[PROOF STEP]
have \<open>rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))
[PROOF STEP]
by (simp add: rotater_rev')
[PROOF STATE]
proof (state)
this:
rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))

goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rotate n (to_bl w) = rev (rotater n (rev (to_bl w)))

goal (1 subgoal):
 1. word_rotl n w = of_bl (rotate n (to_bl w))
[PROOF STEP]
apply (simp add: word_rotl_eq_word_rotr bit_of_bl_iff length_to_bl_eq rev_to_bl_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])) \<Longrightarrow> word_rotr (LENGTH('a) - n mod LENGTH('a)) w = of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); na < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) na = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) na
[PROOF STEP]
subgoal for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) n = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) n
[PROOF STEP]
apply (cases \<open>n < LENGTH('a)\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); n < LENGTH('a); n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) n = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) n
 2. \<lbrakk>rotate n (to_bl w) = rev (rotater n (map (bit w) [0..<LENGTH('a)])); n < LENGTH('a); \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> bit (word_rotr (LENGTH('a) - n mod LENGTH('a)) w) n = bit (of_bl (rev (rotater n (map (bit w) [0..<LENGTH('a)])))) n
[PROOF STEP]
apply (simp_all add: bit_word_rotr_iff bit_of_bl_iff nth_rotater)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
word_rotl n w = of_bl (rotate n (to_bl w))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma to_bl_def': "(to_bl :: 'a::len word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl = bin_to_bl LENGTH('a) \<circ> uint
[PROOF STEP]
by transfer (simp add: fun_eq_iff)

\<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>


[STATEMENT]
lemma td_bl:
  "type_definition
    (to_bl :: 'a::len word \<Rightarrow> bool list)
    of_bl
    {bl. length bl = LENGTH('a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_definition to_bl of_bl {bl. length bl = LENGTH('a)}
[PROOF STEP]
apply (standard; transfer)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. bin_to_bl LENGTH('a) x \<in> {bl. length bl = LENGTH('a)}
 2. \<And>x. take_bit LENGTH('a) (bl_to_bin (bin_to_bl LENGTH('a) x)) = take_bit LENGTH('a) x
 3. \<And>y. y \<in> {bl. length bl = LENGTH('a)} \<Longrightarrow> bin_to_bl LENGTH('a) (bl_to_bin y) = y
[PROOF STEP]
apply (auto dest: sym)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma word_size_bl: "size w = size (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size w = length (to_bl w)
[PROOF STEP]
by (auto simp: word_size)


[STATEMENT]
lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))
[PROOF STEP]
by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])


[STATEMENT]
lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
  for x :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (to_bl x)
[PROOF STEP]
unfolding word_bl_Rep'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < LENGTH('a)
[PROOF STEP]
by (rule len_gt_0)


[STATEMENT]
lemma bl_not_Nil [iff]: "to_bl x \<noteq> []"
  for x :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_bl x \<noteq> []
[PROOF STEP]
by (fact length_bl_gt_0 [unfolded length_greater_0_conv])


[STATEMENT]
lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
  for x :: "'a::len word"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (to_bl x) \<noteq> 0
[PROOF STEP]
by (fact length_bl_gt_0 [THEN gr_implies_not0])


[STATEMENT]
lemma hd_to_bl_iff:
  \<open>hd (to_bl w) \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (to_bl w) = bit w (LENGTH('a) - 1)
[PROOF STEP]
by (simp add: to_bl_eq_rev hd_map hd_rev)


[STATEMENT]
lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (to_bl w) = (bin_sign (sint w) = - 1)
[PROOF STEP]
by (simp add: hd_to_bl_iff bit_last_iff bin_sign_def)