theory CNodeInv_R

lemma reply_masters_rvk_fb_n:
  "reply_masters_rvk_fb n" using reply_masters_rvk_fb_m
        weak_der'.isReplyMaster_eq[OF weak_der_src]
        weak_der'.isReplyMaster_eq[OF weak_der_dest] apply (simp add: reply_masters_rvk_fb_def) apply (frule bspec, rule ranI, rule m_p) apply (frule bspec, rule ranI, rule mdb_ptr_src.m_p) apply (clarsimp simp: ball_ran_eq) apply (case_tac cte, clarsimp) apply (frule n_cap, frule revokable, frule badge_n) apply (simp split: if_split_asm) apply clarsimp apply (elim allE, drule(1) mp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb n proof (prove)
using this:
reply_masters_rvk_fb m
(isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap)
(isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap)

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); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap)\<rbrakk> \<Longrightarrow> \<forall>cte\<in>ran n. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) 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); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap (cteCap (CTE dest_cap dest_node)) \<and> capReplyMaster (cteCap (CTE dest_cap dest_node)) \<longrightarrow> mdbRevocable (cteMDBNode (CTE dest_cap dest_node)) \<and> mdbFirstBadged (cteMDBNode (CTE dest_cap dest_node))\<rbrakk> \<Longrightarrow> \<forall>cte\<in>ran n. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) 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); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap (cteCap (CTE dest_cap dest_node)) \<and> capReplyMaster (cteCap (CTE dest_cap dest_node)) \<longrightarrow> mdbRevocable (cteMDBNode (CTE dest_cap dest_node)) \<and> mdbFirstBadged (cteMDBNode (CTE dest_cap dest_node)); isReplyCap (cteCap (CTE src_cap src_node)) \<and> capReplyMaster (cteCap (CTE src_cap src_node)) \<longrightarrow> mdbRevocable (cteMDBNode (CTE src_cap src_node)) \<and> mdbFirstBadged (cteMDBNode (CTE src_cap src_node))\<rbrakk> \<Longrightarrow> \<forall>cte\<in>ran n. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<And>x cte. \<lbrakk>\<forall>x cte. m x = Some cte \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap dest_cap \<and> capReplyMaster dest_cap \<longrightarrow> mdbRevocable dest_node \<and> mdbFirstBadged dest_node; isReplyCap src_cap \<and> capReplyMaster src_cap \<longrightarrow> mdbRevocable src_node \<and> mdbFirstBadged src_node; n x = Some cte; isReplyCap (cteCap cte); capReplyMaster (cteCap cte)\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2. \<lbrakk>\<forall>x cte. m x = Some cte \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap dest_cap \<and> capReplyMaster dest_cap \<longrightarrow> mdbRevocable dest_node \<and> mdbFirstBadged dest_node; isReplyCap src_cap \<and> capReplyMaster src_cap \<longrightarrow> mdbRevocable src_node \<and> mdbFirstBadged src_node; n x = Some (CTE x1 x2); isReplyCap x1; capReplyMaster x1\<rbrakk> \<Longrightarrow> mdbRevocable x2 \<and> mdbFirstBadged x2 proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2. \<lbrakk>\<forall>x cte. m x = Some cte \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap dest_cap \<and> capReplyMaster dest_cap \<longrightarrow> mdbRevocable dest_node \<and> mdbFirstBadged dest_node; isReplyCap src_cap \<and> capReplyMaster src_cap \<longrightarrow> mdbRevocable src_node \<and> mdbFirstBadged src_node; n x = Some (CTE x1 x2); isReplyCap x1; capReplyMaster x1; if x = src then x1 = dcap else if x = dest then x1 = scap else \<exists>node'. m x = Some (CTE x1 node'); if x = src then mdbRevocable x2 = mdbRevocable dest_node else if x = dest then mdbRevocable x2 = mdbRevocable src_node else \<exists>cap' node'. m x = Some (CTE cap' node') \<and> mdbRevocable x2 = mdbRevocable node'; if x = src then mdbFirstBadged x2 = mdbFirstBadged dest_node else if x = dest then mdbFirstBadged x2 = mdbFirstBadged src_node else \<exists>cap' node'. m x = Some (CTE cap' node') \<and> mdbFirstBadged x2 = mdbFirstBadged node'\<rbrakk> \<Longrightarrow> mdbRevocable x2 \<and> mdbFirstBadged x2 proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2. \<lbrakk>\<exists>cap' node'. m x = Some (CTE cap' node') \<and> mdbFirstBadged x2 = mdbFirstBadged node'; \<forall>x cte. m x = Some cte \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap dest_cap \<and> capReplyMaster dest_cap \<longrightarrow> mdbRevocable dest_node \<and> mdbFirstBadged dest_node; isReplyCap src_cap \<and> capReplyMaster src_cap \<longrightarrow> mdbRevocable src_node \<and> mdbFirstBadged src_node; n x = Some (CTE x1 x2); isReplyCap x1; capReplyMaster x1; x \<noteq> src; \<exists>node'. m x = Some (CTE x1 node'); x \<noteq> dest; \<exists>cap' node'. m x = Some (CTE cap' node') \<and> mdbRevocable x2 = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable x2 \<and> mdbFirstBadged x2 proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 node'. \<lbrakk>\<forall>x cte. m x = Some cte \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte); (isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap dest_cap \<and> capReplyMaster dest_cap \<longrightarrow> mdbRevocable dest_node \<and> mdbFirstBadged dest_node; isReplyCap src_cap \<and> capReplyMaster src_cap \<longrightarrow> mdbRevocable src_node \<and> mdbFirstBadged src_node; n x = Some (CTE x1 x2); isReplyCap x1; capReplyMaster x1; x \<noteq> src; x \<noteq> dest; mdbFirstBadged x2 = mdbFirstBadged node'; m x = Some (CTE x1 node'); mdbRevocable x2 = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 node'. \<lbrakk>(isReplyCap scap \<and> capReplyMaster scap) = (isReplyCap src_cap \<and> capReplyMaster src_cap); (isReplyCap dcap \<and> capReplyMaster dcap) = (isReplyCap dest_cap \<and> capReplyMaster dest_cap); isReplyCap dest_cap \<and> capReplyMaster dest_cap \<longrightarrow> mdbRevocable dest_node \<and> mdbFirstBadged dest_node; isReplyCap src_cap \<and> capReplyMaster src_cap \<longrightarrow> mdbRevocable src_node \<and> mdbFirstBadged src_node; n x = Some (CTE x1 x2); isReplyCap x1; capReplyMaster x1; x \<noteq> src; x \<noteq> dest; mdbFirstBadged x2 = mdbFirstBadged node'; m x = Some (CTE x1 node'); mdbRevocable x2 = mdbRevocable node'; isReplyCap (cteCap (CTE x1 node')) \<and> capReplyMaster (cteCap (CTE x1 node')) \<longrightarrow> mdbRevocable (cteMDBNode (CTE x1 node')) \<and> mdbFirstBadged (cteMDBNode (CTE x1 node'))\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> mdbFirstBadged node' proof (prove)
goal:
No subgoals!