theory CNodeInv_R

lemma (in mdb_swap) n_dest:
  "n dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)))" unfolding n_def n'_def using dest p_0 apply (simp only: dest2_next dest2_prev) apply (cases "mdbPrev src_node = dest") apply (subgoal_tac "dest \<noteq> mdbNext src_node") apply (simp add: modify_map_same modify_map_other) apply (cases src_node, simp) apply clarsimp apply (cases "mdbNext src_node = dest") apply (simp add: modify_map_same modify_map_other) apply (cases src_node, simp) apply (simp add: modify_map_same modify_map_other) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
using this:
m dest = Some (CTE dest_cap dest_node)
dest \<noteq> 0

goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node = dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)))
 2. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node = dest; dest \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)))
 2. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node = dest\<rbrakk> \<Longrightarrow> dest \<noteq> mdbNext src_node
 3. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); mdbPrev src_node = dest; dest \<noteq> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbPrev_update (\<lambda>_. src) src_node = MDB (mdbNext src_node) src (mdbRevocable src_node) (mdbFirstBadged src_node)
 2. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node = dest\<rbrakk> \<Longrightarrow> dest \<noteq> mdbNext src_node
 3. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node = dest\<rbrakk> \<Longrightarrow> dest \<noteq> mdbNext src_node
 2. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)))
 2. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); mdbPrev src_node \<noteq> dest; mdbNext src_node = dest\<rbrakk> \<Longrightarrow> mdbNext_update (\<lambda>_. src) src_node = MDB src (mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)
 2. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m dest = Some (CTE dest_cap dest_node); dest \<noteq> 0; mdbPrev src_node \<noteq> dest; mdbNext src_node \<noteq> dest\<rbrakk> \<Longrightarrow> modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (if dest = mdbPrev src_node then dest else mdbNext dest_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest = Some (CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node))) proof (prove)
goal:
No subgoals!