theory CNodeInv_R

lemma modify_map_dlist2:
  assumes nxt: "valid_dlist (modify_map m ptr f)"
  and     inv: "\<And>cte. cteMDBNode (f cte) = cteMDBNode cte"
  shows  "valid_dlist m" proof (cases "m ptr") case None thus ?thesis using nxt by (simp add: modify_map_def) next case (Some ptrcte) let ?m = "modify_map m ptr f" 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 (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 [where p = ptr] simp: modify_map_same inv) hence ?thesis using peq cp Some by (cases "ptr = mdbPrev (cteMDBNode cte)") (clarsimp simp: inv modify_map_same modify_map_other)+ } 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 modify_map_apply) } 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 (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 [where p = ptr] simp: modify_map_same inv) hence ?thesis using peq cp Some by (cases "ptr = mdbNext (cteMDBNode cte)") (clarsimp simp: inv modify_map_same modify_map_other)+ } 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 modify_map_apply) } 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 m proof (state)
goal (2 subgoals):
 1. m ptr = None \<Longrightarrow> valid_dlist m
 2. \<And>a. m ptr = Some a \<Longrightarrow> valid_dlist m proof (state)
this:
m ptr = None

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

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

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

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

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

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

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (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 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 p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
cteMDBNode cte = cteMDBNode ptrcte

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

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

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

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

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 p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

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

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

goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (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 p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p \<noteq> ptr

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

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 p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p

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

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 (1 subgoal):
 1. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
m p = Some cte
mdbNext (cteMDBNode cte) \<noteq> 0

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

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (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 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 p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
cteMDBNode cte = cteMDBNode ptrcte

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

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

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

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

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 p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p = ptr \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

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

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

goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (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 p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
using this:
p \<noteq> ptr

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

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 p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (state)
this:
p \<noteq> ptr \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p

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

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:
No subgoals! proof (state)
this:
valid_dlist m

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

goal (1 subgoal):
 1. valid_dlist m proof (prove)
using this:
valid_dlist m
m ptr = Some ptrcte

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

goal:
No subgoals!