theory TcbAcc_R

lemma threadSet_sch_act_wf:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and>
        (ksCurThread s = t \<longrightarrow> \<not>(\<forall>tcb. activatable' (tcbState (F tcb))) \<longrightarrow>
                              ksSchedulerAction s \<noteq> ResumeCurrentThread) \<rbrace>
  threadSet F t
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (rule hoare_lift_Pf2 [where f=ksSchedulerAction]) prefer 2 apply wp apply (case_tac x, simp_all) apply (simp add: ct_in_state'_def) apply (rule hoare_lift_Pf2 [where f=ksCurThread]) prefer 2 apply wp[1] apply (wp threadSet_pred_tcb_at_state) apply clarsimp apply wp apply (clarsimp) apply (wp threadSet_pred_tcb_at_state threadSet_tcbDomain_triv' | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (ksCurThread s = t \<longrightarrow> \<not> (\<forall>tcb. activatable' (tcbState (F tcb))) \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. sch_act_wf x s \<and> x \<noteq> SwitchToThread t \<and> (ksCurThread s = t \<longrightarrow> \<not> (\<forall>tcb. activatable' (tcbState (F tcb))) \<longrightarrow> x \<noteq> ResumeCurrentThread)\<rbrace> threadSet F t \<lbrace>\<lambda>_. sch_act_wf x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. sch_act_wf x s \<and> x \<noteq> SwitchToThread t \<and> (ksCurThread s = t \<longrightarrow> \<not> (\<forall>tcb. activatable' (tcbState (F tcb))) \<longrightarrow> x \<noteq> ResumeCurrentThread)\<rbrace> threadSet F t \<lbrace>\<lambda>_. sch_act_wf x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. sch_act_wf x s \<and> x \<noteq> SwitchToThread t \<and> (ksCurThread s = t \<longrightarrow> \<not> (\<forall>tcb. activatable' (tcbState (F tcb))) \<longrightarrow> x \<noteq> ResumeCurrentThread)\<rbrace> threadSet F t \<lbrace>\<lambda>_. sch_act_wf x\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. ct_in_state' activatable' s \<and> (ksCurThread s = t \<longrightarrow> (\<forall>tcb. activatable' (tcbState (F tcb))))\<rbrace> threadSet F t \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 2. \<lbrace>\<lambda>s. True\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. True\<rbrace>
 3. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. st_tcb_at' activatable' (ksCurThread s) s \<and> (ksCurThread s = t \<longrightarrow> (\<forall>tcb. activatable' (tcbState (F tcb))))\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. st_tcb_at' activatable' (ksCurThread s) s\<rbrace>
 2. \<lbrace>\<lambda>s. True\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. True\<rbrace>
 3. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. st_tcb_at' activatable' x s \<and> (x = t \<longrightarrow> (\<forall>tcb. activatable' (tcbState (F tcb))))\<rbrace> threadSet F t \<lbrace>\<lambda>_. st_tcb_at' activatable' x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 3. \<lbrace>\<lambda>s. True\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. True\<rbrace>
 4. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet F t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. st_tcb_at' activatable' x s \<and> (x = t \<longrightarrow> (\<forall>tcb. activatable' (tcbState (F tcb))))\<rbrace> threadSet F t \<lbrace>\<lambda>_. st_tcb_at' activatable' x\<rbrace>
 3. \<lbrace>\<lambda>s. True\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. True\<rbrace>
 4. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. st_tcb_at' activatable' x s \<and> (x = t \<longrightarrow> (\<forall>tcb. activatable' (tcbState (F tcb))))\<rbrace> threadSet F t \<lbrace>\<lambda>_. st_tcb_at' activatable' x\<rbrace>
 2. \<lbrace>\<lambda>s. True\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. True\<rbrace>
 3. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s. st_tcb_at' activatable' x s \<and> (x = t \<longrightarrow> (\<forall>tcb. activatable' (tcbState (F tcb)))) \<Longrightarrow> tcb_at' t s \<longrightarrow> (if x = t then obj_at' (\<lambda>tcb. activatable' (itcbState (tcb_to_itcb' (F tcb)))) t s else st_tcb_at' activatable' x s)
 2. \<lbrace>\<lambda>s. True\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. True\<rbrace>
 3. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. True\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. True\<rbrace>
 2. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x x3. x = SwitchToThread x3 \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrace>\<lambda>s. st_tcb_at' runnable' x3 s \<and> tcb_in_cur_domain' x3 s \<and> x3 \<noteq> t\<rbrace> threadSet F t \<lbrace>\<lambda>_ a. st_tcb_at' runnable' x3 a \<and> tcb_in_cur_domain' x3 a\<rbrace> proof (prove)
goal:
No subgoals!