theory TcbAcc_C

lemma threadSet_ccorres_lemma4:
  "\<lbrakk> \<And>s tcb. \<Gamma> \<turnstile> (Q s tcb) c {s'. (s \<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr};
          \<And>s s' tcb tcb'. \<lbrakk> (s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s;
                             cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb';
                             ctcb_relation tcb tcb'; P' s ; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb \<rbrakk>
         \<Longrightarrow> ccorres dc xfdc (obj_at' (P :: tcb \<Rightarrow> bool) thread and P') R hs (threadSet F thread) c" apply (rule ccorres_from_vcg) apply (rule allI) apply (case_tac "obj_at' P thread \<sigma>") apply (drule obj_at_ko_at', clarsimp) apply (rule conseqPre, rule conseqPost) apply assumption apply clarsimp apply (rule rev_bexI, rule threadSet_eq) apply assumption apply simp apply simp apply clarsimp apply (drule(1) obj_at_cslift_tcb, clarsimp) apply simp apply (rule hoare_complete') apply (simp add: cnvalid_def nvalid_def)  (* pretty *)
   done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (obj_at' P thread and P') R hs (threadSet F thread) c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>x\<in>fst (threadSet F thread \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr}
 2. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'11 \<sigma> ko) c (?Q'14 \<sigma> ko),(?A'14 \<sigma> ko)
 2. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> ?Q'14 \<sigma> ko \<subseteq> {s. \<exists>x\<in>fst (threadSet F thread \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr}
 3. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> ?A'14 \<sigma> ko \<subseteq> {}
 4. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'11 \<sigma> ko
 5. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s'. (?s20 \<sigma> ko\<lparr>ksPSpace := (ksPSpace (?s20 \<sigma> ko))(thread \<mapsto> KOTCB (F (?tcb20 \<sigma> ko)))\<rparr>, s') \<in> rf_sr} \<subseteq> {s. \<exists>x\<in>fst (threadSet F thread \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr}
 2. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {} \<subseteq> {}
 3. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> Q (?s20 \<sigma> ko) (?tcb20 \<sigma> ko)
 4. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> ko x. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko; (?s20 \<sigma> ko\<lparr>ksPSpace := (ksPSpace (?s20 \<sigma> ko))(thread \<mapsto> KOTCB (F (?tcb20 \<sigma> ko)))\<rparr>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (threadSet F thread \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {} \<subseteq> {}
 3. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> Q (?s20 \<sigma> ko) (?tcb20 \<sigma> ko)
 4. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (5 subgoals):
 1. \<And>\<sigma> ko x. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko; (?s20 \<sigma> ko\<lparr>ksPSpace := (ksPSpace (?s20 \<sigma> ko))(thread \<mapsto> KOTCB (F (?tcb20 \<sigma> ko)))\<rparr>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> ko_at' (?tcb29 \<sigma> ko x) thread \<sigma>
 2. \<And>\<sigma> ko x. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko; (?s20 \<sigma> ko\<lparr>ksPSpace := (ksPSpace (?s20 \<sigma> ko))(thread \<mapsto> KOTCB (F (?tcb20 \<sigma> ko)))\<rparr>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> injectKOS (F (?tcb29 \<sigma> ko x)))\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 3. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {} \<subseteq> {}
 4. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> Q (?s20 \<sigma> ko) (?tcb20 \<sigma> ko)
 5. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> ko x. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko; (?s20 \<sigma> ko\<lparr>ksPSpace := (ksPSpace (?s20 \<sigma> ko))(thread \<mapsto> KOTCB (F (?tcb20 \<sigma> ko)))\<rparr>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> case ((), \<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(thread \<mapsto> injectKOS (F ko))\<rparr>) of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr
 2. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {} \<subseteq> {}
 3. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> Q (?s20 \<sigma> ko) (?tcb20 \<sigma> ko)
 4. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {} \<subseteq> {}
 2. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> Q \<sigma> ko
 3. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko\<rbrakk> \<Longrightarrow> {s. obj_at' P thread \<sigma> \<and> P' \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> Q \<sigma> ko
 2. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> ko x. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; ko_at' ko thread \<sigma>; P ko; obj_at' P thread \<sigma>; P' \<sigma>; x \<in> R; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<in> Q \<sigma> ko
 2. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. (obj_at' P thread and P') \<sigma> \<and> s \<in> R \<and> (\<sigma>, s) \<in> rf_sr} c {s. \<exists>(rv, \<sigma>')\<in>fst (threadSet F thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {} c {s. \<exists>x\<in>fst (threadSet F thread \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<And>s tcb. \<Gamma>\<turnstile> (Q s tcb) c {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (F tcb))\<rparr>, s') \<in> rf_sr}; \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; P tcb; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; P' s; s' \<in> R\<rbrakk> \<Longrightarrow> s' \<in> Q s tcb; \<not> obj_at' P thread \<sigma>\<rbrakk> \<Longrightarrow> \<forall>n. \<Gamma>,{}\<Turnstile>n:\<^bsub>/{}\<^esub> {} c {s. \<exists>x\<in>fst (threadSet F thread \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr},{} proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!