theory CSpace_I

lemma no_loops_upd_last:
  assumes noloop: "no_loops m"
  and     nxt: "m \<turnstile> x \<leadsto>\<^sup>+ p"
  shows "m (p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ p" proof - 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 (p \<mapsto> cte) \<turnstile> y \<leadsto> p" using noloop by (auto simp add: mdb_next_update) thus ?case .. next case (step y z) from noloop step have xp: "z \<noteq> p" by (clarsimp dest!: neg_no_loopsI) hence "m (p \<mapsto> cte) \<turnstile> y \<leadsto> z" using step by (simp add: mdb_next_update) moreover from xp have "m (p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p" using step.hyps assms by (auto simp del: fun_upd_apply) ultimately show ?case by (rule trancl_into_trancl2) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ p proof (state)
goal (1 subgoal):
 1. m(p \<mapsto> cte) \<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. m(p \<mapsto> cte) \<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. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ p proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>+ p
x \<noteq> p

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

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

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

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

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> y \<leadsto>\<^sup>+ p proof (state)
this:
m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> y \<leadsto>\<^sup>+ p proof (state)
this:
m \<turnstile> y \<leadsto> z
m \<turnstile> z \<leadsto>\<^sup>+ p
z \<noteq> p \<Longrightarrow> m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p; y \<noteq> p\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> y \<leadsto>\<^sup>+ p proof (prove)
using this:
z \<noteq> p

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p
y \<noteq> p

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

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<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> m(p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p
no_loops m
m \<turnstile> x \<leadsto>\<^sup>+ p

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

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

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

goal:
No subgoals!