theory CNodeInv_R

lemma m_to_src:
  "m \<turnstile> p \<leadsto> src = (p \<noteq> 0 \<and> p = mdbPrev src_node)" apply (insert src) apply (rule iffI) apply (clarsimp simp add: mdb_next_unfold) apply (rule conjI, clarsimp) apply (case_tac z) apply clarsimp apply (erule_tac p=p in dlistEn, clarsimp) apply clarsimp apply (clarsimp simp add: mdb_next_unfold) apply (erule dlistEp, clarsimp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto> src = (p \<noteq> 0 \<and> p = mdbPrev src_node) proof (prove)
goal (1 subgoal):
 1. m src = Some (CTE src_cap src_node) \<Longrightarrow> m \<turnstile> p \<leadsto> src = (p \<noteq> 0 \<and> p = mdbPrev src_node) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); m \<turnstile> p \<leadsto> src\<rbrakk> \<Longrightarrow> p \<noteq> 0 \<and> p = mdbPrev src_node
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> 0 \<and> p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> src proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m (mdbNext (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> p \<noteq> 0 \<and> p = mdbPrev src_node
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> 0 \<and> p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> src proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>m (mdbNext (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> 0 \<and> p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> src proof (prove)
goal (2 subgoals):
 1. \<And>z x1 x2. \<lbrakk>m (mdbNext (cteMDBNode z)) = Some (CTE src_cap src_node); m p = Some z; src = mdbNext (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> 0 \<and> p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> src proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>m (mdbNext x2) = Some (CTE src_cap src_node); m p = Some (CTE x1 x2); src = mdbNext x2\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> 0 \<and> p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> src proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 cte'. \<lbrakk>m (mdbNext x2) = Some (CTE src_cap src_node); src = mdbNext x2; m (mdbNext (cteMDBNode (CTE x1 x2))) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> p = mdbPrev src_node
 2. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> 0 \<and> p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); p \<noteq> 0 \<and> p = mdbPrev src_node\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE src_cap src_node); mdbPrev src_node \<noteq> 0; p = mdbPrev src_node\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbPrev src_node) = Some z \<and> src = mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev src_node \<noteq> 0; p = mdbPrev src_node; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> \<exists>z. m (mdbPrev src_node) = Some z \<and> src = mdbNext (cteMDBNode z) proof (prove)
goal:
No subgoals!