theory CNodeInv_R

lemma modify_map_dlist:
  assumes nxt: "valid_dlist m"
  and     inv: "\<And>cte. cteMDBNode (f cte) = cteMDBNode cte"
  shows "valid_dlist (modify_map m ptr f)" proof (cases "m ptr") case None thus ?thesis using nxt by (simp add: modify_map_def) next case (Some ptrcte) let ?m = "m(ptr \<mapsto> f ptrcte)" have "valid_dlist ?m" proof fix p cte assume cp: "?m p = Some cte" and n0: "mdbPrev (cteMDBNode cte) \<noteq> 0" let ?thesis =
      "\<exists>cte'.(m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and>
      mdbNext (cteMDBNode cte') = p" { assume peq: "p = ptr" hence mdb: "cteMDBNode cte = cteMDBNode ptrcte" using cp Some by (clarsimp simp: inv) hence "\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p" using nxt Some n0 peq by (auto elim: valid_dlistEp) hence ?thesis using peq mdb cp Some by (cases "ptr = mdbPrev (cteMDBNode cte)") simp_all } moreover { assume pne: "p \<noteq> ptr" hence ?thesis using cp Some nxt n0 by (cases "(mdbPrev (cteMDBNode cte)) = ptr") (auto elim: valid_dlistEp simp: inv) } ultimately show ?thesis by (cases "p = ptr") auto next fix p cte assume cp: "?m p = Some cte" and n0: "mdbNext (cteMDBNode cte) \<noteq> 0" let ?thesis =
      "\<exists>cte'.(m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and>
      mdbPrev (cteMDBNode cte') = p" { assume peq: "p = ptr" hence mdb: "cteMDBNode cte = cteMDBNode ptrcte" using cp Some by (clarsimp simp: inv) hence "\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p" using nxt Some n0 peq by (auto elim: valid_dlistEn) hence ?thesis using peq mdb cp Some by (cases "ptr = mdbNext (cteMDBNode cte)") simp_all } moreover { assume pne: "p \<noteq> ptr" hence ?thesis using cp Some nxt n0 by (cases "(mdbNext (cteMDBNode cte)) = ptr") (auto elim: valid_dlistEn simp: inv) } ultimately show ?thesis by (cases "p = ptr") auto qed thus ?thesis using Some by (simp add: modify_map_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist (modify_map m ptr f) proof (state)
goal (2 subgoals):
 1. m ptr = None \<Longrightarrow> valid_dlist (modify_map m ptr f)
 2. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist (modify_map m ptr f) proof (state)
this:
m ptr = None

goal (2 subgoals):
 1. m ptr = None \<Longrightarrow> valid_dlist (modify_map m ptr f)
 2. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist (modify_map m ptr f) proof (prove)
using this:
m ptr = None

goal (1 subgoal):
 1. valid_dlist (modify_map m ptr f) proof (prove)
using this:
m ptr = None
valid_dlist m

goal (1 subgoal):
 1. valid_dlist (modify_map m ptr f) proof (state)
this:
valid_dlist (modify_map m ptr f)

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist (modify_map m ptr f) proof (state)
goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist (modify_map m ptr f) proof (state)
this:
m ptr = Some ptrcte

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist (modify_map m ptr f) proof (state)
goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist (modify_map m ptr f) proof (prove)
goal (1 subgoal):
 1. valid_dlist (m(ptr \<mapsto> f ptrcte)) proof (state)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
(m(ptr \<mapsto> f ptrcte)) p = Some cte
mdbPrev (cteMDBNode cte) \<noteq> 0

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p = ptr

goal (1 subgoal):
 1. cteMDBNode cte = cteMDBNode ptrcte proof (prove)
using this:
p = ptr
(m(ptr \<mapsto> f ptrcte)) p = Some cte
m ptr = Some ptrcte

goal (1 subgoal):
 1. cteMDBNode cte = cteMDBNode ptrcte proof (state)
this:
cteMDBNode cte = cteMDBNode ptrcte

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
cteMDBNode cte = cteMDBNode ptrcte

goal (1 subgoal):
 1. \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (prove)
using this:
cteMDBNode cte = cteMDBNode ptrcte
valid_dlist m
m ptr = Some ptrcte
mdbPrev (cteMDBNode cte) \<noteq> 0
p = ptr

goal (1 subgoal):
 1. \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (prove)
using this:
\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
p = ptr
cteMDBNode cte = cteMDBNode ptrcte
(m(ptr \<mapsto> f ptrcte)) p = Some cte
m ptr = Some ptrcte

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p \<noteq> ptr

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p \<noteq> ptr

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (prove)
using this:
p \<noteq> ptr
(m(ptr \<mapsto> f ptrcte)) p = Some cte
m ptr = Some ptrcte
valid_dlist m
mdbPrev (cteMDBNode cte) \<noteq> 0

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (chain)
picking this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (prove)
using this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
(m(ptr \<mapsto> f ptrcte)) p = Some cte
mdbNext (cteMDBNode cte) \<noteq> 0

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p = ptr

goal (1 subgoal):
 1. cteMDBNode cte = cteMDBNode ptrcte proof (prove)
using this:
p = ptr
(m(ptr \<mapsto> f ptrcte)) p = Some cte
m ptr = Some ptrcte

goal (1 subgoal):
 1. cteMDBNode cte = cteMDBNode ptrcte proof (state)
this:
cteMDBNode cte = cteMDBNode ptrcte

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
cteMDBNode cte = cteMDBNode ptrcte

goal (1 subgoal):
 1. \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
cteMDBNode cte = cteMDBNode ptrcte
valid_dlist m
m ptr = Some ptrcte
mdbNext (cteMDBNode cte) \<noteq> 0
p = ptr

goal (1 subgoal):
 1. \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p
p = ptr
cteMDBNode cte = cteMDBNode ptrcte
(m(ptr \<mapsto> f ptrcte)) p = Some cte
m ptr = Some ptrcte

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p \<noteq> ptr

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p \<noteq> ptr

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p \<noteq> ptr
(m(ptr \<mapsto> f ptrcte)) p = Some cte
m ptr = Some ptrcte
valid_dlist m
mdbNext (cteMDBNode cte) \<noteq> 0

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>(m(ptr \<mapsto> f ptrcte)) p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (chain)
picking this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p = ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal (1 subgoal):
 1. \<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
\<exists>cte'. (m(ptr \<mapsto> f ptrcte)) (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

goal:
No subgoals! proof (state)
this:
valid_dlist (m(ptr \<mapsto> f ptrcte))

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist (modify_map m ptr f) proof (prove)
using this:
valid_dlist (m(ptr \<mapsto> f ptrcte))

goal (1 subgoal):
 1. valid_dlist (modify_map m ptr f) proof (prove)
using this:
valid_dlist (m(ptr \<mapsto> f ptrcte))
m ptr = Some ptrcte

goal (1 subgoal):
 1. valid_dlist (modify_map m ptr f) proof (state)
this:
valid_dlist (modify_map m ptr f)

goal:
No subgoals!