theory Ipc_AI

lemma (in Ipc_AI) derive_cap_objrefs_iszombie:
  "\<And>cap P slot.
    \<lbrace>\<lambda>s::'state_ext state. \<not> is_zombie cap \<longrightarrow> P (obj_refs cap) False s\<rbrace>
      derive_cap slot cap
    \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> P (obj_refs rv) (is_zombie rv) s\<rbrace>,-" apply (case_tac cap, simp_all add: derive_cap_def is_zombie_def) apply ((wpsimp wp: arch_derive_cap_objrefs_iszombie[simplified is_zombie_def] | rule validE_R_validE)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap P slot. \<lbrace>\<lambda>s. \<not> is_zombie cap \<longrightarrow> P (obj_refs cap) False s\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (is_zombie rv) s\<rbrace>, - proof (prove)
goal (12 subgoals):
 1. \<And>cap P. cap = NullCap \<Longrightarrow> \<lbrace>P {} False\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 2. \<And>cap P slot x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>P {} False\<rbrace> doE y <- ensure_no_children slot;
returnOk (UntypedCap x21 x22 x23 x24)
odE \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 3. \<And>cap P x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>P {x31} False\<rbrace> returnOk (EndpointCap x31 x32 x33) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 4. \<And>cap P x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>P {x41} False\<rbrace> returnOk (NotificationCap x41 x42 x43) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 5. \<And>cap P x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>P {} False\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 6. \<And>cap P x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>P {x61} False\<rbrace> returnOk (CNodeCap x61 x62 x63) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 7. \<And>cap P x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>P {x7} False\<rbrace> returnOk (ThreadCap x7) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 8. \<And>cap P. cap = DomainCap \<Longrightarrow> \<lbrace>P {} False\<rbrace> returnOk DomainCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 9. \<And>cap P. cap = IRQControlCap \<Longrightarrow> \<lbrace>P {} False\<rbrace> returnOk NullCap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
 10. \<And>cap P x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>P {} False\<rbrace> returnOk (IRQHandlerCap x10) \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (case rv of Zombie x xa xb \<Rightarrow> True | _ \<Rightarrow> False) s\<rbrace>, -
A total of 12 subgoals... proof (prove)
goal:
No subgoals!