theory Reversed_Bit_Lists

lemma bin_to_bl_aux_bintr:
  "bin_to_bl_aux n (take_bit m bin) bl =
    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl" apply (induct n arbitrary: m bin bl) apply clarsimp apply clarsimp apply (case_tac "m") apply (clarsimp simp: bin_to_bl_zero_aux) apply (erule thin_rl) apply (induct_tac n) apply (auto simp add: take_bit_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl proof (prove)
goal (2 subgoals):
 1. \<And>m bin bl. bin_to_bl_aux 0 (take_bit m bin) bl = replicate (0 - m) False @ bin_to_bl_aux (min 0 m) bin bl
 2. \<And>n m bin bl. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> bin_to_bl_aux (Suc n) (take_bit m bin) bl = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bl. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> bin_to_bl_aux (Suc n) (take_bit m bin) bl = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bl. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl proof (prove)
goal (2 subgoals):
 1. \<And>n m bin bl. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = 0\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
 2. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl proof (prove)
goal (2 subgoals):
 1. \<And>n. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> replicate n False @ [False] = False # replicate n False
 2. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl proof (prove)
goal (2 subgoals):
 1. \<And>n. replicate n False @ [False] = False # replicate n False
 2. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl proof (prove)
goal (3 subgoals):
 1. \<And>n. replicate 0 False @ [False] = False # replicate 0 False
 2. \<And>n na. replicate na False @ [False] = False # replicate na False \<Longrightarrow> replicate (Suc na) False @ [False] = False # replicate (Suc na) False
 3. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl proof (prove)
goal:
No subgoals!