[STATEMENT]
lemma aux_even_pow2_factor: "a > 0 \<Longrightarrow> \<exists>k b. ((a::nat) = (2^k) * b \<and> odd b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> \<exists>k b. a = 2 ^ k * b \<and> odd b
[PROOF STEP]
proof(induction  a rule: full_nat_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n

goal (1 subgoal):
 1. \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
proof (cases "odd n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
 2. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
odd n

goal (2 subgoals):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
 2. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
odd n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
odd n

goal (1 subgoal):
 1. \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
by (metis nat_power_eq_Suc_0_iff power_Suc power_Suc0_right power_commutes)
[PROOF STATE]
proof (state)
this:
\<exists>k b. n = 2 ^ k * b \<and> odd b

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> odd n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
have "(\<exists>t. n = 2 * t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. n = 2 * t
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> odd n

goal (1 subgoal):
 1. \<exists>t. n = 2 * t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t. n = 2 * t

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. n = 2 * t
[PROOF STEP]
obtain t where n_def:"n = 2 * t"
[PROOF STATE]
proof (prove)
using this:
\<exists>t. n = 2 * t

goal (1 subgoal):
 1. (\<And>t. n = 2 * t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
n = 2 * t

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 2 * t
[PROOF STEP]
have "t < n"
[PROOF STATE]
proof (prove)
using this:
n = 2 * t

goal (1 subgoal):
 1. t < n
[PROOF STEP]
using "1.prems"
[PROOF STATE]
proof (prove)
using this:
n = 2 * t
0 < n

goal (1 subgoal):
 1. t < n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
t < n

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t < n
[PROOF STEP]
have ih:"\<exists>r s. t = 2^r * s \<and> odd s"
[PROOF STATE]
proof (prove)
using this:
t < n

goal (1 subgoal):
 1. \<exists>r s. t = 2 ^ r * s \<and> odd s
[PROOF STEP]
using 1 n_def
[PROOF STATE]
proof (prove)
using this:
t < n
\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b)
0 < n
n = 2 * t

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

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r s. t = 2 ^ r * s \<and> odd s
[PROOF STEP]
have "\<exists>r s. n = 2^(Suc r) * s"
[PROOF STATE]
proof (prove)
using this:
\<exists>r s. t = 2 ^ r * s \<and> odd s

goal (1 subgoal):
 1. \<exists>r s. n = 2 ^ Suc r * s
[PROOF STEP]
using n_def
[PROOF STATE]
proof (prove)
using this:
\<exists>r s. t = 2 ^ r * s \<and> odd s
n = 2 * t

goal (1 subgoal):
 1. \<exists>r s. n = 2 ^ Suc r * s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r s. n = 2 ^ Suc r * s

goal (1 subgoal):
 1. \<lbrakk>\<forall>m. Suc m \<le> n \<longrightarrow> 0 < m \<longrightarrow> (\<exists>k b. m = 2 ^ k * b \<and> odd b); 0 < n; \<not> odd n\<rbrakk> \<Longrightarrow> \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r s. n = 2 ^ Suc r * s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>r s. n = 2 ^ Suc r * s

goal (1 subgoal):
 1. \<exists>k b. n = 2 ^ k * b \<and> odd b
[PROOF STEP]
by (metis ih n_def power_commutes semiring_normalization_rules(18)
                          semiring_normalization_rules(28))
[PROOF STATE]
proof (state)
this:
\<exists>k b. n = 2 ^ k * b \<and> odd b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k b. n = 2 ^ k * b \<and> odd b

goal:
No subgoals!
[PROOF STEP]
qed