theory ArchMove_C

lemma ps_clear_is_aligned_ksPSpace_None:
  "\<lbrakk>ps_clear p n s; is_aligned p n; 0<d; d \<le> mask n\<rbrakk>
   \<Longrightarrow> ksPSpace s (p + d) = None" apply (simp add: ps_clear_def add_diff_eq[symmetric] mask_2pm1[symmetric]) apply (drule equals0D[where a="p + d"]) apply (simp add: dom_def word_gt_0 del: word_neq_0_conv) apply (drule mp) apply (rule word_plus_mono_right) apply simp apply (simp add: mask_2pm1) apply (erule is_aligned_no_overflow') apply (drule mp) apply (case_tac "(0::word32)<2^n") apply (frule le_m1_iff_lt[of "(2::word32)^n" d, THEN iffD1]) apply (simp add: mask_2pm1[symmetric]) apply (erule (1) is_aligned_no_wrap') apply (simp add: is_aligned_mask mask_2pm1 not_less word_bits_def
                    power_overflow) by assumption

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear p n s; is_aligned p n; 0 < d; d \<le> mask n\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(mask_range p n - {p}) \<inter> dom (ksPSpace s) = {}; is_aligned p n; 0 < d; d \<le> mask n\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; 0 < d; d \<le> mask n; p + d \<notin> (mask_range p n - {p}) \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; p + d \<le> p + mask n \<longrightarrow> p \<le> p + d \<longrightarrow> ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n\<rbrakk> \<Longrightarrow> p + d \<le> p + mask n
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; p \<le> p + d \<longrightarrow> ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n\<rbrakk> \<Longrightarrow> d \<le> mask n
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n\<rbrakk> \<Longrightarrow> p \<le> p + mask n
 3. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; p \<le> p + d \<longrightarrow> ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n\<rbrakk> \<Longrightarrow> p \<le> p + mask n
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; p \<le> p + d \<longrightarrow> ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> 2 ^ n - 1\<rbrakk> \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; p \<le> p + d \<longrightarrow> ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; p \<le> p + d \<longrightarrow> ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n\<rbrakk> \<Longrightarrow> p \<le> p + d
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; 0 < 2 ^ n\<rbrakk> \<Longrightarrow> p \<le> p + d
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; \<not> 0 < 2 ^ n\<rbrakk> \<Longrightarrow> p \<le> p + d
 3. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; 0 < 2 ^ n; (d \<le> 2 ^ n - 1) = (d < 2 ^ n)\<rbrakk> \<Longrightarrow> p \<le> p + d
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; \<not> 0 < 2 ^ n\<rbrakk> \<Longrightarrow> p \<le> p + d
 3. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; 0 < 2 ^ n; d < 2 ^ n\<rbrakk> \<Longrightarrow> p \<le> p + d
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; \<not> 0 < 2 ^ n\<rbrakk> \<Longrightarrow> p \<le> p + d
 3. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; \<not> 0 < 2 ^ n\<rbrakk> \<Longrightarrow> p \<le> p + d
 2. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; d \<noteq> 0; d \<le> mask n; ksPSpace s (p + d) = None\<rbrakk> \<Longrightarrow> ksPSpace s (p + d) = None