theory CSpace_AI

lemma derive_cap_inv[wp]:
  "\<lbrace>P\<rbrace> derive_cap slot c \<lbrace>\<lambda>rv. P\<rbrace>" apply (case_tac c, simp_all add: derive_cap_def ensure_no_children_def whenE_def is_zombie_def, wp+) apply clarsimp apply (wp arch_derive_cap_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> derive_cap slot c \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>c = UntypedCap x21 x22 x23 x24; P s\<rbrakk> \<Longrightarrow> ((\<exists>a b. cdt s (a, b) = Some slot) \<longrightarrow> P s \<and> True) \<and> ((\<nexists>a b. cdt s (a, b) = Some slot) \<longrightarrow> P s)
 2. \<And>x31 x32 x33. c = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (EndpointCap x31 x32 x33) \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (NotificationCap x41 x42 x43) \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (CNodeCap x61 x62 x63) \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>x7. c = ThreadCap x7 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (ThreadCap x7) \<lbrace>\<lambda>rv. P\<rbrace>
 7. c = DomainCap \<Longrightarrow> \<lbrace>P\<rbrace> returnOk DomainCap \<lbrace>\<lambda>rv. P\<rbrace>
 8. c = IRQControlCap \<Longrightarrow> \<lbrace>P\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv. P\<rbrace>
 9. \<And>x10. c = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (IRQHandlerCap x10) \<lbrace>\<lambda>rv. P\<rbrace>
 10. \<And>x111 x112 x113. c = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv. P\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x31 x32 x33. c = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (EndpointCap x31 x32 x33) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (NotificationCap x41 x42 x43) \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (CNodeCap x61 x62 x63) \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>x7. c = ThreadCap x7 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (ThreadCap x7) \<lbrace>\<lambda>rv. P\<rbrace>
 6. c = DomainCap \<Longrightarrow> \<lbrace>P\<rbrace> returnOk DomainCap \<lbrace>\<lambda>rv. P\<rbrace>
 7. c = IRQControlCap \<Longrightarrow> \<lbrace>P\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv. P\<rbrace>
 8. \<And>x10. c = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk (IRQHandlerCap x10) \<lbrace>\<lambda>rv. P\<rbrace>
 9. \<And>x111 x112 x113. c = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>P\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv. P\<rbrace>
 10. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>P\<rbrace> arch_derive_cap x12 \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!