theory Retype_AI

lemma range_cover_mem:
  "\<lbrakk>x < n; range_cover ptr sz us n\<rbrakk>
       \<Longrightarrow> ptr + (of_nat x) * 2 ^ us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}" apply (clarsimp) apply (intro conjI) apply (rule word_plus_mono_right_split[where sz = sz]) apply (erule range_cover.range_cover_compare) apply ((simp add:range_cover_def)+)[2] apply (subst p_assoc_help) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) apply (subst add.commute) apply (subst add.assoc) apply (rule word_plus_mono_right) apply (simp add:word_le_nat_alt) apply (rule le_trans[OF unat_plus_gt]) apply (subst unat_minus_one[OF power_not_zero]) apply (simp add:range_cover_def) apply (frule(1) range_cover.range_cover_compare) apply (clarsimp simp:range_cover_def le_m1_iff_lt power_not_zero nat_le_Suc_less_imp) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask,OF le_refl ]) apply (simp add:range_cover_def) done

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