theory CSpace_I

lemma mdb_trancl_other_update:
  assumes upd: "m \<turnstile> x \<leadsto>\<^sup>+ y"
  and      np: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows   "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y" using upd proof induct case (base q) from np have "x \<noteq> p" by clarsimp hence"m (p \<mapsto> cte) \<turnstile> x \<leadsto> q" using base by (simp add: mdb_next_update del: fun_upd_apply) thus ?case .. next case (step q r) show ?case proof from step.hyps(1) np have "q \<noteq> p" by (auto elim!: contrapos_nn) thus x: "m(p \<mapsto> cte) \<turnstile> q \<leadsto> r" using step by (simp add: mdb_next_update del: fun_upd_apply) qed fact+ qed

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

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

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

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

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

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto> q proof (prove)
using this:
x \<noteq> p
m \<turnstile> x \<leadsto> q

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

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

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

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

goal (2 subgoals):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ ?b
 2. m(p \<mapsto> cte) \<turnstile> ?b \<leadsto> r proof (prove)
using this:
q \<noteq> p

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> q \<leadsto> r proof (prove)
using this:
q \<noteq> p
m \<turnstile> x \<leadsto>\<^sup>+ q
m \<turnstile> q \<leadsto> r
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ q

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

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

goal:
No subgoals!