theory Ipc_IF

lemma cancel_ipc_blocked_globals_equiv:
  "\<lbrace>globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a\<rbrace>
   cancel_ipc a
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" unfolding cancel_ipc_def apply (rule hoare_seq_ext[OF _ gts_sp]) apply (rule hoare_pre) apply (wpc; (simp,rule blocked_cancel_ipc_globals_equiv)?) apply (rule hoare_pre_cont)+ apply clarsimp apply (case_tac state;(clarsimp simp: pred_tcb_at_def obj_at_def receive_blocked_def)) by (simp add: eq_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a\<rbrace> cancel_ipc a \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a\<rbrace> do state <- get_thread_state a;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state a | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state a | BlockedOnReply \<Rightarrow> reply_cancel_ipc a | BlockedOnNotification event \<Rightarrow> cancel_signal a event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) a and (globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a)\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state a | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state a | BlockedOnReply \<Rightarrow> reply_cancel_ipc a | BlockedOnNotification event \<Rightarrow> cancel_signal a event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<lbrace>?Q4 state\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state a | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state a | BlockedOnReply \<Rightarrow> reply_cancel_ipc a | BlockedOnNotification event \<Rightarrow> cancel_signal a event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>state s. (st_tcb_at ((=) state) a and (globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a)) s \<Longrightarrow> ?Q4 state s proof (prove)
goal (7 subgoals):
 1. \<And>state. state = Running \<Longrightarrow> \<lbrace>?R30 state\<rbrace> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>state. inactive state \<Longrightarrow> \<lbrace>?R29 state\<rbrace> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>state. state = Restart \<Longrightarrow> \<lbrace>?R28 state\<rbrace> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 4. \<And>state. awaiting_reply state \<Longrightarrow> \<lbrace>?R21 state\<rbrace> reply_cancel_ipc a \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R20 state x7\<rbrace> cancel_signal a x7 \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>state. idle state \<Longrightarrow> \<lbrace>?R18 state\<rbrace> return () \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<And>state s. (st_tcb_at ((=) state) a and (globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a)) s \<Longrightarrow> (state = Running \<longrightarrow> ?R30 state s) \<and> (inactive state \<longrightarrow> ?R29 state s) \<and> (state = Restart \<longrightarrow> ?R28 state s) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> (globals_equiv st and valid_arch_state) s) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> (globals_equiv st and valid_arch_state) s) \<and> (awaiting_reply state \<longrightarrow> ?R21 state s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R20 state x s) \<and> (idle state \<longrightarrow> ?R18 state s) proof (prove)
goal (1 subgoal):
 1. \<And>state s. (st_tcb_at ((=) state) a and (globals_equiv st and valid_arch_state and st_tcb_at receive_blocked a)) s \<Longrightarrow> (state = Running \<longrightarrow> False) \<and> (inactive state \<longrightarrow> False) \<and> (state = Restart \<longrightarrow> False) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> (globals_equiv st and valid_arch_state) s) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> (globals_equiv st and valid_arch_state) 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>state s. \<lbrakk>st_tcb_at ((=) state) a s; globals_equiv st s; valid_arch_state s; st_tcb_at receive_blocked a s\<rbrakk> \<Longrightarrow> state \<noteq> Running \<and> state \<noteq> Inactive \<and> state \<noteq> Restart \<and> state \<noteq> BlockedOnReply \<and> (\<forall>x. state \<noteq> BlockedOnNotification x) \<and> state \<noteq> IdleThreadState proof (prove)
goal (1 subgoal):
 1. \<And>s x7 tcb. \<lbrakk>globals_equiv st s; valid_arch_state s; kheap s a = Some (TCB tcb); BlockedOnNotification x7 = tcb_state tcb; case tcb_state tcb of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> False