kings-crown/FVELER_Isabelle huggingface dataset:
theory Reversed_Bit_Lists

lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> odd (bl_to_bin xs)" unfolding bl_to_bin_def by (erule last_bin_last')

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

lemma bin_last_last: "odd w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt)

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

lemma drop_bin2bl_aux:
  "drop m (bin_to_bl_aux n bin bs) =
    bin_to_bl_aux (n - m) bin (drop (m - n) bs)" apply (induction n arbitrary: m bin bs) apply auto apply (case_tac "m \<le> n") apply (auto simp add: not_le Suc_diff_le) apply (case_tac "m - n") apply auto apply (use Suc_diff_Suc in fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs) proof (prove)
goal (2 subgoals):
 1. \<And>m bin bs. drop m (bin_to_bl_aux 0 bin bs) = bin_to_bl_aux (0 - m) bin (drop (m - 0) bs)
 2. \<And>n m bin bs. (\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs)) \<Longrightarrow> drop m (bin_to_bl_aux (Suc n) bin bs) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs) proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bs. (\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs)) \<Longrightarrow> bin_to_bl_aux (n - m) (bin div 2) (drop (m - n) (odd bin # bs)) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs) proof (prove)
goal (2 subgoals):
 1. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); m \<le> n\<rbrakk> \<Longrightarrow> bin_to_bl_aux (n - m) (bin div 2) (drop (m - n) (odd bin # bs)) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs)
 2. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); \<not> m \<le> n\<rbrakk> \<Longrightarrow> bin_to_bl_aux (n - m) (bin div 2) (drop (m - n) (odd bin # bs)) = bin_to_bl_aux (Suc n - m) bin (drop (m - Suc n) bs) proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m\<rbrakk> \<Longrightarrow> drop (m - n) (odd bin # bs) = drop (m - Suc n) bs proof (prove)
goal (2 subgoals):
 1. \<And>n m bin bs. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m; m - n = 0\<rbrakk> \<Longrightarrow> drop (m - n) (odd bin # bs) = drop (m - Suc n) bs
 2. \<And>n m bin bs nat. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m; m - n = Suc nat\<rbrakk> \<Longrightarrow> drop (m - n) (odd bin # bs) = drop (m - Suc n) bs proof (prove)
goal (1 subgoal):
 1. \<And>n m bs nat. \<lbrakk>\<And>m bin bs. drop m (bin_to_bl_aux n bin bs) = bin_to_bl_aux (n - m) bin (drop (m - n) bs); n < m; m - n = Suc nat\<rbrakk> \<Longrightarrow> drop nat bs = drop (m - Suc n) bs proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin" by (simp add: bin_to_bl_def drop_bin2bl_aux)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin
theory Reversed_Bit_Lists

lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w" apply (induct m arbitrary: w bs) apply clarsimp apply clarsimp apply (simp add: bin_to_bl_aux_alt) apply (simp add: bin_to_bl_def) apply (simp add: bin_to_bl_aux_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take m (bin_to_bl_aux m w bs) = bin_to_bl m w proof (prove)
goal (2 subgoals):
 1. \<And>w bs. take 0 (bin_to_bl_aux 0 w bs) = bin_to_bl 0 w
 2. \<And>m w bs. (\<And>w bs. take m (bin_to_bl_aux m w bs) = bin_to_bl m w) \<Longrightarrow> take (Suc m) (bin_to_bl_aux (Suc m) w bs) = bin_to_bl (Suc m) w proof (prove)
goal (1 subgoal):
 1. \<And>m w bs. (\<And>w bs. take m (bin_to_bl_aux m w bs) = bin_to_bl m w) \<Longrightarrow> take (Suc m) (bin_to_bl_aux (Suc m) w bs) = bin_to_bl (Suc m) w proof (prove)
goal (1 subgoal):
 1. \<And>m w bs. (\<And>w bs. take m (bin_to_bl_aux m w bs) = bin_to_bl m w) \<Longrightarrow> take (Suc m) (bin_to_bl_aux m (w div 2) (odd w # bs)) = bin_to_bl (Suc m) w proof (prove)
goal (1 subgoal):
 1. \<And>m w. bin_to_bl m (w div 2) @ [odd w] = bin_to_bl (Suc m) w proof (prove)
goal (1 subgoal):
 1. \<And>m w. bin_to_bl_aux m (w div 2) [] @ [odd w] = bin_to_bl_aux m (w div 2) [odd w] proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)" by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp)

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

lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)" apply (induct n arbitrary: b c) apply clarsimp apply (clarsimp simp: Let_def split: prod.split_asm) apply (simp add: bin_to_bl_def) apply (simp add: take_bin2bl_lem drop_bit_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c) proof (prove)
goal (2 subgoals):
 1. \<And>b c. bin_split 0 c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + 0) c)
 2. \<And>n b c. \<lbrakk>\<And>b c. bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c); bin_split (Suc n) c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + Suc n) c) proof (prove)
goal (1 subgoal):
 1. \<And>n b c. \<lbrakk>\<And>b c. bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c); bin_split (Suc n) c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + Suc n) c) proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>ca. drop_bit n ca = drop_bit (Suc n) c \<Longrightarrow> bin_to_bl m (drop_bit (Suc n) c) = take m (bin_to_bl (m + n) ca); a = drop_bit (Suc n) c\<rbrakk> \<Longrightarrow> bin_to_bl m (drop_bit (Suc n) c) = take m (bin_to_bl (Suc (m + n)) c) proof (prove)
