theory Detype_AI

lemma range_cover_tail_mask:
  "\<lbrakk>range_cover ptr sz us (Suc (Suc n));ptr \<noteq> 0\<rbrakk>
   \<Longrightarrow> ptr  + ((1::machine_word) + of_nat n << us)  && ~~ mask sz = ptr && ~~ mask sz" apply (frule(1) range_cover_ptr_le) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr]) apply (subst add.commute) apply (subst add.assoc) apply (subst is_aligned_add_helper[THEN conjunct2,OF is_aligned_neg_mask]) apply (simp add:range_cover_def) apply (simp add:word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (frule range_cover.range_cover_compare[where p = "Suc n"]) apply simp apply (drule range_cover.sz) apply (simp add:word_arith_nat_Suc shiftl_t2n power_add[symmetric] field_simps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (ptr && ~~ mask sz) + (1 + word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + (1 + word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + ((ptr && mask sz) + (1 + word_of_nat n << us)) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> sz \<le> sz
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (1 + word_of_nat n << us) < 2 ^ sz
 3. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (1 + word_of_nat n << us) < 2 ^ sz
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (1 + word_of_nat n << us)) < unat (2 ^ sz)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (1 + word_of_nat n << us) < unat (2 ^ sz)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> Suc n < Suc (Suc n)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us); unat (ptr && mask sz) + unat (word_of_nat (Suc n) * 2 ^ us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (1 + word_of_nat n << us) < unat (2 ^ sz)
 3. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us); unat (ptr && mask sz) + unat (word_of_nat (Suc n) * 2 ^ us) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (1 + word_of_nat n << us) < unat (2 ^ sz)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us); unat (ptr && mask sz) + unat (word_of_nat (Suc n) * 2 ^ us) < 2 ^ sz; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (1 + word_of_nat n << us) < unat (2 ^ sz)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); ptr \<noteq> 0; ptr \<le> ptr + (1 + word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal:
No subgoals!