theory TcbAcc_R

lemma ethread_set_corresT:
  assumes x: "\<And>tcb'. non_exst_same tcb' (f' tcb')"
  assumes z: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (f' tcb) = getF tcb"
  assumes e: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow>
                         etcb_relation (f etcb) (f' tcb')"
  shows      "corres dc (tcb_at t and valid_etcbs)
                        (tcb_at' t)
                    (ethread_set f t) (threadSet f' t)" apply (simp add: ethread_set_def threadSet_def bind_assoc) apply (rule corres_guard_imp) apply (rule corres_split[OF corres_get_etcb set_eobject_corres]) apply (rule x) apply (erule e) apply (simp add: z)+ apply wp+ apply clarsimp apply (simp add: valid_etcbs_def tcb_at_st_tcb_at[symmetric]) apply (force simp: tcb_at_def get_etcb_def obj_at_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_etcbs) (tcb_at' t) (ethread_set f t) (threadSet f' t) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_etcbs) (tcb_at' t) (do tcb <- gets_the (get_etcb t);
set_eobject t (f tcb)
od) (do tcb <- getObject t;
setObject t (f' tcb)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do tcb <- gets_the (get_etcb t);
set_eobject t (f tcb)
od) (do tcb <- getObject t;
setObject t (f' tcb)
od)
 2. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>tcb tcba. etcb_relation tcb tcba \<Longrightarrow> non_exst_same (?tcb'9 tcba) (f' tcba)
 2. \<And>tcb tcba. \<lbrakk>etcb_relation tcb tcba; etcb_relation (?etcb8 tcb) (?tcb'9 tcba)\<rbrakk> \<Longrightarrow> etcb_relation (f tcb) (f' tcba)
 3. \<And>tcb tcba. etcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcba) = getF (?tcb'9 tcba)
 4. \<And>tcb tcba. etcb_relation tcb tcba \<Longrightarrow> dc () ()
 5. \<lbrace>?Q4\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>tcb. tcb_at t and (\<lambda>s. ekheap s t = Some (?etcb8 tcb))\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' (?tcb'9 tcb) t\<rbrace>
 7. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (is_etcb_at t and ?Q4) s
 8. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>tcb tcba. \<lbrakk>etcb_relation tcb tcba; etcb_relation (?etcb8 tcb) tcba\<rbrakk> \<Longrightarrow> etcb_relation (f tcb) (f' tcba)
 2. \<And>tcb tcba. etcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcba) = getF tcba
 3. \<And>tcb tcba. etcb_relation tcb tcba \<Longrightarrow> dc () ()
 4. \<lbrace>?Q4\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>tcb. tcb_at t and (\<lambda>s. ekheap s t = Some (?etcb8 tcb))\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 6. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (is_etcb_at t and ?Q4) s
 7. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>tcb tcba. etcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcba) = getF tcba
 2. \<And>tcb tcba. etcb_relation tcb tcba \<Longrightarrow> dc () ()
 3. \<lbrace>?Q4\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>tcb. tcb_at t and (\<lambda>s. ekheap s t = Some (?etcb8 tcb))\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 5. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (is_etcb_at t and ?Q4) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> gets_the (get_etcb t) \<lbrace>\<lambda>tcb. tcb_at t and (\<lambda>s. ekheap s t = Some (?etcb8 tcb))\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcb. ko_at' tcb t\<rbrace>
 3. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (is_etcb_at t and ?Q4) s
 4. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (tcb_at t and valid_etcbs) s \<Longrightarrow> (is_etcb_at t and (\<lambda>s. get_etcb t s \<noteq> None \<longrightarrow> (tcb_at t and (\<lambda>sa. ekheap sa t = Some (?etcb8 (the (get_etcb t s))))) s)) s
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at t s; valid_etcbs s\<rbrakk> \<Longrightarrow> is_etcb_at t s \<and> ((\<exists>y. get_etcb t s = Some y) \<longrightarrow> ekheap s t = Some (?etcb8 (the (get_etcb t s))))
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_etcb_at t s; \<forall>ptr. tcb_at ptr s = is_etcb_at ptr s\<rbrakk> \<Longrightarrow> (\<exists>y. get_etcb t s = Some y) \<longrightarrow> ekheap s t = Some (?etcb8 (the (get_etcb t s)))
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!