theory Untyped_DR

lemma free_range_of_untyped_subseteq:
  "range_cover (ptr::word32) sz us n \<Longrightarrow>
  free_range_of_untyped (unat ((ptr && mask sz) + (of_nat n * 2^us))) sz (ptr &&~~ mask sz)
       \<subseteq> {ptr.. (ptr &&~~ mask sz) + 2 ^ sz - 1}" unfolding free_range_of_untyped_def apply clarsimp apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n = sz]) apply (rule word_plus_mono_right) apply (drule range_cover.range_cover_base_le) apply (clarsimp simp:shiftl_t2n field_simps) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) apply (rule le_refl) apply (rule word32_less_sub_le[THEN iffD1]) apply (simp add: range_cover_def word_bits_def) apply (simp add: word_le_nat_alt range_cover_def unat_2p_sub_1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz us n \<Longrightarrow> free_range_of_untyped (unat ((ptr && mask sz) + word_of_nat n * 2 ^ us)) sz (ptr && ~~ mask sz) \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz us n \<Longrightarrow> (if unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - 1 then {(ptr && ~~ mask sz) + word_of_nat (unat ((ptr && mask sz) + word_of_nat n * 2 ^ us))..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && mask sz \<le> (ptr && mask sz) + word_of_nat n * 2 ^ us
 2. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat n << us)\<rbrakk> \<Longrightarrow> ptr && mask sz \<le> (ptr && mask sz) + word_of_nat n * 2 ^ us
 2. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ?sz13 \<le> sz
 2. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat n * 2 ^ us < 2 ^ ?sz13 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat n * 2 ^ us < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat n * 2 ^ us \<le> 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> 2 ^ sz - Suc 0; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ us) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat n * 2 ^ us \<le> 2 ^ sz - 1 proof (prove)
goal:
No subgoals!