theory CNode_DR

lemma in_monad_cap_delete_invs:
  "\<lbrakk> invs sfix;slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix);
     (r, s) \<in> fst (cap_delete slot sfix)\<rbrakk>
  \<Longrightarrow> invs s" using cap_delete_invs[unfolded valid_def,simplified] apply clarsimp apply (case_tac slot) apply (drule_tac x = a in meta_spec) apply (drule_tac x = b in meta_spec) apply (drule_tac x = sfix in spec) apply (clarsimp simp:emptyable_def) apply (auto simp:reply_slot_not_descendant) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs sfix; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete slot sfix)\<rbrakk> \<Longrightarrow> invs s proof (prove)
using this:
\<forall>s. invs s \<and> emptyable ?ptr s \<longrightarrow> (\<forall>x\<in>fst (cap_delete ?ptr s). case x of (r, s') \<Rightarrow> invs s')

goal (1 subgoal):
 1. \<lbrakk>invs sfix; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete slot sfix)\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs sfix; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete slot sfix); \<And>a b. \<forall>s. invs s \<and> emptyable (a, b) s \<longrightarrow> (\<forall>x\<in>fst (cap_delete (a, b) s). case x of (r, x) \<Rightarrow> invs x)\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs sfix; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete slot sfix); \<And>a b. \<forall>s. invs s \<and> emptyable (a, b) s \<longrightarrow> (\<forall>x\<in>fst (cap_delete (a, b) s). case x of (r, x) \<Rightarrow> invs x); slot = (a, b)\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs sfix; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete slot sfix); slot = (a, b); \<And>b. \<forall>s. invs s \<and> emptyable (a, b) s \<longrightarrow> (\<forall>x\<in>fst (cap_delete (a, b) s). case x of (r, x) \<Rightarrow> invs x)\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs sfix; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete slot sfix); slot = (a, b); \<forall>s. invs s \<and> emptyable (a, b) s \<longrightarrow> (\<forall>x\<in>fst (cap_delete (a, b) s). case x of (r, x) \<Rightarrow> invs x)\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs sfix; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete slot sfix); slot = (a, b); invs sfix \<and> emptyable (a, b) sfix \<longrightarrow> (\<forall>x\<in>fst (cap_delete (a, b) sfix). case x of (r, x) \<Rightarrow> invs x)\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs sfix; (a, b) \<in> CSpaceAcc_A.descendants_of slot' (cdt sfix); (r, s) \<in> fst (cap_delete (a, b) sfix); slot = (a, b); (tcb_at a sfix \<and> b = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted a sfix) \<longrightarrow> (\<forall>x\<in>fst (cap_delete (a, b) sfix). case x of (r, x) \<Rightarrow> invs x)\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal:
No subgoals!