theory Move_C

lemma word_minus_1_shiftr:
  notes word_unat.Rep_inject[simp del]
  fixes w :: "'a::len word"
  assumes low_bits_zero: "w && mask n = 0"
  assumes neq_zero: "w \<noteq> 0"
  shows "(w - 1) >> n = (w >> n) - 1" using neq_zero low_bits_zero apply (subgoal_tac "n < LENGTH('a)") prefer 2 apply (metis not_less ucast_id ucast_mask_drop) apply (rule_tac t="w - 1" and s="(w && ~~ mask n) - 1" in subst,
         fastforce simp: low_bits_zero mask_eq_x_eq_0) apply (clarsimp simp: mask_eq_0_eq_x neg_mask_is_div lt1_neq0[symmetric]) apply (subst shiftr_div_2n_w)+ apply (rule word_uint.Rep_eqD) apply (simp only: uint_word_ariths uint_div uint_power_lower) apply (subst mod_pos_pos_trivial, fastforce, fastforce)+ apply (subst mod_pos_pos_trivial) apply (simp add: word_less_def word_le_def) apply (subst uint_1[symmetric]) apply (fastforce intro: uint_sub_lt2p) apply (subst int_div_sub_1, fastforce) apply (clarsimp simp: and_mask_dvd low_bits_zero) apply (subst mod_pos_pos_trivial) apply (simp add: word_le_def) apply (metis mult_zero_left neq_zero div_positive_int linorder_not_le uint_2p_alt word_div_lt_eq_0
                 word_less_def zless2p) apply (metis shiftr_div_2n uint_1 uint_sub_lt2p) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w - 1 >> n = (w >> n) - 1 proof (prove)
using this:
w \<noteq> 0
w && mask n = 0

goal (1 subgoal):
 1. w - 1 >> n = (w >> n) - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w \<noteq> 0; w && mask n = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> w - 1 >> n = (w >> n) - 1
 2. \<lbrakk>w \<noteq> 0; w && mask n = 0\<rbrakk> \<Longrightarrow> n < LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w \<noteq> 0; w && mask n = 0\<rbrakk> \<Longrightarrow> n < LENGTH('a)
 2. \<lbrakk>w \<noteq> 0; w && mask n = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> w - 1 >> n = (w >> n) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<noteq> 0; w && mask n = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> w - 1 >> n = (w >> n) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<noteq> 0; w && mask n = 0; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (w && ~~ mask n) - 1 >> n = (w >> n) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> w - 1 >> n = (w >> n) - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (w - 1) div 2 ^ n = w div 2 ^ n - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint ((w - 1) div 2 ^ n) = uint (w div 2 ^ n - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (uint w - 1 mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) div 2 ^ n = (uint w div 2 ^ n - 1 mod 2 ^ LENGTH('a)) mod 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (uint w - 1) mod 2 ^ LENGTH('a) div 2 ^ n = (uint w div 2 ^ n - 1) mod 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 0 \<le> uint w - 1
 2. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w - 1 < 2 ^ LENGTH('a)
 3. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (uint w - 1) div 2 ^ n = (uint w div 2 ^ n - 1) mod 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w - 1 < 2 ^ LENGTH('a)
 2. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (uint w - 1) div 2 ^ n = (uint w div 2 ^ n - 1) mod 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w - uint 1 < 2 ^ LENGTH('a)
 2. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (uint w - 1) div 2 ^ n = (uint w div 2 ^ n - 1) mod 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (uint w - 1) div 2 ^ n = (uint w div 2 ^ n - 1) mod 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> (if 2 ^ n dvd uint w then uint w div 2 ^ n - 1 else uint w div 2 ^ n) = (uint w div 2 ^ n - 1) mod 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 = (uint w div 2 ^ n - 1) mod 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 0 \<le> uint w div 2 ^ n - 1
 2. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 < 2 ^ LENGTH('a)
 3. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 = uint w div 2 ^ n - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 \<le> uint w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> 0 < uint w div 2 ^ n
 2. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 < 2 ^ LENGTH('a)
 3. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 = uint w div 2 ^ n - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 < 2 ^ LENGTH('a)
 2. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 = uint w div 2 ^ n - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> w; w div 2 ^ n * 2 ^ n = w; n < LENGTH('a)\<rbrakk> \<Longrightarrow> uint w div 2 ^ n - 1 = uint w div 2 ^ n - 1 proof (prove)
goal:
No subgoals!