theory CNodeInv_R

lemma mdb_chain_0_modify_map_0:
  assumes chain: "mdb_chain_0 m"
  and      no0:  "no_0 m"
  shows
  "mdb_chain_0 (modify_map m ptr (cteMDBNode_update (mdbNext_update (%_. 0))))"
  (is "mdb_chain_0 ?M") unfolding mdb_chain_0_def proof fix x assume "x \<in> dom ?M" hence xd: "x \<in> dom m" by (clarsimp simp: modify_map_def dom_def split: if_split_asm) hence x0: "m \<turnstile> x \<leadsto>\<^sup>+ 0" using chain unfolding mdb_chain_0_def by simp show "?M \<turnstile> x \<leadsto>\<^sup>+ 0" proof (cases "m ptr") case None thus ?thesis by (simp add: modify_map_def) (rule x0) next case (Some cte) show ?thesis proof (cases "m \<turnstile> x \<leadsto>\<^sup>* ptr") case False thus ?thesis apply (subst next_update_is_modify [symmetric, OF _ refl]) apply (rule Some) apply (erule mdb_trancl_other_update [OF x0]) done next case True hence "?M \<turnstile> x \<leadsto>\<^sup>* ptr" apply (subst next_update_is_modify [symmetric, OF _ refl]) apply (rule Some) apply (erule next_rtrancl_tranclE) apply simp apply (rule trancl_into_rtrancl) apply (erule no_loops_upd_last [OF mdb_chain_0_no_loops [OF chain no0]]) done moreover have "?M \<turnstile> ptr \<leadsto> 0" apply (subst next_update_is_modify [symmetric, OF _ refl]) apply (rule Some) apply (simp add: mdb_next_update) done ultimately show ?thesis by simp qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0)))) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0)))). modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0)))) \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0)))) \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))))

goal (1 subgoal):
 1. \<And>x. x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0)))) \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))))

goal (1 subgoal):
 1. x \<in> dom m proof (state)
this:
x \<in> dom m

goal (1 subgoal):
 1. \<And>x. x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0)))) \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
x \<in> dom m

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
x \<in> dom m
mdb_chain_0 m

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
x \<in> dom m
\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
m \<turnstile> x \<leadsto>\<^sup>+ 0

goal (1 subgoal):
 1. \<And>x. x \<in> dom (modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0)))) \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (2 subgoals):
 1. m ptr = None \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0
 2. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
m ptr = None

goal (2 subgoals):
 1. m ptr = None \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0
 2. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
m ptr = None

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
m ptr = Some cte

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (2 subgoals):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0
 2. (x, ptr) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
(x, ptr) \<notin> (mdb_next_rel m)\<^sup>*

goal (2 subgoals):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0
 2. (x, ptr) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
(x, ptr) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (2 subgoals):
 1. (x, ptr) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m ptr = Some ?cte'1
 2. (x, ptr) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) ?cte'1) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. (x, ptr) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal:
No subgoals! proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
m \<turnstile> x \<leadsto>\<^sup>* ptr

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>* ptr

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>* ptr proof (prove)
goal (2 subgoals):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> m ptr = Some ?cte'1
 2. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) ?cte'1) \<turnstile> x \<leadsto>\<^sup>* ptr proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) cte) \<turnstile> x \<leadsto>\<^sup>* ptr proof (prove)
goal (2 subgoals):
 1. x = ptr \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) cte) \<turnstile> x \<leadsto>\<^sup>* ptr
 2. \<lbrakk>x \<noteq> ptr; m \<turnstile> x \<leadsto>\<^sup>+ ptr\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) cte) \<turnstile> x \<leadsto>\<^sup>* ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> ptr; m \<turnstile> x \<leadsto>\<^sup>+ ptr\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) cte) \<turnstile> x \<leadsto>\<^sup>* ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> ptr; m \<turnstile> x \<leadsto>\<^sup>+ ptr\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) cte) \<turnstile> x \<leadsto>\<^sup>+ ptr proof (prove)
goal:
No subgoals! proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>* ptr

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>* ptr

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> ptr \<leadsto> 0 proof (prove)
goal (2 subgoals):
 1. m ptr = Some ?cte'
 2. m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) ?cte') \<turnstile> ptr \<leadsto> 0 proof (prove)
goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbNext_update (\<lambda>_. 0)) cte) \<turnstile> ptr \<leadsto> 0 proof (prove)
goal:
No subgoals! proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> ptr \<leadsto> 0

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* ptr \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (chain)
picking this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>* ptr
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> ptr \<leadsto> 0 proof (prove)
using this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>* ptr
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> ptr \<leadsto> 0

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0

goal:
No subgoals! proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0

goal:
No subgoals! proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbNext_update (\<lambda>_. 0))) \<turnstile> x \<leadsto>\<^sup>+ 0

goal:
No subgoals!