theory Tcb_AI

lemma derive_is_arch[wp]:
  "\<lbrace>\<lambda>s. is_arch_cap c\<rbrace> derive_cap slot c \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> is_arch_cap rv\<rbrace>,-" apply (simp add: derive_cap_def cong: cap.case_cong) apply (rule hoare_pre) apply (wp arch_derive_is_arch | wpc | simp only: o_def is_arch_cap_def cap.simps)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_arch_cap c\<rbrace> derive_cap slot c \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> is_arch_cap rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_arch_cap c\<rbrace> case c of UntypedCap dev ptr sz f \<Rightarrow> doE y <- ensure_no_children slot;
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. rv \<noteq> NullCap \<longrightarrow> is_arch_cap rv\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'14\<rbrace> case c of UntypedCap dev ptr sz f \<Rightarrow> doE y <- ensure_no_children slot;
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. rv \<noteq> NullCap \<longrightarrow> is_arch_cap rv\<rbrace>, -
 2. \<And>s. is_arch_cap c \<Longrightarrow> ?P'14 s proof (prove)
goal (1 subgoal):
 1. \<And>s. case c of ArchObjectCap x \<Rightarrow> True | _ \<Rightarrow> False \<Longrightarrow> (c = NullCap \<longrightarrow> NullCap \<noteq> NullCap \<longrightarrow> False) \<and> (\<forall>x xa xb xc. c = UntypedCap x xa xb xc \<longrightarrow> True \<and> (\<not> False \<longrightarrow> False)) \<and> (\<forall>x xa xb. c = EndpointCap x xa xb \<longrightarrow> \<not> False \<longrightarrow> False) \<and> (\<forall>x xa xb. c = NotificationCap x xa xb \<longrightarrow> \<not> False \<longrightarrow> False) \<and> (\<forall>x xa xb. c = ReplyCap x xa xb \<longrightarrow> NullCap \<noteq> NullCap \<longrightarrow> False) \<and> (\<forall>x xa xb. c = CNodeCap x xa xb \<longrightarrow> \<not> False \<longrightarrow> False) \<and> (\<forall>x. c = ThreadCap x \<longrightarrow> \<not> False \<longrightarrow> False) \<and> (c = DomainCap \<longrightarrow> \<not> False \<longrightarrow> False) \<and> (c = IRQControlCap \<longrightarrow> NullCap \<noteq> NullCap \<longrightarrow> False) \<and> (\<forall>x. c = IRQHandlerCap x \<longrightarrow> \<not> False \<longrightarrow> False) \<and> (\<forall>x xa xb. c = Zombie x xa xb \<longrightarrow> NullCap \<noteq> NullCap \<longrightarrow> False) \<and> (\<forall>x. c = ArchObjectCap x \<longrightarrow> True) proof (prove)
goal:
No subgoals!