theory TcbAcc_R

lemma threadSet_cte_wp_at'T:
  assumes x: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (F tcb) = getF tcb"
  shows "\<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s)\<rbrace>" apply (simp add: threadSet_def) apply (rule hoare_seq_ext [where B="\<lambda>rv s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) rv) t s"]) apply (rule setObject_cte_wp_at2') apply (clarsimp simp: updateObject_default_def projectKOs in_monad
                          obj_at'_def objBits_simps' in_magnitude_check prod_eq_iff) apply (case_tac tcb, clarsimp simp: bspec_split [OF spec [OF x]]) apply (clarsimp simp: updateObject_default_def in_monad bind_def
                         projectKOs) apply (wp getObject_tcb_wp) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) tcb) t s\<rbrace> setObject t (F tcb) \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s)\<rbrace>
 2. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> getObject t \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) rv) t s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb x n tcba s ta. \<lbrakk>ta \<in> fst (updateObject (F tcb) (KOTCB tcba) t x n s); obj_at' ((=) tcb) t s; lookupAround2 t (ksPSpace s) = (Some (x, KOTCB tcba), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ta = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcba)
 2. \<And>tcb x n cte s. fst (updateObject (F tcb) (KOCTE cte) t x n s) = {}
 3. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> getObject t \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) rv) t s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb s a b. \<lbrakk>ksPSpace s t = Some (KOTCB tcb); is_aligned t 9; ps_clear t 9 s; (a, b) \<in> ran tcb_cte_cases\<rbrakk> \<Longrightarrow> a (F tcb) = a tcb
 2. \<And>tcb x n cte s. fst (updateObject (F tcb) (KOCTE cte) t x n s) = {}
 3. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> getObject t \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) rv) t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb x n cte s. fst (updateObject (F tcb) (KOCTE cte) t x n s) = {}
 2. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> getObject t \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) rv) t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at' P p s)\<rbrace> getObject t \<lbrace>\<lambda>rv s. P' (cte_wp_at' P p s) \<and> obj_at' ((=) rv) t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P' (cte_wp_at' P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> P' (cte_wp_at' P p s) \<and> obj_at' ((=) ta) t s) proof (prove)
goal:
No subgoals!