theory TcbAcc_R

lemma threadSet_sch_actT_P:
  assumes z: "\<not> P \<Longrightarrow> (\<forall>tcb. tcbState (F tcb) = tcbState tcb
                         \<and> tcbDomain (F tcb) = tcbDomain tcb)"
  assumes z': "P \<Longrightarrow> (\<forall>tcb. tcbState (F tcb) = Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb )
                      \<and> (\<forall>st. Q st \<longrightarrow> st = Inactive)"
  shows "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (P \<longrightarrow> st_tcb_at' Q t s)\<rbrace>
          threadSet F t
         \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" using z z' apply (case_tac P, simp_all add: threadSet_sch_act) apply (clarsimp simp: valid_def) apply (frule_tac P1="\<lambda>sa. sch_act_wf sa s"
                in use_valid [OF _ threadSet_nosch], assumption) 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: ct_in_state'_def pred_tcb_at'_def) apply (subgoal_tac "t \<noteq> ksCurThread s") apply (drule_tac t'1="ksCurThread s"
                 and P1="activatable' \<circ> tcbState"
                  in use_valid [OF _ threadSet_obj_at'_really_strongest]) apply (clarsimp simp: o_def) apply (clarsimp simp: o_def) apply (fastforce simp: obj_at'_def projectKOs) apply (rename_tac word) apply (subgoal_tac "t \<noteq> word") apply (frule_tac t'1=word
                and P1="runnable' \<circ> tcbState"
                 in use_valid [OF _ threadSet_obj_at'_really_strongest]) apply (clarsimp simp: o_def) apply (rule conjI) apply (clarsimp simp: o_def) apply (clarsimp simp: 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)+ apply (fastforce simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (P \<longrightarrow> st_tcb_at' Q t s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
using this:
\<not> P \<Longrightarrow> \<forall>tcb. tcbState (F tcb) = tcbState tcb \<and> tcbDomain (F tcb) = tcbDomain tcb
P \<Longrightarrow> (\<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb) \<and> (\<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive)

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (P \<longrightarrow> st_tcb_at' Q t s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P; (\<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb) \<and> (\<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive)\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' Q t 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; st_tcb_at' Q t s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; st_tcb_at' Q t s; sch_act_wf (ksSchedulerAction b) s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; st_tcb_at' Q t s; sch_act_wf (ksSchedulerAction b) s; ksCurThread s = ksCurThread b\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction b) b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; st_tcb_at' Q t s; sch_act_wf (ksSchedulerAction b) s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread; t \<noteq> ksCurThread s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) b
 2. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s
 3. \<And>s b x3. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; 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 (4 subgoals):
 1. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread; t \<noteq> ksCurThread s\<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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread; t \<noteq> ksCurThread s; obj_at' (activatable' \<circ> tcbState) (ksCurThread s) b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) b
 3. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s
 4. \<And>s b x3. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread; t \<noteq> ksCurThread s; obj_at' (activatable' \<circ> tcbState) (ksCurThread s) b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) b
 2. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s
 3. \<And>s b x3. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. activatable' (tcbState ko)) (ksCurThread b) s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = ResumeCurrentThread\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s
 2. \<And>s b x3. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) x3 s \<and> tcb_in_cur_domain' x3 s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) word b \<and> tcb_in_cur_domain' word b
 2. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> t \<noteq> word proof (prove)
goal (3 subgoals):
 1. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> 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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) word b \<and> tcb_in_cur_domain' word b
 3. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> t \<noteq> word proof (prove)
goal (2 subgoals):
 1. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) word b \<and> tcb_in_cur_domain' word b
 2. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> t \<noteq> word proof (prove)
goal (3 subgoals):
 1. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. runnable' (tcbState ko)) word b
 2. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' word b
 3. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> t \<noteq> word proof (prove)
goal (2 subgoals):
 1. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' word b
 2. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> t \<noteq> word proof (prove)
goal (2 subgoals):
 1. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b
 2. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> t \<noteq> word proof (prove)
goal (3 subgoals):
 1. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s\<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>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word; t \<noteq> word; obj_at' (runnable' \<circ> tcbState) word b; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word s; obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. ksCurDomain b = tcbDomain tcb) word b
 3. \<And>s b word. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; obj_at' (\<lambda>ko. runnable' (tcbState ko)) word s \<and> tcb_in_cur_domain' word s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread word\<rbrakk> \<Longrightarrow> t \<noteq> word proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>P; \<forall>tcb. tcbState (F tcb) = Structures_H.thread_state.Inactive \<and> tcbDomain (F tcb) = tcbDomain tcb; \<forall>st. Q st \<longrightarrow> st = Structures_H.thread_state.Inactive; ((), b) \<in> fst (threadSet F t s); sch_act_wf (ksSchedulerAction s) s; obj_at' (\<lambda>ko. Q (tcbState ko)) t s; ksCurThread s = ksCurThread b; ksCurDomain s = ksCurDomain b; ksSchedulerAction b = SwitchToThread t; obj_at' (\<lambda>ko. runnable' (tcbState ko)) t s; tcb_in_cur_domain' t s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!