theory CNode_AC

lemma derive_cap_clas:
  "\<lbrace>\<lambda>s :: det_ext state. cap_links_asid_slot aag p b \<rbrace>
   derive_cap a b
   \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, -" apply (simp add: derive_cap_def  cong: cap.case_cong) apply (rule hoare_pre) apply (wp arch_derive_cap_clas | wpc)+ apply (auto simp: is_cap_simps cap_links_asid_slot_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_links_asid_slot aag p b\<rbrace> derive_cap a b \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_links_asid_slot aag p b\<rbrace> case b of UntypedCap dev ptr sz f \<Rightarrow> doE y <- ensure_no_children a;
returnOk (UntypedCap dev ptr sz f)
odE | EndpointCap word1 word2 set \<Rightarrow> returnOk (EndpointCap word1 word2 set) | NotificationCap word1 word2 set \<Rightarrow> returnOk (NotificationCap word1 word2 set) | CNodeCap word nat list \<Rightarrow> returnOk (CNodeCap word nat list) | ThreadCap word \<Rightarrow> returnOk (ThreadCap word) | DomainCap \<Rightarrow> returnOk DomainCap | IRQHandlerCap word \<Rightarrow> returnOk (IRQHandlerCap word) | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk NullCap \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'14\<rbrace> case b of UntypedCap dev ptr sz f \<Rightarrow> doE y <- ensure_no_children a;
returnOk (UntypedCap dev ptr sz f)
odE | EndpointCap word1 word2 set \<Rightarrow> returnOk (EndpointCap word1 word2 set) | NotificationCap word1 word2 set \<Rightarrow> returnOk (NotificationCap word1 word2 set) | CNodeCap word nat list \<Rightarrow> returnOk (CNodeCap word nat list) | ThreadCap word \<Rightarrow> returnOk (ThreadCap word) | DomainCap \<Rightarrow> returnOk DomainCap | IRQHandlerCap word \<Rightarrow> returnOk (IRQHandlerCap word) | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk NullCap \<lbrace>\<lambda>rv s. cap_links_asid_slot aag p rv\<rbrace>, -
 2. \<And>s. cap_links_asid_slot aag p b \<Longrightarrow> ?P'14 s proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_links_asid_slot aag p b \<Longrightarrow> (b = NullCap \<longrightarrow> cap_links_asid_slot aag p NullCap) \<and> (\<forall>x xa xb xc. b = UntypedCap x xa xb xc \<longrightarrow> True \<and> cap_links_asid_slot aag p (UntypedCap x xa xb xc)) \<and> (\<forall>x xa xb. b = EndpointCap x xa xb \<longrightarrow> cap_links_asid_slot aag p (EndpointCap x xa xb)) \<and> (\<forall>x xa xb. b = NotificationCap x xa xb \<longrightarrow> cap_links_asid_slot aag p (NotificationCap x xa xb)) \<and> (\<forall>x xa xb. b = ReplyCap x xa xb \<longrightarrow> cap_links_asid_slot aag p NullCap) \<and> (\<forall>x xa xb. b = CNodeCap x xa xb \<longrightarrow> cap_links_asid_slot aag p (CNodeCap x xa xb)) \<and> (\<forall>x. b = ThreadCap x \<longrightarrow> cap_links_asid_slot aag p (ThreadCap x)) \<and> (b = DomainCap \<longrightarrow> cap_links_asid_slot aag p DomainCap) \<and> (b = IRQControlCap \<longrightarrow> cap_links_asid_slot aag p NullCap) \<and> (\<forall>x. b = IRQHandlerCap x \<longrightarrow> cap_links_asid_slot aag p (IRQHandlerCap x)) \<and> (\<forall>x xa xb. b = Zombie x xa xb \<longrightarrow> cap_links_asid_slot aag p NullCap) \<and> (\<forall>x. b = ArchObjectCap x \<longrightarrow> cap_links_asid_slot aag p (ArchObjectCap x)) proof (prove)
goal:
No subgoals!