theory CNodeInv_R

lemma modify_map_next_trancl2:
  assumes nxt: "(modify_map m ptr f) \<turnstile> x \<leadsto>\<^sup>+ y"
  and     inv: "\<And>cte. mdbNext (cteMDBNode (f cte)) = mdbNext (cteMDBNode cte)"
  shows   "m \<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 by (auto intro!: r_into_trancl
        simp: modify_map_def mdb_next_update next_unfold' split: if_split_asm) next case (step q r) show ?case proof show "m \<turnstile> q \<leadsto> r" using step(2) Some inv by (auto simp: modify_map_def mdb_next_update next_unfold' split: if_split_asm) qed fact+ qed thus ?thesis using Some by (simp add: modify_map_def) qed

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!