theory IpcCancel_R

lemma sts_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s
        \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st)\<rbrace>
   setThreadState st t
   \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" including no_pre apply (simp add: setThreadState_def) apply (wp rescheduleRequired_weak_sch_act_wf) apply (rule_tac Q="\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp, simp) apply (simp add: weak_sch_act_wf_def) apply (wp hoare_vcg_all_lift) apply (wps threadSet_nosch) apply (wp hoare_vcg_const_imp_lift threadSet_pred_tcb_at_state threadSet_tcbDomain_triv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st)\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t;
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st)\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>y s. (if \<not> st_tcb_at' runnable' t s \<and> ksCurThread s = t \<and> ksSchedulerAction s = ResumeCurrentThread then \<lambda>_. True else (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st)\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_ s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s) \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st)\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>_ s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ta. \<lbrace>?P15 ta\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv s. ksSchedulerAction s = SwitchToThread ta \<longrightarrow> st_tcb_at' runnable' ta s \<and> tcb_in_cur_domain' ta s\<rbrace>
 2. \<And>s. (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s) \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st) \<Longrightarrow> \<forall>x. ?P15 x s proof (prove)
goal (2 subgoals):
 1. \<And>ta prev_s. \<lbrace>?P16 ta prev_s\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv s'. ksSchedulerAction prev_s = SwitchToThread ta \<longrightarrow> st_tcb_at' runnable' ta s' \<and> tcb_in_cur_domain' ta s'\<rbrace>
 2. \<And>s. (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s) \<and> (ksSchedulerAction s = SwitchToThread t \<longrightarrow> runnable' st) \<Longrightarrow> \<forall>x. ?P16 x s s proof (prove)
goal:
No subgoals!