theory CNodeInv_R

lemma next_modify_map_trancl_last:
  assumes chain: "mdb_chain_0 m"
  and     no0:   "no_0 m"
  and     nxt: "m \<turnstile> x \<leadsto>\<^sup>+ p"
  shows   "modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p" proof - 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 "modify_map m p f \<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 "modify_map m p f \<turnstile> y \<leadsto> z" using step by (clarsimp simp: next_unfold' modify_map_other) moreover from xp have "modify_map m p f \<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. modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p proof (state)
goal (1 subgoal):
 1. modify_map m p f \<turnstile> x \<leadsto>\<^sup>+ p proof (state)
this:
no_loops m

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal:
No subgoals!