theory Bits_Int

lemma bin_rsplit_l [rule_format]:
  "\<forall>bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m bin)" apply (rule_tac a = "m" in wf_less_than [THEN wf_induct]) apply (simp (no_asm) add: bin_rsplitl_def bin_rsplit_def) apply (rule allI) apply (subst bin_rsplitl_aux.simps) apply (subst bin_rsplit_aux.simps) apply (clarsimp simp: Let_def split: prod.split) apply (simp add: ac_simps) apply (subst rsplit_aux_alts(1)) apply (subst rsplit_aux_alts(2)) apply clarsimp unfolding bin_rsplit_def bin_rsplitl_def apply (simp add: drop_bit_take_bit) apply (case_tac \<open>x < n\<close>) apply (simp_all add: not_less min_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, take_bit m bin) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> less_than \<longrightarrow> (\<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin)) \<Longrightarrow> \<forall>bin. bin_rsplitl n (x, bin) = bin_rsplit n (x, take_bit x bin) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>y. (y, x) \<in> less_than \<longrightarrow> (\<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin)) \<Longrightarrow> \<forall>bin. bin_rsplitl_aux n x bin [] = bin_rsplit_aux n x (take_bit x bin) [] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<forall>y. (y, x) \<in> less_than \<longrightarrow> (\<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin)) \<Longrightarrow> bin_rsplitl_aux n x bin [] = bin_rsplit_aux n x (take_bit x bin) [] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<forall>y. (y, x) \<in> less_than \<longrightarrow> (\<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin)) \<Longrightarrow> (if x = 0 \<or> n = 0 then [] else let (a, b) = bin_split (min x n) bin in bin_rsplitl_aux n (x - n) a [b]) = bin_rsplit_aux n x (take_bit x bin) [] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<forall>y. (y, x) \<in> less_than \<longrightarrow> (\<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin)) \<Longrightarrow> (if x = 0 \<or> n = 0 then [] else let (a, b) = bin_split (min x n) bin in bin_rsplitl_aux n (x - n) a [b]) = (if x = 0 \<or> n = 0 then [] else let (a, b) = bin_split n (take_bit x bin) in bin_rsplit_aux n (x - n) a [b]) proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin); 0 < x; 0 < n\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (x - n) (drop_bit (min x n) bin) [take_bit (min x n) bin] = bin_rsplit_aux n (x - n) (drop_bit n (take_bit x bin)) [take_bit (min n x) bin] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin); 0 < x; 0 < n\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (x - n) (drop_bit (min x n) bin) [take_bit (min x n) bin] = bin_rsplit_aux n (x - n) (drop_bit n (take_bit x bin)) [take_bit (min x n) bin] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin); 0 < x; 0 < n\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (x - n) (drop_bit (min x n) bin) [take_bit (min x n) bin] = bin_rsplit_aux n (x - n) (drop_bit n (take_bit x bin)) [] @ [take_bit (min x n) bin] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin); 0 < x; 0 < n\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (x - n) (drop_bit (min x n) bin) [] @ [take_bit (min x n) bin] = bin_rsplit_aux n (x - n) (drop_bit n (take_bit x bin)) [] @ [take_bit (min x n) bin] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl n (y, bin) = bin_rsplit n (y, take_bit y bin); 0 < x; 0 < n\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (x - n) (drop_bit (min x n) bin) [] = bin_rsplit_aux n (x - n) (drop_bit n (take_bit x bin)) [] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl_aux n (fst (y, bin)) (snd (y, bin)) [] = bin_rsplit_aux n (fst (y, take_bit y bin)) (snd (y, take_bit y bin)) []; 0 < x; 0 < n\<rbrakk> \<Longrightarrow> bin_rsplitl_aux n (x - n) (drop_bit (min x n) bin) [] = bin_rsplit_aux n (x - n) (drop_bit n (take_bit x bin)) [] proof (prove)
goal (1 subgoal):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl_aux n y bin [] = bin_rsplit_aux n y (take_bit y bin) []; 0 < x; 0 < n\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (x - n) (take_bit (x - n) (drop_bit (min x n) bin)) [] = bin_rsplit_aux n (x - n) (take_bit (x - n) (drop_bit n bin)) [] proof (prove)
goal (2 subgoals):
 1. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl_aux n y bin [] = bin_rsplit_aux n y (take_bit y bin) []; 0 < x; 0 < n; x < n\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (x - n) (take_bit (x - n) (drop_bit (min x n) bin)) [] = bin_rsplit_aux n (x - n) (take_bit (x - n) (drop_bit n bin)) []
 2. \<And>x bin. \<lbrakk>\<forall>y<x. \<forall>bin. bin_rsplitl_aux n y bin [] = bin_rsplit_aux n y (take_bit y bin) []; 0 < x; 0 < n; \<not> x < n\<rbrakk> \<Longrightarrow> bin_rsplit_aux n (x - n) (take_bit (x - n) (drop_bit (min x n) bin)) [] = bin_rsplit_aux n (x - n) (take_bit (x - n) (drop_bit n bin)) [] proof (prove)
goal:
No subgoals!