[STATEMENT]
lemma bit_signed_drop_bit_iff [bit_simps]:
  \<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (signed_drop_bit m w) n = bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w n. (n < LENGTH('a) \<and> bit ((drop_bit m \<circ> signed_take_bit (LENGTH('a) - Suc 0)) w) n) = ((if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n) < LENGTH('a) \<and> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n))
[PROOF STEP]
apply (auto simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m w n. \<lbrakk>LENGTH('a) - Suc 0 \<le> m + n; n < LENGTH('a) - m; n < LENGTH('a); bit w (LENGTH('a) - Suc 0)\<rbrakk> \<Longrightarrow> bit w (m + n)
 2. \<And>m w n. \<lbrakk>LENGTH('a) - Suc 0 \<le> m + n; n < LENGTH('a) - m; m + n < LENGTH('a); bit w (m + n)\<rbrakk> \<Longrightarrow> bit w (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (metis add.commute le_antisym less_diff_conv less_eq_decr_length_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m w n. \<lbrakk>LENGTH('a) - Suc 0 \<le> m + n; n < LENGTH('a) - m; m + n < LENGTH('a); bit w (m + n)\<rbrakk> \<Longrightarrow> bit w (LENGTH('a) - Suc 0)
[PROOF STEP]
apply (metis le_antisym less_eq_decr_length_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done