theory Reversed_Bit_Lists

lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (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 (subst mult_2 [of \<open>2 ^ length bs\<close>]) apply (simp only: add.assoc) apply (rule pos_add_strict) apply simp_all done qed

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

goal:
No subgoals!