theory Word_Lemmas_Internal

lemma word_ctz_shiftr:
  fixes z::"'a::len word"
  assumes nz: "z \<noteq> 0"
  shows "n < LENGTH('a) \<Longrightarrow> n \<le> word_ctz z \<Longrightarrow> word_ctz (z >> n) = word_ctz z - n" apply (induction n; simp) apply (subst shiftr_Suc) apply (subst word_ctz_shiftr_1, simp) apply clarsimp apply (subgoal_tac "word_ctz z < n", clarsimp) apply (rule word_ctz_bound_above, clarsimp simp: word_size) apply (subst (asm) and_mask_eq_iff_shiftr_0[symmetric], clarsimp simp: nz) apply (rule word_ctz_bound_below, clarsimp simp: word_size) apply (rule mask_zero) apply (rule is_aligned_shiftr, simp add: is_aligned_mask) apply (case_tac "z && mask (Suc n) = 0", simp) apply (frule word_ctz_bound_above[rotated]; clarsimp simp: word_size) apply simp done

\<comment> \<open>Useful for solving goals of the form `(w::32 word) <= 0xFFFFFFFF` by simplification\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) = word_ctz z - n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> Suc n) = word_ctz z - Suc n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n >> 1) = word_ctz z - Suc n proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> z >> n \<noteq> 0
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> 1 \<le> word_ctz (z >> n)
 3. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>word_ctz 0 = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z; z >> n = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> 1 \<le> word_ctz (z >> n)
 3. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>word_ctz 0 = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z; z >> n = 0\<rbrakk> \<Longrightarrow> word_ctz z < n
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> 1 \<le> word_ctz (z >> n)
 3. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>word_ctz 0 = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z; z >> n = 0; z && mask n = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> 1 \<le> word_ctz (z >> n)
 3. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> 1 \<le> word_ctz (z >> n)
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> (z >> n) && mask 1 = 0
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> is_aligned (z >> n) 1
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> z && mask (Suc n) = 0
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z; z && mask (Suc n) \<noteq> 0\<rbrakk> \<Longrightarrow> z && mask (Suc n) = 0
 2. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>word_ctz (z >> n) = word_ctz z - n; Suc n < LENGTH('a); Suc n \<le> word_ctz z\<rbrakk> \<Longrightarrow> word_ctz (z >> n) - 1 = word_ctz z - Suc n proof (prove)
goal:
No subgoals!