theory CSpace_R

lemma m'_next:
  "\<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node)\<rbrakk>
    \<Longrightarrow> mdbNext node'
      = (if p = src then 0
         else if p = dest then mdbNext src_node
         else if mdbNext node = src then dest
         else mdbNext node)" apply(simp, intro conjI impI) apply(clarsimp simp: n m'_def modify_map_def split: if_split_asm) apply(clarsimp simp: n m'_def modify_map_def nullPointer_def) apply(subgoal_tac "mdbPrev src_node = p") prefer 2 apply(erule dlistEn) apply(simp) apply(case_tac "cte'a") apply(clarsimp simp: src) apply(clarsimp simp: n m'_def modify_map_def split: if_split_asm) apply(clarsimp simp: dest n m'_def modify_map_def) apply(clarsimp simp: n m'_def modify_map_def nullPointer_def) apply(clarsimp simp: n m'_def modify_map_def split: if_split_asm) apply(insert m_p no_0) apply(erule_tac p=src in dlistEp) apply(clarsimp simp: no_0_def) apply(clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node)\<rbrakk> \<Longrightarrow> mdbNext node' = (if p = src then 0 else if p = dest then mdbNext src_node else if mdbNext node = src then dest else mdbNext node) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 5. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 6. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 5. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbPrev src_node = p
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 5. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (5 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbPrev src_node = p
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 5. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (6 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); mdbNext node = src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (CTE cte node)) \<noteq> 0
 2. \<And>cte'a. \<lbrakk>m' p = Some (CTE cte' node'); mdbNext node = src; p \<noteq> dest; p \<noteq> src; m (mdbNext (cteMDBNode (CTE cte node))) = Some cte'a; mdbPrev (cteMDBNode cte'a) = p\<rbrakk> \<Longrightarrow> mdbPrev src_node = p
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 5. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 6. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (5 subgoals):
 1. \<And>cte'a. \<lbrakk>m' p = Some (CTE cte' node'); mdbNext node = src; p \<noteq> dest; p \<noteq> src; m (mdbNext (cteMDBNode (CTE cte node))) = Some cte'a; mdbPrev (cteMDBNode cte'a) = p\<rbrakk> \<Longrightarrow> mdbPrev src_node = p
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 5. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (5 subgoals):
 1. \<And>cte'a x1 x2. \<lbrakk>m' p = Some (CTE cte' node'); mdbNext node = src; p \<noteq> dest; p \<noteq> src; m (mdbNext (cteMDBNode (CTE cte node))) = Some cte'a; mdbPrev (cteMDBNode cte'a) = p; cte'a = CTE x1 x2\<rbrakk> \<Longrightarrow> mdbPrev src_node = p
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 5. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (4 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node = src; p \<noteq> dest; p \<noteq> src; mdbPrev src_node = p\<rbrakk> \<Longrightarrow> mdbNext node' = dest
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 4. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext src_node
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 3. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> mdbNext node' = 0
 2. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' p = Some (CTE cte' node'); m p = Some (CTE cte node); mdbNext node \<noteq> src; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> mdbNext node' = mdbNext node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbPrev src_node) = Some (CTE cte' node); mdbNext node \<noteq> src; mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; p = mdbPrev src_node; cte = cte'; node' = mdbNext_update (\<lambda>_. dest) node\<rbrakk> \<Longrightarrow> dest = mdbNext node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbPrev src_node) = Some (CTE cte' node); mdbNext node \<noteq> src; mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; p = mdbPrev src_node; cte = cte'; node' = mdbNext_update (\<lambda>_. dest) node; m src = Some (CTE src_cap src_node); no_0 m\<rbrakk> \<Longrightarrow> dest = mdbNext node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbPrev src_node) = Some (CTE cte' node); mdbNext node \<noteq> src; mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; p = mdbPrev src_node; cte = cte'; node' = mdbNext_update (\<lambda>_. dest) node; no_0 m\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE src_cap src_node)) \<noteq> 0
 2. \<And>cte'a. \<lbrakk>m (mdbPrev src_node) = Some (CTE cte' node); mdbNext node \<noteq> src; mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; p = mdbPrev src_node; cte = cte'; node' = mdbNext_update (\<lambda>_. dest) node; no_0 m; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'a; mdbNext (cteMDBNode cte'a) = src\<rbrakk> \<Longrightarrow> dest = mdbNext node proof (prove)
goal (1 subgoal):
 1. \<And>cte'a. \<lbrakk>m (mdbPrev src_node) = Some (CTE cte' node); mdbNext node \<noteq> src; mdbPrev src_node = 0 \<longrightarrow> mdbNext src_node \<noteq> 0; p = mdbPrev src_node; cte = cte'; node' = mdbNext_update (\<lambda>_. dest) node; no_0 m; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'a; mdbNext (cteMDBNode cte'a) = src\<rbrakk> \<Longrightarrow> dest = mdbNext node proof (prove)
goal:
No subgoals!