theory Detype_AI

lemma range_cover_compare_offset:
  "\<lbrakk>range_cover ptr sz us t; n + 1 < t;ptr \<noteq> 0\<rbrakk>
   \<Longrightarrow> ptr + (of_nat n << us) \<le> ptr + (1 + of_nat n << us)" apply (simp add:shiftl_t2n field_simps) apply (rule order_trans[OF range_cover_bound]) apply (rule range_cover_offset[rotated]) apply (erule_tac n = "n+1" in range_cover_le) apply simp+ apply (simp add:field_simps) apply (rule word_sub_1_le) apply (drule_tac n = "n + 2" and p = "n + 1" in range_cover_no_0) apply (erule range_cover_le) apply simp apply simp apply (simp add:field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us t; n + 1 < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n << us) \<le> ptr + (1 + word_of_nat n << us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ us \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover (ptr + word_of_nat n * 2 ^ us) ?sz3 ?us3 ?n3
 2. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ?n3
 3. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ us + word_of_nat ?n3 * 2 ^ ?us3 - 1 \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover ptr ?sz3 us ?n7
 2. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> n < ?n7
 3. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < ?n7 - n
 4. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ us + word_of_nat (?n7 - n) * 2 ^ us - 1 \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> n + 1 \<le> t
 2. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> n < n + 1
 3. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < n + 1 - n
 4. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ us + word_of_nat (n + 1 - n) * 2 ^ us - 1 \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ us + 2 ^ us - 1 \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) - 1 \<le> ptr + (2 ^ us + word_of_nat n * 2 ^ us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t\<rbrakk> \<Longrightarrow> range_cover ptr ?sz13 ?sbit13 (n + 2)
 2. \<lbrakk>range_cover ptr sz us t; Suc n < t\<rbrakk> \<Longrightarrow> n + 1 < n + 2
 3. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr + word_of_nat (n + 1) * 2 ^ ?sbit13 \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. Suc n < t \<Longrightarrow> n + 2 \<le> t
 2. \<lbrakk>range_cover ptr sz us t; Suc n < t\<rbrakk> \<Longrightarrow> n + 1 < n + 2
 3. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr + word_of_nat (n + 1) * 2 ^ us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t\<rbrakk> \<Longrightarrow> n + 1 < n + 2
 2. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr + word_of_nat (n + 1) * 2 ^ us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us t; Suc n < t; ptr + word_of_nat (n + 1) * 2 ^ us \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (2 ^ us + word_of_nat n * 2 ^ us) \<noteq> 0 proof (prove)
goal:
No subgoals!