kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma next_prev:
  assumes cte: "m p = Some cte"
  and      vd: "valid_dlist m"
  and     no0: "no_0 m"
  and     nxt: "m \<turnstile> q \<leadsto> p"
  shows   "q = mdbPrev (cteMDBNode cte)" proof - from no0 have p0: "p \<noteq> 0" using cte unfolding no_0_def by - (rule, clarsimp) thus ?thesis using nxt vd cte apply - apply (simp add: next_unfold') apply (erule exE conjE)+ apply (erule (1) valid_dlistEn, fastforce) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. q = mdbPrev (cteMDBNode cte) proof (state)
goal (1 subgoal):
 1. q = mdbPrev (cteMDBNode cte) proof (chain)
picking this:
no_0 m proof (prove)
using this:
no_0 m

goal (1 subgoal):
 1. p \<noteq> 0 proof (prove)
using this:
no_0 m
m p = Some cte

goal (1 subgoal):
 1. p \<noteq> 0 proof (prove)
using this:
m 0 = None
m p = Some cte

goal (1 subgoal):
 1. p \<noteq> 0 proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. q = mdbPrev (cteMDBNode cte) proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. q = mdbPrev (cteMDBNode cte) proof (prove)
using this:
p \<noteq> 0
m \<turnstile> q \<leadsto> p
valid_dlist m
m p = Some cte

goal (1 subgoal):
 1. q = mdbPrev (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> 0; m \<turnstile> q \<leadsto> p; valid_dlist m; m p = Some cte\<rbrakk> \<Longrightarrow> q = mdbPrev (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> 0; \<exists>cte. m q = Some cte \<and> mdbNext (cteMDBNode cte) = p; valid_dlist m; m p = Some cte\<rbrakk> \<Longrightarrow> q = mdbPrev (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<And>ctea. \<lbrakk>p \<noteq> 0; valid_dlist m; m p = Some cte; m q = Some ctea; mdbNext (cteMDBNode ctea) = p\<rbrakk> \<Longrightarrow> q = mdbPrev (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<And>ctea cte'. \<lbrakk>p \<noteq> 0; m p = Some cte; m q = Some ctea; mdbNext (cteMDBNode ctea) = p; m (mdbNext (cteMDBNode ctea)) = Some cte'; mdbPrev (cteMDBNode cte') = q\<rbrakk> \<Longrightarrow> q = mdbPrev (cteMDBNode cte) proof (prove)
goal:
No subgoals! proof (state)
this:
q = mdbPrev (cteMDBNode cte)

goal:
No subgoals!
theory CNodeInv_R

lemma modify_map_trancl_other_iff:
  "\<not> m \<turnstile> x \<leadsto>\<^sup>* p \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y" apply - apply (cases "m p") apply (simp add: modify_map_None) apply (subst next_update_is_modify [symmetric]) apply assumption apply simp apply (erule  mdb_trancl_other_update_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = None\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (3 subgoals):
 1. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> m p = Some (?cte'1 a)
 2. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> ?cte1 a = f (?cte'1 a)
 3. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> m(p \<mapsto> ?cte1 a) \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> ?cte1 a = f a
 2. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> m(p \<mapsto> ?cte1 a) \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(x, p) \<notin> (mdb_next_rel m)\<^sup>*; m p = Some a\<rbrakk> \<Longrightarrow> m(p \<mapsto> f a) \<turnstile> x \<leadsto>\<^sup>+ y = m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma next_modify_map_trancl_last_iff:
  assumes c1: "mdb_chain_0 m"
  and   chain: "mdb_chain_0 (modify_map m p f)"
  and     no0:   "no_0 m"
  shows  "modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p = m \<turnstile> x \<leadsto>\<^sup>+ p" using c1 chain no0 by (auto intro: next_modify_map_trancl_last next_modify_map_trancl_last2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p = m \<turnstile> x \<leadsto>\<^sup>+ p proof (prove)
using this:
mdb_chain_0 m
mdb_chain_0 (modify_map m p f)
no_0 m

goal (1 subgoal):
 1. modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p = m \<turnstile> x \<leadsto>\<^sup>+ p
theory CNodeInv_R

lemma next_modify_map_last:
  shows "x \<noteq> p \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto> p = m \<turnstile> x \<leadsto> p" by (clarsimp simp: next_unfold' modify_map_other)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> p \<Longrightarrow> modify_map m p f \<turnstile> x \<leadsto> p = m \<turnstile> x \<leadsto> p
theory CNodeInv_R

lemma next_trancl_nx:
  assumes node: "m ptr = Some (CTE cap node)"
  and       nl: "m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  and      neq: "mdbNext node \<noteq> ptr'"
  shows "m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr'" using nl node neq by (clarsimp dest!: tranclD elim!: next_rtrancl_tranclE simp: next_unfold')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr' proof (prove)
using this:
m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'
m ptr = Some (CTE cap node)
mdbNext node \<noteq> ptr'

goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr'
theory CNodeInv_R

lemma next_rtrancl_xp:
  assumes node: "m ptr' = Some (CTE cap node)"
  and      vd: "valid_dlist m"
  and     no0: "no_0 m"
  and       nl: "m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  shows "m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node" using nl node apply - apply (drule tranclD2) apply clarsimp apply (drule (1) next_prev [OF _ vd no0]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node proof (prove)
using this:
m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'
m ptr' = Some (CTE cap node)

goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'; m ptr' = Some (CTE cap node)\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m ptr' = Some (CTE cap node); \<exists>z. m \<turnstile> ptr \<leadsto>\<^sup>* z \<and> m \<turnstile> z \<leadsto> ptr'\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m ptr' = Some (CTE cap node); m \<turnstile> ptr \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> ptr'\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m \<turnstile> ptr \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> ptr'; z = mdbPrev (cteMDBNode (CTE cap node))\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma next_trancl_xp:
  assumes node: "m ptr' = Some (CTE cap node)"
  and      vd: "valid_dlist m"
  and     no0: "no_0 m"
  and     neq: "mdbPrev node \<noteq> ptr"
  and       nl: "m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  shows "m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node" using neq node nl apply - apply (drule (1) next_rtrancl_xp [OF _ vd no0]) apply (erule next_rtrancl_tranclE) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node proof (prove)
using this:
mdbPrev node \<noteq> ptr
m ptr' = Some (CTE cap node)
m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'

goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev node \<noteq> ptr; m ptr' = Some (CTE cap node); m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev node \<noteq> ptr; m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'; m \<turnstile> ptr \<leadsto>\<^sup>* mdbPrev node\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbPrev node \<noteq> ptr; m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'; ptr = mdbPrev node\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node
 2. \<lbrakk>mdbPrev node \<noteq> ptr; m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'; ptr \<noteq> mdbPrev node; m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev node \<noteq> ptr; m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'; ptr \<noteq> mdbPrev node; m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node\<rbrakk> \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ mdbPrev node proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma next_trancl_np:
  assumes node: "m ptr = Some (CTE cap node)"
  and    node': "m ptr' = Some (CTE cap' node')"
  and      vd: "valid_dlist m"
  and     no0: "no_0 m"
  and     neq: "mdbPrev node' \<noteq> ptr"
  and    neq': "mdbNext node \<noteq> mdbPrev node'"
  and       nl: "m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  shows "m \<turnstile> mdbNext node \<leadsto>\<^sup>+ mdbPrev node'" by (rule next_trancl_nx [OF _ next_trancl_xp]) fact+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>+ mdbPrev node'
theory CNodeInv_R

lemma neg_next_trancl_nx:
  assumes node: "m ptr = Some (CTE cap node)"
  and       nl: "\<not> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  shows "\<not> m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr'" using nl proof (rule contrapos_nn) assume "m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr'" show "m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'" proof (rule trancl_into_trancl2) show "m \<turnstile> ptr \<leadsto> mdbNext node" using node by (rule next_fold, simp) qed fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext node, ptr') \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
using this:
(ptr, ptr') \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (mdbNext node, ptr') \<notin> (mdb_next_rel m)\<^sup>+ proof (state)
goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr' \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (state)
this:
m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr'

goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr' \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (prove)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (state)
goal (2 subgoals):
 1. m \<turnstile> ptr \<leadsto> ?b
 2. m \<turnstile> ?b \<leadsto>\<^sup>+ ptr' proof (prove)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto> mdbNext node proof (prove)
using this:
m ptr = Some (CTE cap node)

goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto> mdbNext node proof (state)
this:
m \<turnstile> ptr \<leadsto> mdbNext node

goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>+ ptr' proof (state)
this:
m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'

goal:
No subgoals!
theory CNodeInv_R

lemma neg_next_rtrancl_nx:
  assumes node: "m ptr = Some (CTE cap node)"
  and       nl: "\<not> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  shows "\<not> m \<turnstile> mdbNext node \<leadsto>\<^sup>* ptr'" using nl proof (rule contrapos_nn) assume "m \<turnstile> mdbNext node \<leadsto>\<^sup>* ptr'" show "m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'" proof (rule rtrancl_into_trancl2) show "m \<turnstile> ptr \<leadsto> mdbNext node" using node by (rule next_fold, simp) qed fact+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext node, ptr') \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
(ptr, ptr') \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (mdbNext node, ptr') \<notin> (mdb_next_rel m)\<^sup>* proof (state)
goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>* ptr' \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (state)
this:
m \<turnstile> mdbNext node \<leadsto>\<^sup>* ptr'

goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>* ptr' \<Longrightarrow> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (prove)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto>\<^sup>+ ptr' proof (state)
goal (2 subgoals):
 1. m \<turnstile> ptr \<leadsto> ?b
 2. m \<turnstile> ?b \<leadsto>\<^sup>* ptr' proof (prove)
goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto> mdbNext node proof (prove)
using this:
m ptr = Some (CTE cap node)

goal (1 subgoal):
 1. m \<turnstile> ptr \<leadsto> mdbNext node proof (state)
this:
m \<turnstile> ptr \<leadsto> mdbNext node

goal (1 subgoal):
 1. m \<turnstile> mdbNext node \<leadsto>\<^sup>* ptr' proof (state)
this:
m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'

goal:
No subgoals!
theory CNodeInv_R

lemma dom_into_not0 [intro?]:
  "\<lbrakk> no_0 m; p \<in> dom m \<rbrakk> \<Longrightarrow> p \<noteq> 0" by (rule, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 m; p \<in> dom m\<rbrakk> \<Longrightarrow> p \<noteq> (0::'a)
theory CNodeInv_R

lemma neg_next_trancl_np:
  assumes node: "m ptr = Some (CTE cap node)"
  and    node': "m ptr' = Some (CTE cap' node')"
  and      dom: "mdbPrev node' \<in> dom m"
  and      no0: "no_0 m"
  and       vd: "valid_dlist m"
  and       nl: "\<not> m \<turnstile> ptr \<leadsto>\<^sup>+ ptr'"
  shows "\<not> m \<turnstile> mdbNext node \<leadsto>\<^sup>+ mdbPrev node'" by (rule neg_next_trancl_nx [OF _ neg_next_trancl_xp]) fact+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext node, mdbPrev node') \<notin> (mdb_next_rel m)\<^sup>+
theory CNodeInv_R

lemma neg_next_trancl_trancl:
  assumes nxt: "m \<turnstile> a \<leadsto>\<^sup>* a'"
  and      ab: "\<not> m \<turnstile> b \<leadsto>\<^sup>* a'"
  and      nl: "\<not> m \<turnstile> a' \<leadsto>\<^sup>* b"
  shows "\<not> m \<turnstile> a \<leadsto>\<^sup>+ b" using nl nxt apply - apply (erule contrapos_nn) apply (erule next_rtrancl_tranclE) apply simp apply (erule (1) next_trancl_split_tt [OF _ _ ab]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
using this:
(a', b) \<notin> (mdb_next_rel m)\<^sup>*
m \<turnstile> a \<leadsto>\<^sup>* a'

goal (1 subgoal):
 1. (a, b) \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a', b) \<notin> (mdb_next_rel m)\<^sup>*; m \<turnstile> a \<leadsto>\<^sup>* a'\<rbrakk> \<Longrightarrow> (a, b) \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>* a'; m \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m \<turnstile> a' \<leadsto>\<^sup>* b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ b; a = a'\<rbrakk> \<Longrightarrow> m \<turnstile> a' \<leadsto>\<^sup>* b
 2. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ b; a \<noteq> a'; m \<turnstile> a \<leadsto>\<^sup>+ a'\<rbrakk> \<Longrightarrow> m \<turnstile> a' \<leadsto>\<^sup>* b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> a \<leadsto>\<^sup>+ b; a \<noteq> a'; m \<turnstile> a \<leadsto>\<^sup>+ a'\<rbrakk> \<Longrightarrow> m \<turnstile> a' \<leadsto>\<^sup>* b proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma ndom_is_0D:
  "\<lbrakk> mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node) \<rbrakk>
  \<Longrightarrow> mdbNext node = 0" apply - apply (frule (1) mdb_chain_0_nextD) apply simp apply (erule next_rtrancl_tranclE) apply simp apply (drule tranclD) apply (clarsimp simp: next_unfold') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node)\<rbrakk> \<Longrightarrow> mdbNext node = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node)\<rbrakk> \<Longrightarrow> mdbNext node = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node); m \<turnstile> mdbNext (cteMDBNode (CTE cap node)) \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> mdbNext node = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node); m \<turnstile> mdbNext node \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> mdbNext node = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node); mdbNext node = 0\<rbrakk> \<Longrightarrow> mdbNext node = 0
 2. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node); mdbNext node \<noteq> 0; m \<turnstile> mdbNext node \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> mdbNext node = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node); mdbNext node \<noteq> 0; m \<turnstile> mdbNext node \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> mdbNext node = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext node \<notin> dom m; mdb_chain_0 m; no_0 m; m ptr = Some (CTE cap node); mdbNext node \<noteq> 0; \<exists>z. m \<turnstile> mdbNext node \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* 0\<rbrakk> \<Longrightarrow> mdbNext node = 0 proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma (in mdb_swap) next_m_n2:
  "n \<turnstile> p \<leadsto> p' = m \<turnstile> s_d_swp p \<leadsto> s_d_swp p'" by (simp add: next_m_n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> p' = m \<turnstile> s_d_swp p \<leadsto> s_d_swp p'
theory CNodeInv_R

lemma (in mdb_swap) n_src [simp]:
  "n src = Some (CTE dcap dest2_node)" unfolding n_def n'_def apply (simp) apply (subst modify_map_same | subst modify_map_other, simp add: dest2_node_def)+ apply (simp add: src) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n src = Some (CTE dcap dest2_node) proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) src = Some (CTE dcap dest2_node) proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const dest2_node))) dest (cteMDBNode_update (const src_node))) (mdbPrev dest2_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext dest2_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) src = Some (CTE dcap dest2_node) proof (prove)
goal (1 subgoal):
 1. map_option (cteMDBNode_update (const dest2_node)) (map_option (cteCap_update (\<lambda>_. dcap)) (m src)) = Some (CTE dcap dest2_node) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma (in mdb_swap) src_prev_next [intro?]:
  "mdbPrev src_node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src" using src apply - apply (erule dlistEp) apply simp apply (rule next_fold) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev src_node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. mdbPrev src_node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev src_node \<noteq> 0; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src proof (prove)
goal (2 subgoals):
 1. mdbPrev src_node \<noteq> 0 \<Longrightarrow> mdbPrev (cteMDBNode (CTE src_cap src_node)) \<noteq> 0
 2. \<And>cte'. \<lbrakk>mdbPrev src_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev src_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev src_node \<leadsto> src proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>mdbPrev src_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> m (mdbPrev src_node) = Some (?cte4 cte')
 2. \<And>cte'. \<lbrakk>mdbPrev src_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (?cte4 cte')) = src proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev src_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte') = src proof (prove)
goal:
No subgoals!