theory Untyped_DR

lemma free_range_of_untyped_subseteq':
  "\<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size (ptr)\<rbrakk>
    \<Longrightarrow> free_range_of_untyped a' sz ptr \<subseteq>free_range_of_untyped a sz ptr" apply (clarsimp simp:free_range_of_untyped_def) apply (rule word_plus_mono_right) apply (drule le_p2_minus_1) apply (rule of_nat_mono_maybe_le[THEN iffD1,rotated -1]) apply simp apply (erule less_le_trans) apply (simp add: word_size) apply (drule(1) le_less_trans) apply (erule less_le_trans) apply (simp add: word_size) apply (erule is_aligned_no_wrap') apply (rule word_of_nat_less) apply (drule le_p2_minus_1) apply (simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr\<rbrakk> \<Longrightarrow> free_range_of_untyped a' sz ptr \<subseteq> free_range_of_untyped a sz ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat a \<le> ptr + word_of_nat a' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat a \<le> word_of_nat a'
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> word_of_nat a \<le> word_of_nat a'
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a \<le> a'
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a' < 2 ^ LENGTH('a)
 3. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a < 2 ^ LENGTH('a)
 4. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a' < 2 ^ LENGTH('a)
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a < 2 ^ LENGTH('a)
 3. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> 2 ^ LENGTH('a)
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a < 2 ^ LENGTH('a)
 3. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a < 2 ^ LENGTH('a)
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz; a < 2 ^ sz\<rbrakk> \<Longrightarrow> a < 2 ^ LENGTH('a)
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> 2 ^ LENGTH('a)
 2. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat a' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> a'; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat a' < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> a'; sz < size ptr; a' \<le> 2 ^ sz - Suc 0; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> a' < unat (2 ^ sz) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> a'; sz < size ptr; ptr + word_of_nat a' \<le> ptr + 2 ^ sz - 1; a' < 2 ^ sz\<rbrakk> \<Longrightarrow> a' < unat (2 ^ sz) proof (prove)
goal:
No subgoals!