theory Tcb_R

lemma bindNotification_corres:
  "corres dc
         (invs and tcb_at t and ntfn_at a) (invs' and tcb_at' t and ntfn_at' a)
         (bind_notification t a) (bindNotification t a)" apply (simp add: bind_notification_def bindNotification_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getNotification_corres]) apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) apply (rule setBoundNotification_corres) apply (wp)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and tcb_at t and ntfn_at a) (invs' and tcb_at' t and ntfn_at' a) (bind_notification t a) (bindNotification t a) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and tcb_at t and ntfn_at a) (invs' and tcb_at' t and ntfn_at' a) (do ntfn <- get_notification a;
y <- set_notification a (ntfn_set_bound_tcb ntfn (Some t));
set_bound_notification t (Some a)
od) (do ntfn <- getNotification a;
y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. Some t) ntfn);
setBoundNotification (Some a) t
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do ntfn <- get_notification a;
y <- set_notification a (ntfn_set_bound_tcb ntfn (Some t));
set_bound_notification t (Some a)
od) (do ntfn <- getNotification a;
y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. Some t) ntfn);
setBoundNotification (Some a) t
od)
 2. \<And>s. (invs and tcb_at t and ntfn_at a) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and tcb_at' t and ntfn_at' a) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> corres dc (?R4 ntfn) (?R'4 ntfna) (do y <- set_notification a (ntfn_set_bound_tcb ntfn (Some t));
set_bound_notification t (Some a)
od) (do y <- setNotification a (ntfnBoundTCB_update (\<lambda>_. Some t) ntfna);
setBoundNotification (Some a) t
od)
 2. \<lbrace>?Q4\<rbrace> get_notification a \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getNotification a \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and tcb_at t and ntfn_at a) s \<Longrightarrow> (ntfn_at a and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t and ntfn_at' a) s \<Longrightarrow> (ntfn_at' a and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> ntfn_relation (ntfn_set_bound_tcb ntfn (Some t)) (ntfnBoundTCB_update (\<lambda>_. Some t) ntfna)
 2. \<And>ntfn ntfna rv y. \<lbrakk>ntfn_relation ntfn ntfna; dc rv y\<rbrakk> \<Longrightarrow> corres dc (?R9 ntfn ntfna rv) (?R'9 ntfn ntfna y) (set_bound_notification t (Some a)) (setBoundNotification (Some a) t)
 3. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q12 ntfn\<rbrace> set_notification a (ntfn_set_bound_tcb ntfn (Some t)) \<lbrace>?R9 ntfn ntfna\<rbrace>
 4. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q'14 ntfna\<rbrace> setNotification a (ntfnBoundTCB_update (\<lambda>_. Some t) ntfna) \<lbrace>?R'9 ntfn ntfna\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_notification a \<lbrace>\<lambda>ntfn. ntfn_at a and ?Q12 ntfn\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getNotification a \<lbrace>\<lambda>ntfna. ntfn_at' a and ?Q'14 ntfna\<rbrace>
 7. \<And>s. (invs and tcb_at t and ntfn_at a) s \<Longrightarrow> (ntfn_at a and ?Q4) s
 8. \<And>s. (invs' and tcb_at' t and ntfn_at' a) s \<Longrightarrow> (ntfn_at' a and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfn ntfna rv y. \<lbrakk>ntfn_relation ntfn ntfna; dc rv y\<rbrakk> \<Longrightarrow> corres dc (?R9 ntfn ntfna rv) (?R'9 ntfn ntfna y) (set_bound_notification t (Some a)) (setBoundNotification (Some a) t)
 2. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q12 ntfn\<rbrace> set_notification a (ntfn_set_bound_tcb ntfn (Some t)) \<lbrace>?R9 ntfn ntfna\<rbrace>
 3. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q'14 ntfna\<rbrace> setNotification a (ntfnBoundTCB_update (\<lambda>_. Some t) ntfna) \<lbrace>?R'9 ntfn ntfna\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_notification a \<lbrace>\<lambda>ntfn. ntfn_at a and ?Q12 ntfn\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getNotification a \<lbrace>\<lambda>ntfna. ntfn_at' a and ?Q'14 ntfna\<rbrace>
 6. \<And>s. (invs and tcb_at t and ntfn_at a) s \<Longrightarrow> (ntfn_at a and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t and ntfn_at' a) s \<Longrightarrow> (ntfn_at' a and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q12 ntfn\<rbrace> set_notification a (ntfn_set_bound_tcb ntfn (Some t)) \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
 2. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q'14 ntfna\<rbrace> setNotification a (ntfnBoundTCB_update (\<lambda>_. Some t) ntfna) \<lbrace>\<lambda>y. tcb_at' t\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_notification a \<lbrace>\<lambda>ntfn. ntfn_at a and ?Q12 ntfn\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getNotification a \<lbrace>\<lambda>ntfna. ntfn_at' a and ?Q'14 ntfna\<rbrace>
 5. \<And>s. (invs and tcb_at t and ntfn_at a) s \<Longrightarrow> (ntfn_at a and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t and ntfn_at' a) s \<Longrightarrow> (ntfn_at' a and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and tcb_at t and ntfn_at a) s \<Longrightarrow> (ntfn_at a and (ntfn_at a and tcb_at t)) s
 2. \<And>s. (invs' and tcb_at' t and ntfn_at' a) s \<Longrightarrow> (ntfn_at' a and (ntfn_at' a and tcb_at' t)) s proof (prove)
goal:
No subgoals!