theory Ipc_DR

lemma cancel_ipc_valid_idle:
  "\<lbrace>valid_idle and not_idle_thread obj_id' and invs :: det_state \<Rightarrow> bool\<rbrace> IpcCancel_A.cancel_ipc obj_id' \<lbrace>\<lambda>_. valid_idle\<rbrace>" apply (clarsimp simp: cancel_ipc_def) apply (wp not_idle_after_blocked_cancel_ipc not_idle_after_reply_cancel_ipc
            not_idle_thread_cancel_signal | wpc | simp)+ apply (rule hoare_strengthen_post[where Q="\<lambda>r. st_tcb_at ((=) r) obj_id'
                                                  and not_idle_thread obj_id' and invs"]) apply (wp gts_sp) apply (clarsimp simp: invs_def valid_state_def valid_pspace_def not_idle_thread_def | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and not_idle_thread obj_id' and invs\<rbrace> IpcCancel_A.cancel_ipc obj_id' \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and not_idle_thread obj_id' and invs\<rbrace> do state <- get_thread_state obj_id';
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state obj_id' | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state obj_id' | BlockedOnReply \<Rightarrow> reply_cancel_ipc obj_id' | BlockedOnNotification event \<Rightarrow> cancel_signal obj_id' event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> valid_idle s) \<and> (inactive state \<longrightarrow> valid_idle s) \<and> (state = Restart \<longrightarrow> valid_idle s) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> valid_idle s \<and> not_idle_thread obj_id' s \<and> valid_objs s \<and> st_tcb_at ((=) (BlockedOnReceive x xa)) obj_id' s) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> valid_idle s \<and> not_idle_thread obj_id' s \<and> valid_objs s \<and> st_tcb_at ((=) (BlockedOnSend x xa)) obj_id' s) \<and> (awaiting_reply state \<longrightarrow> not_idle_thread obj_id' s \<and> invs s) \<and> ((\<exists>x. state = BlockedOnNotification x) \<longrightarrow> not_idle_thread obj_id' s \<and> valid_idle s) \<and> (idle state \<longrightarrow> valid_idle s)\<rbrace>
 2. \<And>s. (valid_idle and not_idle_thread obj_id' and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>r. st_tcb_at ((=) r) obj_id' and not_idle_thread obj_id' and invs\<rbrace>
 2. \<And>rv s. (st_tcb_at ((=) rv) obj_id' and not_idle_thread obj_id' and invs) s \<Longrightarrow> (rv = Running \<longrightarrow> valid_idle s) \<and> (inactive rv \<longrightarrow> valid_idle s) \<and> (rv = Restart \<longrightarrow> valid_idle s) \<and> (\<forall>x xa. rv = BlockedOnReceive x xa \<longrightarrow> valid_idle s \<and> not_idle_thread obj_id' s \<and> valid_objs s \<and> st_tcb_at ((=) (BlockedOnReceive x xa)) obj_id' s) \<and> (\<forall>x xa. rv = BlockedOnSend x xa \<longrightarrow> valid_idle s \<and> not_idle_thread obj_id' s \<and> valid_objs s \<and> st_tcb_at ((=) (BlockedOnSend x xa)) obj_id' s) \<and> (awaiting_reply rv \<longrightarrow> not_idle_thread obj_id' s \<and> invs s) \<and> ((\<exists>x. rv = BlockedOnNotification x) \<longrightarrow> not_idle_thread obj_id' s \<and> valid_idle s) \<and> (idle rv \<longrightarrow> valid_idle s)
 3. \<And>s. (valid_idle and not_idle_thread obj_id' and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (st_tcb_at ((=) rv) obj_id' and not_idle_thread obj_id' and invs) s \<Longrightarrow> (rv = Running \<longrightarrow> valid_idle s) \<and> (inactive rv \<longrightarrow> valid_idle s) \<and> (rv = Restart \<longrightarrow> valid_idle s) \<and> (\<forall>x xa. rv = BlockedOnReceive x xa \<longrightarrow> valid_idle s \<and> not_idle_thread obj_id' s \<and> valid_objs s \<and> st_tcb_at ((=) (BlockedOnReceive x xa)) obj_id' s) \<and> (\<forall>x xa. rv = BlockedOnSend x xa \<longrightarrow> valid_idle s \<and> not_idle_thread obj_id' s \<and> valid_objs s \<and> st_tcb_at ((=) (BlockedOnSend x xa)) obj_id' s) \<and> (awaiting_reply rv \<longrightarrow> not_idle_thread obj_id' s \<and> invs s) \<and> ((\<exists>x. rv = BlockedOnNotification x) \<longrightarrow> not_idle_thread obj_id' s \<and> valid_idle s) \<and> (idle rv \<longrightarrow> valid_idle s)
 2. \<And>s. (valid_idle and not_idle_thread obj_id' and invs) s \<Longrightarrow> not_idle_thread obj_id' s \<and> invs s proof (prove)
goal:
No subgoals!