theory Finalise_AC

lemma finalise_cap_auth':
  "\<lbrace>pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>" including no_pre apply (rule hoare_gen_asm) apply (cases cap, simp_all split del: if_split) apply (wp | simp add: comp_def hoare_post_taut[where P = \<top>] split del: if_split
                       | fastforce simp: aag_cap_auth_Zombie aag_cap_auth_CNode aag_cap_auth_Thread)+ apply (rule hoare_pre) apply (wp | simp)+ apply (wp arch_finalise_cap_auth') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. pas_cap_cur_auth aag cap \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>pas_cap_cur_auth aag (UntypedCap x21 x22 x23 x24); cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 3. \<And>x31 x32 x33. \<lbrakk>pas_cap_cur_auth aag (EndpointCap x31 x32 x33); cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when final (cancel_all_ipc x31)) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 4. \<And>x41 x42 x43. \<lbrakk>pas_cap_cur_auth aag (NotificationCap x41 x42 x43); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 5. \<And>x51 x52 x53. \<lbrakk>pas_cap_cur_auth aag (ReplyCap x51 x52 x53); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 6. \<And>x61 x62 x63. \<lbrakk>pas_cap_cur_auth aag (CNodeCap x61 x62 x63); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> return (if final then Zombie x61 (Some x62) (2 ^ x62) else NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 7. \<And>x7. \<lbrakk>pas_cap_cur_auth aag (ThreadCap x7); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> do y <- when final (unbind_notification x7);
y <- when final (suspend x7);
y <- when final (prepare_thread_delete x7);
return (if final then Zombie x7 None 5 else NullCap, NullCap)
od \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 8. \<lbrakk>pas_cap_cur_auth aag DomainCap; cap = DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 9. \<lbrakk>pas_cap_cur_auth aag IRQControlCap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 10. \<And>x10. \<lbrakk>pas_cap_cur_auth aag (IRQHandlerCap x10); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> if final then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>x10. \<lbrakk>pas_cap_cur_auth aag (IRQHandlerCap x10); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> if final then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 2. \<And>x111 x112 x113. \<lbrakk>pas_cap_cur_auth aag (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> do y <- assert final;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 3. \<And>x12. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x10. \<lbrakk>pas_cap_cur_auth aag (IRQHandlerCap x10); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>?Q68 x10\<rbrace> if final then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 2. \<And>x10 s. \<lbrakk>pas_cap_cur_auth aag (IRQHandlerCap x10); cap = IRQHandlerCap x10; pas_refined aag s\<rbrakk> \<Longrightarrow> ?Q68 x10 s
 3. \<And>x111 x112 x113. \<lbrakk>pas_cap_cur_auth aag (Zombie x111 x112 x113); cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> do y <- assert final;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace>
 4. \<And>x12. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>pas_cap_cur_auth aag (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>rv _. pas_cap_cur_auth aag (fst rv)\<rbrace> proof (prove)
goal:
No subgoals!