[STATEMENT]
lemma shiftr1_bl:
  \<open>shiftr1 w = of_bl (butlast (to_bl w))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shiftr1 w = of_bl (butlast (to_bl w))
[PROOF STEP]
proof (rule bit_word_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
assume \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
show \<open>bit (shiftr1 w) n \<longleftrightarrow> bit (of_bl (butlast (to_bl w)) :: 'a word) n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
proof (cases \<open>n = LENGTH('a) - 1\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
 2. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = LENGTH('a) - 1

goal (2 subgoals):
 1. n = LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
 2. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = LENGTH('a) - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = LENGTH('a) - 1

goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
by (simp add: bit_shiftr1_iff bit_of_bl_iff)
[PROOF STATE]
proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> LENGTH('a) - 1

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
with \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (chain)
picking this:
n < LENGTH('a)
n \<noteq> LENGTH('a) - 1
[PROOF STEP]
have \<open>n < LENGTH('a) - 1\<close>
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)
n \<noteq> LENGTH('a) - 1

goal (1 subgoal):
 1. n < LENGTH('a) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < LENGTH('a) - 1

goal (1 subgoal):
 1. n \<noteq> LENGTH('a) - 1 \<Longrightarrow> bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
with \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (chain)
picking this:
n < LENGTH('a)
n < LENGTH('a) - 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)
n < LENGTH('a) - 1

goal (1 subgoal):
 1. bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n
[PROOF STEP]
by (simp add: bit_shiftr1_iff bit_of_bl_iff rev_nth nth_butlast
        word_size to_bl_nth)
[PROOF STATE]
proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bit (shiftr1 w) n = bit (of_bl (butlast (to_bl w))) n

goal:
No subgoals!
[PROOF STEP]
qed