theory Untyped_R

lemma reset_ineq_eq_idx_0:
  "idx \<le> 2 ^ sz \<Longrightarrow> b \<le> sz
    \<Longrightarrow> (ptr :: obj_ref) \<noteq> 0 \<Longrightarrow> is_aligned ptr sz \<Longrightarrow> sz < word_bits
    \<Longrightarrow> (ptr + of_nat idx - 1 < ptr) = (idx = 0)" apply (cases "idx = 0") apply (simp add: gt0_iff_gem1[symmetric] word_neq_0_conv) apply simp apply (subgoal_tac "ptr \<le> ptr + of_nat idx - 1", simp_all)[1] apply (subst field_simps[symmetric], erule is_aligned_no_wrap') apply (subst word_less_nat_alt) apply simp apply (subst unat_of_nat_minus_1) apply (erule order_le_less_trans, rule power_strict_increasing) apply (simp add: word_bits_def) apply simp apply (rule notI, simp) apply (erule order_less_le_trans[rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits\<rbrakk> \<Longrightarrow> (ptr + word_of_nat idx - 1 < ptr) = (idx = 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; idx = 0\<rbrakk> \<Longrightarrow> (ptr + word_of_nat idx - 1 < ptr) = (idx = 0)
 2. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; idx \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr + word_of_nat idx - 1 < ptr) = (idx = 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; idx \<noteq> 0\<rbrakk> \<Longrightarrow> (ptr + word_of_nat idx - 1 < ptr) = (idx = 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> \<not> ptr + word_of_nat idx - 1 < ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; is_aligned ptr sz; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat idx - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> word_of_nat idx - 1 < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> unat (word_of_nat idx - 1) < unat (2 ^ sz) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> unat (word_of_nat idx - 1) < 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx < 2 ^ LENGTH(32)
 2. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx \<noteq> 0
 3. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx - 1 < 2 ^ sz proof (prove)
goal (4 subgoals):
 1. \<lbrakk>b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<lbrakk>b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx \<noteq> 0
 4. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx - 1 < 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx \<noteq> 0
 3. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx - 1 < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx \<noteq> 0
 2. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx - 1 < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> 2 ^ sz; b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx - 1 < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<le> sz; ptr \<noteq> 0; sz < word_bits; 0 < idx\<rbrakk> \<Longrightarrow> idx - 1 < idx proof (prove)
goal:
No subgoals!