# Theory WeakSimulation

```section ‹The weak simulation›

theory WeakSimulation imports Slice begin

context SDG begin

lemma call_node_notin_slice_return_node_neither:
assumes "call_of_return_node n n'" and "n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
shows "n ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof -
from ‹call_of_return_node n n'› obtain a a' where "return_node n"
and "valid_edge a" and "n' = sourcenode a"
and "valid_edge a'" and "a' ∈ get_return_edges a"
and "n = targetnode a'" by(fastforce simp:call_of_return_node_def)
from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q p r fs
where "kind a = Q:r↪⇘p⇙fs" by(fastforce dest!:only_call_get_return_edges)
with ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
by(fastforce dest!:call_return_edges)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
have "CFG_node (sourcenode a) s-p→⇘sum⇙ CFG_node (targetnode a')"
by(fastforce intro:sum_SDG_call_summary_edge)
show ?thesis
proof
assume "n ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹n = targetnode a'› have "CFG_node (targetnode a') ∈ HRB_slice S"
hence "CFG_node (sourcenode a) ∈ HRB_slice S"
proof(induct "CFG_node (targetnode a')" rule:HRB_slice_cases)
case (phase1 nx)
with ‹CFG_node (sourcenode a) s-p→⇘sum⇙ CFG_node (targetnode a')›
show ?case by(fastforce intro:combine_SDG_slices.combSlice_refl sum_slice1
simp:HRB_slice_def)
next
case (phase2 nx n' n'' p')
from ‹CFG_node (targetnode a') ∈ sum_SDG_slice2 n'›
‹CFG_node (sourcenode a) s-p→⇘sum⇙ CFG_node (targetnode a')› ‹valid_edge a›
have "CFG_node (sourcenode a) ∈ sum_SDG_slice2 n'"
by(fastforce intro:sum_slice2)
with ‹n' ∈ sum_SDG_slice1 nx› ‹n'' s-p'→⇘ret⇙ CFG_node (parent_node n')› ‹nx ∈ S›
show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
simp:HRB_slice_def)
qed
with ‹n' ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹n' = sourcenode a› show False
qed
qed

lemma edge_obs_intra_slice_eq:
assumes "valid_edge a" and "intra_kind (kind a)" and "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
shows "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
proof -
from assms have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_subset)
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
{ fix x assume "x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
and "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
have "∃as. targetnode a -as→⇩ι* x"
proof(cases "method_exit x")
case True
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
then obtain asx where "targetnode a -asx→⇩√* (_Exit_)"
by(fastforce dest:Exit_path)
then obtain as pex where "targetnode a -as→⇩ι* pex" and "method_exit pex"
by -(erule valid_Exit_path_intra_path)
hence "get_proc pex = get_proc (targetnode a)"
by -(rule intra_path_get_procs[THEN sym])
also from ‹valid_edge a› ‹intra_kind (kind a)›
have "… = get_proc (sourcenode a)"
by -(rule get_proc_intra[THEN sym])
also from ‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› True
have "… = get_proc x"
by(fastforce elim:obs_intraE intro:intra_path_get_procs)
finally have "pex = x" using ‹method_exit pex› True
by -(rule method_exit_unique)
with ‹targetnode a -as→⇩ι* pex› show ?thesis by fastforce
next
case False
with ‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "x postdominates (sourcenode a)" by(rule obs_intra_postdominate)
with ‹valid_edge a› ‹intra_kind (kind a)› ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "x postdominates (targetnode a)"
by(fastforce elim:postdominate_inner_path_targetnode path_edge obs_intraE
simp:intra_path_def sourcenodes_def)
thus ?thesis by(fastforce elim:postdominate_implies_inner_path)
qed
then obtain as where "targetnode a -as→⇩ι* x" by blast
from ‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "x ∈ ⌊HRB_slice S⌋⇘CFG⇙" by -(erule obs_intraE)
have "∃x' ∈ ⌊HRB_slice S⌋⇘CFG⇙. ∃as'. targetnode a -as'→⇩ι* x' ∧
(∀a' ∈ set (sourcenodes as'). a' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
proof(cases "∃a' ∈ set (sourcenodes as). a' ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
then obtain zs z zs' where "sourcenodes as = zs@z#zs'"
and "z ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "∀z' ∈ set zs. z' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(erule split_list_first_propE)
then obtain ys y ys'
where "sourcenodes ys = zs" and "as = ys@y#ys'"
and "sourcenode y = z"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹targetnode a -as→⇩ι* x› ‹as = ys@y#ys'›
have "targetnode a -ys@y#ys'→* x" and "∀y' ∈ set ys. intra_kind (kind y')"
from ‹targetnode a -ys@y#ys'→* x› have "targetnode a -ys→* sourcenode y"
by(rule path_split)
with ‹∀y' ∈ set ys. intra_kind (kind y')› ‹sourcenode y = z›
‹∀z' ∈ set zs. z' ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹z ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹sourcenodes ys = zs›
show ?thesis by(fastforce simp:intra_path_def)
next
case False
with ‹targetnode a -as→⇩ι* x› ‹x ∈ ⌊HRB_slice S⌋⇘CFG⇙›
show ?thesis by fastforce
qed
hence "∃y. y ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obs_intra_elem)
with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
have False by simp }
with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹valid_node (sourcenode a)›
show ?thesis by(cases "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
(auto dest!:obs_intra_singleton_disj)
qed

lemma intra_edge_obs_slice:
assumes "ms ≠ []" and "ms'' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a"
and "intra_kind (kind a)"
and disj:"(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "hd ms = sourcenode a" and "ms' = targetnode a#tl ms"
and "∀n ∈ set (tl ms'). return_node n"
shows "ms'' ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙"
proof -
from ‹ms'' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙› ‹∀n ∈ set (tl ms'). return_node n›
obtain msx m msx' mx m' where "ms' = msx@m#msx'" and "ms'' = mx#msx'"
and "mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
and "∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
and imp:"∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
⟶ (∃x'' ∈ set (xs'@[m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
show ?thesis
proof(cases msx)
case Nil
with ‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
disj ‹ms' = msx@m#msx'› ‹hd ms = sourcenode a› ‹ms' = targetnode a#tl ms›
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by(cases ms) auto
from ‹ms' = msx@m#msx'› ‹ms' = targetnode a#tl ms› Nil
have "m = targetnode a" by simp
with ‹valid_edge a› ‹intra_kind (kind a)› ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
have "mx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:edge_obs_intra_subset)
from ‹ms' = msx@m#msx'› Nil ‹ms' = targetnode a # tl ms›
‹hd ms = sourcenode a› ‹ms ≠ []›
have "ms = []@sourcenode a#msx'" by(cases ms) auto
with ‹ms'' = mx#msx'› ‹mx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙› Nil
show ?thesis by(fastforce intro!:obsI)
next
case (Cons x xs)
with ‹ms' = msx@m#msx'› ‹ms' = targetnode a # tl ms›
have "msx = targetnode a#xs" by simp
from Cons ‹ms' = msx@m#msx'› ‹ms' = targetnode a # tl ms› ‹hd ms = sourcenode a›
have "ms = (sourcenode a#xs)@m#msx'" by(cases ms) auto
from disj ‹ms = (sourcenode a#xs)@m#msx'›
‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
have disj2:"(∃m ∈ set (xs@[m]). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce
hence "∀zs z zs'. sourcenode a#xs = zs@z#zs' ∧ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
⟶ (∃z'' ∈ set (zs'@[m]). ∃mx. call_of_return_node z'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
proof(cases "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with ‹hd ms = sourcenode a› have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with ‹valid_edge a› ‹intra_kind (kind a)›
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with imp ‹msx = targetnode a#xs› show ?thesis
by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
next
case False
with ‹hd ms = sourcenode a› ‹valid_edge a›
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
from False disj2
have "∃m ∈ set (xs@[m]). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by simp
with imp ‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}›
‹msx = targetnode a#xs› show ?thesis
by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
qed
with ‹ms' = msx@m#msx'› ‹ms' = targetnode a # tl ms› ‹hd ms = sourcenode a›
‹ms'' = mx#msx'› ‹mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹ms = (sourcenode a#xs)@m#msx'›
show ?thesis by(simp del:obs.simps)(rule obsI,auto)
qed
qed

subsection ‹Silent moves›

inductive silent_move ::
"'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒
(('var ⇀ 'val) × 'ret) list ⇒ 'edge ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
("_,_ ⊢ '(_,_') -_→⇩τ '(_,_')" [51,50,0,0,50,0,0] 51)

where silent_move_intra:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
length s' = length s; length ms = length s;
hd ms = sourcenode a; ms' = (targetnode a)#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"

| silent_move_call:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘p⇙fs;
valid_edge a'; a' ∈ get_return_edges a;
(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
length ms = length s; length s' = Suc(length s);
hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"

| silent_move_return:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q↩⇘p⇙f';
∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙;
∀m ∈ set (tl ms). return_node m; length ms = length s; length s = Suc(length s');
s' ≠ []; hd ms = sourcenode a; hd(tl ms) = targetnode a; ms' = tl ms⟧
⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"

lemma silent_move_valid_nodes:
"⟦S,f ⊢ (ms,s) -a→⇩τ (ms',s'); ∀m ∈ set ms'. valid_node m⟧
⟹ ∀m ∈ set ms. valid_node m"
by(induct rule:silent_move.induct)(case_tac ms,auto)+

lemma silent_move_return_node:
"S,f ⊢ (ms,s) -a→⇩τ (ms',s') ⟹ ∀m ∈ set (tl ms'). return_node m"
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms n⇩c ms')
thus ?case by simp
next
case (silent_move_call f a s s' Q r p fs a' ms n⇩c ms')
from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "return_node (targetnode a')" by(fastforce simp:return_node_def)
with ‹∀m∈set (tl ms). return_node m› ‹ms' = targetnode a # targetnode a' # tl ms›
show ?case by simp
next
case (silent_move_return f a s s' Q p f' ms n⇩c ms')
thus ?case by(cases "tl ms") auto
qed

lemma silent_move_equal_length:
assumes "S,f ⊢ (ms,s) -a→⇩τ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms n⇩c ms')
from ‹pred (f a) s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from ‹length ms = length s› ‹ms' = targetnode a # tl ms›
‹length s' = length s› show ?case by simp
next
case (silent_move_call f a s s' Q r p fs a' ms n⇩c ms')
from ‹pred (f a) s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from ‹length ms = length s› ‹length s' = Suc (length s)›
‹ms' = targetnode a # targetnode a' # tl ms› show ?case by simp
next
case (silent_move_return f a s s' Q p f' ms n⇩c ms')
from ‹length ms = length s› ‹length s = Suc (length s')› ‹ms' = tl ms› ‹s' ≠ []›
show ?case by simp
qed
thus "length ms = length s" and "length ms' = length s'" by simp_all
qed

lemma silent_move_obs_slice:
"⟦S,kind ⊢ (ms,s) -a→⇩τ (ms',s'); msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙;
∀n ∈ set (tl ms'). return_node n⟧
⟹ msx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct S f≡"kind" ms s a ms' s' rule:silent_move.induct)
case (silent_move_intra a s s' ms n⇩c ms')
from ‹pred (kind a) s› ‹length ms = length s› have "ms ≠ []"
by(cases s) auto
with silent_move_intra show ?case by -(rule intra_edge_obs_slice)
next
case (silent_move_call a s s' Q r p fs a' ms S ms')
note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "return_node (targetnode a')" by(fastforce simp:return_node_def)
with ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹valid_edge a'›
have "call_of_return_node (targetnode a') (sourcenode a)"
from ‹pred (kind a) s› ‹length ms = length s›
have "ms ≠ []" by(cases s) auto
from disj
show ?case
proof
assume "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹hd ms = sourcenode a› have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with ‹call_of_return_node (targetnode a') (sourcenode a)›
‹ms' = targetnode a # targetnode a' # tl ms›
have "∃n' ∈ set (tl ms'). ∃nx. call_of_return_node n' nx ∧ nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce
with ‹msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙› ‹ms' = targetnode a # targetnode a' # tl ms›
have "msx ∈ obs (targetnode a' # tl ms) ⌊HRB_slice S⌋⇘CFG⇙" by simp
from ‹valid_edge a› ‹a' ∈ get_return_edges a›
obtain a'' where "valid_edge a''" and [simp]:"sourcenode a'' = sourcenode a"
and [simp]:"targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
by -(drule call_return_node_edge,auto simp:intra_kind_def)
from ‹∀m∈set (tl ms'). return_node m› ‹ms' = targetnode a # targetnode a' # tl ms›
have "∀m∈set (tl ms). return_node m" by simp
with ‹ms ≠ []› ‹msx ∈ obs (targetnode a'#tl ms) ⌊HRB_slice S⌋⇘CFG⇙›
‹valid_edge a''› ‹intra_kind(kind a'')› disj
‹hd ms = sourcenode a›
show ?case by -(rule intra_edge_obs_slice,fastforce+)
next
assume "∃m∈set (tl ms).
∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹ms ≠ []› ‹msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙›
‹ms' = targetnode a # targetnode a' # tl ms›
show ?thesis by(cases ms) auto
qed
next
case (silent_move_return a s s' Q p f' ms S ms')
from ‹length ms = length s› ‹length s = Suc (length s')› ‹s' ≠ []›
have "ms ≠ []" and "tl ms ≠ []" by(auto simp:length_Suc_conv)
from ‹∃m∈set (tl ms).
∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹tl ms ≠ []› ‹hd (tl ms) = targetnode a›
have "(∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
(∃m∈set (tl (tl ms)). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(cases "tl ms") auto
hence "obs ms ⌊HRB_slice S⌋⇘CFG⇙ = obs (tl ms) ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume "∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
from ‹tl ms ≠ []› have "hd (tl ms) ∈ set (tl ms)" by simp
with ‹hd (tl ms) = targetnode a› have "targetnode a ∈ set (tl ms)" by simp
with ‹ms ≠ []›
‹∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
have "∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙" by(cases ms) auto
with ‹ms ≠ []› show ?thesis by(cases ms) auto
next
assume "∃m∈set (tl (tl ms)). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹ms ≠ []› ‹tl ms ≠ []› show ?thesis
by(cases ms,auto simp:Let_def)(case_tac list,auto)+
qed
with ‹ms' = tl ms› ‹msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙› show ?case by simp
qed

lemma silent_move_empty_obs_slice:
assumes "S,f ⊢ (ms,s) -a→⇩τ (ms',s')" and "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}"
shows "obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(rule ccontr)
assume "obs ms ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
then obtain xs where "xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "∀m ∈ set (tl ms). return_node m"
by(fastforce elim!:silent_move.cases simp:call_of_return_node_def)
with ‹xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙›
obtain msx m msx' m' where assms:"ms = msx@m#msx'" "xs = m'#msx'"
"m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
"∀mx ∈ set msx'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
"∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
⟶ (∃x'' ∈ set (xs'@[m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')› ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› assms
show False
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms S ms')
note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
show False
proof(cases msx)
case Nil
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have [simp]:"m = sourcenode a"
and "tl ms = msx'" by simp_all
from Nil ‹ms' = targetnode a # tl ms› ‹ms = msx @ m # msx'›
have "ms' = msx @ targetnode a # msx'" by simp
from msx' disj ‹tl ms = msx'› ‹hd ms = sourcenode a›
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
with ‹valid_edge a› ‹intra_kind (kind a)›
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by(rule edge_obs_intra_slice_eq)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by simp
from msx Nil have "∀xs x xs'. msx = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [targetnode a]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" by simp
with ‹m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙› msx'
‹ms' = msx @ targetnode a # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
next
case (Cons y ys)
with ‹ms = msx @ m # msx'› ‹ms' = targetnode a # tl ms› ‹hd ms = sourcenode a›
have "ms' = targetnode a # ys @ m # msx'" and "y = sourcenode a"
and "tl ms = ys @ m # msx'" by simp_all
{ fix x assume "x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
from this True
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
thus ?thesis by simp
next
case False
from ‹valid_edge a› ‹intra_kind (kind a)› False
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with ‹x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙› show ?thesis
by fastforce
qed }
with msx Cons ‹y = sourcenode a›
have "∀xs x xs'. targetnode a # ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
apply clarsimp apply(case_tac xs) apply auto
apply(erule_tac x="[]" in allE) apply clarsimp
apply(erule_tac x="sourcenode a # list" in allE) apply auto
done
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx'
‹ms' = targetnode a # ys @ m # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
next
case (silent_move_call f a s s' Q r p fs a' ms S ms')
note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain a'' where "valid_edge a''"
and "sourcenode a'' = sourcenode a" and "targetnode a'' = targetnode a'"
and "intra_kind (kind a'')"
by(fastforce dest:call_return_node_edge simp:intra_kind_def)
from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "call_of_return_node (targetnode a') (sourcenode a)"
by(fastforce simp:call_of_return_node_def return_node_def)
show False
proof(cases msx)
case Nil
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have [simp]:"m = sourcenode a"
and "tl ms = msx'" by simp_all
from Nil ‹ms' = targetnode a # targetnode a' # tl ms› ‹ms = msx @ m # msx'›
have "ms' = targetnode a # targetnode a' # msx'" by simp
from msx' disj ‹tl ms = msx'› ‹hd ms = sourcenode a›
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from ‹valid_edge a''› ‹intra_kind (kind a'')› ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹sourcenode a'' = sourcenode a› ‹targetnode a'' = targetnode a'›
have "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:edge_obs_intra_slice_eq)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
have "m' ∈ obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙" by simp
from this msx' have "m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obsI)
from ‹call_of_return_node (targetnode a') (sourcenode a)›
‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
have "∃m' ∈ set (targetnode a'#msx').
∃mx. call_of_return_node m' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce
with ‹m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙›
have "m'#msx' ∈ obs (targetnode a#targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
by simp
with ‹ms' = targetnode a # targetnode a' # msx'› ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}›
show False by simp
next
case (Cons y ys)
with ‹ms = msx @ m # msx'› ‹ms' = targetnode a # targetnode a' # tl ms›
‹hd ms = sourcenode a›
have "ms' = targetnode a # targetnode a' # ys @ m # msx'"
and "y = sourcenode a" and "tl ms = ys @ m # msx'" by simp_all
show False
proof(cases "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (targetnode a' # ys @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
case True
hence imp:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (targetnode a' # ys @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" .
show False
proof(cases "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (ys @ [m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
case True
with imp msx Cons ‹y = sourcenode a›
have "∀xs x xs'. targetnode a # targetnode a' # ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
apply clarsimp apply(case_tac xs) apply fastforce
apply(case_tac list) apply fastforce apply clarsimp
apply(erule_tac x="sourcenode a # lista" in allE) apply auto
done
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx'
‹ms' = targetnode a # targetnode a' # ys @ m # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
next
case False
hence "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
and all:"∀x''∈set (ys @ [m]). ∀mx. call_of_return_node x'' mx ⟶
mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce+
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
from this True
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
thus ?thesis by simp
next
case False
with ‹sourcenode a'' = sourcenode a›
have "sourcenode a'' ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with ‹valid_edge a''› ‹intra_kind (kind a'')›
have "obs_intra (targetnode a'') ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a'') ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with ‹obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}›
‹sourcenode a'' = sourcenode a› ‹targetnode a'' = targetnode a'›
show ?thesis by fastforce
qed
with msx Cons ‹y = sourcenode a› all
show False by simp blast
qed
next
case False
hence "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
and all:"∀x''∈set (targetnode a' # ys @ [m]).
∀mx. call_of_return_node x'' mx ⟶ mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce+
with Cons ‹y = sourcenode a› msx
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}" by auto blast
from ‹call_of_return_node (targetnode a') (sourcenode a)› all
have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
from this ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙›
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
with ‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
qed
next
case (silent_move_return f a s s' Q p f' ms S ms')
note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
show False
proof(cases msx)
case Nil
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have  "tl ms = msx'" by simp
with ‹∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
msx'
show False by fastforce
next
case (Cons y ys)
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› ‹ms' = tl ms›
have "ms' = ys @ m # msx'" and "y = sourcenode a" by simp_all
from msx Cons have "∀xs x xs'. ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶  (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by auto (erule_tac x="y # xs" in allE,auto)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx' ‹ms' = ys @ m # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
qed
qed

inductive silent_moves ::
"'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒
(('var ⇀ 'val) × 'ret) list ⇒ 'edge list ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
("_,_ ⊢ '(_,_') =_⇒⇩τ '(_,_')" [51,50,0,0,50,0,0] 51)

where silent_moves_Nil: "length ms = length s ⟹ S,f ⊢ (ms,s) =[]⇒⇩τ (ms,s)"

| silent_moves_Cons:
"⟦S,f ⊢ (ms,s) -a→⇩τ (ms',s'); S,f ⊢ (ms',s') =as⇒⇩τ (ms'',s'')⟧
⟹ S,f ⊢ (ms,s) =a#as⇒⇩τ (ms'',s'')"

lemma silent_moves_equal_length:
assumes "S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from ‹S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')›
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule:silent_moves.induct)
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "length ms = length s" and "length ms' = length s'"
by(rule silent_move_equal_length)+
with ‹length ms' = length s' ∧ length ms'' = length s''›
show ?case by simp
qed simp
thus "length ms = length s" "length ms' = length s'" by simp_all
qed

lemma silent_moves_Append:
"⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s''); S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')⟧
⟹ S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')"
by(induct rule:silent_moves.induct)(auto intro:silent_moves.intros)

lemma silent_moves_split:
assumes "S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')"
obtains ms'' s'' where "S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s'')"
and "S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')"
proof(atomize_elim)
from ‹S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')›
show "∃ms'' s''. S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s'') ∧ S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')"
proof(induct as arbitrary:ms s)
case Nil
from ‹S,f ⊢ (ms,s) =[] @ as'⇒⇩τ (ms',s')› have "length ms = length s"
by(fastforce intro:silent_moves_equal_length)
hence "S,f ⊢ (ms,s) =[]⇒⇩τ (ms,s)" by(rule silent_moves_Nil)
with ‹S,f ⊢ (ms,s) =[] @ as'⇒⇩τ (ms',s')› show ?case by fastforce
next
case (Cons ax asx)
note IH = ‹⋀ms s. S,f ⊢ (ms,s) =asx @ as'⇒⇩τ (ms',s') ⟹
∃ms'' s''. S,f ⊢ (ms,s) =asx⇒⇩τ (ms'',s'') ∧ S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')›
from ‹S,f ⊢ (ms,s) =(ax # asx) @ as'⇒⇩τ (ms',s')›
obtain msx sx where "S,f ⊢ (ms,s) -ax→⇩τ (msx,sx)"
and "S,f ⊢ (msx,sx) =asx @ as'⇒⇩τ (ms',s')"
by(auto elim:silent_moves.cases)
from IH[OF this(2)] obtain ms'' s'' where "S,f ⊢ (msx,sx) =asx⇒⇩τ (ms'',s'')"
and "S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')" by blast
from ‹S,f ⊢ (ms,s) -ax→⇩τ (msx,sx)› ‹S,f ⊢ (msx,sx) =asx⇒⇩τ (ms'',s'')›
have "S,f ⊢ (ms,s) =ax#asx⇒⇩τ (ms'',s'')" by(rule silent_moves_Cons)
with ‹S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')› show ?case by blast
qed
qed

lemma valid_nodes_silent_moves:
"⟦S,f⊢ (ms,s) =as'⇒⇩τ (ms',s'); ∀m ∈ set ms. valid_node m⟧
⟹ ∀m ∈ set ms'. valid_node m"
proof(induct rule:silent_moves.induct)
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
note IH = ‹∀m∈set ms'. valid_node m ⟹ ∀m∈set ms''. valid_node m›
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')› ‹∀m∈set ms. valid_node m›
have "∀m∈set ms'. valid_node m"
apply - apply(erule silent_move.cases) apply auto
by(cases ms,auto dest:get_return_edges_valid)+
from IH[OF this] show ?case .
qed simp

lemma return_nodes_silent_moves:
"⟦S,f ⊢ (ms,s) =as'⇒⇩τ (ms',s'); ∀m ∈ set (tl ms). return_node m⟧
⟹ ∀m ∈ set (tl ms'). return_node m"
by(induct rule:silent_moves.induct,auto dest:silent_move_return_node)

lemma silent_moves_intra_path:
"⟦S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s'); ∀a ∈ set as. intra_kind(kind a)⟧
⟹ ms = ms' ∧ get_proc m = get_proc m'"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m
rule:silent_moves.induct)
case (silent_moves_Cons S f sx a msx' sx' as s'')
thus ?case
proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
case (silent_move_intra f a s s' n⇩c msx')
note IH = ‹⋀m. ⟦msx' = m # ms; ∀a∈set as. intra_kind (kind a)⟧
⟹ ms = ms' ∧ get_proc m = get_proc m'›
from ‹msx' = targetnode a # tl (m # ms)›
have "msx' = targetnode a # ms" by simp
from ‹∀a∈set (a # as). intra_kind (kind a)› have "∀a∈set as. intra_kind (kind a)"
by simp
from IH[OF ‹msx' = targetnode a # ms› this]
have "ms = ms'" and "get_proc (targetnode a) = get_proc m'" by simp_all
moreover
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
moreover
from ‹hd (m # ms) = sourcenode a› have "m = sourcenode a" by simp
ultimately show ?case using ‹ms = ms'› by simp
qed (auto simp:intra_kind_def)
qed simp

lemma silent_moves_nodestack_notempty:
"⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); ms ≠ []⟧ ⟹ ms' ≠ []"
apply(induct S f ms s as ms' s' rule:silent_moves.induct) apply auto
apply(erule silent_move.cases) apply auto
apply(case_tac "tl msa") by auto

lemma silent_moves_obs_slice:
"⟦S,kind ⊢ (ms,s) =as⇒⇩τ (ms',s'); mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙;
∀n ∈ set (tl ms'). return_node n⟧
⟹ mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀n ∈ set (tl ms). return_node n)"
proof(induct S f≡"kind" ms s as ms' s' rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S ms s a ms' s' as ms'' s'')
note IH = ‹⟦mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙; ∀m∈set (tl ms''). return_node m⟧
⟹ mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀m∈set (tl ms'). return_node m)›
from IH[OF ‹mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙› ‹∀m∈set (tl ms''). return_node m›]
have "mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" and "∀m∈set (tl ms'). return_node m"
by simp_all
with ‹S,kind ⊢ (ms,s) -a→⇩τ (ms',s')›
have "mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce intro:silent_move_obs_slice)
moreover
from ‹S,kind ⊢ (ms,s) -a→⇩τ (ms',s')› have "∀m∈set (tl ms). return_node m"
by(fastforce elim:silent_move.cases)
ultimately show ?case by simp
qed

lemma silent_moves_empty_obs_slice:
"⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}⟧
⟹ obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
note IH = ‹obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {} ⟹ obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}›
from IH[OF ‹obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {}›]
have "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}" by simp
with ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
show ?case by -(rule silent_move_empty_obs_slice,fastforce)
qed

lemma silent_moves_preds_transfers:
assumes "S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')"
shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
from ‹S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')›
have "preds (map f as) s ∧ transfers (map f as) s = s'"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "pred (f a) s" and "transfer (f a) s = s'" by(auto elim:silent_move.cases)
with ‹preds (map f as) s' ∧ transfers (map f as) s' = s''›
show ?case by fastforce
qed
thus "preds (map f as) s" and "transfers (map f as) s = s'" by simp_all
qed

lemma silent_moves_intra_path_obs:
assumes "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙" and "length s = length (m#msx')"
and "∀m ∈ set msx'. return_node m"
obtains as' where "S,slice_kind S ⊢ (m#msx',s) =as'⇒⇩τ (m'#msx',s)"
proof(atomize_elim)
from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
obtain as where "m -as→⇩ι* m'" and "m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by -(erule obs_intraE)
from ‹m -as→⇩ι* m'› obtain x where "distance m m' x" and "x ≤ length as"
by(erule every_path_distance)
from ‹distance m m' x› ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
show "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
proof(induct x arbitrary:m s rule:nat.induct)
fix m fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' 0" and "length s = length (m#msx')"
then obtain as' where "m -as'→⇩ι* m'" and "length as' = 0"
by(auto elim:distance.cases)
hence "m -[]→⇩ι* m'" by(cases as) auto
hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
with ‹length s = length (m#msx')›[THEN sym]
have "S,slice_kind S ⊢ (m#msx',s) =[]⇒⇩τ (m#msx',s)"
by -(rule silent_moves_Nil)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by simp blast
next
fix x m fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' (Suc x)" and "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
and IH:"⋀m s. ⟦distance m m' x; m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙;
length s = length (m#msx'); ∀m ∈ set msx'. return_node m⟧
⟹ ∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› have "valid_node m"
by(rule in_obs_intra_valid)
with ‹distance m m' (Suc x)› have "m ≠ m'"
by(fastforce elim:distance.cases dest:empty_path simp:intra_path_def)
have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume isin:"m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(fastforce intro!:n_in_obs_intra)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› ‹m ≠ m'› show False by simp
qed
from ‹distance m m' (Suc x)› obtain a where "valid_edge a" and "m = sourcenode a"
and "intra_kind(kind a)" and "distance (targetnode a) m' x"
and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m' x ∧
valid_edge a' ∧ intra_kind (kind a') ∧
targetnode a' = mx)"
by -(erule distance_successor_distance,simp+)
from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
by(rule obs_intra_singleton_element)
with ‹valid_edge a› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹intra_kind(kind a)›
have disj:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {} ∨
obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
by -(drule_tac S="⌊HRB_slice S⌋⇘CFG⇙" in edge_obs_intra_subset,auto)
from ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹m = sourcenode a›
have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
by(cases s)
(auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
from ‹distance (targetnode a) m' x› obtain asx where "targetnode a -asx→⇩ι* m'"
and "length asx = x" and "∀as'. targetnode a -as'→⇩ι* m' ⟶ x ≤ length as'"
by(auto elim:distance.cases)
from ‹targetnode a -asx→⇩ι* m'› ‹m' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
obtain mx where "mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(erule path_ex_obs_intra)
with disj have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from IH[OF ‹distance (targetnode a) m' x› this length
‹∀m ∈ set msx'. return_node m›]
obtain asx' where moves:"S,slice_kind S ⊢
(targetnode a#msx',transfer (slice_kind S a) s) =asx'⇒⇩τ
(m'#msx',transfer (slice_kind S a) s)" by blast
have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
proof(cases "kind a")
fix f assume "kind a = ⇑f"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› have "slice_kind S a = ⇑id"
by(fastforce intro:slice_kind_Upd)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q assume "kind a = (Q)⇩√"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› ‹distance (targetnode a) m' x›
‹distance m m' (Suc x)› target
have "slice_kind S a = (λs. True)⇩√"
by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q r p fs assume "kind a = Q:r↪⇘p⇙fs"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
next
fix Q p f assume "kind a = Q↩⇘p⇙f"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
qed
hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
by simp_all
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹valid_edge a›
‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
have "S,slice_kind S ⊢ (sourcenode a#msx',s) -a→⇩τ
(targetnode a#msx',transfer (slice_kind S a) s)"
by(fastforce intro:silent_move_intra)
with moves ‹transfer (slice_kind S a) s = s› ‹m = sourcenode a›
have "S,slice_kind S ⊢ (m#msx',s) =a#asx'⇒⇩τ (m'#msx',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by blast
qed
qed

lemma silent_moves_intra_path_no_obs:
assumes "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}" and "method_exit m'"
and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')"
and "∀m ∈ set msx'. return_node m"
obtains as where "S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
proof(atomize_elim)
from ‹method_exit m'› ‹get_proc m = get_proc m'› ‹valid_node m›
obtain as where "m -as→⇩ι* m'" by(erule intra_path_to_matching_method_exit)
then obtain x where "distance m m' x" and "x ≤ length as"
by(erule every_path_distance)
from ‹distance m m' x› ‹m -as→⇩ι* m'› ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}›
‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
show "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
proof(induct x arbitrary:m as s rule:nat.induct)
fix m fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' 0" and "length s = length (m#msx')"
then obtain as' where "m -as'→⇩ι* m'" and "length as' = 0"
by(auto elim:distance.cases)
hence "m -[]→⇩ι* m'" by(cases as) auto
hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
with ‹length s = length (m#msx')›[THEN sym]
have "S,slice_kind S ⊢ (m#msx',s) =[]⇒⇩τ (m#msx',s)"
by(fastforce intro:silent_moves_Nil)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by simp blast
next
fix x m as fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' (Suc x)" and "m -as→⇩ι* m'"
and "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
and IH:"⋀m as s. ⟦distance m m' x; m -as→⇩ι* m';
obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}; length s = length (m#msx');
∀m ∈ set msx'. return_node m⟧
⟹ ∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
from ‹m -as→⇩ι* m'› have "valid_node m"
by(fastforce intro:path_valid_node simp:intra_path_def)
from ‹m -as→⇩ι* m'› have "get_proc m = get_proc m'" by(rule intra_path_get_procs)
have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(fastforce intro!:n_in_obs_intra)
with ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
from ‹distance m m' (Suc x)› obtain a where "valid_edge a" and "m = sourcenode a"
and "intra_kind(kind a)" and "distance (targetnode a) m' x"
and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m' x ∧
valid_edge a' ∧ intra_kind (kind a') ∧
targetnode a' = mx)"
by -(erule distance_successor_distance,simp+)
from ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹m = sourcenode a›
have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
by(cases s)
(auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
from ‹distance (targetnode a) m' x› obtain asx where "targetnode a -asx→⇩ι* m'"
and "length asx = x" and "∀as'. targetnode a -as'→⇩ι* m' ⟶ x ≤ length as'"
by(auto elim:distance.cases)
from ‹valid_edge a› ‹intra_kind(kind a)› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹m = sourcenode a› ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}›
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
by(fastforce dest:edge_obs_intra_subset)
from IH[OF ‹distance (targetnode a) m' x› ‹targetnode a -asx→⇩ι* m'› this
length ‹∀m ∈ set msx'. return_node m›] obtain as'
where moves:"S,slice_kind S ⊢
(targetnode a#msx',transfer (slice_kind S a) s) =as'⇒⇩τ
(m'#msx',transfer (slice_kind S a) s)" by blast
have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
proof(cases "kind a")
fix f assume "kind a = ⇑f"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› have "slice_kind S a = ⇑id"
by(fastforce intro:slice_kind_Upd)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q assume "kind a = (Q)⇩√"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}› ‹distance (targetnode a) m' x›
‹distance m m' (Suc x)› ‹method_exit m'› ‹get_proc m = get_proc m'› target
have "slice_kind S a = (λs. True)⇩√"
by(fastforce intro:slice_kind_Pred_empty_obs_nearer_SOME)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q r p fs assume "kind a = Q:r↪⇘p⇙fs"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
next
fix Q p f assume "kind a = Q↩⇘p⇙f"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
qed
hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
by simp_all
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹valid_edge a›
‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
have "S,slice_kind S ⊢ (sourcenode a#msx',s) -a→⇩τ
(targetnode a#msx',transfer (slice_kind S a) s)"
by(fastforce intro:silent_move_intra)
with moves ‹transfer (slice_kind S a) s = s› ‹m = sourcenode a›
have "S,slice_kind S ⊢ (m#msx',s) =a#as'⇒⇩τ (m'#msx',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by blast
qed
qed

lemma silent_moves_vpa_path:
assumes "S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
and "ms = targetnodes rs" and "valid_return_list rs m"
and "length rs = length cs"
shows "m -as→* m'" and "valid_path_aux cs as"
proof -
from assms have "m -as→* m' ∧ valid_path_aux cs as"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m cs ms rs
rule:silent_moves.induct)
case (silent_moves_Nil msx sx n⇩c f)
from ‹valid_node m'› have "m' -[]→* m'"
by (rule empty_path)
thus ?case by fastforce
next
case (silent_moves_Cons S f sx a msx' sx' as s'')
thus ?case
proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
case (silent_move_intra f a sx sx' n⇩c msx')
note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs⟧
⟹ m -as→* m' ∧ valid_path_aux cs as›
from ‹msx' = targetnode a # tl (m # ms)›
have "msx' = targetnode a # ms" by simp
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)"
by(rule get_proc_intra)
with ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
have "valid_return_list rs (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from IH[OF ‹msx' = targetnode a # ms› this
‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹ms = targetnodes rs› ‹valid_return_list rs (targetnode a)›
‹length rs = length cs›]
have "targetnode a -as→* m'" and "valid_path_aux cs as" by simp_all
from ‹valid_edge a› ‹targetnode a -as→* m'›
‹hd (m # ms) = sourcenode a›
have "m -a#as→* m'" by(fastforce intro:Cons_path)
moreover
from ‹intra_kind (kind a)› ‹valid_path_aux cs as›
have "valid_path_aux cs (a # as)" by(fastforce simp:intra_kind_def)
ultimately show ?case by simp
next
case (silent_move_call f a sx sx' Q r p fs a' n⇩c msx')
note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs⟧
⟹ m -as→* m' ∧ valid_path_aux cs as›
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from ‹length rs = length cs›
have "length (a'#rs) = length (a#cs)" by simp
from ‹msx' = targetnode a # targetnode a' # tl (m # ms)›
have "msx' = targetnode a # targetnode a' # ms" by simp
from ‹ms = targetnodes rs› have "targetnode a' # ms = targetnodes (a' # rs)"
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
by(rule get_return_edges_valid)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
from ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "get_proc (sourcenode a) = get_proc (targetnode a')"
by(rule get_proc_get_return_edge)
with ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
‹get_proc (targetnode a) = p› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
have "valid_return_list (a' # rs) (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE) apply clarsimp
by(case_tac list)(auto simp:targetnodes_def)
from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹a' ∈ get_return_edges a›
have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
by auto(case_tac i,auto)
from IH[OF ‹msx' = targetnode a # targetnode a' # ms› ‹valid_node (targetnode a)› this
‹targetnode a' # ms = targetnodes (a' # rs)›
‹valid_return_list (a' # rs) (targetnode a)› ‹length (a'#rs) = length (a#cs)›]
have "targetnode a -as→* m'" and "valid_path_aux (a # cs) as" by simp_all
from ‹valid_edge a› ‹targetnode a -as→* m'›
‹hd (m # ms) = sourcenode a›
have "m -a#as→* m'" by(fastforce intro:Cons_path)
moreover
from ‹valid_path_aux (a # cs) as› ‹kind a = Q:r↪⇘p⇙fs›
have "valid_path_aux cs (a # as)" by simp
ultimately show ?case by simp
next
case (silent_move_return f a sx sx' Q p f' n⇩c msx')
note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs⟧
⟹ m -as→* m' ∧ valid_path_aux cs as›
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from ‹length (m # ms) = length sx› ‹length sx = Suc (length sx')›
‹sx' ≠ []›
obtain x xs where "ms = x#xs" by(cases ms) auto
with ‹ms = targetnodes rs› obtain r' rs' where "rs = r'#rs'"
and "x = targetnode r'" and "xs = targetnodes rs'"
by(auto simp:targetnodes_def)
with ‹length rs = length cs› obtain c' cs' where "cs = c'#cs'"
and "length rs' = length cs'"
by(cases cs) auto
from ‹ms = x#xs› ‹length (m # ms) = length sx›
‹length sx = Suc (length sx')›
have "length sx' = Suc (length xs)" by simp
from ‹ms = x#xs› ‹msx' = tl (m # ms)› ‹hd (tl (m # ms)) = targetnode a›
‹length (m # ms) = length sx› ‹length sx = Suc (length sx')› ‹sx' ≠ []›
have "msx' = targetnode a#xs" by simp
from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹rs = r'#rs'› ‹cs = c'#cs'›
have "r' ∈ get_return_edges c'" by fastforce
from ‹ms = x#xs› ‹hd (tl (m # ms)) = targetnode a›
have "x = targetnode a" by simp
with ‹valid_return_list rs m› ‹rs = r'#rs'› ‹x = targetnode r'›
have "valid_return_list rs' (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="r'#cs'" in allE) apply clarsimp
by(case_tac cs')(auto simp:targetnodes_def)
from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹rs = r'#rs'› ‹cs = c'#cs'›
have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
and "r' ∈ get_return_edges c'" by auto
from IH[OF ‹msx' = targetnode a#xs› ‹valid_node (targetnode a)›
‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)› ‹xs = targetnodes rs'›
‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'›]
have "targetnode a -as→* m'" and "valid_path_aux cs' as" by simp_all
from ‹valid_edge a› ‹targetnode a -as→* m'›
‹hd (m # ms) = sourcenode a›
have "m -a#as→* m'" by(fastforce intro:Cons_path)
moreover
from ‹ms = x#xs› ‹hd (tl (m # ms)) = targetnode a›
have "x = targetnode a" by simp
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
have "method_exit (sourcenode a)" by(fastforce simp:method_exit_def)
from ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
‹rs = r'#rs'›
have "get_proc (sourcenode a) = get_proc (sourcenode r') ∧
method_exit (sourcenode r') ∧ valid_edge r'"
apply(clarsimp simp:valid_return_list_def method_exit_def)
apply(erule_tac x="[]" in allE)
by(auto dest:get_proc_return)
hence "get_proc (sourcenode a) = get_proc (sourcenode r')"
and "method_exit (sourcenode r')" and "valid_edge r'" by simp_all
with ‹method_exit (sourcenode a)› have "sourcenode r' = sourcenode a"
by(fastforce intro:method_exit_unique)
with ‹valid_edge a› ‹valid_edge r'› ‹x = targetnode r'› ‹x = targetnode a›
have "r' = a" by(fastforce intro:edge_det)
with ‹r' ∈ get_return_edges c'› ‹valid_path_aux cs' as› ‹cs = c'#cs'›
‹kind a = Q↩⇘p⇙f'›
have "valid_path_aux cs (a # as)" by simp
ultimately show ?case by simp
qed
qed
thus "m -as→* m'" and "valid_path_aux cs as" by simp_all
qed

subsection ‹Observable moves›

inductive observable_move ::
"'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒
(('var ⇀ 'val) × 'ret) list ⇒ 'edge ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
("_,_ ⊢ '(_,_') -_→ '(_,_')" [51,50,0,0,50,0,0] 51)

where observable_move_intra:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length s' = length s; length ms = length s;
hd ms = sourcenode a; ms' = (targetnode a)#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→ (ms',s')"

| observable_move_call:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘p⇙fs;
valid_edge a'; a' ∈ get_return_edges a;
∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length ms = length s; length s' = Suc(length s);
hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→ (ms',s')"

| observable_move_return:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge ```