theory CNodeInv_R

lemma next_modify_map_trancl_last2:
  assumes chain: "mdb_chain_0 (modify_map m p f)"
  and     no0:   "no_0 m"
  and     nxt:   "modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p"
  shows "m \<turnstile> x \<leadsto>\<^sup>+ p" proof - let ?m = "modify_map m p f" have no0': "no_0 ?m" using no0 by simp note noloop = mdb_chain_0_no_loops [OF chain no0'] from noloop nxt have xp: "x \<noteq> p" by (clarsimp dest!: neg_no_loopsI) from nxt show ?thesis using xp proof (induct rule: converse_trancl_induct') case (base y) hence "m \<turnstile> y \<leadsto> p" by (clarsimp simp: next_unfold' modify_map_other) thus ?case .. next case (step y z) from noloop step have xp: "z \<noteq> p" by (clarsimp dest!: neg_no_loopsI) hence "m \<turnstile> y \<leadsto> z" using step by (clarsimp simp: next_unfold' modify_map_other) moreover from xp have "m \<turnstile> z \<leadsto>\<^sup>+ p" using step.hyps by simp ultimately show ?case by (rule trancl_into_trancl2) qed qed

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

goal (1 subgoal):
 1. no_0 (modify_map m p f) proof (state)
this:
no_0 (modify_map m p f)

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

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ p proof (chain)
picking this:
no_loops (modify_map m p f)
modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p proof (prove)
using this:
no_loops (modify_map m p f)
modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p

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

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ p proof (chain)
picking this:
modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p proof (prove)
using this:
modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ p proof (prove)
using this:
modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p
x \<noteq> p

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

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

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

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

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>modify_map m p f \<turnstile> y \<leadsto> z; modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p; z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ p proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>modify_map m p f \<turnstile> y \<leadsto> z; modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p; z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ p proof (state)
this:
modify_map m p f \<turnstile> y \<leadsto> z
modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p
z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p
y \<noteq> p

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>modify_map m p f \<turnstile> y \<leadsto> z; modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p; z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ p proof (chain)
picking this:
no_loops (modify_map m p f)
modify_map m p f \<turnstile> y \<leadsto> z
modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p
z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p
y \<noteq> p proof (prove)
using this:
no_loops (modify_map m p f)
modify_map m p f \<turnstile> y \<leadsto> z
modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p
z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p
y \<noteq> p

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>modify_map m p f \<turnstile> y \<leadsto> z; modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p; z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ p proof (prove)
using this:
z \<noteq> p

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto> z proof (prove)
using this:
z \<noteq> p
modify_map m p f \<turnstile> y \<leadsto> z
modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p
z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p
y \<noteq> p

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>modify_map m p f \<turnstile> y \<leadsto> z; modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p; z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ p proof (state)
this:
m \<turnstile> y \<leadsto> z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>modify_map m p f \<turnstile> y \<leadsto> z; modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p; z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ p proof (chain)
picking this:
z \<noteq> p proof (prove)
using this:
z \<noteq> p

goal (1 subgoal):
 1. m \<turnstile> z \<leadsto>\<^sup>+ p proof (prove)
using this:
z \<noteq> p
modify_map m p f \<turnstile> y \<leadsto> z
modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p
z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p

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

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>modify_map m p f \<turnstile> y \<leadsto> z; modify_map m p f \<turnstile> z \<leadsto>\<^sup>+ p; z \<noteq> p \<Longrightarrow> m \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m \<turnstile> y \<leadsto>\<^sup>+ p proof (chain)
picking this:
m \<turnstile> y \<leadsto> z
m \<turnstile> z \<leadsto>\<^sup>+ p proof (prove)
using this:
m \<turnstile> y \<leadsto> z
m \<turnstile> z \<leadsto>\<^sup>+ p

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

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

goal:
No subgoals!