theory ADT_IF_Refine

lemma kernel_exit_if_corres:
  "corres (=) (invs) (invs') (kernel_exit_if tc) (kernelExit_if tc)" apply (simp add: kernel_exit_if_def kernelExit_if_def) apply (rule corres_guard_imp) apply (rule corres_split[where r'="(=)"]) apply (rule getCurThread_corres) apply simp apply (rule threadGet_corres) apply (erule arch_tcb_context_get_atcbContextGet) apply wp+ apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) invs invs' (kernel_exit_if tc) (kernelExit_if tc) proof (prove)
goal (1 subgoal):
 1. corres (=) invs invs' (gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)) (getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)) (getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch))
 2. \<And>s. invs s \<Longrightarrow> ?Q s
 3. \<And>s. invs' s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres (=) ?P4 ?P'4 (gets cur_thread) getCurThread
 2. \<And>t' t'a. t' = t'a \<Longrightarrow> corres (=) (?R4 t') (?R'4 t'a) (thread_get (arch_tcb_context_get \<circ> tcb_arch) t') (threadGet (atcbContextGet \<circ> tcbArch) t'a)
 3. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>?R'4\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. invs' s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>t' t'a. t' = t'a \<Longrightarrow> corres (=) (?R4 t') (?R'4 t'a) (thread_get (arch_tcb_context_get \<circ> tcb_arch) t') (threadGet (atcbContextGet \<circ> tcbArch) t'a)
 2. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>?R'4\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>t'. corres (=) (?R4 t') (?R'4 t') (thread_get (arch_tcb_context_get \<circ> tcb_arch) t') (threadGet (atcbContextGet \<circ> tcbArch) t')
 2. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>?R'4\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>t' tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> (arch_tcb_context_get \<circ> tcb_arch) tcb = (atcbContextGet \<circ> tcbArch) tcb'
 2. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>tcb_at\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>tcb_at'\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> gets cur_thread \<lbrace>tcb_at\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getCurThread \<lbrace>tcb_at'\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. tcb_at (cur_thread s) s)) s
 2. \<And>s. invs' s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. tcb_at' (ksCurThread s) s)) s proof (prove)
goal:
No subgoals!