theory Access_AC

lemma tro_tcb_generic':
  "\<lbrakk> ko = Some (TCB tcb); ko' = Some (TCB tcb');
     tcb' = tcb \<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>;
     tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag;
     reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap';
     reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap' \<rbrakk>
     \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'" apply clarsimp apply (rule tro_trans_spec) apply (rule tro_tcb_empty_caller[OF refl refl refl];simp) apply (rule tro_trans_spec) apply (rule tro_tcb_empty_ctable[OF refl refl refl];simp) apply (rule tro_trans_spec) apply (rule tro_tcb_unbind'[OF refl refl refl];simp) apply (fastforce intro!: tro_orefl tcb.equality) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' ko ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) ?y1
 2. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' ?y1 (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_caller := cap'\<rparr>))) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_caller := cap'\<rparr>))) ?y13
 2. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' ?y13 (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) ?y25
 2. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' ?y25 (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB (tcb\<lparr>tcb_caller := cap', tcb_ctable := ccap', tcb_bound_notification := ntfn'\<rparr>))) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>))) proof (prove)
goal:
No subgoals!