theory KHeap_DP

lemma derive_cap_rv:
"\<lbrace>\<lambda>s. case cap of FrameCap dev p r sz b x \<Rightarrow> False | otherwise \<Rightarrow> P s\<rbrace>
     derive_cap slot cap
 \<lbrace>\<lambda>rv s. P s \<and> ( rv = cap \<or> rv = NullCap )\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>" apply (clarsimp simp: derive_cap_def returnOk_def split: cdl_cap.splits,safe) apply (wp return_rv whenE_wp | clarsimp simp: ensure_no_children_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case cap of FrameCap dev p r sz b x \<Rightarrow> False | _ \<Rightarrow> P s\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. P s \<and> (rv = cap \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (26 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr NullCap) \<lbrace>\<lambda>rv s. P s \<and> rv = NullCap\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x21 x22 x23. cap = UntypedCap x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> doE y <- ensure_no_children slot;
return (Inr (UntypedCap x21 x22 x23))
odE \<lbrace>\<lambda>rv s. P s \<and> (rv = UntypedCap x21 x22 x23 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr (EndpointCap x31 x32 x33)) \<lbrace>\<lambda>rv s. P s \<and> (rv = EndpointCap x31 x32 x33 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr (NotificationCap x41 x42 x43)) \<lbrace>\<lambda>rv s. P s \<and> (rv = NotificationCap x41 x42 x43 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>x51 x52. cap = ReplyCap x51 x52 \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr NullCap) \<lbrace>\<lambda>rv s. P s \<and> (rv = ReplyCap x51 x52 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>x6. cap = MasterReplyCap x6 \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr NullCap) \<lbrace>\<lambda>rv s. P s \<and> (rv = MasterReplyCap x6 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>x71 x72 x73 x74. cap = CNodeCap x71 x72 x73 x74 \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr (CNodeCap x71 x72 x73 x74)) \<lbrace>\<lambda>rv s. P s \<and> (rv = CNodeCap x71 x72 x73 x74 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>x8. cap = TcbCap x8 \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr (TcbCap x8)) \<lbrace>\<lambda>rv s. P s \<and> (rv = TcbCap x8 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. cap = DomainCap \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr DomainCap) \<lbrace>\<lambda>rv s. P s \<and> (rv = DomainCap \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 10. \<And>x101 x102 x103 x104 x105 x106. cap = PendingSyncSendCap x101 x102 x103 x104 x105 x106 \<Longrightarrow> \<lbrace>P\<rbrace> return (Inr (PendingSyncSendCap x101 x102 x103 x104 x105 x106)) \<lbrace>\<lambda>rv s. P s \<and> (rv = PendingSyncSendCap x101 x102 x103 x104 x105 x106 \<or> rv = NullCap)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
A total of 26 subgoals... proof (prove)
goal:
No subgoals!