theory IpcCancel_R

lemma (in delete_one_conc) suspend_invs'[wp]:
  "\<lbrace>invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace>
   ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: suspend_def) apply (wp sts_tcbSchedDequeue_invs') apply (simp add: updateRestartPC_def | strengthen no_refs_simple_strg')+ prefer 2 apply (wpsimp wp: hoare_drop_imps hoare_vcg_imp_lift'
           | strengthen no_refs_simple_strg')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
tcbSchedDequeue t
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?Q11 y state\<rbrace> updateRestartPC t \<lbrace>\<lambda>ya s. st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s \<and> (t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) \<and> (runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> sch_act_simple s \<and> invs' s\<rbrace>
 2. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R11 y state\<rbrace> return () \<lbrace>\<lambda>ya s. st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s \<and> (t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) \<and> (runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> sch_act_simple s \<and> invs' s\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> ?Q11 y state s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R11 y state s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q11 () Structures_H.thread_state.Running\<rbrace> asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) \<lbrace>\<lambda>r s. st_tcb_at' simple' t s \<and> t \<noteq> ksIdleThread s \<and> sch_act_simple s \<and> invs' s\<rbrace>
 2. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R11 y state\<rbrace> return () \<lbrace>\<lambda>ya s. st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s \<and> (t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) \<and> (runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> sch_act_simple s \<and> invs' s\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> ?Q11 y state s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R11 y state s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>y state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R11 y state\<rbrace> return () \<lbrace>\<lambda>ya s. st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s \<and> (t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) \<and> (runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> sch_act_simple s \<and> invs' s\<rbrace>
 2. \<lbrace>?Q11 () Structures_H.thread_state.Running\<rbrace> asUser t (getRegister Thread_H.nextInstructionRegister >>= setRegister Thread_H.faultRegister) \<lbrace>\<lambda>r s. st_tcb_at' simple' t s \<and> t \<noteq> ksIdleThread s \<and> sch_act_simple s \<and> invs' s\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> ?Q11 y state s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R11 y state s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and tcb_at' t and (\<lambda>s. t \<noteq> ksIdleThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!