theory Reversed_Bit_Lists

lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))" proof (unfold bin_to_bl_def, induction n arbitrary: bin) case 0 then show ?case by simp next case (Suc n) obtain b k where \<open>bin = of_bool b + 2 * k\<close> using bin_exhaust by blast moreover have \<open>(2 * k - 1) div 2 = k - 1\<close> using even_succ_div_2 [of \<open>2 * (k - 1)\<close>] by simp ultimately show ?case using Suc [of \<open>bin div 2\<close>] by simp (auto simp add: bin_to_bl_aux_alt) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1)) 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 (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 (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. rbl_pred (rev (bin_to_bl_aux 0 bin [])) = rev (bin_to_bl_aux 0 (bin - 1) []) 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 (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 (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 (prove)
goal (1 subgoal):
 1. (\<And>b k. bin = of_bool b + 2 * k \<Longrightarrow> thesis) \<Longrightarrow> thesis 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 (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 (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 (prove)
goal (1 subgoal):
 1. (2 * k - 1) div 2 = k - 1 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 (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 (chain)
picking this:
bin = of_bool b + 2 * k
(2 * k - 1) div 2 = k - 1 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 (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 (state)
this:
rbl_pred (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin - 1) [])

goal:
No subgoals!