theory CNodeInv_R

lemma mdb_chain_0_modify_map_replace:
  assumes unf: "mdb_chain_0 (modify_map m p (cteMDBNode_update (mdbNext_update (%_. (mdbNext node)))))"
  shows "mdb_chain_0 (modify_map m p (cteMDBNode_update (\<lambda>m. node)))" proof - have "modify_map m p (cteMDBNode_update (\<lambda>m. node)) =
    modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (%_. (mdbNext node))))) p
          (cteMDBNode_update (mdbPrev_update (%_. (mdbPrev node))))) p
       (cteMDBNode_update (mdbRevocable_update (%_. (mdbRevocable node))))) p
       (cteMDBNode_update (mdbFirstBadged_update (%_. (mdbFirstBadged node))))" apply (cases node) apply (cases "m p") apply (simp add: modify_map_None) apply (case_tac a) apply (rename_tac mdbnode) apply (case_tac mdbnode) apply (clarsimp simp add: next_update_is_modify [symmetric]) done thus ?thesis apply simp apply (rule mdb_chain_0_modify_map_inv) apply (rule mdb_chain_0_modify_map_inv) apply (rule mdb_chain_0_modify_map_inv [OF unf]) apply simp_all done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 (modify_map m p (cteMDBNode_update (\<lambda>m. node))) proof (state)
goal (1 subgoal):
 1. mdb_chain_0 (modify_map m p (cteMDBNode_update (\<lambda>m. node))) proof (prove)
goal (1 subgoal):
 1. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. node = MDB x1 x2 x3 x4 \<Longrightarrow> modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. \<lbrakk>node = MDB x1 x2 x3 x4; m p = None\<rbrakk> \<Longrightarrow> modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node)))
 2. \<And>x1 x2 x3 x4 a. \<lbrakk>node = MDB x1 x2 x3 x4; m p = Some a\<rbrakk> \<Longrightarrow> modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 a. \<lbrakk>node = MDB x1 x2 x3 x4; m p = Some a\<rbrakk> \<Longrightarrow> modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 a x1a x2a. \<lbrakk>node = MDB x1 x2 x3 x4; m p = Some a; a = CTE x1a x2a\<rbrakk> \<Longrightarrow> modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 a x1a mdbnode. \<lbrakk>node = MDB x1 x2 x3 x4; m p = Some a; a = CTE x1a mdbnode\<rbrakk> \<Longrightarrow> modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 a x1a mdbnode x1b x2a x3a x4a. \<lbrakk>node = MDB x1 x2 x3 x4; m p = Some a; a = CTE x1a mdbnode; mdbnode = MDB x1b x2a x3a x4a\<rbrakk> \<Longrightarrow> modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) proof (prove)
goal:
No subgoals! proof (state)
this:
modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node)))

goal (1 subgoal):
 1. mdb_chain_0 (modify_map m p (cteMDBNode_update (\<lambda>m. node))) proof (prove)
using this:
modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node)))

goal (1 subgoal):
 1. mdb_chain_0 (modify_map m p (cteMDBNode_update (\<lambda>m. node))) proof (prove)
goal (1 subgoal):
 1. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node)))) proof (prove)
goal (2 subgoals):
 1. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdb_chain_0 (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node))))
 2. \<And>cte. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdbNext (cteMDBNode (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node)) cte)) = mdbNext (cteMDBNode cte) proof (prove)
goal (3 subgoals):
 1. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdb_chain_0 (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node))))
 2. \<And>cte. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdbNext (cteMDBNode (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)) cte)) = mdbNext (cteMDBNode cte)
 3. \<And>cte. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdbNext (cteMDBNode (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node)) cte)) = mdbNext (cteMDBNode cte) proof (prove)
goal (3 subgoals):
 1. \<And>cte. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdbNext (cteMDBNode (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)) cte)) = mdbNext (cteMDBNode cte)
 2. \<And>cte. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdbNext (cteMDBNode (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)) cte)) = mdbNext (cteMDBNode cte)
 3. \<And>cte. modify_map m p (cteMDBNode_update (\<lambda>m. node)) = modify_map (modify_map (modify_map (modify_map m p (cteMDBNode_update (mdbNext_update (\<lambda>_. mdbNext node)))) p (cteMDBNode_update (mdbPrev_update (\<lambda>_. mdbPrev node)))) p (cteMDBNode_update (mdbRevocable_update (\<lambda>_. mdbRevocable node)))) p (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node))) \<Longrightarrow> mdbNext (cteMDBNode (cteMDBNode_update (mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node)) cte)) = mdbNext (cteMDBNode cte) proof (prove)
goal:
No subgoals! proof (state)
this:
mdb_chain_0 (modify_map m p (cteMDBNode_update (\<lambda>m. node)))

goal:
No subgoals!