theory Finalise_DR

lemma dcorres_revoke_cap_unnecessary:
  "dcorres dc \<top> (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr
    and cte_at (ptr,tcb_cnode_index 2) and not_idle_thread ptr and valid_idle)
    (revoke_cap_simple (ptr, tcb_replycap_slot))
    (return x)" apply (subst transform_tcb_slot_simp[symmetric]) apply (rule corres_guard_imp) apply (rule dcorres_revoke_cap_no_descendants) apply (simp add:transform_tcb_slot_simp[symmetric])+ apply (rule not_waiting_reply_slot_no_descendants) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr and cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) and not_idle_thread ptr and valid_idle) (revoke_cap_simple (ptr, tcb_replycap_slot)) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr and cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) and not_idle_thread ptr and valid_idle) (revoke_cap_simple (transform_cslot_ptr (ptr, tcb_cnode_index 2))) (return x) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (revoke_cap_simple (transform_cslot_ptr (ptr, tcb_cnode_index 2))) (return x)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr and cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) and not_idle_thread ptr and valid_idle) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. transform_cslot_ptr (ptr, tcb_cnode_index 2) = transform_cslot_ptr ?slot4
 2. \<And>s. True \<Longrightarrow> True
 3. \<And>s. (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr and cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) and not_idle_thread ptr and valid_idle) s \<Longrightarrow> valid_mdb s \<and> cte_wp_at (\<lambda>_. True) ?slot4 s \<and> CSpaceAcc_A.descendants_of ?slot4 (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_reply_caps s \<and> valid_objs s \<and> only_idle s \<and> valid_mdb s \<and> st_tcb_at (Not \<circ> awaiting_reply) ptr s \<and> cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) s \<and> not_idle_thread ptr s \<and> valid_idle s \<Longrightarrow> CSpaceAcc_A.descendants_of (ptr, tcb_cnode_index 2) (cdt s) = {} proof (prove)
goal (4 subgoals):
 1. \<And>s. valid_reply_caps s \<and> valid_objs s \<and> only_idle s \<and> valid_mdb s \<and> st_tcb_at (Not \<circ> awaiting_reply) ptr s \<and> cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) s \<and> not_idle_thread ptr s \<and> valid_idle s \<Longrightarrow> st_tcb_at (Not \<circ> awaiting_reply) ptr s
 2. \<And>s. valid_reply_caps s \<and> valid_objs s \<and> only_idle s \<and> valid_mdb s \<and> st_tcb_at (Not \<circ> awaiting_reply) ptr s \<and> cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) s \<and> not_idle_thread ptr s \<and> valid_idle s \<Longrightarrow> valid_reply_caps s
 3. \<And>s. valid_reply_caps s \<and> valid_objs s \<and> only_idle s \<and> valid_mdb s \<and> st_tcb_at (Not \<circ> awaiting_reply) ptr s \<and> cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) s \<and> not_idle_thread ptr s \<and> valid_idle s \<Longrightarrow> valid_objs s
 4. \<And>s. valid_reply_caps s \<and> valid_objs s \<and> only_idle s \<and> valid_mdb s \<and> st_tcb_at (Not \<circ> awaiting_reply) ptr s \<and> cte_wp_at (\<lambda>_. True) (ptr, tcb_cnode_index 2) s \<and> not_idle_thread ptr s \<and> valid_idle s \<Longrightarrow> valid_mdb s proof (prove)
goal:
No subgoals!