theory Detype_AI

lemma range_cover_offset:
  assumes offset: "p < n"
  and     cover : "range_cover ptr sz us n"
  shows "range_cover (ptr + (of_nat p) * 2 ^ us) sz us (n - p)" using assms range_cover.range_cover_compare_bound[OF cover] apply (clarsimp simp:range_cover_def) apply (intro conjI) apply (erule aligned_add_aligned) apply (subst mult.commute) apply (simp add:is_aligned_shiftl_self[unfolded shiftl_t2n]) apply simp apply (rule nat_mult_le_cancel1[where k = "2^ us",THEN iffD1]) apply simp apply (subst diff_mult_distrib2) apply (simp add: add_mult_distrib2) apply (simp add:shiftr_div_2n' field_simps minus_mod_eq_mult_div[symmetric]) apply (rule le_trans[where j = "(n-p) * 2 ^ us + unat (ptr + of_nat p * 2 ^ us && mask sz)"]) apply (clarsimp simp:field_simps diff_mult_distrib diff_le_mono2) apply (subst mask_eqs[symmetric]) apply (subst less_mask_eq[where x = "(ptr && mask sz) + of_nat p * 2 ^ us"]) apply (simp add:word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (erule range_cover.range_cover_compare[OF cover]) apply (simp add:range_cover_unat[OF range_cover_le[OF cover]] field_simps) apply (simp add:range_cover.unat_of_nat_shift[OF cover] diff_mult_distrib) apply (simp add:field_simps power_add[symmetric]
    range_cover.range_cover_compare_bound[OF cover]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover (ptr + word_of_nat p * 2 ^ us) sz us (n - p) proof (prove)
using this:
p < n
range_cover ptr sz us n
n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz

goal (1 subgoal):
 1. range_cover (ptr + word_of_nat p * 2 ^ us) sz us (n - p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat p * 2 ^ us) us \<and> n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p \<le> 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat p * 2 ^ us) us
 2. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p \<le> 2 ^ (sz - us) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat p * 2 ^ us) us
 2. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> us \<le> us
 3. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p \<le> 2 ^ (sz - us) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> is_aligned (2 ^ us * word_of_nat p) us
 2. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> us \<le> us
 3. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p \<le> 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> us \<le> us
 2. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p \<le> 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p \<le> 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> 0 < 2 ^ us
 2. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> 2 ^ us * (n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> 2 ^ us * (n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - p) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> 2 ^ us * (n + unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us)) - 2 ^ us * p \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; n * 2 ^ us + unat (ptr && mask sz) \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> 2 ^ us * n + 2 ^ us * unat (ptr + word_of_nat p * 2 ^ us && mask sz >> us) - 2 ^ us * p \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> n * 2 ^ us + unat (ptr + word_of_nat p * 2 ^ us && mask sz) - (p * 2 ^ us + unat (ptr + word_of_nat p * 2 ^ us && mask sz) mod 2 ^ us) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> n * 2 ^ us + unat (ptr + word_of_nat p * 2 ^ us && mask sz) - (p * 2 ^ us + unat (ptr + word_of_nat p * 2 ^ us && mask sz) mod 2 ^ us) \<le> (n - p) * 2 ^ us + unat (ptr + word_of_nat p * 2 ^ us && mask sz)
 2. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (n - p) * 2 ^ us + unat (ptr + word_of_nat p * 2 ^ us && mask sz) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (n - p) * 2 ^ us + unat (ptr + word_of_nat p * 2 ^ us && mask sz) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (n - p) * 2 ^ us + unat ((ptr && mask sz) + word_of_nat p * 2 ^ us && mask sz) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat p * 2 ^ us < 2 ^ sz
 2. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (n - p) * 2 ^ us + unat ((ptr && mask sz) + word_of_nat p * 2 ^ us) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat p * 2 ^ us) < 2 ^ sz
 2. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (n - p) * 2 ^ us + unat ((ptr && mask sz) + word_of_nat p * 2 ^ us) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ us) < 2 ^ sz
 2. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (n - p) * 2 ^ us + unat ((ptr && mask sz) + word_of_nat p * 2 ^ us) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> (n - p) * 2 ^ us + unat ((ptr && mask sz) + word_of_nat p * 2 ^ us) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + ((n - p) * 2 ^ us + unat (word_of_nat p * 2 ^ us)) \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < n; unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ sz; is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz) div 2 ^ us \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + n * 2 ^ us \<le> 2 ^ us * 2 ^ (sz - us) proof (prove)
goal:
No subgoals!