theory ADT_IF_Refine_C

lemma kernel_exit_corres_C:
  "corres_underlying rf_sr False nf (=) (invs') \<top> (kernelExit_if tc) (kernelExit_C_if tc)" apply (rule corres_underlying_nf_imp2) apply (simp add: kernelExit_if_def kernelExit_C_if_def) apply (rule corres_guard_imp) apply (rule_tac r'="\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv" in corres_split) apply (rule_tac P="\<top>" and P'="\<top>" in corres_inst) apply (clarsimp simp: getCurThread_def rf_sr_def cstate_relation_def Let_def) apply simp apply (rule getContext_corres) apply simp apply wp+ apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False nf (=) invs' (\<lambda>_. True) (kernelExit_if tc) (kernelExit_C_if tc) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False True (=) invs' (\<lambda>_. True) (kernelExit_if tc) (kernelExit_C_if tc) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr False True (=) invs' (\<lambda>_. True) (getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)) (do t <- gets (ksCurThread_' \<circ> globals);
gets (getContext_C t)
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr False True (=) ?Q2 ?Q'2 (getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)) (do t <- gets (ksCurThread_' \<circ> globals);
gets (getContext_C t)
od)
 2. \<And>s. invs' s \<Longrightarrow> ?Q2 s
 3. \<And>s. True \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. corres_underlying rf_sr False True (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv) ?P6 ?P'6 getCurThread (gets (ksCurThread_' \<circ> globals))
 2. \<And>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv \<Longrightarrow> corres_underlying rf_sr False True (=) (?R6 rv) (?R'6 rv') (threadGet (atcbContextGet \<circ> tcbArch) rv) (gets (getContext_C rv'))
 3. \<lbrace>?Q6\<rbrace> getCurThread \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> gets (ksCurThread_' \<circ> globals) \<lbrace>?R'6\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. True \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. corres_underlying rf_sr False True (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv) (\<lambda>_. True) (\<lambda>_. True) getCurThread (gets (ksCurThread_' \<circ> globals))
 2. \<And>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv \<Longrightarrow> corres_underlying rf_sr False True (=) (?R6 rv) (?R'6 rv') (threadGet (atcbContextGet \<circ> tcbArch) rv) (gets (getContext_C rv'))
 3. \<lbrace>?Q6\<rbrace> getCurThread \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> gets (ksCurThread_' \<circ> globals) \<lbrace>?R'6\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. rv' = tcb_ptr_to_ctcb_ptr rv \<Longrightarrow> corres_underlying rf_sr False True (=) (?R6 rv) (?R'6 rv') (threadGet (atcbContextGet \<circ> tcbArch) rv) (gets (getContext_C rv'))
 2. \<lbrace>?Q6\<rbrace> getCurThread \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> gets (ksCurThread_' \<circ> globals) \<lbrace>?R'6\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv. corres_underlying rf_sr False True (=) (?R6 rv) (?R'6 (tcb_ptr_to_ctcb_ptr rv)) (threadGet (atcbContextGet \<circ> tcbArch) rv) (gets (getContext_C (tcb_ptr_to_ctcb_ptr rv)))
 2. \<lbrace>?Q6\<rbrace> getCurThread \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> gets (ksCurThread_' \<circ> globals) \<lbrace>?R'6\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>rv. tcb_ptr_to_ctcb_ptr rv = tcb_ptr_to_ctcb_ptr rv
 2. \<lbrace>?Q6\<rbrace> getCurThread \<lbrace>tcb_at'\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> gets (ksCurThread_' \<circ> globals) \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> getCurThread \<lbrace>tcb_at'\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> gets (ksCurThread_' \<circ> globals) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. tcb_at' (ksCurThread s) s)) s
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s proof (prove)
goal:
No subgoals!