theory Reversed_Bit_Lists

lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)" proof (induction bs arbitrary: w) case Nil then show ?case by simp next case (Cons b bs) from Cons.IH [of \<open>1 + 2 * w\<close>] Cons.IH [of \<open>2 * w\<close>] show ?case apply (auto simp add: algebra_simps) apply (rule add_le_imp_le_left [of \<open>2 ^ length bs\<close>]) apply (rule add_increasing) apply simp_all done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w * 2 ^ length bs \<le> bl_to_bin_aux bs w 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 (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 (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. w * 2 ^ length [] \<le> bl_to_bin_aux [] w 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 (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 (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 (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 (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 (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 (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 (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 (prove)
goal:
No subgoals! proof (state)
this:
w * 2 ^ length (b # bs) \<le> bl_to_bin_aux (b # bs) w

goal:
No subgoals!