theory Retype_AI

lemma range_cover_rel:
  assumes cover: "range_cover ptr sz sbit n"
  assumes le:"sbit' \<le> sbit"
  assumes num_r: "m = 2 ^ (sbit - sbit') * n"
  shows "range_cover ptr sz sbit' m" using cover apply (clarsimp simp:num_r range_cover_def) apply (intro conjI) apply (erule is_aligned_weaken[OF _ le]) apply (erule le_trans[OF le]) apply (drule is_aligned_weaken[OF _ le])+ apply (drule mult_le_mono2[where j = "2^(sz-sbit)" and k = "2^(sbit-sbit')"]) apply (subst (asm) power_add[symmetric]) apply (clarsimp simp:field_simps le) apply (erule le_trans[rotated]) apply clarsimp apply (rule unat_le_helper) apply clarsimp apply (insert le) apply (fold shiftl_t2n) apply (simp add: shiftr_shiftl1) apply (rule eq_refl[OF is_aligned_neg_mask_eq[symmetric]]) apply (rule is_aligned_shiftr[OF is_aligned_weaken]) apply (rule aligned_already_mask[where n = "sbit"]) apply (insert cover) apply (simp add:range_cover_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sbit' m proof (prove)
using this:
range_cover ptr sz sbit n

goal (1 subgoal):
 1. range_cover ptr sz sbit' m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> is_aligned ptr sbit' \<and> sbit' \<le> sz \<and> 2 ^ (sbit - sbit') * n + unat (ptr && mask sz >> sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> is_aligned ptr sbit'
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> sbit' \<le> sz
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> 2 ^ (sbit - sbit') * n + unat (ptr && mask sz >> sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> sbit' \<le> sz
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> 2 ^ (sbit - sbit') * n + unat (ptr && mask sz >> sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> 2 ^ (sbit - sbit') * n + unat (ptr && mask sz >> sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); is_aligned ptr sbit'\<rbrakk> \<Longrightarrow> 2 ^ (sbit - sbit') * n + unat (ptr && mask sz >> sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; 2 ^ (sbit - sbit') * (n + unat (ptr && mask sz >> sbit)) \<le> 2 ^ (sbit - sbit') * 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> 2 ^ (sbit - sbit') * n + unat (ptr && mask sz >> sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; 2 ^ (sbit - sbit') * (n + unat (ptr && mask sz >> sbit)) \<le> 2 ^ (sbit - sbit' + (sz - sbit))\<rbrakk> \<Longrightarrow> 2 ^ (sbit - sbit') * n + unat (ptr && mask sz >> sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; n * 2 ^ (sbit - sbit') + 2 ^ (sbit - sbit') * unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit')\<rbrakk> \<Longrightarrow> unat (ptr && mask sz >> sbit') + n * 2 ^ (sbit - sbit') \<le> 2 ^ (sz - sbit') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'\<rbrakk> \<Longrightarrow> unat (ptr && mask sz >> sbit') + n * 2 ^ (sbit - sbit') \<le> n * 2 ^ (sbit - sbit') + 2 ^ (sbit - sbit') * unat (ptr && mask sz >> sbit) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'\<rbrakk> \<Longrightarrow> unat (ptr && mask sz >> sbit') \<le> 2 ^ (sbit - sbit') * unat (ptr && mask sz >> sbit) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'\<rbrakk> \<Longrightarrow> ptr && mask sz >> sbit' \<le> word_of_nat (2 ^ (sbit - sbit') * unat (ptr && mask sz >> sbit)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'\<rbrakk> \<Longrightarrow> ptr && mask sz >> sbit' \<le> 2 ^ (sbit - sbit') * (ptr && mask sz >> sbit) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> ptr && mask sz >> sbit' \<le> 2 ^ (sbit - sbit') * (ptr && mask sz >> sbit) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> ptr && mask sz >> sbit' \<le> ptr && mask sz >> sbit << sbit - sbit' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> ptr && mask sz >> sbit' \<le> (ptr && mask sz >> sbit') && ~~ mask (sbit - sbit') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask sz >> sbit') (sbit - sbit') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> is_aligned (ptr && mask sz) ?x25
 2. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> sbit - sbit' + sbit' \<le> ?x25 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> is_aligned ptr sbit
 2. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit\<rbrakk> \<Longrightarrow> sbit - sbit' + sbit' \<le> sbit proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> is_aligned ptr sbit
 2. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> sbit - sbit' + sbit' \<le> sbit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); sbit \<le> sz; is_aligned ptr sbit'; sbit' \<le> sbit; range_cover ptr sz sbit n\<rbrakk> \<Longrightarrow> sbit - sbit' + sbit' \<le> sbit proof (prove)
goal:
No subgoals!