theory Bits_Int

lemma bin_rsplit_aux_len_indep:
  "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
    length (bin_rsplit_aux n nw v bs) =
    length (bin_rsplit_aux n nw w cs)" proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) case (1 n m w cs v bs) show ?case proof (cases "m = 0") case True with \<open>length bs = length cs\<close> show ?thesis by simp next case False from "1.hyps" [of \<open>bin_split n w\<close> \<open>drop_bit n w\<close> \<open>take_bit n w\<close>] \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
      length (bin_rsplit_aux n (m - n) v bs) =
      length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs))" using bin_rsplit_aux_len by fastforce from \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> show ?thesis by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; length bs = length cs\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n nw v bs) = length (bin_rsplit_aux n nw w cs) proof (state)
goal (1 subgoal):
 1. \<And>n m c bs v bsa. \<lbrakk>\<And>x xa y v bsa. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x; n \<noteq> 0; length bsa = length (y # bs)\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) v bsa) = length (bin_rsplit_aux n (m - n) xa (y # bs)); n \<noteq> 0; length bsa = length bs\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n m v bsa) = length (bin_rsplit_aux n m c bs) proof (state)
this:
\<lbrakk>\<not> (m = 0 \<or> n = 0); ?x = bin_split n w; (?xa, ?y) = ?x; n \<noteq> 0; length ?bs = length (?y # cs)\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) ?v ?bs) = length (bin_rsplit_aux n (m - n) ?xa (?y # cs))
n \<noteq> 0
length bs = length cs

goal (1 subgoal):
 1. \<And>n m c bs v bsa. \<lbrakk>\<And>x xa y v bsa. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x; n \<noteq> 0; length bsa = length (y # bs)\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) v bsa) = length (bin_rsplit_aux n (m - n) xa (y # bs)); n \<noteq> 0; length bsa = length bs\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n m v bsa) = length (bin_rsplit_aux n m c bs) proof (prove)
goal (1 subgoal):
 1. length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs)
 2. m \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (state)
this:
m = 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs)
 2. m \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (chain)
picking this:
length bs = length cs
m = 0 proof (prove)
using this:
length bs = length cs
m = 0

goal (1 subgoal):
 1. length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (state)
this:
length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs)

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (state)
goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (state)
this:
m \<noteq> 0

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (chain)
picking this:
\<lbrakk>\<not> (m = 0 \<or> n = 0); bin_split n w = bin_split n w; (drop_bit n w, take_bit n w) = bin_split n w; n \<noteq> 0; length ?bs = length (take_bit n w # cs)\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) ?v ?bs) = length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs))
m \<noteq> 0
n \<noteq> 0 proof (prove)
using this:
\<lbrakk>\<not> (m = 0 \<or> n = 0); bin_split n w = bin_split n w; (drop_bit n w, take_bit n w) = bin_split n w; n \<noteq> 0; length ?bs = length (take_bit n w # cs)\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) ?v ?bs) = length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs))
m \<noteq> 0
n \<noteq> 0

goal (1 subgoal):
 1. \<And>v bs. length bs = Suc (length cs) \<Longrightarrow> length (bin_rsplit_aux n (m - n) v bs) = length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs)) proof (prove)
using this:
\<lbrakk>\<not> (m = 0 \<or> n = 0); bin_split n w = bin_split n w; (drop_bit n w, take_bit n w) = bin_split n w; n \<noteq> 0; length ?bs = length (take_bit n w # cs)\<rbrakk> \<Longrightarrow> length (bin_rsplit_aux n (m - n) ?v ?bs) = length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs))
m \<noteq> 0
n \<noteq> 0
?n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux ?n ?nw ?w ?cs) = (?nw + ?n - 1) div ?n + length ?cs

goal (1 subgoal):
 1. \<And>v bs. length bs = Suc (length cs) \<Longrightarrow> length (bin_rsplit_aux n (m - n) v bs) = length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs)) proof (state)
this:
length ?bs = Suc (length cs) \<Longrightarrow> length (bin_rsplit_aux n (m - n) ?v ?bs) = length (bin_rsplit_aux n (m - n) (drop_bit n w) (take_bit n w # cs))

goal (1 subgoal):
 1. m \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (chain)
picking this:
length bs = length cs
n \<noteq> 0 proof (prove)
using this:
length bs = length cs
n \<noteq> 0

goal (1 subgoal):
 1. length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs) proof (state)
this:
length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs)

goal:
No subgoals! proof (state)
this:
length (bin_rsplit_aux n m v bs) = length (bin_rsplit_aux n m w cs)

goal:
No subgoals!