goal (1 subgoal):
 1. \<And>n c. \<lbrakk>\<And>ca. drop_bit n ca = drop_bit (Suc n) c \<Longrightarrow> bin_to_bl_aux m (drop_bit (Suc n) c) [] = take m (bin_to_bl_aux (m + n) ca []); a = drop_bit (Suc n) c\<rbrakk> \<Longrightarrow> bin_to_bl_aux m (drop_bit (Suc n) c) [] = take m (bin_to_bl_aux (m + n) (c div 2) [odd c]) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bin_to_bl_drop_bit:
  "k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)" using bin_split_take by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c) proof (prove)
using this:
bin_split ?n ?c = (?a, ?b) \<Longrightarrow> bin_to_bl ?m ?a = take ?m (bin_to_bl (?m + ?n) ?c)

goal (1 subgoal):
 1. k = m + n \<Longrightarrow> bin_to_bl m (drop_bit n c) = take m (bin_to_bl k c)
theory Reversed_Bit_Lists

lemma bin_split_take1:
  "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)" using bin_split_take by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k = m + n; bin_split n c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c) proof (prove)
using this:
bin_split ?n ?c = (?a, ?b) \<Longrightarrow> bin_to_bl ?m ?a = take ?m (bin_to_bl (?m + ?n) ?c)

goal (1 subgoal):
 1. \<lbrakk>k = m + n; bin_split n c = (a, b)\<rbrakk> \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)
theory Reversed_Bit_Lists

lemma bl_bin_bl_rep_drop:
  "bin_to_bl n (bl_to_bin bl) =
    replicate (n - length bl) False @ drop (length bl - n) bl" by (simp add: bl_to_bin_inj bl_to_bin_rep_F trunc_bl2bin)

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

