theory Tcb_DR

lemma invoke_tcb_corres_bind:
  "\<lbrakk> t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr);
     t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs)
  (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def) apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_bind_notification corres_return_trivial]) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = translate_tcb_invocation t'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.bind_notification obj_id' ntfnptr) (do y <- Tcb_A.bind_notification obj_id' ntfnptr;
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.bind_notification obj_id' ntfnptr >>= return) (do y <- Tcb_A.bind_notification obj_id' ntfnptr;
return []
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr)\<rbrakk> \<Longrightarrow> dcorres dc ?Q3 ?Q'3 (Tcb_D.bind_notification obj_id' ntfnptr >>= return) (do y <- Tcb_A.bind_notification obj_id' ntfnptr;
return []
od)
 2. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr); True\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr); (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'3 s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr)\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> Tcb_D.bind_notification obj_id' ntfnptr \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> Tcb_A.bind_notification obj_id' ntfnptr \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 4. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' (Some ntfnptr); t = cdl_tcb_invocation.NotificationControl obj_id' (Some ntfnptr); (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_etcbs and not_idle_thread obj_id' and ?Q'7) s proof (prove)
goal:
No subgoals!