theory Reversed_Bit_Lists

lemma rbl_add:
  "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
    rev (bin_to_bl n (bina + binb))" apply (unfold bin_to_bl_def) apply (induct n) apply simp apply clarsimp apply (case_tac bina rule: bin_exhaust) apply (case_tac binb rule: bin_exhaust) apply (case_tac b) apply (case_tac [!] "ba") apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina + binb)) proof (prove)
goal (1 subgoal):
 1. \<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []) proof (prove)
goal (2 subgoals):
 1. \<And>bina binb. rbl_add (rev (bin_to_bl_aux 0 bina [])) (rev (bin_to_bl_aux 0 binb [])) = rev (bin_to_bl_aux 0 (bina + binb) [])
 2. \<And>n bina binb. (\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) [])) \<Longrightarrow> rbl_add (rev (bin_to_bl_aux (Suc n) bina [])) (rev (bin_to_bl_aux (Suc n) binb [])) = rev (bin_to_bl_aux (Suc n) (bina + binb) []) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) [])) \<Longrightarrow> rbl_add (rev (bin_to_bl_aux (Suc n) bina [])) (rev (bin_to_bl_aux (Suc n) binb [])) = rev (bin_to_bl_aux (Suc n) (bina + binb) []) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) [])) \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb]) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb]) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb]) proof (prove)
goal (2 subgoals):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; b\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 2. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; \<not> b\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb]) proof (prove)
goal (4 subgoals):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; b; ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 2. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; b; \<not> ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 3. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; \<not> b; ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb])
 4. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_add (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina + binb) []); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa; \<not> b; \<not> ba\<rbrakk> \<Longrightarrow> rbl_add (rev (bin_to_bl_aux n (bina div 2) [odd bina])) (rev (bin_to_bl_aux n (binb div 2) [odd binb])) = rev (bin_to_bl_aux n ((bina + binb) div 2) [even bina = odd binb]) proof (prove)
goal:
No subgoals!