theory IpcCancel_C

lemma getThreadState_ccorres_foo:
  "(\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow>
    ccorres r xf (\<lambda>s. \<forall>ts. st_tcb_at' ((=) ts) t s \<longrightarrow> P ts s)
                 {s. \<forall>ts tcb'. cslift s (tcb_ptr_to_ctcb_ptr t) = Some tcb'
                              \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb')
                            \<longrightarrow> s \<in> P' ts} hs
        (getThreadState t >>= f) c" apply (rule ccorres_symb_exec_l' [OF _ gts_inv' gts_sp' empty_fail_getThreadState]) apply (erule_tac x=rv in meta_allE) apply (erule ccorres_guard_imp2) apply (clarsimp simp: st_tcb_at'_def) apply (drule obj_at_ko_at', clarsimp) apply (erule cmap_relationE1 [OF cmap_relation_tcb]) apply (erule ko_at_projectKO_opt) apply (clarsimp simp: ctcb_relation_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (\<lambda>s. \<forall>ts. st_tcb_at' ((=) ts) t s \<longrightarrow> P ts s) {s. \<forall>ts tcb'. cslift s (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb') \<longrightarrow> s \<in> P' ts} hs (getThreadState t >>= f) c proof (prove)
goal (1 subgoal):
 1. \<And>rv. (\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c) \<Longrightarrow> ccorres r xf (st_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>s. \<forall>ts. st_tcb_at' ((=) ts) t s \<longrightarrow> P ts s)) {s. \<forall>ts tcb'. cslift s (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb') \<longrightarrow> s \<in> P' ts} hs (f rv) c proof (prove)
goal (1 subgoal):
 1. \<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c \<Longrightarrow> ccorres r xf (st_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>s. \<forall>ts. st_tcb_at' ((=) ts) t s \<longrightarrow> P ts s)) {s. \<forall>ts tcb'. cslift s (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb') \<longrightarrow> s \<in> P' ts} hs (f rv) c proof (prove)
goal (1 subgoal):
 1. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; (st_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>s. \<forall>ts. st_tcb_at' ((=) ts) t s \<longrightarrow> P ts s)) s; s' \<in> {s. \<forall>ts tcb'. cslift s (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb') \<longrightarrow> s \<in> P' ts}\<rbrakk> \<Longrightarrow> P rv s \<and> s' \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>rv s s'. \<lbrakk>(s, s') \<in> rf_sr; \<forall>ts. (\<exists>tcb'. cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb')) \<longrightarrow> s' \<in> P' ts; obj_at' ((\<lambda>st. st = rv) \<circ> tcbState) t s; \<forall>ts. obj_at' ((=) ts \<circ> tcbState) t s \<longrightarrow> P ts s\<rbrakk> \<Longrightarrow> P rv s \<and> s' \<in> P' rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko. \<lbrakk>(s, s') \<in> rf_sr; \<forall>ts. (\<exists>tcb'. cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb')) \<longrightarrow> s' \<in> P' ts; \<forall>ts. obj_at' ((=) ts \<circ> tcbState) t s \<longrightarrow> P ts s; ko_at' ko t s\<rbrakk> \<Longrightarrow> P (tcbState ko) s \<and> s' \<in> P' (tcbState ko) proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko. \<lbrakk>\<forall>ts. (\<exists>tcb'. cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb')) \<longrightarrow> s' \<in> P' ts; \<forall>ts. obj_at' ((=) ts \<circ> tcbState) t s \<longrightarrow> P ts s; ko_at' ko t s\<rbrakk> \<Longrightarrow> map_to_tcbs (ksPSpace s) (?x15 s s' ko) = Some (?y15 s s' ko)
 2. \<And>s s' ko y'. \<lbrakk>\<forall>ts. (\<exists>tcb'. cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb')) \<longrightarrow> s' \<in> P' ts; \<forall>ts. obj_at' ((=) ts \<circ> tcbState) t s \<longrightarrow> P ts s; ko_at' ko t s; map_to_tcbs (ksPSpace s) (?x15 s s' ko) = Some (?y15 s s' ko); ctcb_relation (?y15 s s' ko) y'; cslift s' (tcb_ptr_to_ctcb_ptr (?x15 s s' ko)) = Some y'\<rbrakk> \<Longrightarrow> P (tcbState ko) s \<and> s' \<in> P' (tcbState ko) proof (prove)
goal (1 subgoal):
 1. \<And>s s' ko y'. \<lbrakk>\<forall>ts. (\<exists>tcb'. cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb' \<and> cthread_state_relation ts (tcbState_C tcb', tcbFault_C tcb')) \<longrightarrow> s' \<in> P' ts; \<forall>ts. obj_at' ((=) ts \<circ> tcbState) t s \<longrightarrow> P ts s; ko_at' ko t s; map_to_tcbs (ksPSpace s) t = Some ko; ctcb_relation ko y'; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some y'\<rbrakk> \<Longrightarrow> P (tcbState ko) s \<and> s' \<in> P' (tcbState ko) proof (prove)
goal:
No subgoals!