theory Finalise_R

lemma n_nextD:
  "n \<turnstile> p \<leadsto> p' \<Longrightarrow>
  if p = slot then p' = 0
  else if p = mdbPrev s_node
  then m \<turnstile> p \<leadsto> slot \<and> p' = mdbNext s_node
  else m \<turnstile> p \<leadsto> p'" apply (clarsimp simp: mdb_next_unfold split del: if_split cong: if_cong) apply (case_tac z) apply (clarsimp split del: if_split) apply (drule n_next) apply (elim exE conjE) apply (simp split: if_split_asm) apply (frule dlist_prevD [OF m_slot_prev]) apply (clarsimp simp: mdb_next_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> p' \<Longrightarrow> if p = slot then p' = 0 else if p = mdbPrev s_node then m \<turnstile> p \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>n p = Some z; p' = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> if p = slot then mdbNext (cteMDBNode z) = 0 else if p = mdbPrev s_node then (\<exists>z. m (mdbPrev s_node) = Some z \<and> slot = mdbNext (cteMDBNode z)) \<and> mdbNext (cteMDBNode z) = mdbNext s_node else \<exists>za. m p = Some za \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal (1 subgoal):
 1. \<And>z x1 x2. \<lbrakk>n p = Some z; p' = mdbNext (cteMDBNode z); z = CTE x1 x2\<rbrakk> \<Longrightarrow> if p = slot then mdbNext (cteMDBNode z) = 0 else if p = mdbPrev s_node then (\<exists>z. m (mdbPrev s_node) = Some z \<and> slot = mdbNext (cteMDBNode z)) \<and> mdbNext (cteMDBNode z) = mdbNext s_node else \<exists>za. m p = Some za \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>n p = Some (CTE x1 x2); p' = mdbNext x2\<rbrakk> \<Longrightarrow> if p = slot then mdbNext x2 = 0 else if p = mdbPrev s_node then (\<exists>z. m (mdbPrev s_node) = Some z \<and> slot = mdbNext (cteMDBNode z)) \<and> mdbNext x2 = mdbNext s_node else \<exists>z. m p = Some z \<and> mdbNext x2 = mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>p' = mdbNext x2; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then mdbNext x2 = 0 else if p = mdbPrev s_node then mdbNext x2 = mdbNext s_node else mdbNext x2 = mdbNext node')\<rbrakk> \<Longrightarrow> if p = slot then mdbNext x2 = 0 else if p = mdbPrev s_node then (\<exists>z. m (mdbPrev s_node) = Some z \<and> slot = mdbNext (cteMDBNode z)) \<and> mdbNext x2 = mdbNext s_node else \<exists>z. m p = Some z \<and> mdbNext x2 = mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 cap' node'. \<lbrakk>p' = mdbNext x2; m p = Some (CTE cap' node'); if p = slot then mdbNext x2 = 0 else if p = mdbPrev s_node then mdbNext x2 = mdbNext s_node else mdbNext x2 = mdbNext node'\<rbrakk> \<Longrightarrow> if p = slot then mdbNext x2 = 0 else if p = mdbPrev s_node then (\<exists>z. m (mdbPrev s_node) = Some z \<and> slot = mdbNext (cteMDBNode z)) \<and> mdbNext x2 = mdbNext s_node else \<exists>z. m p = Some z \<and> mdbNext x2 = mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<And>x2 cap' node'. \<lbrakk>p' = mdbNext s_node; m (mdbPrev s_node) = Some (CTE cap' node'); p = mdbPrev s_node; mdbNext x2 = mdbNext s_node\<rbrakk> \<Longrightarrow> slot = mdbNext node' proof (prove)
goal (1 subgoal):
 1. \<And>x2 cap' node'. \<lbrakk>p' = mdbNext s_node; m (mdbPrev s_node) = Some (CTE cap' node'); p = mdbPrev s_node; mdbNext x2 = mdbNext s_node; m \<turnstile> mdbPrev s_node \<leadsto> slot\<rbrakk> \<Longrightarrow> slot = mdbNext node' proof (prove)
goal:
No subgoals!