# Theory FundamentalProperty

```section ‹The fundamental property of slicing›

theory FundamentalProperty imports WeakSimulation SemanticsCFG begin

context SDG begin

subsection ‹Auxiliary lemmas for moves in the graph›

lemma observable_set_stack_in_slice:
"S,f ⊢ (ms,s) -a→ (ms',s')
⟹ ∀mx ∈ set (tl ms'). ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct rule:observable_move.induct)
case (observable_move_intra f a s s' ms S ms') thus ?case by simp
next
case (observable_move_call f a s s' Q r p fs a' ms S ms')
from ‹valid_edge a› ‹valid_edge a'› ‹a' ∈ get_return_edges a›
have "call_of_return_node (targetnode a') (sourcenode a)"
by(fastforce simp:return_node_def call_of_return_node_def)
with ‹hd ms = sourcenode a› ‹hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹ms' = targetnode a # targetnode a' # tl ms›
‹∀mx∈set (tl ms). ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
show ?case by fastforce
next
case (observable_move_return f a s s' Q p f' ms S ms')
thus ?case by(cases "tl ms") auto
qed

lemma silent_move_preserves_stacks:
assumes "S,f ⊢ (m#ms,s) -a→⇩τ (m'#ms',s')" and "valid_call_list cs m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
and "length rs = length cs" and "ms = targetnodes rs"
obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
and "valid_return_list rs' m'" and "length rs' = length cs'"
and "ms' = targetnodes rs'" and "upd_cs cs [a] = cs'"
proof(atomize_elim)
from assms show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
(∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
upd_cs cs [a] = cs'"
proof(induct S f "m#ms" s a "m'#ms'" s' rule:silent_move.induct)
case (silent_move_intra f a s s' n⇩c)
from ‹hd (m # ms) = sourcenode a› have "m = sourcenode a" by simp
from ‹m' # ms' = targetnode a # tl (m # ms)›
have [simp]:"m' = targetnode a" "ms' = ms" by simp_all
from ‹valid_edge a› have "valid_node m'" by simp
moreover
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
from ‹valid_call_list cs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_call_list cs m'"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
moreover
from ‹valid_return_list rs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_return_list rs m'"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
moreover
from ‹intra_kind (kind a)› have "upd_cs cs [a] = cs"
by(fastforce simp:intra_kind_def)
ultimately show ?case using ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹length rs = length cs› ‹ms = targetnodes rs›
apply(rule_tac x="cs" in exI)
apply(rule_tac x="rs" in exI)
by clarsimp
next
case (silent_move_call f a s s' Q r p fs a' S)
from ‹hd (m # ms) = sourcenode a›
‹m' # ms' = targetnode a # targetnode a' # tl (m # ms)›
have [simp]:"m = sourcenode a" "m' = targetnode a"
"ms' = targetnode a' # tl (m # ms)"
by simp_all
from ‹valid_edge a› have "valid_node m'" by simp
moreover
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
have "valid_call_list (a # cs) (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE)
by(case_tac list)(auto simp:sourcenodes_def)
moreover
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)
moreover
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'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
by(rule get_proc_return)
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› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
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)
by(case_tac list)(auto simp:targetnodes_def)
moreover
from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
moreover
from ‹ms = targetnodes rs› have "targetnode a' # ms = targetnodes (a' # rs)"
moreover
from ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs [a] = a#cs" by simp
ultimately show ?case
apply(rule_tac x="a#cs" in exI)
apply(rule_tac x="a'#rs" in exI)
by clarsimp
next
case (silent_move_return f a s s' Q p f' S)
from ‹hd (m # ms) = sourcenode a›
‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)› [symmetric]
have [simp]:"m = sourcenode a" "m' = targetnode a" by simp_all
from ‹length (m # ms) = length s› ‹length s = Suc (length s')› ‹s' ≠ []›
‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)›
have "ms = targetnode a # ms'"
by(cases ms) auto
with ‹ms = targetnodes rs›
obtain r' rs' where "rs = r' # rs'"
and "targetnode a = targetnode r'" and "ms' = targetnodes rs'"
by(cases rs)(auto simp:targetnodes_def)
moreover
from ‹rs = r' # rs'› ‹length rs = length cs› obtain c' cs' where "cs = c' # cs'"
and "length rs' = length cs'" by(cases cs) auto
moreover
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
moreover
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
moreover
from ‹valid_call_list cs m› ‹cs = c' # cs'›
obtain p' Q' r fs' where "valid_edge c'" and "kind c' = Q':r↪⇘p'⇙fs'"
and "p' = get_proc m"
apply(auto simp:valid_call_list_def)
by(erule_tac x="[]" in allE) auto
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
have "get_proc (sourcenode a) = p" by(rule get_proc_return)
with ‹p' = get_proc m› have [simp]:"p' = p" by simp
from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'›
have "get_proc (targetnode c') = p" by(fastforce intro:get_proc_call)
from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› have "valid_edge r'"
by(rule get_return_edges_valid)
from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'› ‹r' ∈ get_return_edges c'›
obtain Q'' f'' where "kind r' = Q''↩⇘p⇙f''" by(fastforce dest!:call_return_edges)
with ‹valid_edge r'› have "get_proc (sourcenode r') = p" by(rule get_proc_return)
from ‹valid_edge r'› ‹kind r' = Q''↩⇘p⇙f''› have "method_exit (sourcenode r')"
by(fastforce simp:method_exit_def)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'› have "method_exit (sourcenode a)"
by(fastforce simp:method_exit_def)
with ‹method_exit (sourcenode r')› ‹get_proc (sourcenode r') = p›
‹get_proc (sourcenode a) = p›
have "sourcenode a = sourcenode r'" by(fastforce intro:method_exit_unique)
with ‹valid_edge a› ‹valid_edge r'› ‹targetnode a = targetnode r'›
have "a = r'" by(fastforce intro:edge_det)
from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› ‹targetnode a = targetnode r'›
have "get_proc (sourcenode c') = get_proc (targetnode a)"
by(fastforce intro:get_proc_get_return_edge)
from ‹valid_call_list cs m› ‹cs = c' # cs'›
‹get_proc (sourcenode c') = get_proc (targetnode a)›
have "valid_call_list cs' (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="c' # cs'" in allE)
by(case_tac cs')(auto simp:sourcenodes_def)
moreover
from ‹valid_return_list rs m› ‹rs = r' # rs'› ‹targetnode a = targetnode r'›
have "valid_return_list rs' (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="r' # cs'" in allE)
by(case_tac cs')(auto simp:targetnodes_def)
moreover
from ‹kind a = Q↩⇘p⇙f'› ‹cs = c' # cs'› have "upd_cs cs [a] = cs'" by simp
ultimately show ?case
apply(rule_tac x="cs'" in exI)
apply(rule_tac x="rs'" in exI)
by clarsimp
qed
qed

lemma silent_moves_preserves_stacks:
assumes "S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')"
and "valid_node m" and "valid_call_list cs m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
and "length rs = length cs" and "ms = targetnodes rs"
obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
and "valid_return_list rs' m'" and "length rs' = length cs'"
and "ms' = targetnodes rs'" and "upd_cs cs as = cs'"
proof(atomize_elim)
from assms show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
(∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
upd_cs cs as = cs'"
proof(induct S f "m#ms" s as "m'#ms'" s'
arbitrary:m ms cs rs rule:silent_moves.induct)
case (silent_moves_Nil s n⇩c f)
thus ?case
apply(rule_tac x="cs" in exI)
apply(rule_tac x="rs" in exI)
by clarsimp
next
case (silent_moves_Cons S f s a msx'' s'' as sx')
note IH = ‹⋀m ms cs rs. ⟦msx'' = m # ms; valid_node m; valid_call_list cs m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
valid_return_list rs m; length rs = length cs; ms = targetnodes rs⟧
⟹ ∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
(∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
upd_cs cs as = cs'›
from ‹S,f ⊢ (m # ms,s) -a→⇩τ (msx'',s'')›
obtain m'' ms'' where "msx'' = m''#ms''"
by(cases msx'')(auto elim:silent_move.cases)
with ‹S,f ⊢ (m # ms,s) -a→⇩τ (msx'',s'')› ‹valid_call_list cs m›
‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹valid_return_list rs m›
‹length rs = length cs› ‹ms = targetnodes rs›
obtain cs'' rs'' where hyps:"valid_node m''" "valid_call_list cs'' m''"
"∀i < length rs''. rs''!i ∈ get_return_edges (cs''!i)"
"valid_return_list rs'' m''" "length rs'' = length cs''"
"ms'' = targetnodes rs''" and "upd_cs cs [a] = cs''"
by(auto elim!:silent_move_preserves_stacks)
from IH[OF _ hyps] ‹msx'' = m'' # ms''›
obtain cs' rs' where results:"valid_node m'" "valid_call_list cs' m'"
"∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
"valid_return_list rs' m'" "length rs' = length cs'" "ms' = targetnodes rs'"
and "upd_cs cs'' as = cs'" by blast
from ‹upd_cs cs [a] = cs''› ‹upd_cs cs'' as = cs'›
have "upd_cs cs ([a] @ as) = cs'" by(rule upd_cs_Append)
with results show ?case
apply(rule_tac x="cs'" in exI)
apply(rule_tac x="rs'" in exI)
by clarsimp
qed
qed

lemma observable_move_preserves_stacks:
assumes "S,f ⊢ (m#ms,s) -a→ (m'#ms',s')" and "valid_call_list cs m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
and "length rs = length cs" and "ms = targetnodes rs"
obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
and "valid_return_list rs' m'" and "length rs' = length cs'"
and "ms' = targetnodes rs'" and "upd_cs cs [a] = cs'"
proof(atomize_elim)
from assms show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
(∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
upd_cs cs [a] = cs'"
proof(induct S f "m#ms" s a "m'#ms'" s' rule:observable_move.induct)
case (observable_move_intra f a s s' n⇩c)
from ‹hd (m # ms) = sourcenode a› have "m = sourcenode a" by simp
from ‹m' # ms' = targetnode a # tl (m # ms)›
have [simp]:"m' = targetnode a" "ms' = ms" by simp_all
from ‹valid_edge a› have "valid_node m'" by simp
moreover
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
from ‹valid_call_list cs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_call_list cs m'"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
moreover
from ‹valid_return_list rs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_return_list rs m'"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
moreover
from ‹intra_kind (kind a)› have "upd_cs cs [a] = cs"
by(fastforce simp:intra_kind_def)
ultimately show ?case using ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹length rs = length cs› ‹ms = targetnodes rs›
apply(rule_tac x="cs" in exI)
apply(rule_tac x="rs" in exI)
by clarsimp
next
case (observable_move_call f a s s' Q r p fs a' S)
from ‹hd (m # ms) = sourcenode a›
‹m' # ms' = targetnode a # targetnode a' # tl (m # ms)›
have [simp]:"m = sourcenode a" "m' = targetnode a"
"ms' = targetnode a' # tl (m # ms)"
by simp_all
from ‹valid_edge a› have "valid_node m'" by simp
moreover
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
have "valid_call_list (a # cs) (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE)
by(case_tac list)(auto simp:sourcenodes_def)
moreover
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)
moreover
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'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
by(rule get_proc_return)
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› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
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)
by(case_tac list)(auto simp:targetnodes_def)
moreover
from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
moreover
from ‹ms = targetnodes rs› have "targetnode a' # ms = targetnodes (a' # rs)"
moreover
from ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs [a] = a#cs" by simp
ultimately show ?case
apply(rule_tac x="a#cs" in exI)
apply(rule_tac x="a'#rs" in exI)
by clarsimp
next
case (observable_move_return f a s s' Q p f' S)
from ‹hd (m # ms) = sourcenode a›
‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)› [symmetric]
have [simp]:"m = sourcenode a" "m' = targetnode a" by simp_all
from ‹length (m # ms) = length s› ‹length s = Suc (length s')› ‹s' ≠ []›
‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)›
have "ms = targetnode a # ms'"
by(cases ms) auto
with ‹ms = targetnodes rs›
obtain r' rs' where "rs = r' # rs'"
and "targetnode a = targetnode r'" and "ms' = targetnodes rs'"
by(cases rs)(auto simp:targetnodes_def)
moreover
from ‹rs = r' # rs'› ‹length rs = length cs› obtain c' cs' where "cs = c' # cs'"
and "length rs' = length cs'" by(cases cs) auto
moreover
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
moreover
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
moreover
from ‹valid_call_list cs m› ‹cs = c' # cs'›
obtain p' Q' r fs' where "valid_edge c'" and "kind c' = Q':r↪⇘p'⇙fs'"
and "p' = get_proc m"
apply(auto simp:valid_call_list_def)
by(erule_tac x="[]" in allE) auto
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
have "get_proc (sourcenode a) = p" by(rule get_proc_return)
with ‹p' = get_proc m› have [simp]:"p' = p" by simp
from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'›
have "get_proc (targetnode c') = p" by(fastforce intro:get_proc_call)
from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› have "valid_edge r'"
by(rule get_return_edges_valid)
from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'› ‹r' ∈ get_return_edges c'›
obtain Q'' f'' where "kind r' = Q''↩⇘p⇙f''" by(fastforce dest!:call_return_edges)
with ‹valid_edge r'› have "get_proc (sourcenode r') = p" by(rule get_proc_return)
from ‹valid_edge r'› ‹kind r' = Q''↩⇘p⇙f''› have "method_exit (sourcenode r')"
by(fastforce simp:method_exit_def)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'› have "method_exit (sourcenode a)"
by(fastforce simp:method_exit_def)
with ‹method_exit (sourcenode r')› ‹get_proc (sourcenode r') = p›
‹get_proc (sourcenode a) = p›
have "sourcenode a = sourcenode r'" by(fastforce intro:method_exit_unique)
with ‹valid_edge a› ‹valid_edge r'› ‹targetnode a = targetnode r'›
have "a = r'" by(fastforce intro:edge_det)
from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› ‹targetnode a = targetnode r'›
have "get_proc (sourcenode c') = get_proc (targetnode a)"
by(fastforce intro:get_proc_get_return_edge)
from ‹valid_call_list cs m› ‹cs = c' # cs'›
‹get_proc (sourcenode c') = get_proc (targetnode a)›
have "valid_call_list cs' (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="c' # cs'" in allE)
by(case_tac cs')(auto simp:sourcenodes_def)
moreover
from ‹valid_return_list rs m› ‹rs = r' # rs'› ‹targetnode a = targetnode r'›
have "valid_return_list rs' (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="r' # cs'" in allE)
by(case_tac cs')(auto simp:targetnodes_def)
moreover
from ‹kind a = Q↩⇘p⇙f'› ‹cs = c' # cs'› have "upd_cs cs [a] = cs'" by simp
ultimately show ?case
apply(rule_tac x="cs'" in exI)
apply(rule_tac x="rs'" in exI)
by clarsimp
qed
qed

lemma observable_moves_preserves_stack:
assumes "S,f ⊢ (m#ms,s) =as⇒ (m'#ms',s')"
and "valid_node m" and "valid_call_list cs m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
and "length rs = length cs" and "ms = targetnodes rs"
obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
and "valid_return_list rs' m'" and "length rs' = length cs'"
and "ms' = targetnodes rs'" and "upd_cs cs as = cs'"
proof(atomize_elim)
from ‹S,f ⊢ (m#ms,s) =as⇒ (m'#ms',s')› obtain msx s'' as' a'
where "as = as'@[a']" and "S,f ⊢ (m#ms,s) =as'⇒⇩τ (msx,s'')"
and "S,f ⊢ (msx,s'') -a'→ (m'#ms',s')"
by(fastforce elim:observable_moves.cases)
from ‹S,f ⊢ (msx,s'') -a'→ (m'#ms',s')› obtain m'' ms''
where [simp]:"msx = m''#ms''" by(cases msx)(auto elim:observable_move.cases)
from ‹S,f ⊢ (m#ms,s) =as'⇒⇩τ (msx,s'')› ‹valid_node m› ‹valid_call_list cs m›
‹∀i < length rs. rs!i ∈ get_return_edges (cs!i)› ‹valid_return_list rs m›
‹length rs = length cs› ‹ms = targetnodes rs›
obtain cs'' rs'' where "valid_node m''" and "valid_call_list cs'' m''"
and "∀i < length rs''. rs''!i ∈ get_return_edges (cs''!i)"
and "valid_return_list rs'' m''" and "length rs'' = length cs''"
and "ms'' = targetnodes rs''" and "upd_cs cs as' = cs''"
by(auto elim!:silent_moves_preserves_stacks)
with ‹S,f ⊢ (msx,s'') -a'→ (m'#ms',s')›
obtain cs' rs' where results:"valid_node m'" "valid_call_list cs' m'"
"∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
"valid_return_list rs' m'" "length rs' = length cs'" "ms' = targetnodes rs'"
and "upd_cs cs'' [a'] = cs'"
by(auto elim!:observable_move_preserves_stacks)
from ‹upd_cs cs as' = cs''› ‹upd_cs cs'' [a'] = cs'›
have "upd_cs cs (as'@[a']) = cs'" by(rule upd_cs_Append)
with ‹as = as'@[a']› results
show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
(∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
upd_cs cs as = cs'"
apply(rule_tac x="cs'" in exI)
apply(rule_tac x="rs'" in exI)
by clarsimp
qed

lemma silent_moves_slpa_path:
"⟦S,f ⊢ (m#ms''@ms,s) =as⇒⇩τ (m'#ms',s'); valid_node m; valid_call_list cs m;
∀i < length rs. rs!i ∈ get_return_edges (cs!i); valid_return_list rs m;
length rs = length cs; ms'' = targetnodes rs;
∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
ms'' ≠ [] ⟶ (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'"
proof(induct S f "m#ms''@ms" s as "m'#ms'" s' arbitrary:m ms'' ms cs rs
rule:silent_moves.induct)
case (silent_moves_Nil sx S f) thus ?case
apply(cases ms'' rule:rev_cases) apply(auto intro:empty_path simp:targetnodes_def)
by(cases rs rule:rev_cases,auto)+
next
case (silent_moves_Cons S f sx a msx' sx' as sx'')
thus ?case
proof(induct _ _ "m#ms''@ms" _ _ _ _ rule:silent_move.induct)
case (silent_move_intra f a s s' S msx')
note IH = ‹⋀m ms'' ms cs rs. ⟦msx' = m # ms'' @ ms; valid_node m;
valid_call_list cs m; ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
valid_return_list rs m; length rs = length cs; ms'' = targetnodes rs;
∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
ms'' ≠ [] ⟶
(∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'›
note callstack = ‹∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
note callstack'' = ‹ms'' ≠ [] ⟶
(∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note callstack' = ‹∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
from ‹hd (m # ms'' @ ms) = sourcenode a› have "m = sourcenode a"
by simp
from ‹valid_call_list cs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_call_list cs (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from ‹valid_return_list rs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode 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 ‹msx' = targetnode a # tl (m # ms'' @ ms)›
have "msx' = targetnode a # ms'' @ ms" by simp
from IH[OF this ‹valid_node (targetnode a)› ‹valid_call_list cs (targetnode a)›
‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹valid_return_list rs (targetnode a)› ‹length rs = length cs›
‹ms'' = targetnodes rs› callstack callstack'' callstack']
have "same_level_path_aux cs as" and "upd_cs cs as = []"
and "targetnode a -as→* m'" and "ms = ms'" by simp_all
from ‹intra_kind (kind a)› ‹same_level_path_aux cs as›
have "same_level_path_aux cs (a # as)" by(fastforce simp:intra_kind_def)
moreover
from ‹intra_kind (kind a)› ‹upd_cs cs as = []›
have "upd_cs cs (a # as) = []" by(fastforce simp:intra_kind_def)
moreover
from ‹valid_edge a› ‹m = sourcenode a› ‹targetnode a -as→* m'›
have "m -a # as→* m'" by(fastforce intro:Cons_path)
ultimately show ?case using ‹ms = ms'› by simp
next
case (silent_move_call f a s s' Q r p fs a' S msx')
note IH = ‹⋀m ms'' ms cs rs. ⟦msx' = m # ms'' @ ms; valid_node m; valid_call_list cs m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); valid_return_list rs m;
length rs = length cs; ms'' = targetnodes rs;
∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
ms'' ≠ [] ⟶
(∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'›
note callstack = ‹∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
note callstack'' = ‹ms'' ≠ [] ⟶
(∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note callstack' = ‹∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from ‹hd (m # ms'' @ ms) = sourcenode a› have "m = sourcenode a"
by simp
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
have "valid_call_list (a # cs) (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE)
by(case_tac list)(auto simp:sourcenodes_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 ‹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'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
by(rule get_proc_return)
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› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
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)
by(case_tac list)(auto simp:targetnodes_def)
from ‹length rs = length cs› have "length (a'#rs) = length (a # cs)" by simp
from ‹ms'' = targetnodes rs›
have "targetnode a' # ms'' = targetnodes (a'#rs)" by(simp add:targetnodes_def)
from ‹msx' = targetnode a # targetnode a' # tl (m # ms'' @ ms)›
have "msx' = targetnode a # targetnode a' # ms'' @ ms" by simp
have "∃mx'. call_of_return_node (last (targetnode a' # ms'')) mx' ∧
mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof(cases "ms'' = []")
case True
with ‹(∃m∈set (tl (m # ms'' @ ms)).
∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd (m # ms'' @ ms) ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› callstack
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
by(rule get_return_edges_valid)
with ‹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)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› True show ?thesis by fastforce
next
case False
with callstack'' show ?thesis by fastforce
qed
hence "targetnode a' # ms'' ≠ [] ⟶
(∃mx'. call_of_return_node (last (targetnode a' # ms'')) mx' ∧
mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)" by simp
from IH[OF _ ‹valid_node (targetnode a)› ‹valid_call_list (a # cs) (targetnode a)›
‹∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)›
‹valid_return_list (a'#rs) (targetnode a)› ‹length (a'#rs) = length (a # cs)›
‹targetnode a' # ms'' = targetnodes (a'#rs)› callstack this callstack']
‹msx' = targetnode a # targetnode a' # ms'' @ ms›
have "same_level_path_aux (a # cs) as" and "upd_cs (a # cs) as = []"
and "targetnode a -as→* m'" and "ms = ms'" by simp_all
from ‹kind a = Q:r↪⇘p⇙fs› ‹same_level_path_aux (a # cs) as›
have "same_level_path_aux cs (a # as)" by simp
moreover
from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs (a # cs) as = []› have "upd_cs cs (a # as) = []"
by simp
moreover
from ‹valid_edge a› ‹m = sourcenode a› ‹targetnode a -as→* m'›
have "m -a # as→* m'" by(fastforce intro:Cons_path)
ultimately show ?case using ‹ms = ms'› by simp
next
case (silent_move_return f a s s' Q p f' S msx')
note IH = ‹⋀m ms'' ms cs rs. ⟦msx' = m # ms'' @ ms; valid_node m;
valid_call_list cs m; ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
valid_return_list rs m; length rs = length cs; ms'' = targetnodes rs;
∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
ms'' ≠ [] ⟶
(∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'›
note callstack = ‹∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
note callstack'' = ‹ms'' ≠ [] ⟶
(∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note callstack' = ‹∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
have "ms'' ≠ []"
proof
assume "ms'' = []"
with callstack
‹∃m∈set (tl (m # ms'' @ ms)). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
show False by fastforce
qed
with ‹hd (tl (m # ms'' @ ms)) = targetnode a›
obtain xs where "ms'' = targetnode a # xs" by(cases ms'') auto
with ‹ms'' = targetnodes rs› obtain r' rs' where "rs = r' # rs'"
and "targetnode a = targetnode r'" and "xs = targetnodes rs'"
by(cases rs)(auto simp:targetnodes_def)
from ‹rs = r' # rs'› ‹length rs = length cs› obtain c' cs' where "cs = c' # cs'"
and "length rs' = length cs'" by(cases cs) auto
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 ‹valid_edge a› have "valid_node (targetnode a)" by simp
from ‹hd (m # ms'' @ ms) = sourcenode a› have "m = sourcenode a"
by simp
from ‹valid_call_list cs m› ‹cs = c' # cs'›
obtain p' Q' r fs' where "valid_edge c'" and "kind c' = Q':r↪⇘p'⇙fs'"
and "p' = get_proc m"
apply(auto simp:valid_call_list_def)
by(erule_tac x="[]" in allE) auto
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
have "get_proc (sourcenode a) = p" by(rule get_proc_return)
with ‹m = sourcenode a› ‹p' = get_proc m› have [simp]:"p' = p" by simp
from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'›
have "get_proc (targetnode c') = p" by(fastforce intro:get_proc_call)
from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› have "valid_edge r'"
by(rule get_return_edges_valid)
from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'› ‹r' ∈ get_return_edges c'›
obtain Q'' f'' where "kind r' = Q''↩⇘p⇙f''" by(fastforce dest!:call_return_edges)
with ‹valid_edge r'› have "get_proc (sourcenode r') = p" by(rule get_proc_return)
from ‹valid_edge r'› ‹kind r' = Q''↩⇘p⇙f''› have "method_exit (sourcenode r')"
by(fastforce simp:method_exit_def)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'› have "method_exit (sourcenode a)"
by(fastforce simp:method_exit_def)
with ‹method_exit (sourcenode r')› ‹get_proc (sourcenode r') = p›
‹get_proc (sourcenode a) = p›
have "sourcenode a = sourcenode r'" by(fastforce intro:method_exit_unique)
with ‹valid_edge a› ‹valid_edge r'› ‹targetnode a = targetnode r'›
have "a = r'" by(fastforce intro:edge_det)
from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› ‹targetnode a = targetnode r'›
have "get_proc (sourcenode c') = get_proc (targetnode a)"
by(fastforce intro:get_proc_get_return_edge)
from ‹valid_call_list cs m› ‹cs = c' # cs'›
‹get_proc (sourcenode c') = get_proc (targetnode a)›
have "valid_call_list cs' (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="c' # cs'" in allE)
by(case_tac cs')(auto simp:sourcenodes_def)
from ‹valid_return_list rs m› ‹rs = r' # rs'› ‹targetnode a = targetnode r'›
have "valid_return_list rs' (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="r' # cs'" in allE)
by(case_tac cs')(auto simp:targetnodes_def)
from ‹msx' = tl (m # ms'' @ ms)› ‹ms'' = targetnode a # xs›
have "msx' = targetnode a # xs @ ms" by simp
from callstack'' ‹ms'' = targetnode a # xs›
have "xs ≠ [] ⟶
(∃mx'. call_of_return_node (last xs) mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by fastforce
from IH[OF ‹msx' = targetnode a # xs @ ms› ‹valid_node (targetnode a)›
‹valid_call_list cs' (targetnode a)›
‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)›
‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'›
‹xs = targetnodes rs'› callstack this callstack']
have "same_level_path_aux cs' as" and "upd_cs cs' as = []"
and "targetnode a -as→* m'" and "ms = ms'" by simp_all
from ‹kind a = Q↩⇘p⇙f'› ‹same_level_path_aux cs' as› ‹cs = c' # cs'›
‹r' ∈ get_return_edges c'› ‹a = r'›
have "same_level_path_aux cs (a # as)" by simp
moreover
from ‹upd_cs cs' as = []› ‹kind a = Q↩⇘p⇙f'› ‹cs = c' # cs'›
have "upd_cs cs (a # as) = []" by simp
moreover
from ‹valid_edge a› ‹m = sourcenode a› ‹targetnode a -as→* m'›
have "m -a # as→* m'" by(fastforce intro:Cons_path)
ultimately show ?case using ‹ms = ms'› by simp
qed
qed

lemma silent_moves_slp:
"⟦S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s'); valid_node m;
∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
⟹ m -as→⇘sl⇙* m' ∧ ms = ms'"
by(fastforce dest!:silent_moves_slpa_path
[of _ _ _ "[]" _ _ _ _ _ _ "[]" "[]",simplified]
simp:targetnodes_def valid_call_list_def valid_return_list_def
same_level_path_def slp_def)

lemma slpa_silent_moves_callstacks_eq:
"⟦same_level_path_aux cs as; S,f ⊢ (m#msx@ms,s) =as⇒⇩τ (m'#ms',s');
length ms = length ms'; valid_call_list cs m;
∀i < length rs. rs!i ∈ get_return_edges (cs!i); valid_return_list rs m;
length rs = length cs; msx = targetnodes rs⟧
⟹ ms = ms'"
proof(induct arbitrary:m msx s rs rule:slpa_induct)
case (slpa_empty cs)
from ‹S,f ⊢ (m # msx @ ms,s) =[]⇒⇩τ (m' # ms',s')›
have "msx@ms = ms'" by(fastforce elim:silent_moves.cases)
with ‹length ms = length ms'› show ?case by fastforce
next
case (slpa_intra cs a as)
note IH = ‹⋀m msx s rs. ⟦S,f ⊢ (m # msx @ ms,s) =as⇒⇩τ (m' # ms',s');
length ms = length ms'; valid_call_list cs m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
valid_return_list rs m; length rs = length cs; msx = targetnodes rs⟧
⟹ ms = ms'›
from ‹S,f ⊢ (m # msx @ ms,s) =a # as⇒⇩τ (m' # ms',s')› obtain ms'' s''
where "S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')"
and "S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')"
by(auto elim:silent_moves.cases)
from ‹S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')› ‹intra_kind (kind a)›
have "valid_edge a" and [simp]:"m = sourcenode a" "ms'' = targetnode a # msx @ ms"
by(fastforce elim:silent_move.cases simp:intra_kind_def)+
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
from ‹valid_call_list cs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_call_list cs (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from ‹valid_return_list rs m› ‹m = sourcenode a›
‹get_proc (sourcenode a) = get_proc (targetnode 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 ‹S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')›
have "S,f ⊢ (targetnode a # msx @ ms,s'') =as⇒⇩τ (m' # ms',s')" by simp
from IH[OF this ‹length ms = length ms'› ‹valid_call_list cs (targetnode a)›
‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹valid_return_list rs (targetnode a)› ‹length rs = length cs›
‹msx = targetnodes rs›] show ?case .
next
case (slpa_Call cs a as Q r p fs)
note IH = ‹⋀m msx s rs. ⟦S,f ⊢ (m # msx @ ms,s) =as⇒⇩τ (m' # ms',s');
length ms = length ms'; valid_call_list (a # cs) m;
∀i<length rs. rs ! i ∈ get_return_edges ((a # cs) ! i);
valid_return_list rs m; length rs = length (a # cs);
msx = targetnodes rs⟧
⟹ ms = ms'›
from ‹S,f ⊢ (m # msx @ ms,s) =a # as⇒⇩τ (m' # ms',s')› obtain ms'' s''
where "S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')"
and "S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')"
by(auto elim:silent_moves.cases)
from ‹S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')› ‹kind a = Q:r↪⇘p⇙fs›
obtain a' where "valid_edge a" and [simp]:"m = sourcenode a"
and [simp]:"ms'' = targetnode a # targetnode a' # msx @ ms"
and "a' ∈ get_return_edges a"
by(auto elim:silent_move.cases simp:intra_kind_def)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
have "valid_call_list (a # cs) (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE)
by(case_tac list)(auto simp:sourcenodes_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 ‹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'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
by(rule get_proc_return)
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› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
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)
by(case_tac list)(auto simp:targetnodes_def)
from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
from ‹msx = targetnodes rs› have "targetnode a' # msx = targetnodes (a' # rs)"
from ‹S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')›
have "S,f ⊢ (targetnode a # (targetnode a' # msx) @ ms,s'') =as⇒⇩τ (m' # ms',s')"
by simp
from IH[OF this ‹length ms = length ms'› ‹valid_call_list (a # cs) (targetnode a)›
‹∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)›
‹valid_return_list (a'#rs) (targetnode a)› ‹length (a'#rs) = length (a#cs)›
‹targetnode a' # msx = targetnodes (a' # rs)›] show ?case .
next
case (slpa_Return cs a as Q p f' c' cs')
note IH = ‹⋀m msx s rs. ⟦S,f ⊢ (m # msx @ ms,s) =as⇒⇩τ (m' # ms',s');
length ms = length ms'; valid_call_list cs' m;
∀i<length rs. rs ! i ∈ get_return_edges (cs' ! i); valid_return_list rs m;
length rs = length cs'; msx = targetnodes rs⟧
⟹ ms = ms'›
from ‹S,f ⊢ (m # msx @ ms,s) =a # as⇒⇩τ (m' # ms',s')› obtain ms'' s''
where "S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')"
and "S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')"
by(auto elim:silent_moves.cases)
from ‹S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')› ‹kind a = Q↩⇘p⇙f'›
have "valid_edge a" and "m = sourcenode a" and "hd (msx @ ms) = targetnode a"
and "ms'' = msx @ ms" and "s'' ≠ []" and "length s = Suc(length s'')"
and "length (m # msx @ ms) = length s"
by(auto elim:silent_move.cases simp:intra_kind_def)
from ‹msx = targetnodes rs› ‹length rs = length cs› ‹cs = c' # cs'›
obtain mx' msx' where "msx = mx'#msx'"
by(cases msx)(fastforce simp:targetnodes_def)+
with ‹hd (msx @ ms) = targetnode a› have "mx' = targetnode a" by simp
from ‹valid_call_list cs m› ‹cs = c' # cs'› have "valid_edge c'"
by(fastforce simp:valid_call_list_def)
from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
have "get_proc (sourcenode c') = get_proc (targetnode a)"
by(rule get_proc_get_return_edge)
from ‹valid_call_list cs m› ‹cs = c' # cs'›
‹get_proc (sourcenode c') = get_proc (targetnode a)›
have "valid_call_list cs' (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="c' # cs'" in allE)
by(case_tac cs')(auto simp:sourcenodes_def)
from ‹length rs = length cs› ‹cs = c' # cs'› obtain r' rs'
where [simp]:"rs = r'#rs'" and "length rs' = length cs'" by(cases rs) auto
from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹cs = c' # cs'›
have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
and "r' ∈ get_return_edges c'" by auto
with ‹valid_edge c'› ‹a ∈ get_return_edges c'› have [simp]:"a = r'"
by -(rule get_return_edges_unique)
with ‹valid_return_list rs m›
have "valid_return_list rs' (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="r' # cs'" in allE)
by(case_tac cs')(auto simp:targetnodes_def)
from ‹msx = targetnodes rs› ‹msx = mx'#msx'› ‹rs = r'#rs'›
have "msx' = targetnodes rs'" by(simp add:targetnodes_def)
from ‹S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')› ‹msx = mx'#msx'›
‹ms'' = msx @ ms› ‹mx' = targetnode a›
have "S,f ⊢ (targetnode a # msx' @ ms,s'') =as⇒⇩τ (m' # ms',s')" by simp
from IH[OF this ‹length ms = length ms'› ‹valid_call_list cs' (targetnode a)›
‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)›
‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'›
‹msx' = targetnodes rs'›] show ?case .
qed

lemma silent_moves_same_level_path:
assumes "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "m -as→⇘sl⇙* m'" shows "ms = ms'"
proof -
from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› obtain cf cfs where "s = cf#cfs"
by(cases s)(auto dest:silent_moves_equal_length)
with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')›
have "transfers (kinds as) (cf#cfs) = s'"
by(fastforce intro:silent_moves_preds_transfers simp:kinds_def)
with ‹m -as→⇘sl⇙* m'› obtain cf' where "s' = cf'#cfs"
by -(drule slp_callstack_length_equal,auto)
from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')›
have "length (m#ms) = length s" and "length (m'#ms') = length s'"
by(rule silent_moves_equal_length)+
with ‹s = cf#cfs› ‹s' = cf'#cfs› have "length ms = length ms'" by simp
from ‹m -as→⇘sl⇙* m'› have "same_level_path_aux [] as"
with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹length ms = length ms'›
show ?thesis by(auto elim!:slpa_silent_moves_callstacks_eq
simp:targetnodes_def valid_call_list_def valid_return_list_def)
qed

lemma silent_moves_call_edge:
assumes "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
and callstack:"∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
and rest:"∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
"ms = targetnodes rs" "valid_return_list rs m" "length rs = length cs"
obtains as' a as'' where "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
and "call_of_return_node (hd ms') (sourcenode a)"
and "targetnode a -as''→⇘sl⇙* m'"
| "ms' = ms"
proof(atomize_elim)
from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')›
show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r↪⇘p⇙fs) ∧
call_of_return_node (hd ms') (sourcenode a) ∧ targetnode a -as''→⇘sl⇙* m') ∨
ms' = ms"
proof(induct as arbitrary:m' ms' s' rule:length_induct)
fix as m' ms' s'
assume IH:"∀as'. length as' < length as ⟶
(∀mx msx sx. S,kind ⊢ (m#ms,s) =as'⇒⇩τ (mx#msx,sx) ⟶
(∃asx a asx'. as' = asx @ a # asx' ∧ (∃Q r p fs. kind a = Q:r↪⇘p⇙fs) ∧
call_of_return_node (hd msx) (sourcenode a) ∧ targetnode a -asx'→⇘sl⇙* mx) ∨
msx = ms)"
and "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')"
show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r↪⇘p⇙fs) ∧
call_of_return_node (hd ms') (sourcenode a) ∧ targetnode a -as''→⇘sl⇙* m') ∨
ms' = ms"
proof(cases as rule:rev_cases)
case Nil
with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› have "ms = ms'"
by(fastforce elim:silent_moves.cases)
thus ?thesis by simp
next
case (snoc as' a')
with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')›
obtain ms'' s'' where "S,kind ⊢ (m#ms,s) =as'⇒⇩τ (ms'',s'')"
and "S,kind ⊢ (ms'',s'') =[a']⇒⇩τ (m'#ms',s')"
by(fastforce elim:silent_moves_split)
from snoc have "length as' < length as" by simp
from ‹S,kind ⊢ (ms'',s'') =[a']⇒⇩τ (m'#ms',s')›
have "S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')"
by(fastforce elim:silent_moves.cases)
show ?thesis
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')›
have "valid_edge a'" and "m' = targetnode a'"
by(auto elim:silent_move.cases simp:intra_kind_def)
from ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')› ‹intra_kind (kind a')›
have "ms'' = sourcenode a'#ms'"
by -(erule silent_move.cases,auto simp:intra_kind_def,(cases ms'',auto)+)
with IH ‹length as' < length as› ‹S,kind ⊢ (m#ms,s) =as'⇒⇩τ (ms'',s'')›
have "(∃asx ax asx'. as' = asx @ ax # asx' ∧ (∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
call_of_return_node (hd ms') (sourcenode ax) ∧
targetnode ax -asx'→⇘sl⇙* sourcenode a') ∨ ms' = ms"
by simp blast
thus ?thesis
proof
assume "∃asx ax asx'. as' = asx @ ax # asx' ∧
(∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
call_of_return_node (hd ms') (sourcenode ax) ∧
targetnode ax -asx'→⇘sl⇙* sourcenode a'"
then obtain asx ax asx' where "as' = asx @ ax # asx'"
and "∃Q r p fs. kind ax = Q:r↪⇘p⇙fs"
and "call_of_return_node (hd ms') (sourcenode ax)"
and "targetnode ax -asx'→⇘sl⇙* sourcenode a'"
by blast
from ‹as' = asx @ ax # asx'› have "as'@[a'] = asx @ ax # (asx' @ [a'])"
by simp
moreover
from ‹targetnode ax -asx'→⇘sl⇙* sourcenode a'› ‹intra_kind (kind a')›
‹m' = targetnode a'› ‹valid_edge a'›
have "targetnode ax -asx'@[a']→⇘sl⇙* m'"
by(fastforce intro:path_Append path_edge same_level_path_aux_Append
upd_cs_Append simp:slp_def same_level_path_def intra_kind_def)
ultimately show ?thesis using ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
‹call_of_return_node (hd ms') (sourcenode ax)› snoc by blast
next
assume "ms' = ms" thus ?thesis by simp
qed
next
case (Call Q r p fs)
with ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')› obtain a''
where "valid_edge a'" and "a'' ∈ get_return_edges a'"
and "hd ms'' = sourcenode a'" and "m' = targetnode a'"
and "ms' = (targetnode a'')#tl ms''" and "length ms'' = length s''"
and "pred (kind a') s''"
by(auto elim:silent_move.cases simp:intra_kind_def)
from ‹valid_edge a'› ‹a'' ∈ get_return_edges a'› have "valid_edge a''"
by(rule get_return_edges_valid)
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'› ‹valid_edge a''›
‹a'' ∈ get_return_edges a'› ‹ms' = (targetnode a'')#tl ms''›
have "call_of_return_node (hd ms') (sourcenode a')"
with snoc ‹kind a' = Q:r↪⇘p⇙fs› ‹m' = targetnode a'› ‹valid_edge a'›
show ?thesis by(fastforce intro:empty_path simp:slp_def same_level_path_def)
next
case (Return Q p f)
with ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')›
have "valid_edge a'" and "hd ms'' = sourcenode a'"
and "hd(tl ms'') = targetnode a'" and "m'#ms' = tl ms''"
and "length ms'' = length s''" and "length s'' = Suc(length s')"
and "s' ≠ []"
by(auto elim:silent_move.cases simp:intra_kind_def)
hence "ms'' = sourcenode a' # targetnode a' # ms'" by(cases ms'') auto
with ‹length as' < length as› ‹S,kind ⊢ (m#ms,s) =as'⇒⇩τ (ms'',s'')› IH
have "(∃asx ax asx'. as' = asx @ ax # asx' ∧ (∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
call_of_return_node (targetnode a') (sourcenode ax) ∧
targetnode ax -asx'→⇘sl⇙* sourcenode a') ∨ ms = targetnode a' # ms'"
apply - apply(erule_tac x="as'" in allE) apply clarsimp
apply(erule_tac x="sourcenode a'" in allE)
apply(erule_tac x="targetnode a' # ms'" in allE)
by fastforce
thus ?thesis
proof
assume "∃asx ax asx'. as' = asx @ ax # asx' ∧
(∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
call_of_return_node (targetnode a') (sourcenode ax) ∧
targetnode ax -asx'→⇘sl⇙* sourcenode a'"
then obtain asx ax asx' where "as' = asx @ ax # asx'"
and "∃Q r p fs. kind ax = Q:r↪⇘p⇙fs"
and "call_of_return_node (targetnode a') (sourcenode ax)"
and "targetnode ax -asx'→⇘sl⇙* sourcenode a'" by blast
from ‹as' = asx @ ax # asx'› snoc have"length asx < length as" by simp
moreover
from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› snoc ‹as' = asx @ ax # asx'›
obtain msx sx where "S,kind ⊢ (m#ms,s) =asx⇒⇩τ (msx,sx)"
and "S,kind ⊢ (msx,sx) =ax#asx'@[a']⇒⇩τ (m'#ms',s')"
by(fastforce elim:silent_moves_split)
from ‹S,kind ⊢ (msx,sx) =ax#asx'@[a']⇒⇩τ (m'#ms',s')›
obtain xs x ys y where "S,kind ⊢ (msx,sx) -ax→⇩τ (xs,x)"
and "S,kind ⊢ (xs,x) =asx'⇒⇩τ (ys,y)"
and "S,kind ⊢ (ys,y) =[a']⇒⇩τ (m'#ms',s')"
apply - apply(erule silent_moves.cases) apply auto
by(erule silent_moves_split) auto
from ‹S,kind ⊢ (msx,sx) -ax→⇩τ (xs,x)› ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
obtain msx' ax' where "msx = sourcenode ax#msx'"
and "ax' ∈ get_return_edges ax"
and [simp]:"xs = (targetnode ax)#(targetnode ax')#msx'"
and "length x = Suc(length sx)" and "length msx = length sx"
apply - apply(erule silent_move.cases) apply(auto simp:intra_kind_def)
by(cases msx,auto)+
from ‹S,kind ⊢ (ys,y) =[a']⇒⇩τ (m'#ms',s')› obtain msy
where "ys = sourcenode a'#msy"
apply - apply(erule silent_moves.cases) apply auto
apply(erule silent_move.cases)
by(cases ys,auto)+
with ‹S,kind ⊢ (xs,x) =asx'⇒⇩τ (ys,y)›
‹targetnode ax -asx'→⇘sl⇙* sourcenode a'›
‹xs = (targetnode ax)#(targetnode ax')#msx'›
have "(targetnode ax')#msx' = msy" apply simp
by(fastforce intro:silent_moves_same_level_path)
with ‹S,kind ⊢ (ys,y) =[a']⇒⇩τ (m'#ms',s')› ‹kind a' = Q↩⇘p⇙f›
‹ys = sourcenode a'#msy›
have "m' = targetnode a'" and "msx' = ms'"
by(fastforce elim:silent_moves.cases silent_move.cases
simp:intra_kind_def)+
with ‹S,kind ⊢ (m#ms,s) =asx⇒⇩τ (msx,sx)› ‹msx = sourcenode ax#msx'›
have "S,kind ⊢ (m#ms,s) =asx⇒⇩τ (sourcenode ax#ms',sx)" by simp
ultimately have "(∃xs x xs'. asx = xs@x#xs' ∧
(∃Q r p fs. kind x = Q:r↪⇘p⇙fs) ∧
call_of_return_node (hd ms') (sourcenode x) ∧
targetnode x -xs'→⇘sl⇙* sourcenode ax) ∨ ms = ms'" using IH
by simp blast
thus ?thesis
proof
assume "∃xs x xs'. asx = xs@x#xs' ∧ (∃Q r p fs. kind x = Q:r↪⇘p⇙fs) ∧
call_of_return_node (hd ms') (sourcenode x) ∧
targetnode x -xs'→⇘sl⇙* sourcenode ax"
then obtain xs x xs' where "asx = xs@x#xs'"
and "∃Q r p fs. kind x = Q:r↪⇘p⇙fs"
and "call_of_return_node (hd ms') (sourcenode x)"
and "targetnode x -xs'→⇘sl⇙* sourcenode ax" by blast
from ‹asx = xs@x#xs'› ‹as' = asx @ ax # asx'› snoc
have "as = xs@x#(xs'@ax#asx'@[a'])" by simp
from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹valid_node m› rest
have "m -as→* m'" and "valid_path_aux cs as"
by(auto dest:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ rs cs]
simp:valid_call_list_def valid_return_list_def targetnodes_def)
hence "m -as→⇩√* m'"
by(fastforce intro:valid_path_aux_valid_path simp:vp_def)
with snoc have "m -as'→⇩√* sourcenode a'"
by(auto elim:path_split_snoc dest:valid_path_aux_split
simp:vp_def valid_path_def)
with ‹as' = asx @ ax # asx'›
have "valid_edge ax" and "targetnode ax -asx'→* sourcenode a'"
by(auto dest:path_split simp:vp_def)
hence "sourcenode ax -ax#asx'→* sourcenode a'"
by(fastforce intro:Cons_path)
from ‹valid_edge a'› have "sourcenode a' -[a']→* targetnode a'"
by(rule path_edge)
with ‹sourcenode ax -ax#asx'→* sourcenode a'›
have "sourcenode ax -(ax#asx')@[a']→* targetnode a'"
by(rule path_Append)
from ‹m -as→⇩√* m'› snoc ‹as' = asx @ ax # asx'› snoc
have "valid_path_aux ([]@(upd_cs [] asx)) (ax # asx' @ [a'])"
by(fastforce dest:valid_path_aux_split simp:vp_def valid_path_def)
hence "valid_path_aux [] (ax#asx'@[a'])"
by(rule valid_path_aux_callstack_prefix)
with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
have "valid_path_aux [ax] (asx'@[a'])" by fastforce
hence "valid_path_aux (upd_cs [ax] asx') [a']"
by(rule valid_path_aux_split)
from ‹targetnode ax -asx'→⇘sl⇙* sourcenode a'›
have "same_level_path_aux [] asx'" and "upd_cs [] asx' = []"
hence "upd_cs ([]@[ax]) asx' = []@[ax]"
by(rule same_level_path_upd_cs_callstack_Append)
with ‹valid_path_aux (upd_cs [ax] asx') [a']›
have "valid_path_aux [ax] [a']" by(simp del:valid_path_aux.simps)
with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs› ‹kind a' = Q↩⇘p⇙f›
have "a' ∈ get_return_edges ax" by simp
with ‹upd_cs ([]@[ax]) asx' = []@[ax]› ‹kind a' = Q↩⇘p⇙f›
have "upd_cs [ax] (asx'@[a']) = []" by(fastforce intro:upd_cs_Append)
with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
have "upd_cs [] (ax#asx'@[a']) = []" by fastforce
from ‹targetnode ax -asx'→⇘sl⇙* sourcenode a'›
have "same_level_path_aux [] asx'" and "upd_cs [] asx' = []"
hence "same_level_path_aux ([]@[ax]) asx'"
by -(rule same_level_path_aux_callstack_Append)
with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs› ‹kind a' = Q↩⇘p⇙f›
‹a' ∈ get_return_edges ax› ‹upd_cs ([]@[ax]) asx' = []@[ax]›
have "same_level_path_aux [] ((ax#asx')@[a'])"
by(fastforce intro:same_level_path_aux_Append)
with ‹upd_cs [] (ax#asx'@[a']) = []›
‹sourcenode ax -(ax#asx')@[a']→* targetnode a'›
have "sourcenode ax -(ax#asx')@[a']→⇘sl⇙* targetnode a'"
with ‹targetnode x -xs'→⇘sl⇙* sourcenode ax›
have "targetnode x -xs'@((ax#asx')@[a'])→⇘sl⇙* targetnode a'"
by(rule slp_Append)
with ‹∃Q r p fs. kind x = Q:r↪⇘p⇙fs›
‹call_of_return_node (hd ms') (sourcenode x)›
‹as = xs@x#(xs'@ax#asx'@[a'])› ‹m' = targetnode a'›
show ?thesis by simp blast
next
assume "ms = ms'" thus ?thesis by simp
qed
next
assume "ms = targetnode a' # ms'"
from ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')› ‹kind a' = Q↩⇘p⇙f›
‹ms'' = sourcenode a' # targetnode a' # ms'›
have "∃m ∈ set (targetnode a' # ms'). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce elim!:silent_move.cases simp:intra_kind_def)
with ‹ms = targetnode a' # ms'› callstack
have False by fastforce
thus ?thesis by simp
qed
qed
qed
qed
qed

lemma silent_moves_called_node_in_slice1_hd_nodestack_in_slice1:
assumes "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
and "CFG_node m' ∈ sum_SDG_slice1 nx"
and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
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"
obtains as' a as'' where "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
and "call_of_return_node (hd ms') (sourcenode a)"
and "targetnode a -as''→⇘sl⇙* m'" and "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx"
| "ms' = ms"
proof(atomize_elim)
from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹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›
have "m -as→* m'"
by(auto dest:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ rs cs]
simp:valid_call_list_def valid_return_list_def targetnodes_def)
from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹valid_node m›
‹∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
‹∀i < length rs.```