theory TcbAcc_R

lemma threadSet_corres_noopT:
  assumes x: "\<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow>
                         tcb_relation tcb (fn tcb')"
  assumes y: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (fn tcb) = getF tcb"
  assumes e: "\<And>tcb'. exst_same tcb' (fn tcb')"
  shows      "corres dc \<top> (tcb_at' t)
                           (return v) (threadSet fn t)" proof - have S: "\<And>t s. tcb_at t s \<Longrightarrow> return v s = (thread_set id t >>= (\<lambda>x. return v)) s" apply (clarsimp simp: tcb_at_def) apply (simp add: return_def thread_set_def gets_the_def
                     assert_opt_def simpler_gets_def set_object_def get_object_def
                     put_def get_def bind_def assert_def a_type_def[split_simps kernel_object.split arch_kernel_obj.split]) apply (subgoal_tac "(kheap s)(t \<mapsto> TCB tcb) = kheap s", simp) apply (simp add: map_upd_triv get_tcb_SomeD) apply (simp add: get_tcb_SomeD map_upd_triv) done show ?thesis apply (rule stronger_corres_guard_imp) apply (subst corres_cong [OF refl refl S refl refl]) defer apply (subst bind_return [symmetric],
              rule corres_underlying_split [OF threadset_corresT]) apply (simp add: x) apply simp apply (rule y) apply (rule e) apply (rule corres_noop [where P=\<top> and P'=\<top>]) apply wpsimp+ apply (erule pspace_relation_tcb_at[rotated]) apply clarsimp apply simp apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (return v) (threadSet fn t) proof (state)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (return v) (threadSet fn t) proof (prove)
goal (1 subgoal):
 1. \<And>t s. tcb_at t s \<Longrightarrow> return v s = (do x <- thread_set id t;
return v
od) s proof (prove)
goal (1 subgoal):
 1. \<And>t s tcb. get_tcb t s = Some tcb \<Longrightarrow> return v s = (do x <- thread_set id t;
return v
od) s proof (prove)
goal (1 subgoal):
 1. \<And>t s tcb. get_tcb t s = Some tcb \<Longrightarrow> ((case the (kheap s t) of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB \<longrightarrow> ((\<exists>y. kheap s t = Some y) \<longrightarrow> s = s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) \<and> (\<exists>y. kheap s t = Some y)) \<and> ((case the (kheap s t) of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> ATCB \<longrightarrow> kheap s t = None \<and> (\<exists>y. kheap s t = Some y)) proof (prove)
goal (2 subgoals):
 1. \<And>t s tcb. \<lbrakk>get_tcb t s = Some tcb; (kheap s)(t \<mapsto> TCB tcb) = kheap s\<rbrakk> \<Longrightarrow> ((case the (kheap s t) of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = ATCB \<longrightarrow> (\<exists>y. kheap s t = Some y)) \<and> ((case the (kheap s t) of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) \<noteq> ATCB \<longrightarrow> kheap s t = None \<and> (\<exists>y. kheap s t = Some y))
 2. \<And>t s tcb. get_tcb t s = Some tcb \<Longrightarrow> (kheap s)(t \<mapsto> TCB tcb) = kheap s proof (prove)
goal (1 subgoal):
 1. \<And>t s tcb. get_tcb t s = Some tcb \<Longrightarrow> (kheap s)(t \<mapsto> TCB tcb) = kheap s proof (prove)
goal:
No subgoals! proof (state)
this:
tcb_at ?t ?s \<Longrightarrow> return v ?s = (do x <- thread_set id ?t;
return v
od) ?s

goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (return v) (threadSet fn t) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (tcb_at' t) (return v) (threadSet fn t) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (return v) (threadSet fn t)
 2. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; ?Q s; ?Q' s'\<rbrakk> \<Longrightarrow> tcb_at (?t5 s) s
 2. corres dc ?Q ?Q' (\<lambda>s. (do x <- thread_set id (?t5 s);
return v
od) s) (threadSet fn t)
 3. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q s
 4. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (4 subgoals):
 1. corres dc ?Q ?Q' (\<lambda>s. (do x <- thread_set id (?t5 s);
return v
od) s) (threadSet fn t)
 2. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q' s'
 4. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; ?Q s; ?Q' s'\<rbrakk> \<Longrightarrow> tcb_at (?t5 s) s proof (prove)
goal (10 subgoals):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation (id tcb) (fn tcb')
 2. \<And>tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (id tcb) = getF tcb
 3. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (fn tcb) = getF tcb
 4. \<And>tcb'. exst_same tcb' (fn tcb')
 5. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (?Q10 rv) (?Q'10 rv') (return v) (return rv')
 6. \<lbrace>tcb_at t\<rbrace> thread_set id t \<lbrace>?Q10\<rbrace>
 7. \<lbrace>tcb_at' t\<rbrace> threadSet fn t \<lbrace>?Q'10\<rbrace>
 8. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at t s
 9. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 10. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (9 subgoals):
 1. \<And>tcb. \<forall>(getF, setF)\<in>ran tcb_cap_cases. getF (id tcb) = getF tcb
 2. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (fn tcb) = getF tcb
 3. \<And>tcb'. exst_same tcb' (fn tcb')
 4. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (?Q10 rv) (?Q'10 rv') (return v) (return rv')
 5. \<lbrace>tcb_at t\<rbrace> thread_set id t \<lbrace>?Q10\<rbrace>
 6. \<lbrace>tcb_at' t\<rbrace> threadSet fn t \<lbrace>?Q'10\<rbrace>
 7. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at t s
 8. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 9. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (8 subgoals):
 1. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (fn tcb) = getF tcb
 2. \<And>tcb'. exst_same tcb' (fn tcb')
 3. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (?Q10 rv) (?Q'10 rv') (return v) (return rv')
 4. \<lbrace>tcb_at t\<rbrace> thread_set id t \<lbrace>?Q10\<rbrace>
 5. \<lbrace>tcb_at' t\<rbrace> threadSet fn t \<lbrace>?Q'10\<rbrace>
 6. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at t s
 7. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 8. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (7 subgoals):
 1. \<And>tcb'. exst_same tcb' (fn tcb')
 2. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (?Q10 rv) (?Q'10 rv') (return v) (return rv')
 3. \<lbrace>tcb_at t\<rbrace> thread_set id t \<lbrace>?Q10\<rbrace>
 4. \<lbrace>tcb_at' t\<rbrace> threadSet fn t \<lbrace>?Q'10\<rbrace>
 5. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at t s
 6. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 7. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> corres dc (?Q10 rv) (?Q'10 rv') (return v) (return rv')
 2. \<lbrace>tcb_at t\<rbrace> thread_set id t \<lbrace>?Q10\<rbrace>
 3. \<lbrace>tcb_at' t\<rbrace> threadSet fn t \<lbrace>?Q'10\<rbrace>
 4. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at t s
 5. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 6. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' s. \<lbrakk>dc rv rv'; True\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> True\<rbrace> return rv' \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation \<and> dc v rv\<rbrace>
 2. \<And>rv rv' s. \<lbrakk>dc rv rv'; True; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> True) (return rv')
 3. \<lbrace>tcb_at t\<rbrace> thread_set id t \<lbrace>\<lambda>rv _. True\<rbrace>
 4. \<lbrace>tcb_at' t\<rbrace> threadSet fn t \<lbrace>\<lambda>rv' _. True\<rbrace>
 5. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at t s
 6. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 7. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at t s
 2. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 3. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (3 subgoals):
 1. \<And>s s'. (s, s') \<in> state_relation \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 2. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 3. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>True; tcb_at' t s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> tcb_at' t s'
 2. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; tcb_at t s; tcb_at' t s'\<rbrakk> \<Longrightarrow> tcb_at t s proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (\<lambda>_. True) (tcb_at' t) (return v) (threadSet fn t)

goal:
No subgoals!