theory CSpace_I

lemma mdb_chain_0_update:
  assumes x: "m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0"
  and    np: "\<not> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* p"
  assumes p: "p \<noteq> 0"
  assumes 0: "no_0 m"
  assumes n: "mdb_chain_0 m"
  shows "mdb_chain_0 (m(p \<mapsto> cte))" unfolding mdb_chain_0_def proof rule fix x assume "x \<in> dom (m(p \<mapsto> cte))" hence x: "x = p \<or> x \<in> dom m" by simp have cnxt: "m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0" by (rule mdb_rtrancl_other_update) fact+ from x show "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0" proof assume xp: "x = p" show ?thesis proof (rule rtrancl_into_trancl2 [OF _ cnxt]) show "m(p \<mapsto> cte) \<turnstile> x \<leadsto> mdbNext (cteMDBNode cte)" using xp by (simp add: mdb_next_update) qed next assume x: "x \<in> dom m" show ?thesis proof (cases "m \<turnstile> x \<leadsto>\<^sup>* p") case False from n have "m \<turnstile> x \<leadsto>\<^sup>+ 0" unfolding mdb_chain_0_def using x by auto thus ?thesis by (rule mdb_trancl_other_update) fact+ next case True hence "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* p" proof (cases rule: next_rtrancl_tranclE) case eq thus ?thesis by simp next case trancl have "no_loops m" by (rule mdb_chain_0_no_loops) fact+ thus ?thesis by (rule trancl_into_rtrancl [OF no_loops_upd_last]) fact+ qed moreover have "m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte)" by (simp add: mdb_next_update) ultimately show ?thesis using cnxt by simp qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 (m(p \<mapsto> cte)) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (m(p \<mapsto> cte)). m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> dom (m(p \<mapsto> cte)) \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> dom (m(p \<mapsto> cte)) \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
x \<in> dom (m(p \<mapsto> cte))

goal (1 subgoal):
 1. \<And>x. x \<in> dom (m(p \<mapsto> cte)) \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
x \<in> dom (m(p \<mapsto> cte))

goal (1 subgoal):
 1. x = p \<or> x \<in> dom m proof (state)
this:
x = p \<or> x \<in> dom m

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

goal (1 subgoal):
 1. \<And>x. x \<in> dom (m(p \<mapsto> cte)) \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (chain)
picking this:
x = p \<or> x \<in> dom m proof (prove)
using this:
x = p \<or> x \<in> dom m

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (2 subgoals):
 1. x = p \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0
 2. x \<in> dom m \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
x = p

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

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

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

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

goal (1 subgoal):
 1. x \<in> dom m \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
goal (2 subgoals):
 1. m \<turnstile> x \<leadsto>\<^sup>* p \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0
 2. (x, p) \<notin> (mdb_next_rel m)\<^sup>* \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0 proof (state)
this:
(x, p) \<notin> (mdb_next_rel m)\<^sup>*

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

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ 0 proof (prove)
using this:
\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0
x \<in> dom m

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> p; m \<turnstile> x \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* p proof (prove)
goal (1 subgoal):
 1. no_loops m proof (state)
this:
no_loops m

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

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

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

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

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

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

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

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

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

goal:
No subgoals!