theory IpcCancel_AI

lemma cancel_ipc_simple [wp]:
  "\<lbrace>\<top>\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>" apply (simp add: cancel_ipc_def) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (case_tac state, simp_all) apply (wp hoare_strengthen_post [OF blocked_cancel_ipc_simple]
                   hoare_strengthen_post [OF cancel_signal_simple]
                   hoare_strengthen_post
                      [OF reply_cancel_ipc_st_tcb_at_simple [where t=t]]
                   sts_st_tcb_at_cases
                   hoare_drop_imps
                        | clarsimp elim!: pred_tcb_weakenE pred_tcb_at_tcb_at)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<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>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and (\<lambda>_. True)\<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>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<lbrace>st_tcb_at ((=) Running) t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 2. \<lbrace>st_tcb_at ((=) Inactive) t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 3. \<lbrace>st_tcb_at ((=) Restart) t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 4. \<And>state x41 x42. state = BlockedOnReceive x41 x42 \<Longrightarrow> \<lbrace>st_tcb_at ((=) (BlockedOnReceive x41 x42)) t\<rbrace> blocked_cancel_ipc (BlockedOnReceive x41 x42) t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 5. \<And>state x51 x52. state = BlockedOnSend x51 x52 \<Longrightarrow> \<lbrace>st_tcb_at ((=) (BlockedOnSend x51 x52)) t\<rbrace> blocked_cancel_ipc (BlockedOnSend x51 x52) t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 6. \<lbrace>st_tcb_at ((=) BlockedOnReply) t\<rbrace> reply_cancel_ipc t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 7. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>st_tcb_at ((=) (BlockedOnNotification x7)) t\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 8. \<lbrace>st_tcb_at ((=) IdleThreadState) t\<rbrace> return () \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal:
No subgoals!