theory Word_64

lemma mask_step_down_64:
  \<open>\<exists>x. mask x = b\<close> if \<open>b && 1 = 1\<close>
    and \<open>\<exists>x. x < 64 \<and> mask x = b >> 1\<close> for b :: \<open>64word\<close> proof - from \<open>b && 1 = 1\<close> have \<open>odd b\<close> by (auto simp add: mod_2_eq_odd and_one_eq) then have \<open>b mod 2 = 1\<close> using odd_iff_mod_2_eq_one by blast from \<open>\<exists>x. x < 64 \<and> mask x = b >> 1\<close> obtain x where \<open>x < 64\<close> \<open>mask x = b >> 1\<close> by blast then have \<open>mask x = b div 2\<close> using shiftr1_is_div_2 [of b] by simp with \<open>b mod 2 = 1\<close> have \<open>2 * mask x + 1 = 2 * (b div 2) + b mod 2\<close> by (simp only:) also have \<open>\<dots> = b\<close> by (simp add: mult_div_mod_eq) finally have \<open>2 * mask x + 1 = b\<close> . moreover have \<open>mask (Suc x) = 2 * mask x + (1 :: 'a::len word)\<close> by (simp add: mask_Suc_rec) ultimately show ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. mask x = b proof (state)
goal (1 subgoal):
 1. \<exists>x. mask x = b proof (chain)
picking this:
b && 1 = 1 proof (prove)
using this:
b && 1 = 1

goal (1 subgoal):
 1. odd b proof (state)
this:
odd b

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (chain)
picking this:
odd b proof (prove)
using this:
odd b

goal (1 subgoal):
 1. b mod 2 = 1 proof (prove)
using this:
odd b
odd ?a = (?a mod (2::?'a) = (1::?'a))

goal (1 subgoal):
 1. b mod 2 = 1 proof (state)
this:
b mod 2 = 1

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (chain)
picking this:
\<exists>x<64. mask x = b >> 1 proof (prove)
using this:
\<exists>x<64. mask x = b >> 1

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x < 64; mask x = b >> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
x < 64
mask x = b >> 1

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (chain)
picking this:
x < 64
mask x = b >> 1 proof (prove)
using this:
x < 64
mask x = b >> 1

goal (1 subgoal):
 1. mask x = b div 2 proof (prove)
using this:
x < 64
mask x = b >> 1
b >> 1 = b div 2

goal (1 subgoal):
 1. mask x = b div 2 proof (state)
this:
mask x = b div 2

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (chain)
picking this:
b mod 2 = 1
mask x = b div 2 proof (prove)
using this:
b mod 2 = 1
mask x = b div 2

goal (1 subgoal):
 1. 2 * mask x + 1 = 2 * (b div 2) + b mod 2 proof (state)
this:
2 * mask x + 1 = 2 * (b div 2) + b mod 2

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (state)
this:
2 * mask x + 1 = 2 * (b div 2) + b mod 2

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (prove)
goal (1 subgoal):
 1. 2 * (b div 2) + b mod 2 = b proof (state)
this:
2 * (b div 2) + b mod 2 = b

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (chain)
picking this:
2 * mask x + 1 = b proof (prove)
using this:
2 * mask x + 1 = b

goal (1 subgoal):
 1. 2 * mask x + 1 = b proof (state)
this:
2 * mask x + 1 = b

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (state)
this:
2 * mask x + 1 = b

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (prove)
goal (1 subgoal):
 1. mask (Suc x) = 2 * mask x + 1 proof (state)
this:
mask (Suc x) = 2 * mask x + 1

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (chain)
picking this:
2 * mask x + 1 = b
mask (Suc x) = 2 * mask x + 1 proof (prove)
using this:
2 * mask x + 1 = b
mask (Suc x) = 2 * mask x + 1

goal (1 subgoal):
 1. \<exists>x. mask x = b proof (state)
this:
\<exists>x. mask x = b

goal:
No subgoals!