lemma bl_to_bin_aux_cat:
  "bl_to_bin_aux bs (concat_bit nv v w) =
    concat_bit (nv + length bs) (bl_to_bin_aux bs v) w" by (rule bit_eqI)
    (auto simp add: bin_nth_of_bl_aux bin_nth_cat algebra_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux bs (concat_bit nv v w) = concat_bit (nv + length bs) (bl_to_bin_aux bs v) w
theory Reversed_Bit_Lists

lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = concat_bit (length bs) (bl_to_bin bs) w" using bl_to_bin_aux_cat [where nv = "0" and v = "0"] by (simp add: bl_to_bin_def [symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux bs w = concat_bit (length bs) (bl_to_bin bs) w proof (prove)
using this:
bl_to_bin_aux ?bs (concat_bit 0 0 ?w) = concat_bit (0 + length ?bs) (bl_to_bin_aux ?bs 0) ?w

goal (1 subgoal):
 1. bl_to_bin_aux bs w = concat_bit (length bs) (bl_to_bin bs) w
theory Reversed_Bit_Lists

lemma bin_to_bl_cat:
  "bin_to_bl (nv + nw) (concat_bit nw w v) =
    bin_to_bl_aux nv v (bin_to_bl nw w)" by (simp add: bin_to_bl_def bin_to_bl_aux_cat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (nv + nw) (concat_bit nw w v) = bin_to_bl_aux nv v (bin_to_bl nw w)
theory Reversed_Bit_Lists

lemma bl_to_bin_app_cat:
  "bl_to_bin (bsa @ bs) = concat_bit (length bs) (bl_to_bin bs) (bl_to_bin bsa)" by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bsa @ bs) = concat_bit (length bs) (bl_to_bin bs) (bl_to_bin bsa)
theory Reversed_Bit_Lists

lemma bin_to_bl_cat_app:
  "bin_to_bl (n + nw) (concat_bit nw wa w) = bin_to_bl n w @ bin_to_bl nw wa" by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (n + nw) (concat_bit nw wa w) = bin_to_bl n w @ bin_to_bl nw wa
theory Reversed_Bit_Lists

lemma bl_to_bin_app_cat_alt: "concat_bit n w (bl_to_bin cs) = bl_to_bin (cs @ bin_to_bl n w)" by (simp add: bl_to_bin_app_cat)

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

