theory Aligned

lemma is_alignedE:
  fixes w :: \<open>'a::len word\<close>
  assumes \<open>is_aligned w n\<close>
  obtains q where \<open>w = 2 ^ n * word_of_nat q\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close> proof (cases \<open>n < LENGTH('a)\<close>) case False with assms have \<open>w = 0\<close> by (simp add: is_aligned_beyond_length) with that [of 0] show thesis by simp next case True moreover define m where \<open>m = LENGTH('a) - n\<close> ultimately have l: \<open>LENGTH('a) = n + m\<close> and \<open>m \<noteq> 0\<close> by simp_all from \<open>n < LENGTH('a)\<close> have *: \<open>unat (2 ^ n :: 'a word) = 2 ^ n\<close> by transfer simp from assms have \<open>2 ^ n udvd w\<close> by (simp add: is_aligned_iff_udvd) then obtain v :: \<open>'a word\<close>
    where \<open>unat w = unat (2 ^ n :: 'a word) * unat v\<close> .. moreover define q where \<open>q = unat v\<close> ultimately have unat_w: \<open>unat w = 2 ^ n * q\<close> by (simp add: *) then have \<open>word_of_nat (unat w) = (word_of_nat (2 ^ n * q) :: 'a word)\<close> by simp then have w: \<open>w = 2 ^ n * word_of_nat q\<close> by simp moreover have \<open>q < 2 ^ (LENGTH('a) - n)\<close> proof (rule ccontr) assume \<open>\<not> q < 2 ^ (LENGTH('a) - n)\<close> then have \<open>2 ^ (LENGTH('a) - n) \<le> q\<close> by simp then have \<open>2 ^ LENGTH('a) \<le> 2 ^ n * q\<close> by (simp add: l power_add) with unat_w [symmetric] show False by (metis le_antisym nat_less_le unsigned_less) qed ultimately show thesis using that by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
this:
\<not> n < LENGTH('a)

goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
is_aligned w n
\<not> n < LENGTH('a) proof (prove)
using this:
is_aligned w n
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. w = 0 proof (state)
this:
w = 0

goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
\<lbrakk>w = 2 ^ n * word_of_nat 0; 0 < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = 0 proof (prove)
using this:
\<lbrakk>w = 2 ^ n * word_of_nat 0; 0 < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = 0

goal (1 subgoal):
 1. thesis proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
this:
m = LENGTH('a) - n

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
n < LENGTH('a)
m = LENGTH('a) - n proof (prove)
using this:
n < LENGTH('a)
m = LENGTH('a) - n

goal (1 subgoal):
 1. LENGTH('a) = n + m &&& m \<noteq> 0 proof (state)
this:
LENGTH('a) = n + m
m \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
n < LENGTH('a) proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. unat (2 ^ n) = 2 ^ n proof (state)
this:
unat (2 ^ n) = 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
is_aligned w n proof (prove)
using this:
is_aligned w n

goal (1 subgoal):
 1. 2 ^ n udvd w proof (state)
this:
2 ^ n udvd w

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
2 ^ n udvd w proof (prove)
using this:
2 ^ n udvd w

goal (1 subgoal):
 1. (\<And>v. unat w = unat (2 ^ n) * unat v \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
unat w = unat (2 ^ n) * unat v

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
this:
unat w = unat (2 ^ n) * unat v

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
this:
q = unat v

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
unat w = unat (2 ^ n) * unat v
q = unat v proof (prove)
using this:
unat w = unat (2 ^ n) * unat v
q = unat v

goal (1 subgoal):
 1. unat w = 2 ^ n * q proof (state)
this:
unat w = 2 ^ n * q

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
unat w = 2 ^ n * q proof (prove)
using this:
unat w = 2 ^ n * q

goal (1 subgoal):
 1. word_of_nat (unat w) = word_of_nat (2 ^ n * q) proof (state)
this:
word_of_nat (unat w) = word_of_nat (2 ^ n * q)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
word_of_nat (unat w) = word_of_nat (2 ^ n * q) proof (prove)
using this:
word_of_nat (unat w) = word_of_nat (2 ^ n * q)

goal (1 subgoal):
 1. w = 2 ^ n * word_of_nat q proof (state)
this:
w = 2 ^ n * word_of_nat q

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (state)
this:
w = 2 ^ n * word_of_nat q

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. q < 2 ^ (LENGTH('a) - n) proof (state)
goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False proof (state)
this:
\<not> q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False proof (chain)
picking this:
\<not> q < 2 ^ (LENGTH('a) - n) proof (prove)
using this:
\<not> q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - n) \<le> q proof (state)
this:
2 ^ (LENGTH('a) - n) \<le> q

goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False proof (chain)
picking this:
2 ^ (LENGTH('a) - n) \<le> q proof (prove)
using this:
2 ^ (LENGTH('a) - n) \<le> q

goal (1 subgoal):
 1. 2 ^ LENGTH('a) \<le> 2 ^ n * q proof (state)
this:
2 ^ LENGTH('a) \<le> 2 ^ n * q

goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False proof (chain)
picking this:
2 ^ n * q = unat w
2 ^ LENGTH('a) \<le> 2 ^ n * q proof (prove)
using this:
2 ^ n * q = unat w
2 ^ LENGTH('a) \<le> 2 ^ n * q

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals! proof (state)
this:
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis proof (chain)
picking this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n) proof (prove)
using this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. thesis proof (prove)
using this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)
\<lbrakk>w = 2 ^ n * word_of_nat ?q; ?q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis proof (state)
this:
thesis

goal:
No subgoals!