theory CSpace_R

lemma mdb_next_trans_next_pres:
  "\<lbrakk> m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v) \<rbrakk> \<Longrightarrow>
   m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b = m \<turnstile> a \<leadsto>\<^sup>+ b" apply (rule iffI) apply (erule trancl_induct) apply (fastforce simp: mdb_next_pres) apply (erule trancl_trans) apply (rule r_into_trancl) apply (fastforce simp: mdb_next_pres) apply (erule trancl_induct) apply (rule r_into_trancl) apply (simp add: mdb_next_pres del: fun_upd_apply) apply (erule trancl_trans) apply (fastforce simp: mdb_next_pres simp del: fun_upd_apply) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v)\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b = m \<turnstile> a \<leadsto>\<^sup>+ b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ b
 2. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m(p \<mapsto> x) \<turnstile> a \<leadsto> y\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y; m(p \<mapsto> x) \<turnstile> y \<leadsto> z; m \<turnstile> a \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ z
 3. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y; m(p \<mapsto> x) \<turnstile> y \<leadsto> z; m \<turnstile> a \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ z
 2. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y; m(p \<mapsto> x) \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ z
 2. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y; m(p \<mapsto> x) \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto> z
 2. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ b\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ b proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto> y\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto> y\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto> y
 2. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> a \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m p = Some v; mdbNext (cteMDBNode x) = mdbNext (cteMDBNode v); m \<turnstile> a \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> m(p \<mapsto> x) \<turnstile> y \<leadsto>\<^sup>+ z proof (prove)
goal:
No subgoals!