theory CSpace_I

lemma mdb_trancl_update_other:
  assumes  upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y"
  and   nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows "m \<turnstile> x \<leadsto>\<^sup>+ y" using upd nopath proof induct case (base y) have "m \<turnstile> x \<leadsto> y" proof (rule mdb_next_update_other) from base show "p \<noteq> x" by clarsimp qed fact+ thus ?case .. next case (step y z) hence ih: "m \<turnstile> x \<leadsto>\<^sup>+ y" by auto from ih show ?case proof show "m \<turnstile> y \<leadsto> z" proof (rule mdb_next_update_other) show "p \<noteq> y" proof (cases "x = p") case True thus ?thesis using step.prems by simp next case False thus ?thesis using step.prems ih by - (erule contrapos_nn, rule trancl_into_rtrancl, simp) qed qed fact+ qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y
(x, p) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ y proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y; m(p \<mapsto> cte) \<turnstile> y \<leadsto> z; (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ z proof (state)
this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto> y
(x, p) \<notin> (mdb_next_rel m)\<^sup>*

goal (2 subgoals):
 1. \<And>y. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y; m(p \<mapsto> cte) \<turnstile> y \<leadsto> z; (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto> y proof (state)
goal (2 subgoals):
 1. m(?x \<mapsto> ?y) \<turnstile> x \<leadsto> y
 2. ?x \<noteq> x proof (chain)
picking this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto> y
(x, p) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto> y
(x, p) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. p \<noteq> x proof (state)
this:
p \<noteq> x

goal (1 subgoal):
 1. m(p \<mapsto> ?y) \<turnstile> x \<leadsto> y proof (state)
this:
m \<turnstile> x \<leadsto> y

goal (2 subgoals):
 1. \<And>y. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto> y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y; m(p \<mapsto> cte) \<turnstile> y \<leadsto> z; (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ z proof (prove)
using this:
m \<turnstile> x \<leadsto> 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>y z. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y; m(p \<mapsto> cte) \<turnstile> y \<leadsto> z; (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y; m(p \<mapsto> cte) \<turnstile> y \<leadsto> z; (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ z proof (state)
this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y
m(p \<mapsto> cte) \<turnstile> y \<leadsto> z
(x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y
(x, p) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y; m(p \<mapsto> cte) \<turnstile> y \<leadsto> z; (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ z proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y
m(p \<mapsto> cte) \<turnstile> y \<leadsto> z
(x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y
(x, p) \<notin> (mdb_next_rel m)\<^sup>*

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>m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y; m(p \<mapsto> cte) \<turnstile> y \<leadsto> z; (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ y; (x, p) \<notin> (mdb_next_rel m)\<^sup>*\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ z 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 \<turnstile> x \<leadsto>\<^sup>+ z proof (state)
goal (1 subgoal):
 1. m \<turnstile> y \<leadsto> z proof (prove)
goal (1 subgoal):
 1. m \<turnstile> y \<leadsto> z proof (state)
goal (2 subgoals):
 1. m(?x \<mapsto> ?y) \<turnstile> y \<leadsto> z
 2. ?x \<noteq> y proof (prove)
goal (1 subgoal):
 1. p \<noteq> y proof (state)
goal (2 subgoals):
 1. x = p \<Longrightarrow> p \<noteq> y
 2. x \<noteq> p \<Longrightarrow> p \<noteq> y proof (state)
this:
x = p

goal (2 subgoals):
 1. x = p \<Longrightarrow> p \<noteq> y
 2. x \<noteq> p \<Longrightarrow> p \<noteq> y proof (prove)
using this:
x = p

goal (1 subgoal):
 1. p \<noteq> y proof (prove)
using this:
x = p
(x, p) \<notin> (mdb_next_rel m)\<^sup>*

goal (1 subgoal):
 1. p \<noteq> y proof (state)
this:
p \<noteq> y

goal (1 subgoal):
 1. x \<noteq> p \<Longrightarrow> p \<noteq> y proof (state)
goal (1 subgoal):
 1. x \<noteq> p \<Longrightarrow> p \<noteq> y proof (state)
this:
x \<noteq> p

goal (1 subgoal):
 1. x \<noteq> p \<Longrightarrow> p \<noteq> y proof (prove)
using this:
x \<noteq> p

goal (1 subgoal):
 1. p \<noteq> y proof (prove)
using this:
x \<noteq> p
(x, p) \<notin> (mdb_next_rel m)\<^sup>*
m \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. p \<noteq> y proof (state)
this:
p \<noteq> y

goal:
No subgoals! proof (state)
this:
p \<noteq> y

goal (1 subgoal):
 1. m(p \<mapsto> ?y) \<turnstile> y \<leadsto> z proof (state)
this:
m \<turnstile> y \<leadsto> z

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

goal:
No subgoals!