theory CSpace_R

lemma reply_masters_rvk_fb' [simp]:
  "reply_masters_rvk_fb n'" using reply_masters_rvk_fb simple apply (simp add: reply_masters_rvk_fb_def n'_def
                    n_def ball_ran_modify_map_eq) apply (subst ball_ran_modify_map_eq) apply (clarsimp simp: modify_map_def m_p is_simple_cap'_def) apply (simp add: ball_ran_modify_map_eq m_p is_simple_cap'_def
                    dest_cap isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb n' proof (prove)
using this:
reply_masters_rvk_fb m
is_simple_cap' c'

goal (1 subgoal):
 1. reply_masters_rvk_fb n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); is_simple_cap' c'\<rbrakk> \<Longrightarrow> \<forall>cte\<in>ran (modify_map (modify_map m dest (cteCap_update (\<lambda>_. c'))) dest (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))). isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); is_simple_cap' c'\<rbrakk> \<Longrightarrow> \<forall>v. modify_map m dest (cteCap_update (\<lambda>_. c')) dest = Some v \<longrightarrow> (isReplyCap (cteCap (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) v)) \<and> capReplyMaster (cteCap (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) v)) \<longrightarrow> mdbRevocable (cteMDBNode (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) v)) \<and> mdbFirstBadged (cteMDBNode (cteMDBNode_update (\<lambda>m. mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))) v))) = (isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v))
 2. \<lbrakk>\<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); is_simple_cap' c'\<rbrakk> \<Longrightarrow> \<forall>v\<in>ran (modify_map m dest (cteCap_update (\<lambda>_. c'))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); is_simple_cap' c'\<rbrakk> \<Longrightarrow> \<forall>v\<in>ran (modify_map m dest (cteCap_update (\<lambda>_. c'))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) proof (prove)
goal:
No subgoals!