theory Refine_C

lemma getContext_corres:
  "t' = tcb_ptr_to_ctcb_ptr t \<Longrightarrow>
  corres_underlying rf_sr False True (=) (tcb_at' t) \<top>
                    (threadGet (atcbContextGet o tcbArch) t) (gets (getContext_C t'))" apply (clarsimp simp: corres_underlying_def simpler_gets_def) apply (drule obj_at_ko_at') apply clarsimp apply (frule threadGet_eq) apply (rule bexI) prefer 2 apply assumption apply clarsimp apply (clarsimp simp: getContext_C_def) apply (drule cmap_relation_ko_atD [rotated]) apply fastforce apply (clarsimp simp: typ_heap_simps ctcb_relation_def carch_tcb_relation_def from_user_context_C) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t' = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> corres_underlying rf_sr False True (=) (tcb_at' t) (\<lambda>_. True) (threadGet (atcbContextGet \<circ> tcbArch) t) (gets (getContext_C t')) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; tcb_at' t a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet (atcbContextGet \<circ> tcbArch) t a). case x of (r, ta) \<Rightarrow> (ta, b) \<in> rf_sr \<and> r = getContext_C (tcb_ptr_to_ctcb_ptr t) b proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; \<exists>ko. ko_at' ko t a \<and> True\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet (atcbContextGet \<circ> tcbArch) t a). case x of (r, ta) \<Rightarrow> (ta, b) \<in> rf_sr \<and> r = getContext_C (tcb_ptr_to_ctcb_ptr t) b proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet (atcbContextGet \<circ> tcbArch) t a). case x of (r, ta) \<Rightarrow> (ta, b) \<in> rf_sr \<and> r = getContext_C (tcb_ptr_to_ctcb_ptr t) b proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; (?f30 a b ko ko, a) \<in> fst (threadGet (?f30 a b ko) t a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (threadGet (atcbContextGet \<circ> tcbArch) t a). case x of (r, ta) \<Rightarrow> (ta, b) \<in> rf_sr \<and> r = getContext_C (tcb_ptr_to_ctcb_ptr t) b proof (prove)
goal (2 subgoals):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; (?f30 a b ko ko, a) \<in> fst (threadGet (?f30 a b ko) t a)\<rbrakk> \<Longrightarrow> case ?x32 a b ko of (r, ta) \<Rightarrow> (ta, b) \<in> rf_sr \<and> r = getContext_C (tcb_ptr_to_ctcb_ptr t) b
 2. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; (?f30 a b ko ko, a) \<in> fst (threadGet (?f30 a b ko) t a)\<rbrakk> \<Longrightarrow> ?x32 a b ko \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a) proof (prove)
goal (2 subgoals):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; (?f30 a b ko ko, a) \<in> fst (threadGet (?f30 a b ko) t a)\<rbrakk> \<Longrightarrow> ?x32 a b ko \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a)
 2. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; (?f30 a b ko ko, a) \<in> fst (threadGet (?f30 a b ko) t a)\<rbrakk> \<Longrightarrow> case ?x32 a b ko of (r, ta) \<Rightarrow> (ta, b) \<in> rf_sr \<and> r = getContext_C (tcb_ptr_to_ctcb_ptr t) b proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; ((atcbContextGet \<circ> tcbArch) ko, a) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a)\<rbrakk> \<Longrightarrow> case ((atcbContextGet \<circ> tcbArch) ko, a) of (r, ta) \<Rightarrow> (ta, b) \<in> rf_sr \<and> r = getContext_C (tcb_ptr_to_ctcb_ptr t) b proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; (atcbContextGet (tcbArch ko), a) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a)\<rbrakk> \<Longrightarrow> atcbContextGet (tcbArch ko) = getContext_C (tcb_ptr_to_ctcb_ptr t) b proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; ko_at' ko t a; (atcbContextGet (tcbArch ko), a) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a)\<rbrakk> \<Longrightarrow> atcbContextGet (tcbArch ko) = from_user_context_C (tcbContext_C (the (cslift b (PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C'']))))) proof (prove)
goal (2 subgoals):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; (atcbContextGet (tcbArch ko), a) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a)\<rbrakk> \<Longrightarrow> cmap_relation (map_to_tcbs (ksPSpace a)) (cslift (?s'35 a b ko)) (?f35 a b ko) (?rel35 a b ko)
 2. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; (atcbContextGet (tcbArch ko), a) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a); \<exists>ko'. cslift (?s'35 a b ko) (?f35 a b ko t) = Some ko' \<and> ?rel35 a b ko ko ko'\<rbrakk> \<Longrightarrow> atcbContextGet (tcbArch ko) = from_user_context_C (tcbContext_C (the (cslift b (PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C'']))))) proof (prove)
goal (1 subgoal):
 1. \<And>a b ko. \<lbrakk>t' = tcb_ptr_to_ctcb_ptr t; (a, b) \<in> rf_sr; (atcbContextGet (tcbArch ko), a) \<in> fst (threadGet (atcbContextGet \<circ> tcbArch) t a); \<exists>ko'. cslift b (tcb_ptr_to_ctcb_ptr t) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> atcbContextGet (tcbArch ko) = from_user_context_C (tcbContext_C (the (cslift b (PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbArch_C'']))))) proof (prove)
goal:
No subgoals!