theory TcbAcc_R

lemma sts'_valid_pspace'_inv[wp]:
  "\<lbrace> valid_pspace' and tcb_at' t and valid_tcb_state' st \<rbrace>
  setThreadState st t
  \<lbrace> \<lambda>rv. valid_pspace' \<rbrace>" apply (simp add: valid_pspace'_def) apply (rule hoare_pre) apply (wp sts_valid_objs') apply (simp add: setThreadState_def threadSet_def
                    setQueue_def bind_assoc valid_mdb'_def) apply (wp getObject_obj_at_tcb | simp)+ apply (clarsimp simp: valid_mdb'_def) apply (drule obj_at_ko_at') apply clarsimp apply (erule obj_at'_weakenE) apply (simp add: tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_tcb_state' st) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_tcb_state' st) s \<Longrightarrow> (valid_objs' and valid_tcb_state' st) s \<and> ?P'8 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> do x <- getObject t;
y <- setObject t (tcbState_update (\<lambda>_. st) x);
runnable <- isRunnable t;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s)\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_tcb_state' st) s \<Longrightarrow> (valid_objs' and valid_tcb_state' st) s \<and> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> tcb_at' t s \<and> valid_tcb_state' st s \<Longrightarrow> valid_mdb_ctes (ctes_of s) \<and> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbState_update (\<lambda>_. st) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); tcb_at' t s; valid_tcb_state' st s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbState_update (\<lambda>_. st) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); valid_tcb_state' st s; \<exists>ko. ko_at' ko t s \<and> True\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbState_update (\<lambda>_. st) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); valid_tcb_state' st s; ko_at' ko t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbState_update (\<lambda>_. st) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s ko k. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); valid_tcb_state' st s; k = ko\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF k = getF (tcbState_update (\<lambda>_. st) k) proof (prove)
goal:
No subgoals!