theory Reversed_Bit_Lists

lemma bin_nth_of_bl_aux:
  "bit (bl_to_bin_aux bl w) n =
    (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bit w (n - size bl))" apply (induction bl arbitrary: w) apply simp_all apply safe apply (simp_all add: not_le nth_append bit_double_iff even_bit_succ_iff split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)) proof (prove)
goal (2 subgoals):
 1. \<And>w. bit (bl_to_bin_aux [] w) n = (n < length [] \<and> rev [] ! n \<or> length [] \<le> n \<and> bit w (n - length []))
 2. \<And>a bl w. (\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl))) \<Longrightarrow> bit (bl_to_bin_aux (a # bl) w) n = (n < length (a # bl) \<and> rev (a # bl) ! n \<or> length (a # bl) \<le> n \<and> bit w (n - length (a # bl))) proof (prove)
goal (1 subgoal):
 1. \<And>a bl w. (\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl))) \<Longrightarrow> (a \<longrightarrow> (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit (1 + 2 * w) (n - length bl)) = (n < Suc (length bl) \<and> (rev bl @ [True]) ! n \<or> Suc (length bl) \<le> n \<and> bit w (n - Suc (length bl)))) \<and> (\<not> a \<longrightarrow> (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit (2 * w) (n - length bl)) = (n < Suc (length bl) \<and> (rev bl @ [False]) ! n \<or> Suc (length bl) \<le> n \<and> bit w (n - Suc (length bl)))) proof (prove)
goal (32 subgoals):
 1. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 2. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 3. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 4. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < length bl; rev bl ! n; \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 5. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 6. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> Suc (length bl) \<le> n\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 7. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> n < Suc (length bl)
 8. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; length bl \<le> n; bit (1 + 2 * w) (n - length bl); \<not> bit w (n - Suc (length bl))\<rbrakk> \<Longrightarrow> (rev bl @ [True]) ! n
 9. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < Suc (length bl); (rev bl @ [True]) ! n; \<not> length bl \<le> n\<rbrakk> \<Longrightarrow> n < length bl
 10. \<And>a bl w. \<lbrakk>\<And>w. bit (bl_to_bin_aux bl w) n = (n < length bl \<and> rev bl ! n \<or> length bl \<le> n \<and> bit w (n - length bl)); a; n < Suc (length bl); (rev bl @ [True]) ! n; \<not> length bl \<le> n\<rbrakk> \<Longrightarrow> rev bl ! n
A total of 32 subgoals... proof (prove)
goal:
No subgoals!