theory Finalise_R

lemma reply_masters_rvk_fb_n [simp]: "reply_masters_rvk_fb n" using reply_masters_rvk_fb_m apply (simp add: reply_masters_rvk_fb_def n_def
                   ball_ran_modify_map_eq
                   modify_map_comp[symmetric]) apply (subst ball_ran_modify_map_eq) apply (frule bspec, rule ranI, rule slot) apply (simp add: nullMDBNode_def isCap_simps modify_map_def
                    slot) apply (subst ball_ran_modify_map_eq) apply (clarsimp simp add: modify_map_def) apply fastforce apply (simp add: ball_ran_modify_map_eq) done

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

goal (1 subgoal):
 1. reply_masters_rvk_fb n proof (prove)
goal (1 subgoal):
 1. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>cte\<in>ran (modify_map (modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)))) slot (cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap))). isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) proof (prove)
goal (2 subgoals):
 1. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v. modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))) slot = Some v \<longrightarrow> (isReplyCap (cteCap ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v)) \<and> capReplyMaster (cteCap ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v)) \<longrightarrow> mdbRevocable (cteMDBNode ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v)) \<and> mdbFirstBadged (cteMDBNode ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v))) = (isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v))
 2. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v\<in>ran (modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) 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); isReplyCap (cteCap (CTE s_cap s_node)) \<and> capReplyMaster (cteCap (CTE s_cap s_node)) \<longrightarrow> mdbRevocable (cteMDBNode (CTE s_cap s_node)) \<and> mdbFirstBadged (cteMDBNode (CTE s_cap s_node))\<rbrakk> \<Longrightarrow> \<forall>v. modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb))) slot = Some v \<longrightarrow> (isReplyCap (cteCap ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v)) \<and> capReplyMaster (cteCap ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v)) \<longrightarrow> mdbRevocable (cteMDBNode ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v)) \<and> mdbFirstBadged (cteMDBNode ((cteMDBNode_update (const nullMDBNode) \<circ> cteCap_update (\<lambda>_. capability.NullCap)) v))) = (isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v))
 2. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v\<in>ran (modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) proof (prove)
goal (1 subgoal):
 1. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v\<in>ran (modify_map (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))) (mdbNext s_node) (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) proof (prove)
goal (2 subgoals):
 1. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v. modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node))) (mdbNext s_node) = Some v \<longrightarrow> (isReplyCap (cteCap (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)) v)) \<and> capReplyMaster (cteCap (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)) v)) \<longrightarrow> mdbRevocable (cteMDBNode (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)) v)) \<and> mdbFirstBadged (cteMDBNode (cteMDBNode_update (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) mdb)) v))) = (isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v))
 2. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v\<in>ran (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>\<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0; m (mdbNext s_node) = Some v\<rbrakk> \<Longrightarrow> (isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> (mdbFirstBadged (cteMDBNode v) \<or> mdbFirstBadged s_node)) = (isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v))
 2. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v\<in>ran (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) proof (prove)
goal (1 subgoal):
 1. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>v\<in>ran (modify_map m (mdbPrev s_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext s_node)))). isReplyCap (cteCap v) \<and> capReplyMaster (cteCap v) \<longrightarrow> mdbRevocable (cteMDBNode v) \<and> mdbFirstBadged (cteMDBNode v) proof (prove)
goal:
No subgoals!