theory Ipc_R

lemma valid_ipc_buffer_ptr'D2:
  "\<lbrakk>valid_ipc_buffer_ptr' a s; y < max_ipc_words * 4; is_aligned y 2\<rbrakk> \<Longrightarrow> typ_at' UserDataT (a + y && ~~ mask pageBits) s" unfolding valid_ipc_buffer_ptr'_def apply clarsimp apply (subgoal_tac "(a + y) && ~~ mask pageBits = a  && ~~ mask pageBits") apply simp apply (rule mask_out_first_mask_some [where n = msg_align_bits]) apply (erule is_aligned_add_helper [THEN conjunct2]) apply (erule order_less_le_trans) apply (simp add: msg_align_bits max_ipc_words ) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_ipc_buffer_ptr' a s; y < max_ipc_words * 4; is_aligned y 2\<rbrakk> \<Longrightarrow> typ_at' UserDataT (a + y && ~~ mask pageBits) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a msg_align_bits \<and> typ_at' UserDataT (a && ~~ mask pageBits) s; y < max_ipc_words * 4; is_aligned y 2\<rbrakk> \<Longrightarrow> typ_at' UserDataT (a + y && ~~ mask pageBits) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> typ_at' UserDataT (a + y && ~~ mask pageBits) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s; a + y && ~~ mask pageBits = a && ~~ mask pageBits\<rbrakk> \<Longrightarrow> typ_at' UserDataT (a + y && ~~ mask pageBits) s
 2. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> a + y && ~~ mask pageBits = a && ~~ mask pageBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> a + y && ~~ mask pageBits = a && ~~ mask pageBits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> a + y && ~~ mask msg_align_bits = a
 2. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> y < 2 ^ msg_align_bits
 2. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned y 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> max_ipc_words * 4 \<le> 2 ^ msg_align_bits
 2. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y < max_ipc_words * 4; is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> msg_align_bits \<le> pageBits proof (prove)
goal:
No subgoals!