theory More_Word_Operations

lemma aligned_mask_range_offset_subset:
  assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'"
  and szv: "sz' \<le> sz"
  and xsz: "x < 2 ^ sz"
  shows "mask_range (ptr+x) sz' \<subseteq> mask_range ptr sz" using al proof (rule is_aligned_get_word_bits) assume p0: "ptr = 0" and szv': "LENGTH ('a) \<le> sz" then have "(2 ::'a word) ^ sz = 0" by simp show ?thesis using p0 by (simp add: \<open>2 ^ sz = 0\<close> mask_eq_decr_exp) next assume szv': "sz < LENGTH('a)" hence blah: "2 ^ (sz - sz') < (2 :: nat) ^ LENGTH('a)" using szv by auto show ?thesis using szv szv' apply auto using al assms(4) is_aligned_no_wrap' apply blast apply (simp only: flip: add_diff_eq add_mask_fold) apply (subst add.assoc, rule word_plus_mono_right) using al' is_aligned_add_less_t2n xsz apply fastforce apply (simp add: field_simps szv al is_aligned_no_overflow) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (prove)
using this:
is_aligned ptr sz

goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> sz\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (state)
this:
ptr = 0
LENGTH('a) \<le> sz

goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> sz\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (chain)
picking this:
ptr = 0
LENGTH('a) \<le> sz proof (prove)
using this:
ptr = 0
LENGTH('a) \<le> sz

goal (1 subgoal):
 1. 2 ^ sz = 0 proof (state)
this:
2 ^ sz = 0

goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz
 2. \<lbrakk>ptr = 0; LENGTH('a) \<le> sz\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (prove)
goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (prove)
using this:
ptr = 0

goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (state)
this:
mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (state)
this:
sz < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ (sz - sz') < 2 ^ LENGTH('a) proof (prove)
using this:
sz < LENGTH('a)
sz' \<le> sz

goal (1 subgoal):
 1. 2 ^ (sz - sz') < 2 ^ LENGTH('a) proof (state)
this:
2 ^ (sz - sz') < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (prove)
goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (prove)
using this:
sz' \<le> sz
sz < LENGTH('a)

goal (1 subgoal):
 1. mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr \<le> ptr + x
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr + x + mask sz' \<le> ptr + mask sz proof (prove)
using this:
is_aligned ptr sz
x < 2 ^ sz
\<lbrakk>is_aligned ?ptr ?sz; ?off < 2 ^ ?sz\<rbrakk> \<Longrightarrow> ?ptr \<le> ?ptr + ?off

goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr \<le> ptr + x
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr + x + mask sz' \<le> ptr + mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + mask sz'\<rbrakk> \<Longrightarrow> ptr + x + mask sz' \<le> ptr + mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr + x + (2 ^ sz' - 1) \<le> ptr + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> x + (2 ^ sz' - 1) \<le> 2 ^ sz - 1
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ sz - 1) proof (prove)
using this:
is_aligned x sz'
\<lbrakk>is_aligned ?p ?n; ?d < 2 ^ ?n; ?n \<le> ?m; ?p < 2 ^ ?m\<rbrakk> \<Longrightarrow> ?p + ?d < 2 ^ ?m
x < 2 ^ sz

goal (2 subgoals):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> x + (2 ^ sz' - 1) \<le> 2 ^ sz - 1
 2. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz' \<le> sz; sz < LENGTH('a); ptr + x \<le> ptr + x + (2 ^ sz' - 1)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ sz - 1) proof (prove)
goal:
No subgoals! proof (state)
this:
mask_range (ptr + x) sz' \<subseteq> mask_range ptr sz

goal:
No subgoals!