theory More_Word_Operations

lemma aligned_mask_diff:
  "\<lbrakk> is_aligned (dest :: 'a :: len word) bits; is_aligned (ptr :: 'a :: len word) sz;
     bits \<le> sz; sz < LENGTH('a); dest < ptr \<rbrakk>
   \<Longrightarrow> mask bits + dest < ptr" apply (frule_tac p' = ptr in aligned_mask_range_cases, assumption) apply (elim disjE) apply (drule_tac is_aligned_no_overflow_mask, simp)+ apply (simp add: algebra_split_simps word_le_not_less) apply (drule is_aligned_no_overflow_mask; fastforce) apply (simp add: is_aligned_weaken algebra_split_simps) apply (auto simp add: not_le) using is_aligned_no_overflow_mask leD apply blast apply (meson aligned_add_mask_less_eq is_aligned_weaken le_less_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr\<rbrakk> \<Longrightarrow> mask bits + dest < ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<inter> mask_range ptr sz = {} \<or> mask_range dest bits \<subseteq> mask_range ptr sz \<or> mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<inter> mask_range ptr sz = {}\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<subseteq> mask_range ptr sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 3. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bits \<le> sz; sz < LENGTH('a); dest < ptr; \<not> ptr \<le> dest + mask bits; dest \<le> dest + mask bits; ptr \<le> ptr + mask sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<subseteq> mask_range ptr sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 3. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range dest bits \<subseteq> mask_range ptr sz\<rbrakk> \<Longrightarrow> mask bits + dest < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; mask_range ptr sz \<subseteq> mask_range dest bits\<rbrakk> \<Longrightarrow> mask bits + dest < ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; ptr \<le> ptr + mask sz \<longrightarrow> dest \<le> ptr \<and> ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; ptr + mask sz < ptr\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; dest \<le> ptr; ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr proof (prove)
using this:
is_aligned ?x ?n \<Longrightarrow> ?x \<le> ?x + mask ?n
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (2 subgoals):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; ptr + mask sz < ptr\<rbrakk> \<Longrightarrow> dest + mask bits < ptr
 2. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; dest \<le> ptr; ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned dest bits; is_aligned ptr sz; bits \<le> sz; sz < LENGTH('a); dest < ptr; dest \<le> ptr; ptr + mask sz \<le> dest + mask bits\<rbrakk> \<Longrightarrow> dest + mask bits < ptr proof (prove)
goal:
No subgoals!