theory CSpace_R

lemma src_next_eq:
  "m \<turnstile> p \<leadsto> mdbNext src_node = (if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0)" using src apply - apply (rule iffI) prefer 2 apply (clarsimp split: if_split_asm) apply clarsimp apply (rule conjI) apply clarsimp apply (frule (1) dlist_nextD0) apply (clarsimp simp: m_prev_of_next) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> mdbNext src_node = (if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0) proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> mdbNext src_node = (if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0) proof (prove)
goal (1 subgoal):
 1. m src = Some (CTE src_cap src_node) \<Longrightarrow> m \<turnstile> p \<leadsto> mdbNext src_node = (if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0
 2. \<lbrakk>m src = Some (CTE src_cap src_node); if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> mdbNext src_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> mdbNext src_node
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> if mdbNext src_node \<noteq> 0 then p = src else m \<turnstile> p \<leadsto> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> (mdbNext src_node \<noteq> 0 \<longrightarrow> p = src) \<and> (mdbNext src_node = 0 \<longrightarrow> m \<turnstile> p \<leadsto> 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node \<noteq> 0 \<longrightarrow> p = src
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0 \<longrightarrow> m \<turnstile> p \<leadsto> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> p = src
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0 \<longrightarrow> m \<turnstile> p \<leadsto> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node; mdbNext src_node \<noteq> 0; m \<turnstile> p \<leftarrow> mdbNext src_node\<rbrakk> \<Longrightarrow> p = src
 2. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0 \<longrightarrow> m \<turnstile> p \<leadsto> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> mdbNext src_node\<rbrakk> \<Longrightarrow> mdbNext src_node = 0 \<longrightarrow> m \<turnstile> p \<leadsto> 0 proof (prove)
goal:
No subgoals!