theory Move_C

lemma word_highbits_bounded_highbits_eq:
  "\<lbrakk>x \<le> (y :: 'a::len word); y < (x >> n) + 1 << n\<rbrakk> \<Longrightarrow> x >> n  = y >> n" apply (cases "n < LENGTH('a)") prefer 2 apply (simp add: shiftr_eq_0) apply (drule_tac n=n in le_shiftr) apply (subst (asm) word_shiftl_add_distrib) apply (drule_tac word_less_sub_1) apply (simp only: add_diff_eq[symmetric] mask_def[symmetric] and_not_mask[symmetric]) apply (drule_tac u=y and n=n in le_shiftr) apply (subgoal_tac "(x && ~~ mask n) + mask n >> n \<le> x >> n") apply fastforce apply (subst aligned_shift') apply (fastforce simp: mask_lt_2pn) apply (fastforce simp: is_aligned_neg_mask) apply fastforce apply (fastforce simp: mask_shift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y < (x >> n) + 1 << n\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y < (x >> n) + 1 << n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x >> n = y >> n
 2. \<lbrakk>x \<le> y; y < (x >> n) + 1 << n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> y; y < (x >> n) + 1 << n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> x >> n = y >> n
 2. \<lbrakk>x \<le> y; y < (x >> n) + 1 << n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; y < (x >> n) + 1 << n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < (x >> n) + 1 << n; n < LENGTH('a); x >> n \<le> y >> n\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < (x >> n << n) + (1 << n); n < LENGTH('a); x >> n \<le> y >> n\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y \<le> (x >> n << n) + (1 << n) - 1\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y \<le> (x && ~~ mask n) + mask n\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> x >> n = y >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n; (x && ~~ mask n) + mask n >> n \<le> x >> n\<rbrakk> \<Longrightarrow> x >> n = y >> n
 2. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> (x && ~~ mask n) + mask n >> n \<le> x >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> (x && ~~ mask n) + mask n >> n \<le> x >> n proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> mask n < 2 ^ n
 2. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> is_aligned (x && ~~ mask n) n
 3. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> n \<le> LENGTH('a)
 4. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> x && ~~ mask n >> n \<le> x >> n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> is_aligned (x && ~~ mask n) n
 2. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> n \<le> LENGTH('a)
 3. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> x && ~~ mask n >> n \<le> x >> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> n \<le> LENGTH('a)
 2. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> x && ~~ mask n >> n \<le> x >> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < LENGTH('a); x >> n \<le> y >> n; y >> n \<le> (x && ~~ mask n) + mask n >> n\<rbrakk> \<Longrightarrow> x && ~~ mask n >> n \<le> x >> n proof (prove)
goal:
No subgoals!