theory Reversed_Bit_Lists

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 (induct bl arbitrary: w) case Nil show ?case by simp next case (Cons b bl) show ?case proof (cases "m - length bl") case 0 then have "Suc (length bl) - m = Suc (length bl - m)" by simp with Cons show ?thesis by simp next case (Suc n) then have "m - Suc (length bl) = n" by simp with Cons Suc show ?thesis by (simp add: take_bit_Suc ac_simps) qed qed

(* Proof state trace *)
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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (chain)
picking this:
m - length bl = 0 proof (prove)
using this:
m - length bl = 0

goal (1 subgoal):
 1. Suc (length bl) - m = Suc (length bl - m) 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 (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 (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 (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 (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 (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 (chain)
picking this:
m - length bl = Suc n proof (prove)
using this:
m - length bl = Suc n

goal (1 subgoal):
 1. m - Suc (length bl) = n 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 (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 (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 (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 (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!