theory CNode_DR

lemma descendants_emptyable:
  "\<lbrakk>invs s; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt s)\<rbrakk> \<Longrightarrow> emptyable slot s" apply (case_tac slot) apply (clarsimp simp:emptyable_def st_tcb_at_def obj_at_def is_tcb_def) apply (clarsimp split:Structures_A.kernel_object.splits) apply (frule reply_slot_not_descendant) apply (simp add:tcb_at_def) apply (rule exI) apply (erule get_tcb_rev) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt s)\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs s; slot \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, b)\<rbrakk> \<Longrightarrow> emptyable slot s proof (prove)
goal (1 subgoal):
 1. \<And>a ko. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> \<exists>tcb. ko = TCB tcb \<and> halted (tcb_state tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> halted (tcb_state x2) proof (prove)
goal (2 subgoals):
 1. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> tcb_at (?t37 a x2) s
 2. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2); (?t37 a x2, tcb_cnode_index 2) \<notin> CSpaceAcc_A.descendants_of (?ptr37 a x2) (cdt s)\<rbrakk> \<Longrightarrow> halted (tcb_state x2) proof (prove)
goal (2 subgoals):
 1. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> \<exists>tcb. get_tcb (?t37 a x2) s = Some tcb
 2. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2); (?t37 a x2, tcb_cnode_index 2) \<notin> CSpaceAcc_A.descendants_of (?ptr37 a x2) (cdt s)\<rbrakk> \<Longrightarrow> halted (tcb_state x2) proof (prove)
goal (2 subgoals):
 1. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2)\<rbrakk> \<Longrightarrow> get_tcb (?t37 a x2) s = Some (?tcb40 a x2)
 2. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2); (?t37 a x2, tcb_cnode_index 2) \<notin> CSpaceAcc_A.descendants_of (?ptr37 a x2) (cdt s)\<rbrakk> \<Longrightarrow> halted (tcb_state x2) proof (prove)
goal (1 subgoal):
 1. \<And>a x2. \<lbrakk>invs s; (a, tcb_cnode_index 2) \<in> CSpaceAcc_A.descendants_of slot' (cdt s); slot = (a, tcb_cnode_index 2); kheap s a = Some (TCB x2); (a, tcb_cnode_index 2) \<notin> CSpaceAcc_A.descendants_of (?ptr37 a x2) (cdt s)\<rbrakk> \<Longrightarrow> halted (tcb_state x2) proof (prove)
goal:
No subgoals!