theory DomainSepInv

lemma finalise_cap_domain_sep_inv_cap:
  "\<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace>
   finalise_cap cap b
   \<lbrace>\<lambda>rv s :: det_ext state. domain_sep_inv_cap irqs (fst rv)\<rbrace>" including no_pre apply (case_tac cap) apply (wp | simp add: o_def split del: if_split  split: cap.splits
                       | fastforce split: if_splits simp: domain_sep_inv_cap_def)+ apply (rule hoare_pre, wp, fastforce) apply (rule hoare_pre, simp, wp, fastforce simp: domain_sep_inv_cap_def) apply (wpc | wp arch_finalise_cap_rv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs (IRQHandlerCap x10)\<rbrace> if b then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 2. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 3. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace>
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>s. domain_sep_inv_cap irqs cap\<rbrace> finalise_cap cap b \<lbrace>\<lambda>rv s. domain_sep_inv_cap irqs (fst rv)\<rbrace> proof (prove)
goal:
No subgoals!