kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

lemma bin_to_bl_aux_zero_minus_simp [simp]:
  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)" by (cases n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)
theory Reversed_Bit_Lists

lemma bin_to_bl_aux_minus1_minus_simp [simp]:
  "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)" by (cases n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)
theory Reversed_Bit_Lists

lemma bin_to_bl_aux_one_minus_simp [simp]:
  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)" by (cases n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)
theory Reversed_Bit_Lists

lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
  "0 < n \<Longrightarrow>
    bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)" by (cases n) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n (numeral (num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)
theory Reversed_Bit_Lists

lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
  "0 < n \<Longrightarrow>
    bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)" by (cases n) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n (numeral (num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)
theory Reversed_Bit_Lists

lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" by (induct bs arbitrary: w) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)
theory Reversed_Bit_Lists

lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" by (induct n arbitrary: w bs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)
theory Reversed_Bit_Lists

lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)" unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs) proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux (bs @ cs) 0 = bl_to_bin_aux cs (bl_to_bin_aux bs 0)
theory Reversed_Bit_Lists

lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" by (simp add: bin_to_bl_def bin_to_bl_aux_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n w bs = bin_to_bl n w @ bs
theory Reversed_Bit_Lists

lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []" by (auto simp: bin_to_bl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl 0 bs = []
theory Reversed_Bit_Lists

lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs" by (induct n arbitrary: w bs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl_aux n w bs) = n + length bs
theory Reversed_Bit_Lists

lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n" by (simp add: bin_to_bl_def size_bin_to_bl_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl n w) = n
theory Reversed_Bit_Lists

lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs" apply (induct bs arbitrary: w n) apply auto apply (simp_all only: add_Suc [symmetric]) apply (auto simp add: bin_to_bl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs proof (prove)
goal (2 subgoals):
 1. \<And>w n. bin_to_bl (n + length []) (bl_to_bin_aux [] w) = bin_to_bl_aux n w []
 2. \<And>a bs w n. (\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs) \<Longrightarrow> bin_to_bl (n + length (a # bs)) (bl_to_bin_aux (a # bs) w) = bin_to_bl_aux n w (a # bs) proof (prove)
goal (3 subgoals):
 1. \<And>w n. bin_to_bl n w = bin_to_bl_aux n w []
 2. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; a\<rbrakk> \<Longrightarrow> bin_to_bl (Suc (n + length bs)) (bl_to_bin_aux bs (1 + 2 * w)) = bin_to_bl_aux n w (True # bs)
 3. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; \<not> a\<rbrakk> \<Longrightarrow> bin_to_bl (Suc (n + length bs)) (bl_to_bin_aux bs (2 * w)) = bin_to_bl_aux n w (False # bs) proof (prove)
goal (3 subgoals):
 1. \<And>w n. bin_to_bl n w = bin_to_bl_aux n w []
 2. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; a\<rbrakk> \<Longrightarrow> bin_to_bl_aux (Suc n) (1 + 2 * w) bs = bin_to_bl_aux n w (True # bs)
 3. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; \<not> a\<rbrakk> \<Longrightarrow> bin_to_bl_aux (Suc n) (2 * w) bs = bin_to_bl_aux n w (False # bs) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs" unfolding bl_to_bin_def apply (rule box_equals) apply (rule bl_bin_bl') prefer 2 apply (rule bin_to_bl_aux.Z) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (length bs) (bl_to_bin bs) = bs proof (prove)
goal (1 subgoal):
 1. bin_to_bl (length bs) (bl_to_bin_aux bs 0) = bs proof (prove)
goal (3 subgoals):
 1. ?a = ?b
 2. ?a = bin_to_bl (length bs) (bl_to_bin_aux bs 0)
 3. ?b = bs proof (prove)
goal (2 subgoals):
 1. bin_to_bl (?n4 + length ?bs4) (bl_to_bin_aux ?bs4 ?w4) = bin_to_bl (length bs) (bl_to_bin_aux bs 0)
 2. bin_to_bl_aux ?n4 ?w4 ?bs4 = bs proof (prove)
goal (2 subgoals):
 1. bin_to_bl_aux ?n4 ?w4 ?bs4 = bs
 2. bin_to_bl (?n4 + length ?bs4) (bl_to_bin_aux ?bs4 ?w4) = bin_to_bl (length bs) (bl_to_bin_aux bs 0) proof (prove)
goal (1 subgoal):
 1. bin_to_bl (0 + length bs) (bl_to_bin_aux bs ?w4) = bin_to_bl (length bs) (bl_to_bin_aux bs 0) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs" apply (rule_tac box_equals) defer apply (rule bl_bin_bl) apply (rule bl_bin_bl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> bs = cs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = ?b
 2. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = bs
 3. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?b = cs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = bs
 2. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?b = cs
 3. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = ?b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?b = cs
 2. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> bin_to_bl (length bs) (bl_to_bin bs) = ?b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> bin_to_bl (length bs) (bl_to_bin bs) = bin_to_bl (length cs) (bl_to_bin cs) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" by (auto simp: bl_to_bin_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (False # bl) = bl_to_bin bl
theory Reversed_Bit_Lists

lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0" by (auto simp: bl_to_bin_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin [] = 0
theory Reversed_Bit_Lists

lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl" by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n 0 bl = replicate n False @ bl
theory Reversed_Bit_Lists

lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False" by (simp add: bin_to_bl_def bin_to_bl_zero_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n 0 = replicate n False
theory Reversed_Bit_Lists

lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl" by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n (- 1) bl = replicate n True @ bl
theory Reversed_Bit_Lists

lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True" by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (- 1) = replicate n True
theory Reversed_Bit_Lists

lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (take_bit n w)" by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (take_bit n w)
theory Reversed_Bit_Lists

lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = take_bit n w" by (auto simp: bin_to_bl_def bin_bl_bin')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bin_to_bl n w) = take_bit n w
theory Reversed_Bit_Lists

lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (replicate n False @ bl) = bl_to_bin bl
theory Reversed_Bit_Lists

lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (take_bit m w) = bin_to_bl n w" by (auto intro: bl_to_bin_inj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> bin_to_bl n (take_bit m w) = bin_to_bl n w
theory Reversed_Bit_Lists

lemma bin_to_bl_bintr:
  "bin_to_bl n (take_bit m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin" unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (take_bit m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n (take_bit m bin) [] = replicate (n - m) False @ bin_to_bl_aux (min n m) bin []
theory Reversed_Bit_Lists

lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" by (induct n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (replicate n False) = 0
theory Reversed_Bit_Lists

lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs" by (fact size_bin_to_bl_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl_aux n w bs) = n + length bs
theory Reversed_Bit_Lists

lemma len_bin_to_bl: "length (bin_to_bl n w) = n" by (fact size_bin_to_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl n w) = n
theory Reversed_Bit_Lists

lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w" by (induction bs arbitrary: w) (simp_all add: bin_sign_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign (bl_to_bin_aux bs w) = bin_sign w
theory Reversed_Bit_Lists

lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0" by (simp add: bl_to_bin_def sign_bl_bin')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign (bl_to_bin bs) = 0
theory Reversed_Bit_Lists

lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (signed_take_bit n w) = -1)" by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (signed_take_bit n w) = - 1)
theory Reversed_Bit_Lists

lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (signed_take_bit n w) = -1)" unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hd (bin_to_bl (Suc n) w) = (bin_sign (signed_take_bit n w) = - 1) proof (prove)
goal (1 subgoal):
 1. hd (bin_to_bl_aux (Suc n) w []) = (bin_sign (signed_take_bit n w) = - 1)
theory Reversed_Bit_Lists

lemma bin_nth_of_bl: "bit (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)" by (simp add: bl_to_bin_def bin_nth_of_bl_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bit (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)
theory Reversed_Bit_Lists

lemma bin_nth_bl: "n < m \<Longrightarrow> bit w n = nth (rev (bin_to_bl m w)) n" by (metis bin_bl_bin bin_nth_of_bl nth_bintr size_bin_to_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> bit w n = rev (bin_to_bl m w) ! n
theory Reversed_Bit_Lists

lemma nth_bin_to_bl_aux:
  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
    (if n < m then bit w (m - 1 - n) else bl ! (n - m))" apply (induction bl arbitrary: w) apply simp_all apply (simp add: bin_nth_bl [of \<open>m - Suc n\<close> m] rev_nth flip: bin_to_bl_def) apply (metis One_nat_def Suc_pred add_diff_cancel_left'
     add_diff_cancel_right' bin_to_bl_aux_alt bin_to_bl_def
     diff_Suc_Suc diff_is_0_eq diff_zero less_Suc_eq_0_disj
     less_antisym less_imp_Suc_add list.size(3) nat_less_le nth_append size_bin_to_bl_aux) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m)) proof (prove)
goal (2 subgoals):
 1. \<And>w. n < m + length [] \<Longrightarrow> bin_to_bl_aux m w [] ! n = (if n < m then bit w (m - 1 - n) else [] ! (n - m))
 2. \<And>a bl w. \<lbrakk>\<And>w. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m)); n < m + length (a # bl)\<rbrakk> \<Longrightarrow> bin_to_bl_aux m w (a # bl) ! n = (if n < m then bit w (m - 1 - n) else (a # bl) ! (n - m)) proof (prove)
goal (2 subgoals):
 1. \<And>w. n < m \<Longrightarrow> bin_to_bl_aux m w [] ! n = bit w (m - Suc n)
 2. \<And>a bl w. \<lbrakk>\<And>w. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m)); n < Suc (m + length bl)\<rbrakk> \<Longrightarrow> (n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = bit w (m - Suc n)) \<and> (\<not> n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = (a # bl) ! (n - m)) proof (prove)
goal (1 subgoal):
 1. \<And>a bl w. \<lbrakk>\<And>w. n < m + length bl \<Longrightarrow> bin_to_bl_aux m w bl ! n = (if n < m then bit w (m - 1 - n) else bl ! (n - m)); n < Suc (m + length bl)\<rbrakk> \<Longrightarrow> (n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = bit w (m - Suc n)) \<and> (\<not> n < m \<longrightarrow> bin_to_bl_aux m w (a # bl) ! n = (a # bl) ! (n - m)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bit w (m - Suc n)" by (simp add: bin_to_bl_def nth_bin_to_bl_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> bin_to_bl m w ! n = bit w (m - Suc n)
theory Reversed_Bit_Lists

lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))" apply (rule nth_equalityI) apply simp apply (clarsimp simp: nth_takefill rev_nth nth_bin_to_bl bin_nth_of_bl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl))) proof (prove)
goal (2 subgoals):
 1. length (takefill False n bl) = length (rev (bin_to_bl n (bl_to_bin (rev bl))))
 2. \<And>i. i < length (takefill False n bl) \<Longrightarrow> takefill False n bl ! i = rev (bin_to_bl n (bl_to_bin (rev bl))) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (takefill False n bl) \<Longrightarrow> takefill False n bl ! i = rev (bin_to_bl n (bl_to_bin (rev bl))) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))" by (simp add: takefill_bintrunc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))
theory Reversed_Bit_Lists

lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)" proof (induct bs) case Nil then show ?case by simp next case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1] show ?case by (simp add: bl_to_bin_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin bs < 2 ^ length (dropWhile Not bs) proof (state)
goal (2 subgoals):
 1. bl_to_bin [] < 2 ^ length (dropWhile Not [])
 2. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs)) proof (state)
