theory Finalise_R

lemma n_next_eq:
  "n \<turnstile> p \<leadsto> p' =
  (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 (rule iffI) apply (erule n_nextD) apply (clarsimp simp: mdb_next_unfold split: if_split_asm) apply (simp add: n_def modify_map_if slot) apply hypsubst_thin apply (case_tac z) apply simp apply (drule m_next) apply clarsimp apply (case_tac z) apply simp apply (drule m_next) apply clarsimp done

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