theory TcbAcc_R

lemma threadSet_runnable_sch_act:
  "(\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb) \<Longrightarrow>
   \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
    threadSet F t
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (clarsimp simp: valid_def) apply (frule_tac P1="(=) (ksSchedulerAction s)"
                in use_valid [OF _ threadSet_nosch],
         rule refl) apply (frule_tac P1="(=) (ksCurThread s)"
                in use_valid [OF _ threadSet_ct],
         rule refl) apply (frule_tac P1="(=) (ksCurDomain s)"
                in use_valid [OF _ threadSet_cd],
         rule refl) apply (case_tac "ksSchedulerAction b",
         simp_all add: sch_act_simple_def ct_in_state'_def pred_tcb_at'_def) apply (drule_tac t'1="ksCurThread s"
                and P1="activatable' \<circ> tcbState"
                 in use_valid [OF _ threadSet_obj_at'_really_strongest]) apply (clarsimp elim!: obj_at'_weakenE) apply (simp add: o_def) apply (rename_tac word) apply (rule conjI) apply (frule_tac t'1=word
               and P1="runnable' \<circ> tcbState"
                in use_valid [OF _ threadSet_obj_at'_really_strongest]) apply (clarsimp elim!: obj_at'_weakenE, clarsimp simp: obj_at'_def projectKOs) apply (simp add: tcb_in_cur_domain'_def) apply (frule_tac t'1=word
               and P1="\<lambda>tcb. ksCurDomain b = tcbDomain tcb"
                in use_valid [OF _ threadSet_obj_at'_really_strongest]) apply (clarsimp simp: o_def tcb_in_cur_domain'_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb) \<Longrightarrow> \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; sch_act_wf (ksSchedulerAction s) s; ((), b) \<in> fst (threadSet F t s)\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; sch_act_wf (ksSchedulerAction s) s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = ksSchedulerAction b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; sch_act_wf (ksSchedulerAction s) s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = ksSchedulerAction b; ksCurThread s = ksCurThread b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; sch_act_wf (ksSchedulerAction s) s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = ksSchedulerAction b; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = ResumeCurrentThread; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) b
 2. \<And>s b x3. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread x3; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread x3\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 b \<and> tcb_in_cur_domain' x3 b proof (prove)
goal (3 subgoals):
 1. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ksCurThread s then (activatable' \<circ> tcbState) (F obj) else (activatable' \<circ> tcbState) obj) (ksCurThread s) s
 2. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread; obj_at' (activatable' \<circ> tcbState) (ksCurThread s) b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) b
 3. \<And>s b x3. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread x3; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread x3\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 b \<and> tcb_in_cur_domain' x3 b proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksSchedulerAction s = ResumeCurrentThread; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread; obj_at' (activatable' \<circ> tcbState) (ksCurThread s) b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) b
 2. \<And>s b x3. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread x3; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread x3\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 b \<and> tcb_in_cur_domain' x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s b x3. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread x3; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread x3\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 b \<and> tcb_in_cur_domain' x3 b proof (prove)
goal (1 subgoal):
 1. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) word b \<and> tcb_in_cur_domain' word b proof (prove)
goal (2 subgoals):
 1. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) word b
 2. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' word b proof (prove)
goal (3 subgoals):
 1. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = word then (runnable' \<circ> tcbState) (F obj) else (runnable' \<circ> tcbState) obj) word s
 2. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; obj_at' (runnable' \<circ> tcbState) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) word b
 3. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' word b proof (prove)
goal (1 subgoal):
 1. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' word b proof (prove)
goal (1 subgoal):
 1. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b proof (prove)
goal (2 subgoals):
 1. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = word then ksCurDomain b = tcbDomain (F obj) else ksCurDomain b = tcbDomain obj) word s
 2. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b proof (prove)
goal (1 subgoal):
 1. \<And>s b word. \<lbrakk>\<And>tcb. runnable' (tcbState (F tcb)) \<and> tcbDomain (F tcb) = tcbDomain tcb \<and> tcbPriority (F tcb) = tcbPriority tcb; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; ((), b) \<in> fst (threadSet F t s); ksSchedulerAction s = SwitchToThread word; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b proof (prove)
goal:
No subgoals!