lemma mask_lem: "(bl_to_bin (True # replicate n False)) = bl_to_bin (replicate n True) + 1" apply (unfold bl_to_bin_def) apply (induct n) apply simp apply (simp only: Suc_eq_plus1 replicate_add append_Cons [symmetric] bl_to_bin_aux_append) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (True # replicate n False) = bl_to_bin (replicate n True) + 1 proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1 proof (prove)
goal (2 subgoals):
 1. bl_to_bin_aux (True # replicate 0 False) 0 = bl_to_bin_aux (replicate 0 True) 0 + 1
 2. \<And>n. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1 \<Longrightarrow> bl_to_bin_aux (True # replicate (Suc n) False) 0 = bl_to_bin_aux (replicate (Suc n) True) 0 + 1 proof (prove)
goal (1 subgoal):
 1. \<And>n. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1 \<Longrightarrow> bl_to_bin_aux (True # replicate (Suc n) False) 0 = bl_to_bin_aux (replicate (Suc n) True) 0 + 1 proof (prove)
goal (1 subgoal):
 1. \<And>n. bl_to_bin_aux (True # replicate n False) 0 = bl_to_bin_aux (replicate n True) 0 + 1 \<Longrightarrow> bl_to_bin_aux (replicate 1 False) (bl_to_bin_aux (replicate n True) 0 + 1) = bl_to_bin_aux (replicate 1 True) (bl_to_bin_aux (replicate n True) 0) + 1 proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma bin_exhaust:
  "(\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q" for bin :: int apply (cases \<open>even bin\<close>) apply (auto elim!: evenE oddE) apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q) \<Longrightarrow> Q proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q; even bin\<rbrakk> \<Longrightarrow> Q
 2. \<lbrakk>\<And>x b. bin = of_bool b + 2 * x \<Longrightarrow> Q; odd bin\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>\<And>x ba. 2 * b = of_bool ba + 2 * x \<Longrightarrow> Q; bin = 2 * b\<rbrakk> \<Longrightarrow> Q
 2. \<And>b. \<lbrakk>\<And>x ba. 2 * b + 1 = of_bool ba + 2 * x \<Longrightarrow> Q; bin = 2 * b + 1\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>\<And>x ba. 2 * b + 1 = of_bool ba + 2 * x \<Longrightarrow> Q; bin = 2 * b + 1\<rbrakk> \<Longrightarrow> Q proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma size_rbl_pred: "length (rbl_pred bl) = length bl" by (induct bl) auto

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

lemma size_rbl_succ: "length (rbl_succ bl) = length bl" by (induct bl) auto

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

lemma size_rbl_add: "length (rbl_add bl cl) = length bl" by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ)

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

lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl" by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add)

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

lemma rbl_add_take2:
  "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb" apply (induct bla arbitrary: blb) apply simp apply clarsimp apply (case_tac blb, clarsimp) apply (clarsimp simp: Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb proof (prove)
goal (2 subgoals):
 1. \<And>blb. length [] \<le> length blb \<Longrightarrow> rbl_add [] (take (length []) blb) = rbl_add [] blb
 2. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_add (a # bla) (take (length (a # bla)) blb) = rbl_add (a # bla) blb proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_add (a # bla) (take (length (a # bla)) blb) = rbl_add (a # bla) blb proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; Suc (length bla) \<le> length blb\<rbrakk> \<Longrightarrow> (let ws = rbl_add bla (tl (take (Suc (length bla)) blb)) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws)) = (let ws = rbl_add bla (tl blb) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws)) proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb aa list. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb; Suc (length bla) \<le> length blb; blb = aa # list\<rbrakk> \<Longrightarrow> (let ws = rbl_add bla (tl (take (Suc (length bla)) blb)) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws)) = (let ws = rbl_add bla (tl blb) in (a = (\<not> hd blb)) # (if hd blb \<and> a then rbl_succ ws else ws)) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb" apply (induct bla arbitrary: blb) apply simp apply clarsimp apply (case_tac blb, clarsimp) apply (clarsimp simp: Let_def rbl_add_app2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb proof (prove)
goal (2 subgoals):
 1. \<And>blb. length [] \<le> length blb \<Longrightarrow> rbl_mult [] (blb @ blc) = rbl_mult [] blb
 2. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_mult (a # bla) (blb @ blc) = rbl_mult (a # bla) blb proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; length (a # bla) \<le> length blb\<rbrakk> \<Longrightarrow> rbl_mult (a # bla) (blb @ blc) = rbl_mult (a # bla) blb proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; Suc (length bla) \<le> length blb\<rbrakk> \<Longrightarrow> (let ws = False # rbl_mult bla blb in if a then rbl_add ws (blb @ blc) else ws) = (let ws = False # rbl_mult bla blb in if a then rbl_add ws blb else ws) proof (prove)
goal (1 subgoal):
 1. \<And>a bla blb aa list. \<lbrakk>\<And>blb. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb; Suc (length bla) \<le> length blb; blb = aa # list\<rbrakk> \<Longrightarrow> (let ws = False # rbl_mult bla blb in if a then rbl_add ws (blb @ blc) else ws) = (let ws = False # rbl_mult bla blb in if a then rbl_add ws blb else ws) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma rbl_mult_take2:
  "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb" apply (rule trans) apply (rule rbl_mult_app2 [symmetric]) apply simp apply (rule_tac f = "rbl_mult bla" in arg_cong) apply (rule append_take_drop_id) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb proof (prove)
goal (2 subgoals):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb) = ?s
 2. length bla \<le> length blb \<Longrightarrow> ?s = rbl_mult bla blb proof (prove)
goal (2 subgoals):
 1. length bla \<le> length blb \<Longrightarrow> length bla \<le> length (take (length bla) blb)
 2. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb @ ?blc3) = rbl_mult bla blb proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> rbl_mult bla (take (length bla) blb @ ?blc3) = rbl_mult bla blb proof (prove)
goal (1 subgoal):
 1. length bla \<le> length blb \<Longrightarrow> take (length bla) blb @ ?blc3 = blb proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma rbl_add_split:
  "P (rbl_add (y # ys) (x # xs)) =
    (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow>
      (y \<longrightarrow> ((x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws)))) \<and>
      (\<not> y \<longrightarrow> P (x # ws)))" by (cases y) (auto simp: Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (rbl_add (y # ys) (x # xs)) = (\<forall>ws. length ws = length ys \<longrightarrow> ws = rbl_add ys xs \<longrightarrow> (y \<longrightarrow> (x \<longrightarrow> P (False # rbl_succ ws)) \<and> (\<not> x \<longrightarrow> P (True # ws))) \<and> (\<not> y \<longrightarrow> P (x # ws)))
theory Reversed_Bit_Lists

lemma rbl_mult_split:
  "P (rbl_mult (y # ys) xs) =
    (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow>
      (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))" by (auto simp: Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (rbl_mult (y # ys) xs) = (\<forall>ws. length ws = Suc (length ys) \<longrightarrow> ws = False # rbl_mult ys xs \<longrightarrow> (y \<longrightarrow> P (rbl_add ws xs)) \<and> (\<not> y \<longrightarrow> P ws))
theory Reversed_Bit_Lists

lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))" apply (unfold bin_to_bl_def) apply (induction n arbitrary: bin) apply simp_all apply (case_tac bin rule: bin_exhaust) apply (simp_all add: bin_to_bl_aux_alt ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1)) proof (prove)
goal (1 subgoal):
 1. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) []) proof (prove)
goal (2 subgoals):
 1. \<And>bin. rbl_succ (rev (bin_to_bl_aux 0 bin [])) = rev (bin_to_bl_aux 0 (bin + 1) [])
 2. \<And>n bin. (\<And>bin. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) [])) \<Longrightarrow> rbl_succ (rev (bin_to_bl_aux (Suc n) bin [])) = rev (bin_to_bl_aux (Suc n) (bin + 1) []) proof (prove)