this:


goal (2 subgoals):
 1. bl_to_bin [] < 2 ^ length (dropWhile Not [])
 2. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs)) proof (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. bl_to_bin [] < 2 ^ length (dropWhile Not []) proof (state)
this:
bl_to_bin [] < 2 ^ length (dropWhile Not [])

goal (1 subgoal):
 1. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs)) proof (state)
goal (1 subgoal):
 1. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs)) proof (state)
this:
bl_to_bin bs < 2 ^ length (dropWhile Not bs)

goal (1 subgoal):
 1. \<And>a bs. bl_to_bin bs < 2 ^ length (dropWhile Not bs) \<Longrightarrow> bl_to_bin (a # bs) < 2 ^ length (dropWhile Not (a # bs)) proof (chain)
picking this:
bl_to_bin_aux ?bs 1 < (1 + 1) * 2 ^ length ?bs
bl_to_bin bs < 2 ^ length (dropWhile Not bs) proof (prove)
using this:
bl_to_bin_aux ?bs 1 < (1 + 1) * 2 ^ length ?bs
bl_to_bin bs < 2 ^ length (dropWhile Not bs)

goal (1 subgoal):
 1. bl_to_bin (b # bs) < 2 ^ length (dropWhile Not (b # bs)) proof (state)
this:
bl_to_bin (b # bs) < 2 ^ length (dropWhile Not (b # bs))

goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs" by (metis bin_bl_bin bintr_lt2p bl_bin_bl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin bs < 2 ^ length bs
theory Reversed_Bit_Lists

lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0" apply (unfold bl_to_bin_def) apply (rule xtrans(4)) apply (rule bl_to_bin_ge2p_aux) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> bl_to_bin bs proof (prove)
goal (1 subgoal):
 1. 0 \<le> bl_to_bin_aux bs 0 proof (prove)
goal (2 subgoals):
 1. ?b \<le> bl_to_bin_aux bs 0
 2. ?b = 0 proof (prove)
goal (1 subgoal):
 1. 0 * 2 ^ length bs = 0 proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (w div 2)" apply (unfold bin_to_bl_def) apply (cases n, clarsimp) apply clarsimp apply (auto simp add: bin_to_bl_aux_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. butlast (bin_to_bl n w) = bin_to_bl (n - 1) (w div 2) proof (prove)
goal (1 subgoal):
 1. butlast (bin_to_bl_aux n w []) = bin_to_bl_aux (n - 1) (w div 2) [] proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> butlast (bin_to_bl_aux n w []) = bin_to_bl_aux (n - 1) (w div 2) [] proof (prove)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> butlast (bin_to_bl_aux nat (w div 2) [odd w]) = bin_to_bl_aux nat (w div 2) [] proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bl_to_bin bl div 2)" using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. butlast bl = bin_to_bl (length bl - Suc 0) (bl_to_bin bl div 2) proof (prove)
using this:
butlast (bin_to_bl (length bl) (bl_to_bin bl)) = bin_to_bl (length bl - 1) (bl_to_bin bl div 2)

goal (1 subgoal):
 1. butlast bl = bin_to_bl (length bl - Suc 0) (bl_to_bin bl div 2)
theory Reversed_Bit_Lists

lemma butlast_rest_bl2bin_aux:
  "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bl_to_bin_aux bl w div 2" by (induct bl arbitrary: w) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bl_to_bin_aux bl w div 2
theory Reversed_Bit_Lists

lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bl_to_bin bl div 2" by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (butlast bl) = bl_to_bin bl div 2
theory Reversed_Bit_Lists

lemma trunc_bl2bin: "take_bit m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)" by (simp add: bl_to_bin_def trunc_bl2bin_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)
theory Reversed_Bit_Lists

lemma trunc_bl2bin_len [simp]: "take_bit (length bl) (bl_to_bin bl) = bl_to_bin bl" by (simp add: trunc_bl2bin)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit (length bl) (bl_to_bin bl) = bl_to_bin bl
theory Reversed_Bit_Lists

lemma bl2bin_drop: "bl_to_bin (drop k bl) = take_bit (length bl - k) (bl_to_bin bl)" apply (rule trans) prefer 2 apply (rule trunc_bl2bin [symmetric]) apply (cases "k \<le> length bl") apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (drop k bl) = take_bit (length bl - k) (bl_to_bin bl) proof (prove)
goal (2 subgoals):
 1. bl_to_bin (drop k bl) = ?s
 2. ?s = take_bit (length bl - k) (bl_to_bin bl) proof (prove)
goal (2 subgoals):
 1. ?s = take_bit (length bl - k) (bl_to_bin bl)
 2. bl_to_bin (drop k bl) = ?s proof (prove)
goal (1 subgoal):
 1. bl_to_bin (drop k bl) = bl_to_bin (drop (length bl - (length bl - k)) bl) proof (prove)
goal (2 subgoals):
 1. k \<le> length bl \<Longrightarrow> bl_to_bin (drop k bl) = bl_to_bin (drop (length bl - (length bl - k)) bl)
 2. \<not> k \<le> length bl \<Longrightarrow> bl_to_bin (drop k bl) = bl_to_bin (drop (length bl - (length bl - k)) bl) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w)" apply (rule nth_equalityI) apply simp apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w) proof (prove)
goal (2 subgoals):
 1. m \<le> n \<Longrightarrow> length (take m (bin_to_bl n w)) = length (bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w))
 2. \<And>i. \<lbrakk>m \<le> n; i < length (take m (bin_to_bl n w))\<rbrakk> \<Longrightarrow> take m (bin_to_bl n w) ! i = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w) ! i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>m \<le> n; i < length (take m (bin_to_bl n w))\<rbrakk> \<Longrightarrow> take m (bin_to_bl n w) ! i = bin_to_bl m (((\<lambda>w. w div 2) ^^ (n - m)) w) ! i proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> odd (bl_to_bin_aux xs w)" by (induct xs arbitrary: w) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < length xs \<Longrightarrow> last xs = odd (bl_to_bin_aux xs w)