theory Tcb_AI

lemma derived_cap_cnode_valid:
  "\<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> valid_cap c s\<rbrace>
  derive_cap sl c
  \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> valid_cap rv s\<rbrace>,-" apply (cases c) apply (simp_all add: derive_cap_def validE_R_def return_def
                               validE_def valid_def returnOk_def) apply (clarsimp simp: in_monad) apply (clarsimp simp add: liftME_def in_monad) apply (frule use_valid[OF _ arch_derive_is_arch[simplified validE_def validE_R_def]], simp) apply (clarsimp simp: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, - proof (prove)
goal (12 subgoals):
 1. c = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 2. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 3. \<And>x31 x32 x33. c = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 4. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 5. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 6. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 7. \<And>x7. c = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 8. c = DomainCap \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 9. c = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
 10. \<And>x10. c = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. is_cnode_cap c \<longrightarrow> s \<turnstile> c\<rbrace> derive_cap sl c \<lbrace>\<lambda>rv s. is_cnode_cap rv \<longrightarrow> s \<turnstile> rv\<rbrace>, -
A total of 12 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<forall>s. \<forall>(r, s')\<in>fst ((doE y <- ensure_no_children sl;
\<lambda>s. ({(Inr (UntypedCap x21 x22 x23 x24), s)}, False)
odE) s). \<forall>ra. r = Inr ra \<longrightarrow> is_cnode_cap ra \<longrightarrow> s' \<turnstile> ra
 2. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<forall>s. \<forall>(r, s')\<in>fst (arch_derive_cap x12 s). \<forall>ra. r = Inr ra \<longrightarrow> is_cnode_cap ra \<longrightarrow> s' \<turnstile> ra proof (prove)
goal (1 subgoal):
 1. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<forall>s. \<forall>(r, s')\<in>fst (arch_derive_cap x12 s). \<forall>ra. r = Inr ra \<longrightarrow> is_cnode_cap ra \<longrightarrow> s' \<turnstile> ra proof (prove)
goal (1 subgoal):
 1. \<And>x12 s b r. \<lbrakk>c = ArchObjectCap x12; (Inr r, b) \<in> fst (arch_derive_cap x12 s); is_cnode_cap r\<rbrakk> \<Longrightarrow> b \<turnstile> r proof (prove)
goal (1 subgoal):
 1. \<And>x12 s b r. \<lbrakk>c = ArchObjectCap x12; (Inr r, b) \<in> fst (arch_derive_cap x12 s); is_cnode_cap r; case Inr r of Inl e \<Rightarrow> True | Inr r \<Rightarrow> r \<noteq> NullCap \<longrightarrow> is_arch_cap r\<rbrakk> \<Longrightarrow> b \<turnstile> r proof (prove)
goal:
No subgoals!