theory Retype_C

lemma range_cover_not_in_neqD:
  "\<lbrakk> x \<notin> {ptr..ptr + (of_nat n << APIType_capBits newType userSize) - 1};
    range_cover ptr sz (APIType_capBits newType userSize) n; n' < n \<rbrakk>
  \<Longrightarrow> x \<noteq> ptr + (of_nat n' << APIType_capBits newType userSize)" apply (clarsimp simp only: shiftl_t2n mult.commute) apply (erule notE, rule subsetD, erule_tac p=n' in range_cover_subset) apply simp+ apply (rule is_aligned_no_overflow) apply (rule aligned_add_aligned) apply (erule range_cover.aligned) apply (simp add: is_aligned_mult_triv2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> {ptr..ptr + (word_of_nat n << APIType_capBits newType userSize) - 1}; range_cover ptr sz (APIType_capBits newType userSize) n; n' < n\<rbrakk> \<Longrightarrow> x \<noteq> ptr + (word_of_nat n' << APIType_capBits newType userSize) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize \<notin> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits newType userSize - 1}; range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> n' < n
 2. \<lbrakk>n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize \<in> {ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize..ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize + 2 ^ APIType_capBits newType userSize - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize \<le> ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize + 2 ^ APIType_capBits newType userSize - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize) (APIType_capBits newType userSize) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> is_aligned ptr ?n11
 2. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n' * 2 ^ APIType_capBits newType userSize) (APIType_capBits newType userSize)
 3. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize \<le> ?n11 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat n' * 2 ^ APIType_capBits newType userSize) (APIType_capBits newType userSize)
 2. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize \<le> APIType_capBits newType userSize proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) n; n' < n; x = ptr + word_of_nat n' * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> APIType_capBits newType userSize \<le> APIType_capBits newType userSize proof (prove)
goal:
No subgoals!