theory TcbAcc_R

lemma setObject_update_TCB_corres:
  "\<lbrakk> tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu';
     \<forall>(getF, v) \<in> ran tcb_cap_cases. getF tcbu = getF tcb;
     \<forall>(getF, v) \<in> ran tcb_cte_cases. getF tcbu' = getF tcb';
     r () (); exst_same tcb' tcbu'\<rbrakk>
   \<Longrightarrow> corres r (\<lambda>s. get_tcb add s = Some tcb)
               (\<lambda>s'. (tcb', s') \<in> fst (getObject add s'))
               (set_object add (TCB tcbu)) (setObject add tcbu')" apply (rule corres_guard_imp) apply (erule (3) setObject_update_TCB_corres', force) apply fastforce apply (clarsimp simp: getObject_def in_monad split_def obj_at'_def
                        loadObject_default_def projectKOs objBits_simps'
                        in_magnitude_check) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF tcbu = getF tcb; \<forall>(getF, v)\<in>ran tcb_cte_cases. getF tcbu' = getF tcb'; r () (); exst_same tcb' tcbu'\<rbrakk> \<Longrightarrow> corres r (\<lambda>s. get_tcb add s = Some tcb) (\<lambda>s'. (tcb', s') \<in> fst (getObject add s')) (set_object add (TCB tcbu)) (setObject add tcbu') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF tcbu = getF tcb; \<forall>(getF, v)\<in>ran tcb_cte_cases. getF tcbu' = getF tcb'; r () (); exst_same tcb' tcbu'\<rbrakk> \<Longrightarrow> corres r ?Q ?Q' (set_object add (TCB tcbu)) (setObject add tcbu')
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF tcbu = getF tcb; \<forall>(getF, v)\<in>ran tcb_cte_cases. getF tcbu' = getF tcb'; r () (); exst_same tcb' tcbu'; get_tcb add s = Some tcb\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF tcbu = getF tcb; \<forall>(getF, v)\<in>ran tcb_cte_cases. getF tcbu' = getF tcb'; r () (); exst_same tcb' tcbu'; (tcb', s) \<in> fst (getObject add s)\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF tcbu = getF tcb; \<forall>(getF, v)\<in>ran tcb_cte_cases. getF tcbu' = getF tcb'; r () (); exst_same tcb' tcbu'; get_tcb add s = Some tcb\<rbrakk> \<Longrightarrow> ko_at (TCB tcb) add s
 2. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF tcbu = getF tcb; \<forall>(getF, v)\<in>ran tcb_cte_cases. getF tcbu' = getF tcb'; r () (); exst_same tcb' tcbu'; (tcb', s) \<in> fst (getObject add s)\<rbrakk> \<Longrightarrow> ko_at' tcb' add s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF tcbu = getF tcb; \<forall>(getF, v)\<in>ran tcb_cte_cases. getF tcbu' = getF tcb'; r () (); exst_same tcb' tcbu'; (tcb', s) \<in> fst (getObject add s)\<rbrakk> \<Longrightarrow> ko_at' tcb' add s proof (prove)
goal:
No subgoals!