[STATEMENT]
lemma aux0_digit_wise_equiv:"a > 0 \<Longrightarrow> (\<exists>k. nth_bit a k = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
assume a_geq_0: "a > 0"
[PROOF STATE]
proof (state)
this:
0 < a

goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
consider (odd) "a mod 2 = 1" | (even) "a mod 2 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a mod 2 = 1 \<Longrightarrow> thesis; a mod 2 = 0 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>a mod 2 = 1 \<Longrightarrow> ?thesis; a mod 2 = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a mod 2 = 1 \<Longrightarrow> ?thesis; a mod 2 = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a mod 2 = 1 \<Longrightarrow> ?thesis; a mod 2 = 0 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a mod 2 = 1 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
 2. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
case odd
[PROOF STATE]
proof (state)
this:
a mod 2 = 1

goal (2 subgoals):
 1. a mod 2 = 1 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
 2. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod 2 = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a mod 2 = 1

goal (1 subgoal):
 1. \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
by (metis div_by_1 nth_bit_def power_0)
[PROOF STATE]
proof (state)
this:
\<exists>k. a \<exclamdown> k = 1

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
case even
[PROOF STATE]
proof (state)
this:
a mod 2 = 0

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a mod 2 = 0
[PROOF STEP]
have bk_def:"\<exists>k b. (a = (2^k) * b \<and> odd b)"
[PROOF STATE]
proof (prove)
using this:
a mod 2 = 0

goal (1 subgoal):
 1. \<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
using aux_even_pow2_factor a_geq_0
[PROOF STATE]
proof (prove)
using this:
a mod 2 = 0
0 < ?a \<Longrightarrow> \<exists>k b. ?a = 2 ^ k * b \<and> odd b
0 < a

goal (1 subgoal):
 1. \<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k b. a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
obtain b k where bk_cond:"(a = (2^k) * b \<and> odd b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k b. a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. (\<And>k b. a = 2 ^ k * b \<and> odd b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = 2 ^ k * b \<and> odd b
[PROOF STEP]
have "b = a div (2^k)"
[PROOF STATE]
proof (prove)
using this:
a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. b = a div 2 ^ k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = a div 2 ^ k

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = a div 2 ^ k
[PROOF STEP]
have digi_b:"nth_bit b 0 = 1"
[PROOF STATE]
proof (prove)
using this:
b = a div 2 ^ k

goal (1 subgoal):
 1. b \<exclamdown> 0 = 1
[PROOF STEP]
using bk_def
[PROOF STATE]
proof (prove)
using this:
b = a div 2 ^ k
\<exists>k b. a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. b \<exclamdown> 0 = 1
[PROOF STEP]
using bk_cond nth_bit_def odd_iff_mod_2_eq_one
[PROOF STATE]
proof (prove)
using this:
b = a div 2 ^ k
\<exists>k b. a = 2 ^ k * b \<and> odd b
a = 2 ^ k * b \<and> odd b
?num \<exclamdown> ?k = ?num div 2 ^ ?k mod 2
odd ?a = (?a mod (2::?'a) = (1::?'a))

goal (1 subgoal):
 1. b \<exclamdown> 0 = 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
b \<exclamdown> 0 = 1

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<exclamdown> 0 = 1
[PROOF STEP]
have "nth_bit a k = (nth_bit b 0)"
[PROOF STATE]
proof (prove)
using this:
b \<exclamdown> 0 = 1

goal (1 subgoal):
 1. a \<exclamdown> k = b \<exclamdown> 0
[PROOF STEP]
using nth_bit_def bk_cond
[PROOF STATE]
proof (prove)
using this:
b \<exclamdown> 0 = 1
?num \<exclamdown> ?k = ?num div 2 ^ ?k mod 2
a = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. a \<exclamdown> k = b \<exclamdown> 0
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
a \<exclamdown> k = b \<exclamdown> 0

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<exclamdown> k = b \<exclamdown> 0
[PROOF STEP]
have "nth_bit a k = 1"
[PROOF STATE]
proof (prove)
using this:
a \<exclamdown> k = b \<exclamdown> 0

goal (1 subgoal):
 1. a \<exclamdown> k = 1
[PROOF STEP]
using digi_b
[PROOF STATE]
proof (prove)
using this:
a \<exclamdown> k = b \<exclamdown> 0
b \<exclamdown> 0 = 1

goal (1 subgoal):
 1. a \<exclamdown> k = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<exclamdown> k = 1

goal (1 subgoal):
 1. a mod 2 = 0 \<Longrightarrow> \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<exclamdown> k = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<exclamdown> k = 1

goal (1 subgoal):
 1. \<exists>k. a \<exclamdown> k = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k. a \<exclamdown> k = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. a \<exclamdown> k = 1

goal:
No subgoals!
[PROOF STEP]
qed