theory CSpace1_R

lemma update_prev_next_trancl:
  assumes nxt: "m \<turnstile> x \<leadsto>\<^sup>+ y"
  shows "(modify_map m ptr (cteMDBNode_update (mdbPrev_update z))) \<turnstile> x \<leadsto>\<^sup>+ y" proof (cases "m ptr") case None thus ?thesis using nxt by (simp add: modify_map_def) next case (Some cte) let ?m = "m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte)" from nxt have "?m \<turnstile> x \<leadsto>\<^sup>+ y" proof induct case (base y) thus ?case using Some by - (rule r_into_trancl, clarsimp simp: next_unfold') next case (step q r) show ?case proof (rule trancl_into_trancl) show "?m \<turnstile> q \<leadsto> r" using step(2) Some by (simp only: mdb_next_update, clarsimp simp: next_unfold') qed fact+ qed thus ?thesis using Some by (simp add: modify_map_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (2 subgoals):
 1. m ptr = None \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
this:
m ptr = None

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

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
m ptr = None
m \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y

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

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (chain)
picking this:
m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (2 subgoals):
 1. \<And>y. m \<turnstile> x \<leadsto> y \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>y za. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> za; m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ za proof (state)
this:
m \<turnstile> x \<leadsto> y

goal (2 subgoals):
 1. \<And>y. m \<turnstile> x \<leadsto> y \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>y za. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> za; m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ za proof (prove)
using this:
m \<turnstile> x \<leadsto> y

goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
m \<turnstile> x \<leadsto> y
m ptr = Some cte

goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
this:
m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. \<And>y za. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> za; m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ za proof (state)
goal (1 subgoal):
 1. \<And>y za. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> za; m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ za proof (state)
this:
m \<turnstile> x \<leadsto>\<^sup>+ q
m \<turnstile> q \<leadsto> r
m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ q

goal (1 subgoal):
 1. \<And>y za. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> za; m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ za proof (prove)
goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ r proof (state)
goal (2 subgoals):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ ?b
 2. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> ?b \<leadsto> r proof (prove)
goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> q \<leadsto> r proof (prove)
using this:
m \<turnstile> q \<leadsto> r
m ptr = Some cte

goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> q \<leadsto> r proof (state)
this:
m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> q \<leadsto> r

goal (1 subgoal):
 1. m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ q proof (state)
this:
m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ r

goal:
No subgoals! proof (state)
this:
m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
m(ptr \<mapsto> cteMDBNode_update (mdbPrev_update z) cte) \<turnstile> x \<leadsto>\<^sup>+ y
m ptr = Some cte

goal (1 subgoal):
 1. modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
this:
modify_map m ptr (cteMDBNode_update (mdbPrev_update z)) \<turnstile> x \<leadsto>\<^sup>+ y

goal:
No subgoals!