theory Tcb_AC

lemma invoke_tcb_unbind_notification_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and simple_sched_action and einvs
                       and tcb_inv_wf (NotificationControl t None)
                       and K (authorised_tcb_inv aag (NotificationControl t None))\<rbrace>
   invoke_tcb (tcb_invocation.NotificationControl t None)
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (clarsimp) apply (wp unbind_notification_respects) apply (clarsimp simp: authorised_tcb_inv_def tcb_at_def pred_tcb_def2) apply (clarsimp split: option.split) apply (frule(1) bound_tcb_at_implies_reset[unfolded pred_tcb_def2, OF _ exI, OF _ conjI]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and simple_sched_action and einvs and tcb_inv_wf (NotificationControl t None) and K (authorised_tcb_inv aag (NotificationControl t None))\<rbrace> invoke_tcb (NotificationControl t None) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and simple_sched_action and einvs and (tcb_at t and ex_nonz_cap_to t) and (\<lambda>y. authorised_tcb_inv aag (NotificationControl t None))\<rbrace> liftE (do y <- unbind_notification t;
return []
od) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and pas_refined aag and simple_sched_action and einvs and (tcb_at t and ex_nonz_cap_to t) and (\<lambda>y. authorised_tcb_inv aag (NotificationControl t None))) s \<Longrightarrow> (integrity aag X st and pas_refined aag and bound_tcb_at (\<lambda>a. case a of None \<Rightarrow> True | Some ntfn \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag) t) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>integrity aag X st s; pas_refined aag s; simple_sched_action s; invs s; valid_list s; valid_sched s; get_tcb t s = Some tcb; ex_nonz_cap_to t s; is_subject aag t\<rbrakk> \<Longrightarrow> case tcb_bound_notification tcb of None \<Rightarrow> True | Some ntfn \<Rightarrow> (pasSubject aag, Reset, pasObjectAbs aag ntfn) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x2. \<lbrakk>integrity aag X st s; pas_refined aag s; simple_sched_action s; invs s; valid_list s; valid_sched s; get_tcb t s = Some tcb; ex_nonz_cap_to t s; is_subject aag t; tcb_bound_notification tcb = Some x2\<rbrakk> \<Longrightarrow> (pasSubject aag, Reset, pasObjectAbs aag x2) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s tcb x2. \<lbrakk>integrity aag X st s; pas_refined aag s; simple_sched_action s; invs s; valid_list s; valid_sched s; get_tcb t s = Some tcb; ex_nonz_cap_to t s; is_subject aag t; tcb_bound_notification tcb = Some x2\<rbrakk> \<Longrightarrow> Some (?x26 s tcb x2) = itcb_bound_notification (tcb_to_itcb tcb)
 2. \<And>s tcb x2. \<lbrakk>integrity aag X st s; pas_refined aag s; simple_sched_action s; invs s; valid_list s; valid_sched s; get_tcb t s = Some tcb; ex_nonz_cap_to t s; is_subject aag t; tcb_bound_notification tcb = Some x2; (pasObjectAbs aag t, Reset, pasObjectAbs aag (?x26 s tcb x2)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Reset, pasObjectAbs aag x2) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s tcb x2. \<lbrakk>integrity aag X st s; pas_refined aag s; simple_sched_action s; invs s; valid_list s; valid_sched s; get_tcb t s = Some tcb; ex_nonz_cap_to t s; is_subject aag t; tcb_bound_notification tcb = Some x2; (pasObjectAbs aag t, Reset, pasObjectAbs aag x2) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Reset, pasObjectAbs aag x2) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!