[STATEMENT]
lemma bit_and_int_iff:
  \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close> for k l :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (k AND l) n = (bit k n \<and> bit l n)
[PROOF STEP]
proof (induction n arbitrary: k l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k l. bit (k AND l) 0 = (bit k 0 \<and> bit l 0)
 2. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. \<And>k l. bit (k AND l) 0 = (bit k 0 \<and> bit l 0)
 2. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (k AND l) 0 = (bit k 0 \<and> bit l 0)
[PROOF STEP]
by (simp add: and_int_rec [of k l] bit_0)
[PROOF STATE]
proof (state)
this:
bit (k AND l) 0 = (bit k 0 \<and> bit l 0)

goal (1 subgoal):
 1. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
bit (?k AND ?l) n = (bit ?k n \<and> bit ?l n)

goal (1 subgoal):
 1. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bit (?k AND ?l) n = (bit ?k n \<and> bit ?l n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bit (?k AND ?l) n = (bit ?k n \<and> bit ?l n)

goal (1 subgoal):
 1. bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
by (simp add: and_int_rec [of k l] bit_Suc)
[PROOF STATE]
proof (state)
this:
bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed