theory Finalise_R

lemma unbindNotification_corres:
  "corres dc
      (invs and tcb_at t)
      (invs' and tcb_at' t)
      (unbind_notification t)
      (unbindNotification t)" supply option.case_cong_weak[cong] apply (simp add: unbind_notification_def unbindNotification_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getBoundNotification_corres]) apply (rule corres_option_split) apply simp apply (rule corres_return_trivial) apply (rule corres_split[OF getNotification_corres]) apply clarsimp apply (rule corres_split[OF setNotification_corres]) apply (clarsimp simp: ntfn_relation_def split:Structures_A.ntfn.splits) apply (rule setBoundNotification_corres) apply (wp gbn_wp' gbn_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
                   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
                  split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and tcb_at t) (invs' and tcb_at' t) (unbind_notification t) (unbindNotification t) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and tcb_at t) (invs' and tcb_at' t) (unbind_notification t) (unbindNotification t) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and tcb_at t) (invs' and tcb_at' t) (do ntfnptr <- get_bound_notification t;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t
od
od) (do ntfnPtr <- getBoundNotification t;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
doUnbindNotification ntfnPtr' ntfn t
od
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do ntfnptr <- get_bound_notification t;
case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t
od
od) (do ntfnPtr <- getBoundNotification t;
case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
doUnbindNotification ntfnPtr' ntfn t
od
od)
 2. \<And>s. (invs and tcb_at t) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>ntfnptr ntfnPtr. ntfnptr = ntfnPtr \<Longrightarrow> corres dc (?R4 ntfnptr) (?R'4 ntfnPtr) (case ntfnptr of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
do_unbind_notification ntfnptr' ntfn t
od) (case ntfnPtr of None \<Rightarrow> return () | Some ntfnPtr' \<Rightarrow> do ntfn <- getNotification ntfnPtr';
doUnbindNotification ntfnPtr' ntfn t
od)
 2. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfnptr ntfnPtr. ntfnptr = ntfnPtr \<Longrightarrow> ntfnptr = ntfnPtr
 2. \<And>ntfnptr ntfnPtr. ntfnptr = ntfnPtr \<Longrightarrow> corres dc (?P10 ntfnptr) (?P'13 ntfnPtr) (return ()) (return ())
 3. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> corres dc (?Q11 ntfnptr x) (?Q'14 ntfnPtr x) (do ntfn <- get_notification x;
do_unbind_notification x ntfn t
od) (do ntfn <- getNotification x;
doUnbindNotification x ntfn t
od)
 4. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> ?P10 ntfnptr | Some x \<Rightarrow> ?Q11 ntfnptr x\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> ?P'13 ntfnPtr | Some x \<Rightarrow> ?Q'14 ntfnPtr x\<rbrace>
 6. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>ntfnptr ntfnPtr. ntfnptr = ntfnPtr \<Longrightarrow> corres dc (?P10 ntfnptr) (?P'13 ntfnPtr) (return ()) (return ())
 2. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> corres dc (?Q11 ntfnptr x) (?Q'14 ntfnPtr x) (do ntfn <- get_notification x;
do_unbind_notification x ntfn t
od) (do ntfn <- getNotification x;
doUnbindNotification x ntfn t
od)
 3. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> ?P10 ntfnptr | Some x \<Rightarrow> ?Q11 ntfnptr x\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> ?P'13 ntfnPtr | Some x \<Rightarrow> ?Q'14 ntfnPtr x\<rbrace>
 5. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> corres dc (?Q11 ntfnptr x) (?Q'14 ntfnPtr x) (do ntfn <- get_notification x;
do_unbind_notification x ntfn t
od) (do ntfn <- getNotification x;
doUnbindNotification x ntfn t
od)
 2. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ?Q11 ntfnptr x\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ?Q'14 ntfnPtr x\<rbrace>
 4. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>ntfnptr ntfnPtr x ntfn ntfna. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x; ntfn_relation ntfn ntfna\<rbrakk> \<Longrightarrow> corres dc (?R20 ntfnptr ntfnPtr x ntfn) (?R'20 ntfnptr ntfnPtr x ntfna) (do_unbind_notification x ntfn t) (doUnbindNotification x ntfna t)
 2. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 ntfnptr x\<rbrace> get_notification x \<lbrace>?R20 ntfnptr ntfnPtr x\<rbrace>
 3. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 ntfnPtr x\<rbrace> getNotification x \<lbrace>?R'20 ntfnptr ntfnPtr x\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at x and ?Q23 ntfnptr x\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' x and ?Q'25 ntfnPtr x\<rbrace>
 6. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> corres dc (?R20 (Some x) (Some x) x ntfn) (?R'20 (Some x) (Some x) x ntfna) (do y <- set_notification x (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od) (do y <- setNotification x (ntfnBoundTCB_update (\<lambda>_. None) ntfna);
setBoundNotification None t
od)
 2. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 ntfnptr x\<rbrace> get_notification x \<lbrace>?R20 ntfnptr ntfnPtr x\<rbrace>
 3. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 ntfnPtr x\<rbrace> getNotification x \<lbrace>?R'20 ntfnptr ntfnPtr x\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at x and ?Q23 ntfnptr x\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' x and ?Q'25 ntfnPtr x\<rbrace>
 6. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> ntfn_relation (ntfn_set_bound_tcb ntfn None) (ntfnBoundTCB_update (\<lambda>_. None) ntfna)
 2. \<And>x ntfn ntfna y ya. \<lbrakk>ntfn_relation ntfn ntfna; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R33 x ntfn ntfna y) (?R'33 x ntfn ntfna ya) (set_bound_notification t None) (setBoundNotification None t)
 3. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q39 (Some x) (Some x) x ntfn\<rbrace> set_notification x (ntfn_set_bound_tcb ntfn None) \<lbrace>?R33 x ntfn ntfna\<rbrace>
 4. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q'37 (Some x) (Some x) x ntfna\<rbrace> setNotification x (ntfnBoundTCB_update (\<lambda>_. None) ntfna) \<lbrace>?R'33 x ntfn ntfna\<rbrace>
 5. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 ntfnptr x\<rbrace> get_notification x \<lbrace>\<lambda>a. ntfn_at x and ?Q39 ntfnptr ntfnPtr x a\<rbrace>
 6. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 ntfnPtr x\<rbrace> getNotification x \<lbrace>\<lambda>a. ntfn_at' x and ?Q'37 ntfnptr ntfnPtr x a\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at x and ?Q23 ntfnptr x\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' x and ?Q'25 ntfnPtr x\<rbrace>
 9. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 10. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>x ntfn ntfna y ya. \<lbrakk>ntfn_relation ntfn ntfna; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R33 x ntfn ntfna y) (?R'33 x ntfn ntfna ya) (set_bound_notification t None) (setBoundNotification None t)
 2. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q39 (Some x) (Some x) x ntfn\<rbrace> set_notification x (ntfn_set_bound_tcb ntfn None) \<lbrace>?R33 x ntfn ntfna\<rbrace>
 3. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q'37 (Some x) (Some x) x ntfna\<rbrace> setNotification x (ntfnBoundTCB_update (\<lambda>_. None) ntfna) \<lbrace>?R'33 x ntfn ntfna\<rbrace>
 4. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 ntfnptr x\<rbrace> get_notification x \<lbrace>\<lambda>a. ntfn_at x and ?Q39 ntfnptr ntfnPtr x a\<rbrace>
 5. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 ntfnPtr x\<rbrace> getNotification x \<lbrace>\<lambda>a. ntfn_at' x and ?Q'37 ntfnptr ntfnPtr x a\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at x and ?Q23 ntfnptr x\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' x and ?Q'25 ntfnPtr x\<rbrace>
 8. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 9. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q39 (Some x) (Some x) x ntfn\<rbrace> set_notification x (ntfn_set_bound_tcb ntfn None) \<lbrace>\<lambda>y. tcb_at t\<rbrace>
 2. \<And>x ntfn ntfna. ntfn_relation ntfn ntfna \<Longrightarrow> \<lbrace>?Q'37 (Some x) (Some x) x ntfna\<rbrace> setNotification x (ntfnBoundTCB_update (\<lambda>_. None) ntfna) \<lbrace>\<lambda>ya. tcb_at' t\<rbrace>
 3. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 ntfnptr x\<rbrace> get_notification x \<lbrace>\<lambda>a. ntfn_at x and ?Q39 ntfnptr ntfnPtr x a\<rbrace>
 4. \<And>ntfnptr ntfnPtr x. \<lbrakk>ntfnptr = ntfnPtr; ntfnptr = Some x\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 ntfnPtr x\<rbrace> getNotification x \<lbrace>\<lambda>a. ntfn_at' x and ?Q'37 ntfnptr ntfnPtr x a\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfnptr. case ntfnptr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at x and ?Q23 ntfnptr x\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> getBoundNotification t \<lbrace>\<lambda>ntfnPtr. case ntfnPtr of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' x and ?Q'25 ntfnPtr x\<rbrace>
 7. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 8. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (tcb_at t and (\<lambda>s. \<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> (case ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at x and (ntfn_at x and tcb_at t)) s)) s
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) t s \<longrightarrow> (case ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' x and (ntfn_at' x and tcb_at' t)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) t s \<longrightarrow> (case ntfn of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> ntfn_at' x and (ntfn_at' x and tcb_at' t)) s)) s proof (prove)
goal:
No subgoals!