theory TcbAcc_C

lemma threadSet_corres_lemma:
  assumes spec: "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. P s\<rbrace> Call f {t. Q s t}"
  and      mod: "modifies_heap_spec f"
  and  rl: "\<And>\<sigma> x t ko. \<lbrakk>(\<sigma>, x) \<in> rf_sr; Q x t; x \<in> P'; ko_at' ko thread \<sigma>\<rbrakk>
             \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (g ko))\<rparr>,
                  t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr"
  and  g:  "\<And>s x. \<lbrakk>tcb_at' thread s; x \<in> P'; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> P x"
  shows "ccorres dc xfdc (tcb_at' thread) P' [] (threadSet g thread) (Call f)" apply (rule ccorres_Call_call_for_vcg) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre) apply (rule HoarePartial.ProcModifyReturnNoAbr [where return' = "\<lambda>s t. t\<lparr> globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t) \<rparr>\<rparr>"]) apply (rule HoarePartial.ProcSpecNoAbrupt [OF _ _ spec]) apply (rule subset_refl) apply vcg prefer 2 apply (rule mod) apply (clarsimp simp: mex_def meq_def) apply clarsimp apply (rule conjI) apply (erule (2) g) apply clarsimp apply (frule obj_at_ko_at') apply clarsimp apply (rule bexI [rotated]) apply (erule threadSet_eq) apply simp apply (rule_tac x1 = "t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>" in iffD1 [OF rf_sr_upd], simp_all)[1] apply (erule (3) rl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread) P' [] (threadSet g thread) (Call f) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread) P' [] (threadSet g thread) (call id f (\<lambda>s t. t) (\<lambda>s t. Basic id)) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} call id f (\<lambda>s t. t) (\<lambda>s t. Basic id) {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'6 \<sigma>) call id f (\<lambda>s t. t) (\<lambda>s t. Basic id) {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'6 \<sigma> proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'6 \<sigma>) call id f (\<lambda>s t. t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) (\<lambda>s t. Basic id) {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 3. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 4. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'6 \<sigma> proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma>. ?P'6 \<sigma> \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> ?R14 \<sigma> s t)}
 2. \<And>\<sigma>. \<forall>s t. \<Gamma>\<turnstile> (?R14 \<sigma> s t) Basic id {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 3. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 4. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 5. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'6 \<sigma> proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. \<forall>s t. \<Gamma>\<turnstile> (?R14 \<sigma> s t) Basic id {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 3. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 4. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> ?R14 \<sigma> s t)} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 2. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 3. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> dc rv (xfdc (id s))})} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<forall>\<sigma>'. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>'} Call f (?Modif9 \<sigma> \<sigma>')
 2. \<And>\<sigma>. \<forall>s t. t \<in> ?Modif9 \<sigma> (id s) \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 3. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> dc rv (xfdc (id s))})} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<forall>s t. t \<in> {t. mex (\<lambda>t_hrs_'. t may_not_modify_globals globals (id s))} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> = t
 2. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> dc rv (xfdc (id s))})} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. tcb_at' thread \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>Z. id s \<in> \<lbrace>Z. P Z\<rbrace> \<and> (\<forall>t. t \<in> {t. Q Z t} \<longrightarrow> t\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet g thread \<sigma>). (\<sigma>', id s) \<in> rf_sr \<and> dc rv (xfdc (id s))})} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> P x \<and> (\<forall>t. Q x t \<longrightarrow> (\<exists>xa\<in>fst (threadSet g thread \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr)) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> P x
 2. \<And>\<sigma> x. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<forall>t. Q x t \<longrightarrow> (\<exists>xa\<in>fst (threadSet g thread \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<forall>t. Q x t \<longrightarrow> (\<exists>xa\<in>fst (threadSet g thread \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (threadSet g thread \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t; \<exists>ko. ko_at' ko thread \<sigma> \<and> True\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (threadSet g thread \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t ko. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (threadSet g thread \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x t ko. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> ?x50 \<sigma> x t ko \<in> fst (threadSet g thread \<sigma>)
 2. \<And>\<sigma> x t ko. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> case ?x50 \<sigma> x t ko of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t ko. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> injectKOS (g ko))\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t ko. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (g ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x t ko. \<lbrakk>tcb_at' thread \<sigma>; x \<in> P'; (\<sigma>, x) \<in> rf_sr; Q x t; ko_at' ko thread \<sigma>\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> KOTCB (g ko))\<rparr>, t\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr proof (prove)
goal:
No subgoals!