goal (1 subgoal):
 1. \<And>n bin. (\<And>bin. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) [])) \<Longrightarrow> rbl_succ (rev (bin_to_bl_aux n (bin div 2) [odd bin])) = rev (bin_to_bl_aux n ((bin + 1) div 2) [even bin]) proof (prove)
goal (1 subgoal):
 1. \<And>n bin x b. \<lbrakk>\<And>bin. rbl_succ (rev (bin_to_bl_aux n bin [])) = rev (bin_to_bl_aux n (bin + 1) []); bin = of_bool b + 2 * x\<rbrakk> \<Longrightarrow> rbl_succ (rev (bin_to_bl_aux n (bin div 2) [odd bin])) = rev (bin_to_bl_aux n ((bin + 1) div 2) [even bin]) proof (prove)
goal:
No subgoals!
theory Reversed_Bit_Lists

lemma rbl_add_long:
  "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
    rev (bin_to_bl n (bina + binb))" apply (rule box_equals [OF _ rbl_add_take2 rbl_add]) apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) apply (rule rev_swap [THEN iffD1]) apply (simp add: rev_take drop_bin2bl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = rev (bin_to_bl n (bina + binb)) proof (prove)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (take (length (rev (bin_to_bl n bina))) (rev (bin_to_bl m binb))) = rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))
 2. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb)) proof (prove)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> take (length (rev (bin_to_bl n bina))) (rev (bin_to_bl m binb)) = rev (bin_to_bl n binb)
 2. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb)) proof (prove)
goal (2 subgoals):
 1. n \<le> m \<Longrightarrow> rev (take (length (rev (bin_to_bl n bina))) (rev (bin_to_bl m binb))) = bin_to_bl n binb
 2. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb)) proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> length (rev (bin_to_bl n bina)) \<le> length (rev (bin_to_bl m binb)) proof (prove)
goal:
No subgoals!