theory CNodeInv_R

lemma (in mdb_move) m'_badged:
  "m' p = Some (CTE cap node)
  \<Longrightarrow> if p = dest then mdbFirstBadged node = mdbFirstBadged src_node \<and> cap = cap'
     else if p = src then \<not> mdbFirstBadged node \<and> cap = NullCap
     else \<exists>node'. m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node'" using src dest neq apply (clarsimp simp: m'_def n_def modify_map_cases nullMDBNode_def) apply (rule conjI, clarsimp) apply clarsimp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m' p = Some (CTE cap node) \<Longrightarrow> if p = dest then mdbFirstBadged node = mdbFirstBadged src_node \<and> cap = cap' else if p = src then \<not> mdbFirstBadged node \<and> cap = capability.NullCap else \<exists>node'. m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
using this:
m src = Some (CTE src_cap src_node)
m dest = Some (CTE capability.NullCap old_dest_node)
src \<noteq> dest

goal (1 subgoal):
 1. m' p = Some (CTE cap node) \<Longrightarrow> if p = dest then mdbFirstBadged node = mdbFirstBadged src_node \<and> cap = cap' else if p = src then \<not> mdbFirstBadged node \<and> cap = capability.NullCap else \<exists>node'. m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); src \<noteq> dest; mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> MDB nullPointer nullPointer False False = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> MDB nullPointer nullPointer False False = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); mdbNext src_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> src_node = node) \<and> MDB nullPointer nullPointer False False = nodea))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> src_node = nodea) \<and> MDB nullPointer nullPointer False False = node)) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node)\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> \<not> mdbFirstBadged node \<and> cap = capability.NullCap) \<and> (p \<noteq> src \<longrightarrow> p \<noteq> dest \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); src \<noteq> dest; mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = nodea) \<and> MDB nullPointer nullPointer False False = node))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node)) \<and> src_node = node) \<and> MDB nullPointer nullPointer False False = nodea)) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); mdbNext src_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = nodea)) \<and> (src = p \<longrightarrow> (\<exists>node. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap node)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> src_node = node) \<and> MDB nullPointer nullPointer False False = nodea))) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. (src \<noteq> p \<longrightarrow> (dest \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (dest = p \<longrightarrow> (\<exists>node cap. m p = Some (CTE cap node)) \<and> cap' = cap \<and> src_node = node)) \<and> (src = p \<longrightarrow> (\<exists>nodea. (dest \<noteq> p \<longrightarrow> (\<exists>cap. m p = Some (CTE cap nodea)) \<and> capability.NullCap = cap) \<and> (dest = p \<longrightarrow> src_node = nodea) \<and> MDB nullPointer nullPointer False False = node)) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node)\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> p \<noteq> dest \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE capability.NullCap old_dest_node); src \<noteq> dest; mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node)); mdbNext src_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node); p \<noteq> src; p \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>node'. m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
goal:
No subgoals!