theory Finalise_R

lemma n_prev_eq:
  "n \<turnstile> p \<leftarrow> p' =
  (if p' = slot then p = 0
  else if p' = mdbNext s_node
  then m \<turnstile> slot \<leftarrow> p' \<and> p = mdbPrev s_node
  else m \<turnstile> p \<leftarrow> p')" apply (rule iffI) apply (clarsimp simp: mdb_prev_def split del: if_split cong: if_cong) apply (case_tac z) apply (clarsimp split del: if_split) apply (drule n_prev) apply (elim exE conjE) apply (simp split: if_split_asm) apply (frule dlist_nextD [OF m_slot_next]) apply (clarsimp simp: mdb_prev_def) apply (clarsimp simp: mdb_prev_def split: if_split_asm) apply (simp add: n_def modify_map_if slot) apply hypsubst_thin apply (case_tac z) apply clarsimp apply (drule m_prev) apply clarsimp apply (case_tac z) apply simp apply (drule m_prev) apply clarsimp done

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