theory Reversed_Bit_Lists

lemma rbl_mult:
  "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
    rev (bin_to_bl n (bina * binb))" apply (induct n arbitrary: bina binb) apply simp_all apply (unfold bin_to_bl_def) apply clarsimp apply (case_tac bina rule: bin_exhaust) apply (case_tac binb rule: bin_exhaust) apply (simp_all add: bin_to_bl_aux_alt) apply (simp_all add: rbbl_Cons rbl_mult_Suc rbl_add algebra_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb)) proof (prove)
goal (2 subgoals):
 1. \<And>bina binb. rbl_mult (rev (bin_to_bl 0 bina)) (rev (bin_to_bl 0 binb)) = rev (bin_to_bl 0 (bina * binb))
 2. \<And>n bina binb. (\<And>bina binb. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb))) \<Longrightarrow> rbl_mult (rev (bin_to_bl (Suc n) bina)) (rev (bin_to_bl (Suc n) binb)) = rev (bin_to_bl (Suc n) (bina * binb)) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb))) \<Longrightarrow> rbl_mult (rev (bin_to_bl (Suc n) bina)) (rev (bin_to_bl (Suc n) binb)) = rev (bin_to_bl (Suc n) (bina * binb)) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb. (\<And>bina binb. rbl_mult (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina * binb) [])) \<Longrightarrow> rbl_mult (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_mult (rev (bin_to_bl_aux n bina [])) (rev (bin_to_bl_aux n binb [])) = rev (bin_to_bl_aux n (bina * binb) [])) \<Longrightarrow> rbl_mult (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) [odd bina \<and> odd binb]) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b. \<lbrakk>\<And>bina binb. rbl_mult (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_mult (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) [odd bina \<and> odd binb]) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_mult (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_mult (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) [odd bina \<and> odd binb]) proof (prove)
goal (1 subgoal):
 1. \<And>n bina binb x b xa ba. \<lbrakk>\<And>bina binb. rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = rev (bin_to_bl n (bina * binb)); bina = of_bool b + 2 * x; binb = of_bool ba + 2 * xa\<rbrakk> \<Longrightarrow> (b \<longrightarrow> (ba \<longrightarrow> rbl_add (rbl_mult (rev (bin_to_bl n x)) (True # rev (bin_to_bl n xa))) (rev (bin_to_bl n xa)) = rev (bin_to_bl n ((1 + 2 * x) * (1 + 2 * xa) div 2))) \<and> (\<not> ba \<longrightarrow> rbl_add (rbl_mult (rev (bin_to_bl n x)) (False # rev (bin_to_bl n xa))) (rev (bin_to_bl n xa)) = rev (bin_to_bl n ((1 + 2 * x) * xa)))) \<and> (\<not> b \<longrightarrow> (ba \<longrightarrow> rbl_mult (rev (bin_to_bl n x)) (True # rev (bin_to_bl n xa)) = rev (bin_to_bl n (x * (1 + 2 * xa)))) \<and> (\<not> ba \<longrightarrow> rbl_mult (rev (bin_to_bl n x)) (False # rev (bin_to_bl n xa)) = rev (bin_to_bl n (2 * x * xa)))) proof (prove)
goal:
No subgoals!