theory Intent_DR

lemma bound_preserve_mask:
  "\<lbrakk> is_aligned (x::word32) n; x\<le> mask k; (z::word32)\<le> mask n; n < 32; k < 32; n \<le> k \<rbrakk> \<Longrightarrow>
   x+z \<le> mask k" apply (rule order_trans[where y = "(mask k && ~~ mask n) + mask n"]) apply (rule order_trans[where y = "x + mask n"]) apply (erule word_plus_mono_right) apply (rule is_aligned_no_wrap') apply simp apply (rule mask_lt_2pn) apply (simp add: word_size) apply (rule word_plus_mono_left) apply (rule order_trans[where y = "x && ~~ mask n"]) apply (simp add: mask_out_sub_mask is_aligned_mask) apply (erule neg_mask_mono_le) apply (simp add: mask_out_sub_mask mask_and_mask min_def cong: if_cong) apply (rule word_leI) apply (clarsimp simp: word_size) apply (simp add: mask_out_sub_mask mask_and_mask min_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + z \<le> mask k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + z \<le> (mask k && ~~ mask n) + mask n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + z \<le> x + mask n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + mask n \<le> (mask k && ~~ mask n) + mask n
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x \<le> x + mask n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + mask n \<le> (mask k && ~~ mask n) + mask n
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> is_aligned x ?sz9
 2. \<lbrakk>is_aligned x n; x \<le> mask k; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> mask n < 2 ^ ?sz9
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + mask n \<le> (mask k && ~~ mask n) + mask n
 4. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> mask n < 2 ^ n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + mask n \<le> (mask k && ~~ mask n) + mask n
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> n < LENGTH(32)
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + mask n \<le> (mask k && ~~ mask n) + mask n
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x + mask n \<le> (mask k && ~~ mask n) + mask n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x \<le> mask k && ~~ mask n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> mask n \<le> mask n + (mask k && ~~ mask n)
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x \<le> x && ~~ mask n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x && ~~ mask n \<le> mask k && ~~ mask n
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> mask n \<le> mask n + (mask k && ~~ mask n)
 4. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> x && ~~ mask n \<le> mask k && ~~ mask n
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> mask n \<le> mask n + (mask k && ~~ mask n)
 3. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> mask n \<le> mask n + (mask k && ~~ mask n)
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> mask n \<le> mask k
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; k < 32; n \<le> k; na < size (mask n); mask n !! na\<rbrakk> \<Longrightarrow> mask k !! na
 2. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x \<le> mask k; z \<le> mask n; n < 32; k < 32; n \<le> k\<rbrakk> \<Longrightarrow> (mask k && ~~ mask n) + mask n \<le> mask k proof (prove)
goal:
No subgoals!