theory Bits_Int

lemma bin_nth_rsplit [rule_format] :
  "n > 0 \<Longrightarrow> m < n \<Longrightarrow>
    \<forall>w k nw.
      rev sw = bin_rsplit n (nw, w) \<longrightarrow>
      k < size sw \<longrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (sw ! k) m = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w (k * n + m)" apply (induct sw) apply clarsimp apply clarsimp apply (drule bthrs) apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) apply (erule allE, erule impE, erule exI) apply (case_tac k) apply clarsimp prefer 2 apply clarsimp apply (erule allE) apply (erule (1) impE) apply (simp add: bit_drop_bit_eq ac_simps) apply (simp add: bit_take_bit_iff ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; m < n\<rbrakk> \<Longrightarrow> \<forall>w k nw. rev sw = bin_rsplit n (nw, w) \<longrightarrow> k < length sw \<longrightarrow> bit (sw ! k) m = bit w (k * n + m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; m < n\<rbrakk> \<Longrightarrow> \<forall>w k nw. rev [] = bin_rsplit n (nw, w) \<longrightarrow> k < length [] \<longrightarrow> bit ([] ! k) m = bit w (k * n + m)
 2. \<And>a sw. \<lbrakk>\<lbrakk>0 < n; m < n\<rbrakk> \<Longrightarrow> \<forall>w k nw. rev sw = bin_rsplit n (nw, w) \<longrightarrow> k < length sw \<longrightarrow> bit (sw ! k) m = bit w (k * n + m); 0 < n; m < n\<rbrakk> \<Longrightarrow> \<forall>w k nw. rev (a # sw) = bin_rsplit n (nw, w) \<longrightarrow> k < length (a # sw) \<longrightarrow> bit ((a # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (1 subgoal):
 1. \<And>a sw. \<lbrakk>\<lbrakk>0 < n; m < n\<rbrakk> \<Longrightarrow> \<forall>w k nw. rev sw = bin_rsplit n (nw, w) \<longrightarrow> k < length sw \<longrightarrow> bit (sw ! k) m = bit w (k * n + m); 0 < n; m < n\<rbrakk> \<Longrightarrow> \<forall>w k nw. rev (a # sw) = bin_rsplit n (nw, w) \<longrightarrow> k < length (a # sw) \<longrightarrow> bit ((a # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (1 subgoal):
 1. \<And>a sw w nw k. \<lbrakk>\<forall>w. (\<exists>nw. rev sw = bin_rsplit n (nw, w)) \<longrightarrow> (\<forall>k<length sw. bit (sw ! k) m = bit w (k * n + m)); m < n; rev sw @ [a] = bin_rsplit n (nw, w); k < Suc (length sw)\<rbrakk> \<Longrightarrow> bit ((a # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (1 subgoal):
 1. \<And>a sw w nw k. \<lbrakk>\<forall>w. (\<exists>nw. rev sw = bin_rsplit n (nw, w)) \<longrightarrow> (\<forall>k<length sw. bit (sw ! k) m = bit w (k * n + m)); m < n; k < Suc (length sw); rev sw @ [a] = (if fst (nw, w) = 0 \<or> n = 0 then [] else let (a, b) = bin_split n (snd (nw, w)) in bin_rsplit n (fst (nw, w) - n, a) @ [b])\<rbrakk> \<Longrightarrow> bit ((a # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (1 subgoal):
 1. \<And>sw w nw k. \<lbrakk>\<forall>w. (\<exists>nw. rev sw = bin_rsplit n (nw, w)) \<longrightarrow> (\<forall>k<length sw. bit (sw ! k) m = bit w (k * n + m)); m < n; k < Suc (length sw); 0 < nw \<and> 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w)\<rbrakk> \<Longrightarrow> bit ((take_bit n w # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (1 subgoal):
 1. \<And>sw w nw k. \<lbrakk>m < n; k < Suc (length sw); 0 < nw \<and> 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit ((take_bit n w # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (2 subgoals):
 1. \<And>sw w nw k. \<lbrakk>m < n; k < Suc (length sw); 0 < nw \<and> 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m); k = 0\<rbrakk> \<Longrightarrow> bit ((take_bit n w # sw) ! k) m = bit w (k * n + m)
 2. \<And>sw w nw k nat. \<lbrakk>m < n; k < Suc (length sw); 0 < nw \<and> 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m); k = Suc nat\<rbrakk> \<Longrightarrow> bit ((take_bit n w # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (2 subgoals):
 1. \<And>sw w nw. \<lbrakk>m < n; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit (take_bit n w) m = bit w m
 2. \<And>sw w nw k nat. \<lbrakk>m < n; k < Suc (length sw); 0 < nw \<and> 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m); k = Suc nat\<rbrakk> \<Longrightarrow> bit ((take_bit n w # sw) ! k) m = bit w (k * n + m) proof (prove)
goal (2 subgoals):
 1. \<And>sw w nw k nat. \<lbrakk>m < n; k < Suc (length sw); 0 < nw \<and> 0 < n; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m); k = Suc nat\<rbrakk> \<Longrightarrow> bit ((take_bit n w # sw) ! k) m = bit w (k * n + m)
 2. \<And>sw w nw. \<lbrakk>m < n; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit (take_bit n w) m = bit w m proof (prove)
goal (2 subgoals):
 1. \<And>sw w nw nat. \<lbrakk>m < n; nat < length sw; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit (drop_bit n w) (nat * n + m) = bit w (n + nat * n + m)
 2. \<And>sw w nw. \<lbrakk>m < n; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit (take_bit n w) m = bit w m proof (prove)
goal (2 subgoals):
 1. \<And>sw w nw nat. \<lbrakk>m < n; nat < length sw; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); ?k40 sw w nw nat < length sw \<longrightarrow> bit (sw ! ?k40 sw w nw nat) m = bit (drop_bit n w) (?k40 sw w nw nat * n + m)\<rbrakk> \<Longrightarrow> bit (drop_bit n w) (nat * n + m) = bit w (n + nat * n + m)
 2. \<And>sw w nw. \<lbrakk>m < n; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit (take_bit n w) m = bit w m proof (prove)
goal (2 subgoals):
 1. \<And>sw w nw nat. \<lbrakk>m < n; nat < length sw; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); bit (sw ! nat) m = bit (drop_bit n w) (nat * n + m)\<rbrakk> \<Longrightarrow> bit (drop_bit n w) (nat * n + m) = bit w (n + nat * n + m)
 2. \<And>sw w nw. \<lbrakk>m < n; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit (take_bit n w) m = bit w m proof (prove)
goal (1 subgoal):
 1. \<And>sw w nw. \<lbrakk>m < n; 0 < nw; rev sw = bin_rsplit n (nw - n, drop_bit n w); \<forall>k<length sw. bit (sw ! k) m = bit (drop_bit n w) (k * n + m)\<rbrakk> \<Longrightarrow> bit (take_bit n w) m = bit w m proof (prove)
goal:
No subgoals!