theory Finalise_R

lemma typ_at'_valid_tcb'_lift:
  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_tcb' tcb s\<rbrace> f \<lbrace>\<lambda>rv s. valid_tcb' tcb s\<rbrace>" including no_pre apply (simp add: valid_tcb'_def) apply (case_tac "tcbState tcb", simp_all add: valid_tcb_state'_def split_def valid_bound_ntfn'_def) apply (wp hoare_vcg_const_Ball_lift typ_at_lifts[OF P]
               | case_tac "tcbBoundNotification tcb", simp_all)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_tcb' tcb\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_tcb' tcb\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb' tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF tcb)) s) \<and> valid_tcb_state' (tcbState tcb) s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> valid_bound_ntfn' (tcbBoundNotification tcb) s \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> valid_cap' (cteCap (getF tcb)) s) \<and> valid_tcb_state' (tcbState tcb) s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> valid_bound_ntfn' (tcbBoundNotification tcb) s \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12. tcbState tcb = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> ep_at' x11 s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> ep_at' x11 s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace>
 2. awaiting_reply' (tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace>
 3. \<And>x3. tcbState tcb = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> ntfn_at' x3 s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> ntfn_at' x3 s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace>
 4. tcbState tcb = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace>
 5. tcbState tcb = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace>
 6. idle' (tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace>
 7. \<And>x71 x72 x73 x74 x75. tcbState tcb = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> ep_at' x71 s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> ep_at' x71 s \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace>
 8. tcbState tcb = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cte_cases. valid_cap' (cteCap (fst x tcb)) s) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> (case tcbBoundNotification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at' a s) \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority\<rbrace> proof (prove)
goal:
No subgoals!