theory TcbAcc_R

lemma asUser_corres':
  assumes y: "corres_underlying Id False True r \<top> \<top> f g"
  shows      "corres r (tcb_at t)
                       (tcb_at' t)
                       (as_user t f) (asUser t g)" proof - note arch_tcb_context_get_def[simp] note atcbContextGet_def[simp] note arch_tcb_context_set_def[simp] note atcbContextSet_def[simp] have L1: "corres (\<lambda>tcb con. (arch_tcb_context_get o tcb_arch) tcb = con)
             (tcb_at t) (tcb_at' t)
             (gets_the (get_tcb t)) (threadGet (atcbContextGet o tcbArch) t)" apply (rule corres_guard_imp) apply (rule corres_gets_the) apply (simp add: threadGet_def) apply (rule corres_rel_imp [OF corres_get_tcb]) apply (simp add: tcb_relation_def arch_tcb_relation_def) apply (simp add: tcb_at_def)+ done have L2: "\<And>tcb tcb' con con'. \<lbrakk> tcb_relation tcb tcb'; con = con'\<rbrakk>
              \<Longrightarrow> tcb_relation (tcb \<lparr> tcb_arch := arch_tcb_context_set con (tcb_arch tcb) \<rparr>)
                               (tcb' \<lparr> tcbArch := atcbContextSet con' (tcbArch tcb') \<rparr>)" by (simp add: tcb_relation_def arch_tcb_relation_def) have L3: "\<And>r add tcb tcb' con con'. \<lbrakk> r () (); con = con'\<rbrakk> \<Longrightarrow>
            corres r (\<lambda>s. get_tcb add s = Some tcb)
                     (\<lambda>s'. (tcb', s') \<in> fst (getObject add s'))
                     (set_object add (TCB (tcb \<lparr> tcb_arch := arch_tcb_context_set con (tcb_arch tcb) \<rparr>)))
                     (setObject add (tcb' \<lparr> tcbArch := atcbContextSet con' (tcbArch tcb') \<rparr>))" by (rule setObject_update_TCB_corres [OF L2],
        (simp add: tcb_cte_cases_def tcb_cap_cases_def exst_same_def)+) have L4: "\<And>con con'. con = con' \<Longrightarrow>
            corres (\<lambda>(irv, nc) (irv', nc'). r irv irv' \<and> nc = nc')
                   \<top> \<top> (select_f (f con)) (select_f (g con'))" using y by (fastforce simp: corres_underlying_def select_f_def split_def Id_def) show ?thesis apply (simp add: as_user_def asUser_def) apply (rule corres_guard_imp) apply (rule_tac r'="\<lambda>tcb con. (arch_tcb_context_get o tcb_arch) tcb = con"
           in corres_split) apply simp apply (rule L1[simplified]) apply (rule corres_split) apply (rule L4; simp) apply clarsimp apply (rule corres_split_nor) apply (simp add: threadSet_def) apply (rule corres_symb_exec_r) prefer 4 apply (rule no_fail_pre_and, wp) apply (rule L3[simplified]) apply simp apply simp apply (wp select_f_inv | simp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (state)
goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (state)
this:
arch_tcb_context_get ?a_tcb \<equiv> tcb_context ?a_tcb

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (state)
this:
atcbContextGet \<equiv> atcbContext

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (state)
this:
arch_tcb_context_set ?uc ?a_tcb \<equiv> ?a_tcb\<lparr>tcb_context := ?uc\<rparr>

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (state)
this:
atcbContextSet ?uc ?atcb \<equiv> atcbContext_update (\<lambda>_. ?uc) ?atcb

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>tcb. (=) ((arch_tcb_context_get \<circ> tcb_arch) tcb)) (tcb_at t) (tcb_at' t) (gets_the (get_tcb t)) (threadGet (atcbContextGet \<circ> tcbArch) t) proof (prove)
goal (3 subgoals):
 1. corres (\<lambda>tcb. (=) ((arch_tcb_context_get \<circ> tcb_arch) tcb)) ?Q ?Q' (gets_the (get_tcb t)) (threadGet (atcbContextGet \<circ> tcbArch) t)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres ((\<lambda>tcb. (=) ((arch_tcb_context_get \<circ> tcb_arch) tcb)) \<circ> the) ?P4 ?Q' (gets (get_tcb t)) (threadGet (atcbContextGet \<circ> tcbArch) t)
 2. \<And>s. tcb_at t s \<Longrightarrow> (?P4 and (\<lambda>s. get_tcb t s \<noteq> None)) s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres (\<lambda>x. (=) (tcb_context (tcb_arch (the x))) \<circ> (atcbContext \<circ> tcbArch)) ?P4 ?Q' (gets (get_tcb t)) (getObject t)
 2. \<And>s. tcb_at t s \<Longrightarrow> (?P4 and (\<lambda>s. get_tcb t s \<noteq> None)) s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<And>x y. (tcb_relation \<circ> the) x y \<Longrightarrow> ((=) (tcb_context (tcb_arch (the x))) \<circ> (atcbContext \<circ> tcbArch)) y
 2. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and (\<lambda>s. get_tcb t s \<noteq> None)) s
 3. \<And>s. tcb_at' t s \<Longrightarrow> tcb_at' t 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)) s
 2. \<And>s. tcb_at' t s \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals! proof (state)
this:
corres (\<lambda>tcb. (=) ((arch_tcb_context_get \<circ> tcb_arch) tcb)) (tcb_at t) (tcb_at' t) (gets_the (get_tcb t)) (threadGet (atcbContextGet \<circ> tcbArch) t)

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (prove)
goal (1 subgoal):
 1. \<And>tcb tcb' con con'. \<lbrakk>tcb_relation tcb tcb'; con = con'\<rbrakk> \<Longrightarrow> tcb_relation (tcb\<lparr>tcb_arch := arch_tcb_context_set con (tcb_arch tcb)\<rparr>) (tcbArch_update (\<lambda>_. atcbContextSet con' (tcbArch tcb')) tcb') proof (state)
this:
\<lbrakk>tcb_relation ?tcb ?tcb'; ?con = ?con'\<rbrakk> \<Longrightarrow> tcb_relation (?tcb\<lparr>tcb_arch := arch_tcb_context_set ?con (tcb_arch ?tcb)\<rparr>) (tcbArch_update (\<lambda>_. atcbContextSet ?con' (tcbArch ?tcb')) ?tcb')

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (prove)
goal (1 subgoal):
 1. \<And>r add tcb tcb' con con'. \<lbrakk>r () (); con = con'\<rbrakk> \<Longrightarrow> corres r (\<lambda>s. get_tcb add s = Some tcb) (\<lambda>s'. (tcb', s') \<in> fst (getObject add s')) (set_object add (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set con (tcb_arch tcb)\<rparr>))) (setObject add (tcbArch_update (\<lambda>_. atcbContextSet con' (tcbArch tcb')) tcb')) proof (state)
this:
\<lbrakk>?r () (); ?con = ?con'\<rbrakk> \<Longrightarrow> corres ?r (\<lambda>s. get_tcb ?add s = Some ?tcb) (\<lambda>s'. (?tcb', s') \<in> fst (getObject ?add s')) (set_object ?add (TCB (?tcb\<lparr>tcb_arch := arch_tcb_context_set ?con (tcb_arch ?tcb)\<rparr>))) (setObject ?add (tcbArch_update (\<lambda>_. atcbContextSet ?con' (tcbArch ?tcb')) ?tcb'))

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (prove)
goal (1 subgoal):
 1. \<And>con con'. con = con' \<Longrightarrow> corres (\<lambda>(irv, nc) (irv', nc'). r irv irv' \<and> nc = nc') (\<lambda>_. True) (\<lambda>_. True) (select_f (f con)) (select_f (g con')) proof (prove)
using this:
corres_underlying Id False True r (\<lambda>_. True) (\<lambda>_. True) f g

goal (1 subgoal):
 1. \<And>con con'. con = con' \<Longrightarrow> corres (\<lambda>(irv, nc) (irv', nc'). r irv irv' \<and> nc = nc') (\<lambda>_. True) (\<lambda>_. True) (select_f (f con)) (select_f (g con')) proof (state)
this:
?con = ?con' \<Longrightarrow> corres (\<lambda>(irv, nc) (irv', nc'). r irv irv' \<and> nc = nc') (\<lambda>_. True) (\<lambda>_. True) (select_f (f ?con)) (select_f (g ?con'))

goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (prove)
goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g) proof (prove)
goal (1 subgoal):
 1. corres r (tcb_at t) (tcb_at' t) (do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (f (tcb_context (tcb_arch tcb)));
y <- set_object t (TCB (tcb\<lparr>tcb_arch := tcb_arch tcb\<lparr>tcb_context := uc'\<rparr>\<rparr>));
return a
od) (do uc <- threadGet (atcbContext \<circ> tcbArch) t;
(a, uc') <- select_f (g uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. uc') (tcbArch tcb)) tcb) t;
return a
od) proof (prove)
goal (3 subgoals):
 1. corres r ?Q ?Q' (do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (f (tcb_context (tcb_arch tcb)));
y <- set_object t (TCB (tcb\<lparr>tcb_arch := tcb_arch tcb\<lparr>tcb_context := uc'\<rparr>\<rparr>));
return a
od) (do uc <- threadGet (atcbContext \<circ> tcbArch) t;
(a, uc') <- select_f (g uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. uc') (tcbArch tcb)) tcb) t;
return a
od)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres (\<lambda>tcb. (=) ((arch_tcb_context_get \<circ> tcb_arch) tcb)) ?P4 ?P'4 (gets_the (get_tcb t)) (threadGet (atcbContext \<circ> tcbArch) t)
 2. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> corres r (?R4 rv) (?R'4 rv') (do (a, uc') <- select_f (f (tcb_context (tcb_arch rv)));
y <- set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := uc'\<rparr>\<rparr>));
return a
od) (do (a, uc') <- select_f (g rv');
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. uc') (tcbArch tcb)) tcb) t;
return a
od)
 3. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>?R'4\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. corres (\<lambda>tcb. (=) (tcb_context (tcb_arch tcb))) ?P4 ?P'4 (gets_the (get_tcb t)) (threadGet (atcbContext \<circ> tcbArch) t)
 2. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> corres r (?R4 rv) (?R'4 rv') (do (a, uc') <- select_f (f (tcb_context (tcb_arch rv)));
y <- set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := uc'\<rparr>\<rparr>));
return a
od) (do (a, uc') <- select_f (g rv');
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. uc') (tcbArch tcb)) tcb) t;
return a
od)
 3. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>?R'4\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> corres r (?R4 rv) (?R'4 rv') (do (a, uc') <- select_f (f (tcb_context (tcb_arch rv)));
y <- set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := uc'\<rparr>\<rparr>));
return a
od) (do (a, uc') <- select_f (g rv');
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. uc') (tcbArch tcb)) tcb) t;
return a
od)
 2. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) 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 (8 subgoals):
 1. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> corres (?r'6 rv rv') (?P7 rv) (?P'9 rv') (select_f (f (tcb_context (tcb_arch rv)))) (select_f (g rv'))
 2. \<And>rv rv' rva rv'a. \<lbrakk>(arch_tcb_context_get \<circ> tcb_arch) rv = rv'; ?r'6 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> corres r (?R6 rv rv' rva) (?R'6 rv rv' rv'a) (case rva of (a, uc') \<Rightarrow> do y <- set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := uc'\<rparr>\<rparr>));
return a
od) (case rv'a of (a, uc') \<Rightarrow> do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. uc') (tcbArch tcb)) tcb) t;
return a
od)
 3. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>?R6 rv rv'\<rbrace>
 4. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>?R'6 rv rv'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. ?P7 rv and ?Q8 rv\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. ?P'9 rv' and ?Q'10 rv'\<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>rv rv' rva rv'a. \<lbrakk>(arch_tcb_context_get \<circ> tcb_arch) rv = rv'; (case rva of (irv, nc) \<Rightarrow> \<lambda>(irv', nc'). r irv irv' \<and> nc = nc') rv'a\<rbrakk> \<Longrightarrow> corres r (?R6 rv rv' rva) (?R'6 rv rv' rv'a) (case rva of (a, uc') \<Rightarrow> do y <- set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := uc'\<rparr>\<rparr>));
return a
od) (case rv'a of (a, uc') \<Rightarrow> do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. uc') (tcbArch tcb)) tcb) t;
return a
od)
 2. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>?R6 rv rv'\<rbrace>
 3. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>?R'6 rv rv'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'10 rv'\<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>rv a aa ba. r a aa \<Longrightarrow> corres r (?R6 rv (tcb_context (tcb_arch rv)) (a, ba)) (?R'6 rv (tcb_context (tcb_arch rv)) (aa, ba)) (do y <- set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>));
return a
od) (do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t;
return aa
od)
 2. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>?R6 rv rv'\<rbrace>
 3. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>?R'6 rv rv'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'10 rv'\<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 (10 subgoals):
 1. \<And>rv a aa ba. r a aa \<Longrightarrow> corres dc (?P39 rv (tcb_context (tcb_arch rv)) (a, ba)) (?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba)) (set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>))) (threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t)
 2. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 3. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 4. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 5. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. ?P39 rv rv' a and ?Q37 rv rv' a\<rbrace>
 6. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. ?P'35 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'10 rv'\<rbrace>
 9. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 10. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>rv a aa ba. r a aa \<Longrightarrow> corres dc (?P39 rv (tcb_context (tcb_arch rv)) (a, ba)) (?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba)) (set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>))) (do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb)
