theory Tcb_DR

lemma invoke_tcb_corres_unbind:
  "\<lbrakk> t' = tcb_invocation.NotificationControl obj_id' None;
     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_unbind_notification corres_return_trivial]) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; 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' None; t = cdl_tcb_invocation.NotificationControl obj_id' None\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (PageTableUnmap_D.unbind_notification obj_id') (do y <- IpcCancel_A.unbind_notification obj_id';
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; t = cdl_tcb_invocation.NotificationControl obj_id' None\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (PageTableUnmap_D.unbind_notification obj_id' >>= return) (do y <- IpcCancel_A.unbind_notification obj_id';
return []
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; t = cdl_tcb_invocation.NotificationControl obj_id' None\<rbrakk> \<Longrightarrow> dcorres dc ?Q3 ?Q'3 (PageTableUnmap_D.unbind_notification obj_id' >>= return) (do y <- IpcCancel_A.unbind_notification obj_id';
return []
od)
 2. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; t = cdl_tcb_invocation.NotificationControl obj_id' None; True\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; t = cdl_tcb_invocation.NotificationControl obj_id' None; (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' None; t = cdl_tcb_invocation.NotificationControl obj_id' None\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> PageTableUnmap_D.unbind_notification obj_id' \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; t = cdl_tcb_invocation.NotificationControl obj_id' None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> IpcCancel_A.unbind_notification obj_id' \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; t = cdl_tcb_invocation.NotificationControl obj_id' None; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 4. \<And>s. \<lbrakk>t' = tcb_invocation.NotificationControl obj_id' None; t = cdl_tcb_invocation.NotificationControl obj_id' None; (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!