theory TcbAcc_R

lemma threadset_corresT:
  assumes x: "\<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow>
                         tcb_relation (f tcb) (f' tcb')"
  assumes y: "\<And>tcb. \<forall>(getF, setF) \<in> ran tcb_cap_cases. getF (f tcb) = getF tcb"
  assumes z: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (f' tcb) = getF tcb"
  assumes e: "\<And>tcb'. exst_same tcb' (f' tcb')"
  shows      "corres dc (tcb_at t)
                        (tcb_at' t)
                    (thread_set f t) (threadSet f' t)" apply (simp add: thread_set_def threadSet_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getObject_TCB_corres]) apply (rule setObject_update_TCB_corres') apply (erule x) apply (rule y) apply (clarsimp simp: bspec_split [OF spec [OF z]]) apply fastforce apply simp apply (rule e) apply wp+ apply (clarsimp simp add: tcb_at_def obj_at_def) apply (drule get_tcb_SomeD) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (thread_set f t) (threadSet f' t) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t) (tcb_at' t) (do tcb <- gets_the (get_tcb t);
set_object t (TCB (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_tcb t);
set_object t (TCB (f tcb))
od) (do tcb <- getObject t;
setObject t (f' tcb)
od)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> corres dc (?R4 tcb) (?R'4 tcba) (set_object t (TCB (f tcb))) (setObject t (f' tcba))
 2. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>?R'4\<rbrace>
 4. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>tcb tcba. \<lbrakk>tcb_relation tcb tcba; tcb_relation (?tcb10 tcb) (?tcb'12 tcba)\<rbrakk> \<Longrightarrow> tcb_relation (f tcb) (f' tcba)
 2. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF (?tcb10 tcb)
 3. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcba) = getF (?tcb'12 tcba)
 4. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> dc () ()
 5. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> exst_same (?tcb'12 tcba) (f' tcba)
 6. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>tcb. ko_at (TCB (?tcb10 tcb)) t\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcba. ko_at' (?tcb'12 tcba) t\<rbrace>
 8. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 9. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (f tcb) = getF (?tcb10 tcb)
 2. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcba) = getF (?tcb'12 tcba)
 3. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> dc () ()
 4. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> exst_same (?tcb'12 tcba) (f' tcba)
 5. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>tcb. ko_at (TCB (?tcb10 tcb)) t\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcba. ko_at' (?tcb'12 tcba) t\<rbrace>
 7. \<And>s. tcb_at t s \<Longrightarrow> (tcb_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. tcb_relation tcb tcba \<Longrightarrow> \<forall>(getF, v)\<in>ran tcb_cte_cases. getF (f' tcba) = getF (?tcb'12 tcba)
 2. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> dc () ()
 3. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> exst_same (?tcb'12 tcba) (f' tcba)
 4. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>tcb. ko_at (TCB tcb) t\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcba. ko_at' (?tcb'12 tcba) t\<rbrace>
 6. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>tcb tcba a b. \<lbrakk>tcb_relation tcb tcba; (a, b) \<in> ran tcb_cte_cases\<rbrakk> \<Longrightarrow> a tcba = a (?tcb'12 tcba)
 2. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> dc () ()
 3. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> exst_same (?tcb'12 tcba) (f' tcba)
 4. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>tcb. ko_at (TCB tcb) t\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcba. ko_at' (?tcb'12 tcba) t\<rbrace>
 6. \<And>s. tcb_at t s \<Longrightarrow> (tcb_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. tcb_relation tcb tcba \<Longrightarrow> dc () ()
 2. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> exst_same tcba (f' tcba)
 3. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>tcb. ko_at (TCB tcb) t\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcba. ko_at' tcba t\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>tcb tcba. tcb_relation tcb tcba \<Longrightarrow> exst_same tcba (f' tcba)
 2. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>tcb. ko_at (TCB tcb) t\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcba. ko_at' tcba t\<rbrace>
 4. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<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_tcb t) \<lbrace>\<lambda>tcb. ko_at (TCB tcb) t\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getObject t \<lbrace>\<lambda>tcba. ko_at' tcba t\<rbrace>
 3. \<And>s. tcb_at t s \<Longrightarrow> (tcb_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 s \<Longrightarrow> (tcb_at t and (\<lambda>s. get_tcb t s \<noteq> None \<longrightarrow> ko_at (TCB (the (get_tcb t s))) t 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 ko y. \<lbrakk>kheap s t = Some ko; is_tcb ko; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> ko = TCB y
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>_. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s ko y. \<lbrakk>kheap s t = Some ko; is_tcb ko; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> ko = TCB y
 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!