theory CSpace1_R

lemma next_update_lhs_trancl:
  assumes np: "\<not> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* p"
  shows   "(m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x) = (m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x)" proof assume "m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x" thus "m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x" proof (cases rule: tranclE2') case base thus ?thesis by (simp add: next_update_lhs) next case (trancl q) hence "m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>+ x" by (simp add: next_update_lhs) thus ?thesis by (rule trancl_into_rtrancl [OF mdb_trancl_update_other]) fact+ qed next assume "m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x" hence "m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x" by (rule mdb_rtrancl_other_update) fact+ moreover have "m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte)" by (simp add:  next_update_lhs) ultimately show "m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x = m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
goal (2 subgoals):
 1. m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x
 2. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (state)
this:
m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x

goal (2 subgoals):
 1. m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x
 2. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
goal (2 subgoals):
 1. m(p \<mapsto> cte) \<turnstile> p \<leadsto> x \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x
 2. \<And>c. \<lbrakk>m(p \<mapsto> cte) \<turnstile> p \<leadsto> c; m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
this:
m(p \<mapsto> cte) \<turnstile> p \<leadsto> x

goal (2 subgoals):
 1. m(p \<mapsto> cte) \<turnstile> p \<leadsto> x \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x
 2. \<And>c. \<lbrakk>m(p \<mapsto> cte) \<turnstile> p \<leadsto> c; m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> p \<leadsto> x

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
this:
m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. \<And>c. \<lbrakk>m(p \<mapsto> cte) \<turnstile> p \<leadsto> c; m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>m(p \<mapsto> cte) \<turnstile> p \<leadsto> c; m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
this:
m(p \<mapsto> cte) \<turnstile> p \<leadsto> q
m(p \<mapsto> cte) \<turnstile> q \<leadsto>\<^sup>+ x

goal (1 subgoal):
 1. \<And>c. \<lbrakk>m(p \<mapsto> cte) \<turnstile> p \<leadsto> c; m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> p \<leadsto> q
m(p \<mapsto> cte) \<turnstile> q \<leadsto>\<^sup>+ x

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>+ x proof (state)
this:
m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>+ x

goal (1 subgoal):
 1. \<And>c. \<lbrakk>m(p \<mapsto> cte) \<turnstile> p \<leadsto> c; m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>+ x

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
this:
m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x

goal:
No subgoals! proof (state)
this:
m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (state)
goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (state)
this:
m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (prove)
using this:
m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x proof (state)
this:
m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (state)
this:
m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (prove)
goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte) proof (state)
this:
m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte)

goal (1 subgoal):
 1. m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> p \<leadsto>\<^sup>+ x proof (chain)
picking this:
m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x
m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte) proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* x
m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte)

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

goal:
No subgoals!