theory CNodeInv_R

lemma modify_map_next_trancl:
  assumes nxt: "m \<turnstile> x \<leadsto>\<^sup>+ y"
  and     inv: "\<And>cte. mdbNext (cteMDBNode (f cte)) = mdbNext (cteMDBNode cte)"
  shows "(modify_map m ptr f) \<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> f cte)" from nxt have "?m \<turnstile> x \<leadsto>\<^sup>+ y" proof induct case (base y) thus ?case using Some inv r_into_trancl next_unfold' by fastforce next case (step q r) show ?case proof (rule trancl_into_trancl) show "?m \<turnstile> q \<leadsto> r" using step(2) Some inv 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 f \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (2 subgoals):
 1. m ptr = None \<Longrightarrow> modify_map m ptr f \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr f \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
this:
m ptr = None

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

goal (1 subgoal):
 1. modify_map m ptr f \<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 f \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
this:
modify_map m ptr f \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr f \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr f \<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 f \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (1 subgoal):
 1. \<And>a. m ptr = Some a \<Longrightarrow> modify_map m ptr f \<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> f cte) \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (2 subgoals):
 1. \<And>y. m \<turnstile> x \<leadsto> y \<Longrightarrow> m(ptr \<mapsto> f cte) \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m(ptr \<mapsto> f cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(ptr \<mapsto> f cte) \<turnstile> x \<leadsto>\<^sup>+ z proof (state)
this:
m \<turnstile> x \<leadsto> y

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

goal (1 subgoal):
 1. m(ptr \<mapsto> f cte) \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
m \<turnstile> x \<leadsto> y
m ptr = Some cte
mdbNext (cteMDBNode (f ?cte)) = mdbNext (cteMDBNode ?cte)
(?a, ?b) \<in> ?r \<Longrightarrow> (?a, ?b) \<in> ?r\<^sup>+
?m \<turnstile> ?c \<leadsto> ?y = (\<exists>cte. ?m ?c = Some cte \<and> mdbNext (cteMDBNode cte) = ?y)

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

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

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

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

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

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

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

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

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

goal:
No subgoals!