theory Finalise_R

lemma unbindMaybeNotification_corres:
  "corres dc
      (invs and ntfn_at ntfnptr) (invs' and ntfn_at' ntfnptr)
      (unbind_maybe_notification ntfnptr)
      (unbindMaybeNotification ntfnptr)" apply (simp add: unbind_maybe_notification_def unbindMaybeNotification_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getNotification_corres]) apply (rule corres_option_split) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) apply (rule corres_return_trivial) apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) apply (rule setBoundNotification_corres) apply (wp get_simple_ko_wp getNotification_wp)+ apply (clarsimp elim!: obj_at_valid_objsE
                   dest!: bound_tcb_at_state_refs_ofD invs_valid_objs
                    simp: valid_obj_def is_tcb tcb_ntfn_is_bound_def
                          valid_tcb_def valid_bound_ntfn_def valid_ntfn_def
                   split: option.splits) apply (clarsimp dest!: obj_at_valid_objs' bound_tcb_at_state_refs_ofD' invs_valid_objs'
                   simp: projectKOs valid_obj'_def valid_tcb'_def valid_bound_ntfn'_def
                         tcb_ntfn_is_bound'_def valid_ntfn'_def
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and ntfn_at ntfnptr) (invs' and ntfn_at' ntfnptr) (unbind_maybe_notification ntfnptr) (unbindMaybeNotification ntfnptr) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and ntfn_at ntfnptr) (invs' and ntfn_at' ntfnptr) (do ntfn <- get_notification ntfnptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od
od) (do ntfn <- getNotification ntfnptr;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q4 ?Q'4 (do ntfn <- get_notification ntfnptr;
case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od
od) (do ntfn <- getNotification ntfnptr;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od)
 2. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> ?Q4 s
 3. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> corres dc (?R8 ntfn) (?R'8 ntfna) (case ntfn_bound_tcb ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od) (case ntfnBoundTCB ntfna of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfna);
setBoundNotification None t
od)
 2. \<lbrace>?Q8\<rbrace> get_notification ntfnptr \<lbrace>?R8\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> getNotification ntfnptr \<lbrace>?R'8\<rbrace>
 4. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q8) s
 5. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> ntfn_bound_tcb ntfn = ntfnBoundTCB ntfna
 2. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> corres dc (?P14 ntfn) (?P'17 ntfna) (return ()) (return ())
 3. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfn x) (?Q'18 ntfna x) (do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification x None
od) (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfna);
setBoundNotification None x
od)
 4. \<lbrace>?Q8\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn. case ntfn_bound_tcb ntfn of None \<Rightarrow> ?P14 ntfn | Some x \<Rightarrow> ?Q15 ntfn x\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfna. case ntfnBoundTCB ntfna of None \<Rightarrow> ?P'17 ntfna | Some x \<Rightarrow> ?Q'18 ntfna x\<rbrace>
 6. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q8) s
 7. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> corres dc (?P14 ntfn) (?P'17 ntfna) (return ()) (return ())
 2. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfn x) (?Q'18 ntfna x) (do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification x None
od) (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfna);
setBoundNotification None x
od)
 3. \<lbrace>?Q8\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn. case ntfn_bound_tcb ntfn of None \<Rightarrow> ?P14 ntfn | Some x \<Rightarrow> ?Q15 ntfn x\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfna. case ntfnBoundTCB ntfna of None \<Rightarrow> ?P'17 ntfna | Some x \<Rightarrow> ?Q'18 ntfna x\<rbrace>
 5. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q8) s
 6. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> corres dc (?Q15 ntfn x) (?Q'18 ntfna x) (do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification x None
od) (do y <- setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfna);
setBoundNotification None x
od)
 2. \<lbrace>?Q8\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn. case ntfn_bound_tcb ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ?Q15 ntfn x\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfna. case ntfnBoundTCB ntfna of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ?Q'18 ntfna x\<rbrace>
 4. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q8) s
 5. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_bound_tcb ntfn None) (ntfnBoundTCB_update (\<lambda>_. None) ntfna)
 2. \<And>ntfn ntfna x rv rv'. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R24 ntfn ntfna x rv) (?R'24 ntfn ntfna x rv') (set_bound_notification x None) (setBoundNotification None x)
 3. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q27 ntfn x\<rbrace> set_notification ntfnptr (ntfn_set_bound_tcb ntfn None) \<lbrace>?R24 ntfn ntfna x\<rbrace>
 4. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 ntfna x\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfna) \<lbrace>?R'24 ntfn ntfna x\<rbrace>
 5. \<lbrace>?Q8\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn. case ntfn_bound_tcb ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at ntfnptr and ?Q27 ntfn x\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfna. case ntfnBoundTCB ntfna of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' ntfnptr and ?Q'29 ntfna x\<rbrace>
 7. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q8) s
 8. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfn ntfna x rv rv'. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R24 ntfn ntfna x rv) (?R'24 ntfn ntfna x rv') (set_bound_notification x None) (setBoundNotification None x)
 2. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q27 ntfn x\<rbrace> set_notification ntfnptr (ntfn_set_bound_tcb ntfn None) \<lbrace>?R24 ntfn ntfna x\<rbrace>
 3. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 ntfna x\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfna) \<lbrace>?R'24 ntfn ntfna x\<rbrace>
 4. \<lbrace>?Q8\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn. case ntfn_bound_tcb ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at ntfnptr and ?Q27 ntfn x\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfna. case ntfnBoundTCB ntfna of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' ntfnptr and ?Q'29 ntfna x\<rbrace>
 6. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q8) s
 7. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q27 ntfn x\<rbrace> set_notification ntfnptr (ntfn_set_bound_tcb ntfn None) \<lbrace>\<lambda>rv. tcb_at x\<rbrace>
 2. \<And>ntfn ntfna x. \<lbrakk>ntfn_relation ntfn ntfna; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 ntfna x\<rbrace> setNotification ntfnptr (ntfnBoundTCB_update (\<lambda>_. None) ntfna) \<lbrace>\<lambda>rv'. tcb_at' x\<rbrace>
 3. \<lbrace>?Q8\<rbrace> get_notification ntfnptr \<lbrace>\<lambda>ntfn. case ntfn_bound_tcb ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at ntfnptr and ?Q27 ntfn x\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> getNotification ntfnptr \<lbrace>\<lambda>ntfna. case ntfnBoundTCB ntfna of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' ntfnptr and ?Q'29 ntfna x\<rbrace>
 5. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and ?Q8) s
 6. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and ntfn_at ntfnptr) s \<Longrightarrow> (ntfn_at ntfnptr and (\<lambda>s. \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (case ntfn_bound_tcb ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at ntfnptr and tcb_at x) s)) s
 2. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and (\<lambda>s. \<forall>ntfn. ko_at' ntfn ntfnptr s \<longrightarrow> (case ntfnBoundTCB ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' ntfnptr and tcb_at' x) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ntfn_at' ntfnptr) s \<Longrightarrow> (ntfn_at' ntfnptr and (\<lambda>s. \<forall>ntfn. ko_at' ntfn ntfnptr s \<longrightarrow> (case ntfnBoundTCB ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' ntfnptr and tcb_at' x) s)) s proof (prove)
goal:
No subgoals!