od)
 2. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 3. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 4. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 5. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. ?P39 rv rv' a and ?Q37 rv rv' a\<rbrace>
 6. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. ?P'35 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'10 rv'\<rbrace>
 9. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 10. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (13 subgoals):
 1. \<And>rv a aa ba rva. r a aa \<Longrightarrow> corres dc (?P39 rv (tcb_context (tcb_arch rv)) (a, ba)) (?Q'45 rv a aa ba rva) (set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>))) (setObject t (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch rva)) rva))
 2. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> getObject t \<lbrace>?Q'45 rv a aa ba\<rbrace>
 3. \<And>rv a aa ba s. \<lbrakk>r a aa; ?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject t \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv a aa ba. \<lbrakk>r a aa; True\<rbrakk> \<Longrightarrow> no_fail (?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba)) (getObject t)
 5. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 6. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 7. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 8. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. ?P39 rv rv' a and ?Q37 rv rv' a\<rbrace>
 9. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. ?P'35 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 10. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv a aa ba. \<lbrakk>r a aa; True\<rbrakk> \<Longrightarrow> no_fail (?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba)) (getObject t)
 2. \<And>rv a aa ba rva. r a aa \<Longrightarrow> corres dc (?P39 rv (tcb_context (tcb_arch rv)) (a, ba)) (?Q'45 rv a aa ba rva) (set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>))) (setObject t (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch rva)) rva))
 3. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> getObject t \<lbrace>?Q'45 rv a aa ba\<rbrace>
 4. \<And>rv a aa ba s. \<lbrakk>r a aa; ?P'35 rv (tcb_context (tcb_arch rv)) (aa, ba) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject t \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 6. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 7. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 8. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. ?P39 rv rv' a and ?Q37 rv rv' a\<rbrace>
 9. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. ?P'35 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 10. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv a aa ba rva. r a aa \<Longrightarrow> corres dc (?P39 rv (tcb_context (tcb_arch rv)) (a, ba)) (?Q'45 rv a aa ba rva) (set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>))) (setObject t (tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch rva)) rva))
 2. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> getObject t \<lbrace>?Q'45 rv a aa ba\<rbrace>
 3. \<And>rv a aa ba s. \<lbrakk>r a aa; (tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject t \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 5. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 6. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 7. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. ?P39 rv rv' a and ?Q37 rv rv' a\<rbrace>
 8. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. tcb_at' t and ?Q56 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 9. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'10 rv'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv a aa ba rva. r a aa \<Longrightarrow> dc () ()
 2. \<And>rv a aa ba rva. r a aa \<Longrightarrow> ba = ba
 3. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> getObject t \<lbrace>\<lambda>rva s'. (rva, s') \<in> fst (getObject t s')\<rbrace>
 4. \<And>rv a aa ba s. \<lbrakk>r a aa; (tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject t \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 6. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 7. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 8. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. (\<lambda>a. get_tcb t a = Some rv) and ?Q37 rv rv' a\<rbrace>
 9. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. tcb_at' t and ?Q56 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 10. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv a aa ba rva. r a aa \<Longrightarrow> ba = ba
 2. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> getObject t \<lbrace>\<lambda>rva s'. (rva, s') \<in> fst (getObject t s')\<rbrace>
 3. \<And>rv a aa ba s. \<lbrakk>r a aa; (tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject t \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 5. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 6. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 7. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. (\<lambda>a. get_tcb t a = Some rv) and ?Q37 rv rv' a\<rbrace>
 8. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. tcb_at' t and ?Q56 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 9. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'10 rv'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> getObject t \<lbrace>\<lambda>rva s'. (rva, s') \<in> fst (getObject t s')\<rbrace>
 2. \<And>rv a aa ba s. \<lbrakk>r a aa; (tcb_at' t and ?Q56 rv (tcb_context (tcb_arch rv)) (aa, ba)) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getObject t \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv a aa ba. r a aa \<Longrightarrow> corres r (?R26 rv a aa ba) (?R'26 rv a aa ba) (return a) (return aa)
 4. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q37 rv (tcb_context (tcb_arch rv)) (a, ba)\<rbrace> set_object t (TCB (rv\<lparr>tcb_arch := tcb_arch rv\<lparr>tcb_context := ba\<rparr>\<rparr>)) \<lbrace>\<lambda>x. ?R26 rv a aa ba\<rbrace>
 5. \<And>rv a aa ba. r a aa \<Longrightarrow> \<lbrace>?Q'33 rv (tcb_context (tcb_arch rv)) (aa, ba)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContext_update (\<lambda>_. ba) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>x. ?R'26 rv a aa ba\<rbrace>
 6. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q8 rv\<rbrace> select_f (f (tcb_context (tcb_arch rv))) \<lbrace>\<lambda>a. (\<lambda>a. get_tcb t a = Some rv) and ?Q37 rv rv' a\<rbrace>
 7. \<And>rv rv'. (arch_tcb_context_get \<circ> tcb_arch) rv = rv' \<Longrightarrow> \<lbrace>?Q'10 rv'\<rbrace> select_f (g rv') \<lbrace>\<lambda>a. tcb_at' t and ?Q56 rv rv' a and ?Q'33 rv rv' a\<rbrace>
 8. \<lbrace>?Q4\<rbrace> gets_the (get_tcb t) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q8 rv\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> threadGet (atcbContext \<circ> tcbArch) t \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'10 rv'\<rbrace>
 10. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal:
No subgoals! proof (state)
this:
corres r (tcb_at t) (tcb_at' t) (as_user t f) (asUser t g)

goal:
No subgoals!