theory Ipc_AC

lemma cancel_ipc_receive_blocked_mdb:
  "\<lbrace>\<lambda>s :: det_ext state. P (cdt s) \<and> st_tcb_at receive_blocked t s\<rbrace>
   cancel_ipc t
   \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>" apply (clarsimp simp: cancel_ipc_def) apply (rule hoare_seq_ext[OF _ gts_sp]) apply (rule hoare_pre) apply (wp gts_wp | wpc | simp)+ apply (rule hoare_pre_cont)+ apply (clarsimp simp: st_tcb_def2 receive_blocked_def) apply (clarsimp split: thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s) \<and> st_tcb_at receive_blocked t s\<rbrace> cancel_ipc t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s) \<and> st_tcb_at receive_blocked t s\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and (\<lambda>s. P (cdt s) \<and> st_tcb_at receive_blocked t s)\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<lbrace>?Q4 state\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>state s. (st_tcb_at ((=) state) t and (\<lambda>s. P (cdt s) \<and> st_tcb_at receive_blocked t s)) s \<Longrightarrow> ?Q4 state s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?R20 BlockedOnReply\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R19 state x7\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>state. idle state \<Longrightarrow> \<lbrace>?R17 state\<rbrace> return () \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 4. \<And>state s. (st_tcb_at ((=) state) t and (\<lambda>s. P (cdt s) \<and> st_tcb_at receive_blocked t s)) s \<Longrightarrow> (state = Running \<longrightarrow> P (cdt s)) \<and> (inactive state \<longrightarrow> P (cdt s)) \<and> (state = Restart \<longrightarrow> P (cdt s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (cdt s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (cdt s)) \<and> (awaiting_reply state \<longrightarrow> ?R20 state s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R19 state x s) \<and> (idle state \<longrightarrow> ?R17 state s) proof (prove)
goal (1 subgoal):
 1. \<And>state s. (st_tcb_at ((=) state) t and (\<lambda>s. P (cdt s) \<and> st_tcb_at receive_blocked t s)) s \<Longrightarrow> (state = Running \<longrightarrow> P (cdt s)) \<and> (inactive state \<longrightarrow> P (cdt s)) \<and> (state = Restart \<longrightarrow> P (cdt s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (cdt s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (cdt s)) \<and> (awaiting_reply state \<longrightarrow> False) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> False) \<and> (idle state \<longrightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>P (cdt s); get_tcb t s = Some tcb; case tcb_state tcb of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> tcb_state tcb \<noteq> BlockedOnReply \<and> (\<forall>x. tcb_state tcb \<noteq> BlockedOnNotification x) \<and> tcb_state tcb \<noteq> IdleThreadState proof (prove)
goal:
No subgoals!