theory IpcCancel_C

lemma ccorres_abstract_ksCurThread:
  assumes ceqv: "\<And>rv' t t'. ceqv \<Gamma> (\<lambda>s. ksCurThread_' (globals s)) rv' t t' d (d' rv')"
  and       cc: "\<And>ct. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (G ct) (G' ct) hs a (d' (tcb_ptr_to_ctcb_ptr ct))"
  shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s)
            {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} hs a d" apply (rule ccorres_guard_imp) prefer 2 apply assumption apply (rule ccorres_abstract[OF ceqv, where G'="\<lambda>ct. \<lbrace>ct = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr ct)"]) apply (subgoal_tac "\<exists>t. rv' = tcb_ptr_to_ctcb_ptr t") apply clarsimp apply (rule ccorres_guard_imp2) apply (rule cc) apply (clarsimp simp: rf_sr_ksCurThread) apply (metis tcb_ptr_to_tcb_ptr) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s) {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} hs a d proof (prove)
goal (3 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?Q ?Q' hs a d
 2. \<And>s. G (ksCurThread s) s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<And>s. G (ksCurThread s) s \<Longrightarrow> ?Q s
 2. ccorres_underlying rf_sr \<Gamma> r xf arrel axf ?Q ?Q' hs a d
 3. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s) ?Q' hs a d
 2. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>rv'. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s) (\<lbrace>rv' = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr rv')) hs a (d' rv')
 2. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> {s. s \<in> \<lbrace>\<^bsup>s\<^esup>ksCurThread = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} proof (prove)
goal (3 subgoals):
 1. \<And>rv'. \<exists>t. rv' = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s) (\<lbrace>rv' = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr rv')) hs a (d' rv')
 2. \<And>rv'. \<exists>t. rv' = tcb_ptr_to_ctcb_ptr t
 3. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> {s. s \<in> \<lbrace>\<^bsup>s\<^esup>ksCurThread = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} proof (prove)
goal (3 subgoals):
 1. \<And>t. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s) (\<lbrace>tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread\<rbrace> \<inter> G' t) hs a (d' (tcb_ptr_to_ctcb_ptr t))
 2. \<And>rv'. \<exists>t. rv' = tcb_ptr_to_ctcb_ptr t
 3. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> {s. s \<in> \<lbrace>\<^bsup>s\<^esup>ksCurThread = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} proof (prove)
goal (4 subgoals):
 1. \<And>t. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q11 t) (?Q'11 t) hs a (d' (tcb_ptr_to_ctcb_ptr t))
 2. \<And>t s s'. \<lbrakk>(s, s') \<in> rf_sr; G (ksCurThread s) s; s' \<in> \<lbrace>tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread\<rbrace> \<inter> G' t\<rbrakk> \<Longrightarrow> ?Q11 t s \<and> s' \<in> ?Q'11 t
 3. \<And>rv'. \<exists>t. rv' = tcb_ptr_to_ctcb_ptr t
 4. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> {s. s \<in> \<lbrace>\<^bsup>s\<^esup>ksCurThread = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} proof (prove)
goal (3 subgoals):
 1. \<And>t s s'. \<lbrakk>(s, s') \<in> rf_sr; G (ksCurThread s) s; s' \<in> \<lbrace>tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread\<rbrace> \<inter> G' t\<rbrakk> \<Longrightarrow> G t s \<and> s' \<in> G' t
 2. \<And>rv'. \<exists>t. rv' = tcb_ptr_to_ctcb_ptr t
 3. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> {s. s \<in> \<lbrace>\<^bsup>s\<^esup>ksCurThread = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} proof (prove)
goal (2 subgoals):
 1. \<And>rv'. \<exists>t. rv' = tcb_ptr_to_ctcb_ptr t
 2. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> {s. s \<in> \<lbrace>\<^bsup>s\<^esup>ksCurThread = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> {s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} \<Longrightarrow> s \<in> {s. s \<in> \<lbrace>\<^bsup>s\<^esup>ksCurThread = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} proof (prove)
goal:
No subgoals!