theory Retype_AI

lemma range_cover_cell_subset:
  "\<lbrakk>range_cover ptr sz us n;x < of_nat n\<rbrakk>
       \<Longrightarrow> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}" proof - assume cover:"range_cover ptr sz us n"
  and      cmp:"x<of_nat n" have sh: "(2^us * (ptr && mask sz >> us)) = ptr && mask sz" apply (subst shiftl_t2n[symmetric]) apply (subst and_not_mask[symmetric]) apply (rule is_aligned_neg_mask_eq) using cover apply (simp add:is_aligned_mask mask_twice range_cover_def min_def) done show ?thesis using cover cmp apply clarsimp apply (intro conjI) apply (rule word_plus_mono_right_split) apply (drule range_cover.range_cover_compare[where p = "unat x"]) apply (erule unat_less_helper) apply (simp add: range_cover.unat_of_nat_shift[where gbits = us]) apply (simp add:range_cover_def) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) apply (subst add.commute) apply (simp add:p_assoc_help) apply (subst add.assoc)+ apply (rule word_plus_mono_right) apply (cut_tac nasty_split_lt[where x="((ptr && mask sz) >> us) + x" and n=us and m=sz]) apply (simp add: sh field_simps) apply (clarsimp simp:range_cover_def word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (erule less_le_trans[rotated]) apply (clarsimp simp:range_cover.unat_of_nat_n[OF cover]) apply (simp add:range_cover_def p_assoc_help[symmetric])+ apply (simp add: is_aligned_no_overflow) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (state)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (state)
this:
range_cover ptr sz us n
x < word_of_nat n

goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. 2 ^ us * (ptr && mask sz >> us) = ptr && mask sz proof (prove)
goal (1 subgoal):
 1. ptr && mask sz >> us << us = ptr && mask sz proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz) && ~~ mask us = ptr && mask sz proof (prove)
goal (1 subgoal):
 1. is_aligned (ptr && mask sz) us proof (prove)
using this:
range_cover ptr sz us n

goal (1 subgoal):
 1. is_aligned (ptr && mask sz) us proof (prove)
goal:
No subgoals! proof (state)
this:
2 ^ us * (ptr && mask sz >> us) = ptr && mask sz

goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
using this:
range_cover ptr sz us n
x < word_of_nat n

goal (1 subgoal):
 1. {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + x * 2 ^ us \<and> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + x * 2 ^ us
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> unat (ptr && mask ?sz4) + unat (x * 2 ^ us) < 2 ^ ?sz4
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ?sz4 < LENGTH('a)
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> unat x < n
 2. \<lbrakk>x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1; unat (ptr && mask sz) + unat (word_of_nat (unat x) * 2 ^ us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask ?sz4) + unat (x * 2 ^ us) < 2 ^ ?sz4
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ?sz4 < LENGTH('a)
 4. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1; unat (ptr && mask sz) + unat (word_of_nat (unat x) * 2 ^ us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask ?sz4) + unat (x * 2 ^ us) < 2 ^ ?sz4
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ?sz4 < LENGTH('a)
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (ptr && ~~ mask sz) + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + x * 2 ^ us + 2 ^ us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + x * 2 ^ us + (2 ^ us - 1) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + ((ptr && mask sz) + (x * 2 ^ us + (2 ^ us - 1))) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (x * 2 ^ us + (2 ^ us - 1)) \<le> 2 ^ sz - 1
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1); ((ptr && mask sz >> us) + x) * 2 ^ us + (2 ^ us - 1) \<le> 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (x * 2 ^ us + (2 ^ us - 1)) \<le> 2 ^ sz - 1
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> (ptr && mask sz >> us) + x < 2 ^ (sz - us)
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> us \<le> sz
 4. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 5. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> (ptr && mask sz >> us) + x < 2 ^ (sz - us)
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> us \<le> sz
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 4. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>unat x < unat (word_of_nat n); ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1); is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz >> us) + x) < 2 ^ (sz - us)
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> us \<le> sz
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 4. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>unat x < unat (word_of_nat n); ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1); is_aligned ptr us; sz < LENGTH('a); us \<le> sz; n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz >> us) + unat x < 2 ^ (sz - us)
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> us \<le> sz
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 4. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>unat x < unat (word_of_nat n); ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1); is_aligned ptr us; sz < LENGTH('a); us \<le> sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz >> us) + unat x < n + unat (ptr && mask sz >> us)
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> us \<le> sz
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 4. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> us \<le> sz
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr us \<and> sz < LENGTH('a) \<and> us \<le> sz \<and> n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us); x < word_of_nat n; ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + 2 ^ us - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal:
No subgoals! proof (state)
this:
{ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}

goal:
No subgoals!