Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory FundamentalPropertyheader {* \isaheader{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 \<turnstile> (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 \<turnstile> (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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges a`
obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'" by(fastforce dest!:call_return_edges)
from `valid_edge a'` `kind a' = Q'\<hookleftarrow>⇘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'\<hookleftarrow>⇘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)"
by(simp add:targetnodes_def)
moreover
from `kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p'⇙fs'` `r' ∈ get_return_edges c'`
obtain Q'' f'' where "kind r' = Q''\<hookleftarrow>⇘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''\<hookleftarrow>⇘p⇙f''` have "method_exit (sourcenode r')"
by(fastforce simp:method_exit_def)
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘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(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\<hookleftarrow>⇘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 \<turnstile> (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 \<turnstile> (m # ms,s) -a->⇣τ (msx'',s'')`
obtain m'' ms'' where "msx'' = m''#ms''"
by(cases msx'')(auto elim:silent_move.cases)
with `S,f \<turnstile> (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 \<turnstile> (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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges a`
obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'" by(fastforce dest!:call_return_edges)
from `valid_edge a'` `kind a' = Q'\<hookleftarrow>⇘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'\<hookleftarrow>⇘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)"
by(simp add:targetnodes_def)
moreover
from `kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p'⇙fs'` `r' ∈ get_return_edges c'`
obtain Q'' f'' where "kind r' = Q''\<hookleftarrow>⇘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''\<hookleftarrow>⇘p⇙f''` have "method_exit (sourcenode r')"
by(fastforce simp:method_exit_def)
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘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(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\<hookleftarrow>⇘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 \<turnstile> (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 \<turnstile> (m#ms,s) =as=> (m'#ms',s')` obtain msx s'' as' a'
where "as = as'@[a']" and "S,f \<turnstile> (m#ms,s) =as'=>⇣τ (msx,s'')"
and "S,f \<turnstile> (msx,s'') -a'-> (m'#ms',s')"
by(fastforce elim:observable_moves.cases)
from `S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges a`
obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'" by(fastforce dest!:call_return_edges)
from `valid_edge a'` `kind a' = Q'\<hookleftarrow>⇘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'\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p'⇙fs'` `r' ∈ get_return_edges c'`
obtain Q'' f'' where "kind r' = Q''\<hookleftarrow>⇘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''\<hookleftarrow>⇘p⇙f''` have "method_exit (sourcenode r')"
by(fastforce simp:method_exit_def)
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘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(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\<hookleftarrow>⇘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\<hookleftarrow>⇘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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (m # msx @ ms,s) =a # as=>⇣τ (m' # ms',s')` obtain ms'' s''
where "S,f \<turnstile> (m # msx @ ms,s) -a->⇣τ (ms'',s'')"
and "S,f \<turnstile> (ms'',s'') =as=>⇣τ (m' # ms',s')"
by(auto elim:silent_moves.cases)
from `S,f \<turnstile> (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 \<turnstile> (ms'',s'') =as=>⇣τ (m' # ms',s')`
have "S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (m # msx @ ms,s) =a # as=>⇣τ (m' # ms',s')` obtain ms'' s''
where "S,f \<turnstile> (m # msx @ ms,s) -a->⇣τ (ms'',s'')"
and "S,f \<turnstile> (ms'',s'') =as=>⇣τ (m' # ms',s')"
by(auto elim:silent_moves.cases)
from `S,f \<turnstile> (m # msx @ ms,s) -a->⇣τ (ms'',s'')` `kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges a`
obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'" by(fastforce dest!:call_return_edges)
from `valid_edge a'` `kind a' = Q'\<hookleftarrow>⇘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'\<hookleftarrow>⇘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)"
by(simp add:targetnodes_def)
from `S,f \<turnstile> (ms'',s'') =as=>⇣τ (m' # ms',s')`
have "S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (m # msx @ ms,s) =a # as=>⇣τ (m' # ms',s')` obtain ms'' s''
where "S,f \<turnstile> (m # msx @ ms,s) -a->⇣τ (ms'',s'')"
and "S,f \<turnstile> (ms'',s'') =as=>⇣τ (m' # ms',s')"
by(auto elim:silent_moves.cases)
from `S,f \<turnstile> (m # msx @ ms,s) -a->⇣τ (ms'',s'')` `kind a = Q\<hookleftarrow>⇘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(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 \<turnstile> (ms'',s'') =as=>⇣τ (m' # ms',s')` `msx = mx'#msx'`
`ms'' = msx @ ms` `mx' = targetnode a`
have "S,f \<turnstile> (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 \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')" and "m -as->⇘sl⇙* m'" shows "ms = ms'"
proof -
from `S,kind \<turnstile> (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 \<turnstile> (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 \<turnstile> (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"
by(simp add:slp_def same_level_path_def)
with `S,kind \<turnstile> (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 \<turnstile> (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\<hookrightarrow>⇘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 \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')`
show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘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 \<turnstile> (m#ms,s) =as'=>⇣τ (mx#msx,sx) -->
(∃asx a asx'. as' = asx @ a # asx' ∧ (∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs) ∧
call_of_return_node (hd msx) (sourcenode a) ∧ targetnode a -asx'->⇘sl⇙* mx) ∨
msx = ms)"
and "S,kind \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')"
show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘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 \<turnstile> (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 \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')`
obtain ms'' s'' where "S,kind \<turnstile> (m#ms,s) =as'=>⇣τ (ms'',s'')"
and "S,kind \<turnstile> (ms'',s'') =[a']=>⇣τ (m'#ms',s')"
by(fastforce elim:silent_moves_split)
from snoc have "length as' < length as" by simp
from `S,kind \<turnstile> (ms'',s'') =[a']=>⇣τ (m'#ms',s')`
have "S,kind \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (m#ms,s) =as'=>⇣τ (ms'',s'')`
have "(∃asx ax asx'. as' = asx @ ax # asx' ∧ (∃Q r p fs. kind ax = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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 \<turnstile> (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')"
by(simp add:call_of_return_node_def) blast
with snoc `kind a' = Q:r\<hookrightarrow>⇘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 \<turnstile> (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 \<turnstile> (m#ms,s) =as'=>⇣τ (ms'',s'')` IH
have "(∃asx ax asx'. as' = asx @ ax # asx' ∧ (∃Q r p fs. kind ax = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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 \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')` snoc `as' = asx @ ax # asx'`
obtain msx sx where "S,kind \<turnstile> (m#ms,s) =asx=>⇣τ (msx,sx)"
and "S,kind \<turnstile> (msx,sx) =ax#asx'@[a']=>⇣τ (m'#ms',s')"
by(fastforce elim:silent_moves_split)
from `S,kind \<turnstile> (msx,sx) =ax#asx'@[a']=>⇣τ (m'#ms',s')`
obtain xs x ys y where "S,kind \<turnstile> (msx,sx) -ax->⇣τ (xs,x)"
and "S,kind \<turnstile> (xs,x) =asx'=>⇣τ (ys,y)"
and "S,kind \<turnstile> (ys,y) =[a']=>⇣τ (m'#ms',s')"
apply - apply(erule silent_moves.cases) apply auto
by(erule silent_moves_split) auto
from `S,kind \<turnstile> (msx,sx) -ax->⇣τ (xs,x)` `∃Q r p fs. kind ax = Q:r\<hookrightarrow>⇘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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (ys,y) =[a']=>⇣τ (m'#ms',s')` `kind a' = Q\<hookleftarrow>⇘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 \<turnstile> (m#ms,s) =asx=>⇣τ (msx,sx)` `msx = sourcenode ax#msx'`
have "S,kind \<turnstile> (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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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 \<turnstile> (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->⇣\<surd>* m'"
by(fastforce intro:valid_path_aux_valid_path simp:vp_def)
with snoc have "m -as'->⇣\<surd>* 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->⇣\<surd>* 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\<hookrightarrow>⇘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' = []"
by(simp_all add:slp_def same_level_path_def)
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\<hookrightarrow>⇘p⇙fs` `kind a' = Q\<hookleftarrow>⇘p⇙f`
have "a' ∈ get_return_edges ax" by simp
with `upd_cs ([]@[ax]) asx' = []@[ax]` `kind a' = Q\<hookleftarrow>⇘p⇙f`
have "upd_cs [ax] (asx'@[a']) = []" by(fastforce intro:upd_cs_Append)
with `∃Q r p fs. kind ax = Q:r\<hookrightarrow>⇘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' = []"
by(simp_all add:slp_def same_level_path_def)
hence "same_level_path_aux ([]@[ax]) asx'"
by -(rule same_level_path_aux_callstack_Append)
with `∃Q r p fs. kind ax = Q:r\<hookrightarrow>⇘p⇙fs` `kind a' = Q\<hookleftarrow>⇘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'"
by(simp add:slp_def same_level_path_def)
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\<hookrightarrow>⇘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 \<turnstile> (ms'',s'') -a'->⇣τ (m'#ms',s')` `kind a' = Q\<hookleftarrow>⇘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 \<turnstile> (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\<hookrightarrow>⇘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 \<turnstile> (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 \<turnstile> (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. rs!i ∈ get_return_edges (cs!i)` `ms = targetnodes rs`
`valid_return_list rs m` `length rs = length cs`
show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs) ∧
call_of_return_node (hd ms') (sourcenode a) ∧ targetnode a -as''->⇘sl⇙* m' ∧
CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx) ∨ ms' = ms"
proof(rule silent_moves_call_edge)
fix as' a as'' assume "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs"
and "call_of_return_node (hd ms') (sourcenode a)"
and "targetnode a -as''->⇘sl⇙* m'"
from `∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs` obtain Q r p fs
where "kind a = Q:r\<hookrightarrow>⇘p⇙fs" by blast
from `targetnode a -as''->⇘sl⇙* m'` obtain asx where "targetnode a -asx->⇣ι* m'"
by -(erule same_level_path_inner_path)
from `m -as->* m'` `as = as'@a#as''` have "valid_edge a"
by(fastforce dest:path_split simp:vp_def)
have "m' ≠ (_Exit_)"
proof
assume "m' = (_Exit_)"
have "get_proc (_Exit_) = Main" by(rule get_proc_Exit)
from `targetnode a -asx->⇣ι* m'`
have "get_proc (targetnode a) = get_proc m'" by(rule intra_path_get_procs)
with `m' = (_Exit_)` `get_proc (_Exit_) = Main`
have "get_proc (targetnode a) = Main" by simp
with `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `valid_edge a`
have "kind a = Q:r\<hookrightarrow>⇘Main⇙fs" by(fastforce dest:get_proc_call)
with `valid_edge a` show False by(rule Main_no_call_target)
qed
show ?thesis
proof(cases "targetnode a = m'")
case True
with `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "CFG_node (sourcenode a) s-p->⇘call⇙ CFG_node m'"
by(fastforce intro:sum_SDG_call_edge)
with `CFG_node m' ∈ sum_SDG_slice1 nx`
have "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx" by -(rule call_slice1)
with `as = as'@a#as''` `∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`call_of_return_node (hd ms') (sourcenode a)`
`targetnode a -as''->⇘sl⇙* m'` show ?thesis by blast
next
case False
with `targetnode a -asx->⇣ι* m'` `m' ≠ (_Exit_)` `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
obtain ns where "CFG_node (targetnode a) cd-ns->⇣d* CFG_node m'"
by(fastforce elim!:in_proc_cdep_SDG_path)
hence "CFG_node (targetnode a) is-ns->⇣d* CFG_node m'"
by(fastforce intro:intra_SDG_path_is_SDG_path cdep_SDG_path_intra_SDG_path)
with `CFG_node m' ∈ sum_SDG_slice1 nx`
have "CFG_node (targetnode a) ∈ sum_SDG_slice1 nx"
by -(rule is_SDG_path_slice1)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "CFG_node (sourcenode a) s-p->⇘call⇙ CFG_node (targetnode a)"
by(fastforce intro:sum_SDG_call_edge)
with `CFG_node (targetnode a) ∈ sum_SDG_slice1 nx`
have "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx" by -(rule call_slice1)
with `as = as'@a#as''` `∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`call_of_return_node (hd ms') (sourcenode a)`
`targetnode a -as''->⇘sl⇙* m'` show ?thesis by blast
qed
next
assume "ms' = ms" thus ?thesis by simp
qed
qed
lemma silent_moves_called_node_in_slice1_nodestack_in_slice1:
"[|S,kind \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s'); valid_node m;
CFG_node m' ∈ sum_SDG_slice1 nx; nx ∈ S;
∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
∀i < length rs. rs!i ∈ get_return_edges (cs!i); ms = targetnodes rs;
valid_return_list rs m; length rs = length cs|]
==> ∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct ms' arbitrary:as m' s')
case (Cons mx msx)
note IH = `!!as m' s'. [|S,kind \<turnstile> (m#ms,s) =as=>⇣τ (m' # msx,s'); valid_node m;
CFG_node m' ∈ sum_SDG_slice1 nx; nx ∈ S;
∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); ms = targetnodes rs;
valid_return_list rs m; length rs = length cs|]
==> ∀mx∈set msx. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
from `S,kind \<turnstile> (m#ms,s) =as=>⇣τ (m' # mx # msx,s')` `valid_node m`
`CFG_node m' ∈ sum_SDG_slice1 nx`
`∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀i < length rs. rs!i ∈ get_return_edges (cs!i)` `ms = targetnodes rs`
`valid_return_list rs m` `length rs = length cs`
show ?case
proof(rule silent_moves_called_node_in_slice1_hd_nodestack_in_slice1)
fix as' a as'' assume "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs"
and "call_of_return_node (hd (mx # msx)) (sourcenode a)"
and "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx"
and "targetnode a -as''->⇘sl⇙* m'"
from `CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx` `nx ∈ S`
have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:combSlice_refl simp:SDG_to_CFG_set_def HRB_slice_def)
from `S,kind \<turnstile> (m#ms,s) =as=>⇣τ (m' # mx # msx,s')` `as = as'@a#as''`
obtain xs x where "S,kind \<turnstile> (m#ms,s) =as'=>⇣τ (xs,x)"
and "S,kind \<turnstile> (xs,x) =a#as''=>⇣τ (m' # mx # msx,s')"
by(fastforce elim:silent_moves_split)
from `S,kind \<turnstile> (xs,x) =a#as''=>⇣τ (m' # mx # msx,s')`
obtain ys y where "S,kind \<turnstile> (xs,x) -a->⇣τ (ys,y)"
and "S,kind \<turnstile> (ys,y) =as''=>⇣τ (m' # mx # msx,s')"
by(fastforce elim:silent_moves.cases)
from `S,kind \<turnstile> (xs,x) -a->⇣τ (ys,y)` `∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs`
obtain xs' a' where "xs = sourcenode a#xs'"
and "ys = targetnode a#targetnode a'#xs'"
apply - apply(erule silent_move.cases) apply(auto simp:intra_kind_def)
by(cases xs,auto)+
from `S,kind \<turnstile> (ys,y) =as''=>⇣τ (m' # mx # msx,s')`
`ys = targetnode a#targetnode a'#xs'` `targetnode a -as''->⇘sl⇙* m'`
have "mx = targetnode a'" and "xs' = msx"
by(auto dest:silent_moves_same_level_path)
with `xs = sourcenode a#xs'` `S,kind \<turnstile> (m#ms,s) =as'=>⇣τ (xs,x)`
have "S,kind \<turnstile> (m#ms,s) =as'=>⇣τ (sourcenode a#msx,x)" by simp
from IH[OF `S,kind \<turnstile> (m#ms,s) =as'=>⇣τ (sourcenode a#msx,x)`
`valid_node m` `CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx` `nx ∈ S`
`∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀i < length rs. rs!i ∈ get_return_edges (cs!i)` `ms = targetnodes rs`
`valid_return_list rs m` `length rs = length cs`]
have callstack:"∀mx∈set msx.
∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙" .
with `as = as'@a#as''` `call_of_return_node (hd (mx # msx)) (sourcenode a)`
`sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` show ?thesis by fastforce
next
assume "mx # msx = ms"
with `∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
show ?thesis by fastforce
qed
qed simp
lemma silent_moves_slice_intra_path:
assumes "S,slice_kind S \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')"
and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
shows "∀a ∈ set as. intra_kind (kind a)"
proof(rule ccontr)
assume "¬ (∀a∈set as. intra_kind (kind a))"
hence "∃a ∈ set as. ¬ intra_kind (kind a)" by fastforce
then obtain asx ax asx' where "as = asx@ax#asx'"
and "∀a∈set asx. intra_kind (kind a)" and "¬ intra_kind (kind ax)"
by(fastforce elim!:split_list_first_propE)
from `S,slice_kind S \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')` `as = asx@ax#asx'`
obtain msx sx msx' sx' where "S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (msx,sx)"
and "S,slice_kind S \<turnstile> (msx,sx) -ax->⇣τ (msx',sx')"
and "S,slice_kind S \<turnstile> (msx',sx') =asx'=>⇣τ (m'#ms',s')"
by(auto elim!:silent_moves_split elim:silent_moves.cases)
from `S,slice_kind S \<turnstile> (msx,sx) -ax->⇣τ (msx',sx')` obtain xs
where [simp]:"msx = sourcenode ax#xs" by(cases msx)(auto elim:silent_move.cases)
from `S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (msx,sx)` `∀a∈set asx. intra_kind (kind a)`
have [simp]:"xs = ms" by(fastforce dest:silent_moves_intra_path)
show False
proof(cases "kind ax" rule:edge_kind_cases)
case Intra with `¬ intra_kind (kind ax)` show False by simp
next
case (Call Q r p fs)
with `S,slice_kind S \<turnstile> (msx,sx) -ax->⇣τ (msx',sx')`
`∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "sourcenode ax ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "pred (slice_kind S ax) sx"
by(auto elim!:silent_move.cases simp:intra_kind_def)
from `sourcenode ax ∉ ⌊HRB_slice S⌋⇘CFG⇙` `kind ax = Q:r\<hookrightarrow>⇘p⇙fs`
have "slice_kind S ax = (λcf. False):r\<hookrightarrow>⇘p⇙fs"
by(rule slice_kind_Call)
with `pred (slice_kind S ax) sx` show False by(cases sx) auto
next
case (Return Q p f)
with `S,slice_kind S \<turnstile> (msx,sx) -ax->⇣τ (msx',sx')`
`∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
show False by(fastforce elim!:silent_move.cases simp:intra_kind_def)
qed
qed
lemma silent_moves_slice_keeps_state:
assumes "S,slice_kind S \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')"
and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
shows "s = s'"
proof -
from assms have "∀a ∈ set as. intra_kind (kind a)"
by(rule silent_moves_slice_intra_path)
with assms show ?thesis
proof(induct S "slice_kind S" "m#ms" s as "m'#ms'" s'
arbitrary:m rule:silent_moves.induct)
case (silent_moves_Nil sx n⇣c) thus ?case by simp
next
case (silent_moves_Cons S sx a msx' sx' as s'')
note IH = `!!m.
[|msx' = m # ms;
∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
∀a∈set as. intra_kind (kind a)|] ==> sx' = s''`
note callstack = `∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
from `∀a∈set (a # as). intra_kind (kind a)` have "intra_kind (kind a)"
and "∀a∈set as. intra_kind (kind a)" by simp_all
from `S,slice_kind S \<turnstile> (m # ms,sx) -a->⇣τ (msx',sx')` `intra_kind (kind a)`
callstack
have [simp]:"msx' = targetnode a#ms" and "sx' = transfer (slice_kind S a) sx"
and "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a" and "sx ≠ []"
by(auto elim!:silent_move.cases simp:intra_kind_def)
from IH[OF `msx' = targetnode a#ms` callstack `∀a∈set as. intra_kind (kind a)`]
have "sx' = s''" .
from `intra_kind (kind a)`
have "sx = sx'"
proof(cases "kind a")
case (UpdateEdge f')
with `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have "slice_kind S a = \<Up>id" by(rule slice_kind_Upd)
with `sx' = transfer (slice_kind S a) sx` `sx ≠ []`
show ?thesis by(cases sx) auto
next
case (PredicateEdge Q)
with `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙` `valid_edge a`
obtain Q' where "slice_kind S a = (Q')⇣\<surd>"
by -(erule kind_Predicate_notin_slice_slice_kind_Predicate)
with `sx' = transfer (slice_kind S a) sx` `sx ≠ []`
show ?thesis by(cases sx) auto
qed (auto simp:intra_kind_def)
with `sx' = s''` show ?case by simp
qed
qed
subsection {* Definition of @{text "slice_edges"} *}
definition slice_edge :: "'node SDG_node set => 'edge list => 'edge => bool"
where "slice_edge S cs a ≡ (∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙) ∧
(case (kind a) of Q\<hookleftarrow>⇘p⇙f => True | _ => sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙)"
lemma silent_move_no_slice_edge:
"[|S,f \<turnstile> (ms,s) -a->⇣τ (ms',s'); tl ms = targetnodes rs; length rs = length cs;
∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))|]
==> ¬ slice_edge S cs a"
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⇙`
from `pred (f a) s` `length ms = length s` obtain x xs where "ms = x#xs"
by(cases ms) auto
from `length rs = length cs` `tl ms = targetnodes rs`
have "length (tl ms) = length cs" by(simp add:targetnodes_def)
from disj show ?case
proof
assume "∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with `∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
`length (tl ms) = length cs`
have "∃c ∈ set cs. sourcenode c ∉ ⌊HRB_slice S⌋⇘CFG⇙"
apply(auto simp:in_set_conv_nth)
by(erule_tac x="i" in allE) auto
thus ?thesis by(auto simp:slice_edge_def)
next
assume "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with `hd ms = sourcenode a` `intra_kind (kind a)`
show ?case by(auto simp:slice_edge_def simp:intra_kind_def)
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⇙`
from `pred (f a) s` `length ms = length s` obtain x xs where "ms = x#xs"
by(cases ms) auto
from `length rs = length cs` `tl ms = targetnodes rs`
have "length (tl ms) = length cs" by(simp add:targetnodes_def)
from disj show ?case
proof
assume "∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with `∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
`length (tl ms) = length cs`
have "∃c ∈ set cs. sourcenode c ∉ ⌊HRB_slice S⌋⇘CFG⇙"
apply(auto simp:in_set_conv_nth)
by(erule_tac x="i" in allE) auto
thus ?thesis by(auto simp:slice_edge_def)
next
assume "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with `hd ms = sourcenode a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
show ?case by(auto simp:slice_edge_def)
qed
next
case (silent_move_return f a s s' Q p f' ms S ms')
from `pred (f a) s` `length ms = length s` obtain x xs where "ms = x#xs"
by(cases ms) auto
from `length rs = length cs` `tl ms = targetnodes rs`
have "length (tl ms) = length cs" by(simp add:targetnodes_def)
from `∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
`∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`length (tl ms) = length cs`
have "∃c ∈ set cs. sourcenode c ∉ ⌊HRB_slice S⌋⇘CFG⇙"
apply(auto simp:in_set_conv_nth)
by(erule_tac x="i" in allE) auto
thus ?case by(auto simp:slice_edge_def)
qed
lemma observable_move_slice_edge:
"[|S,f \<turnstile> (ms,s) -a-> (ms',s'); tl ms = targetnodes rs; length rs = length cs;
∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))|]
==> slice_edge S cs a"
proof(induct rule:observable_move.induct)
case (observable_move_intra f a s s' ms S ms')
from `pred (f a) s` `length ms = length s` obtain x xs where "ms = x#xs"
by(cases ms) auto
from `length rs = length cs` `tl ms = targetnodes rs`
have "length (tl ms) = length cs" by(simp add:targetnodes_def)
with `∀m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))`
have "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
apply(auto simp:in_set_conv_nth)
by(erule_tac x="i" in allE) auto
with `hd ms = sourcenode a` `hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙` `intra_kind (kind a)`
show ?case by(auto simp:slice_edge_def simp:intra_kind_def)
next
case (observable_move_call f a s s' Q r p fs a' ms S ms')
from `pred (f a) s` `length ms = length s` obtain x xs where "ms = x#xs"
by(cases ms) auto
from `length rs = length cs` `tl ms = targetnodes rs`
have "length (tl ms) = length cs" by(simp add:targetnodes_def)
with `∀m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))`
have "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
apply(auto simp:in_set_conv_nth)
by(erule_tac x="i" in allE) auto
with `hd ms = sourcenode a` `hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
show ?case by(auto simp:slice_edge_def)
next
case (observable_move_return f a s s' Q p f' ms S ms')
from `pred (f a) s` `length ms = length s` obtain x xs where "ms = x#xs"
by(cases ms) auto
from `length rs = length cs` `tl ms = targetnodes rs`
have "length (tl ms) = length cs" by(simp add:targetnodes_def)
with `∀m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))`
have "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
apply(auto simp:in_set_conv_nth)
by(erule_tac x="i" in allE) auto
with `kind a = Q\<hookleftarrow>⇘p⇙f'` show ?case by(auto simp:slice_edge_def)
qed
function slice_edges :: "'node SDG_node set => 'edge list => 'edge list => 'edge list"
where "slice_edges S cs [] = []"
| "slice_edge S cs a ==>
slice_edges S cs (a#as) = a#slice_edges S (upd_cs cs [a]) as"
| "¬ slice_edge S cs a ==>
slice_edges S cs (a#as) = slice_edges S (upd_cs cs [a]) as"
by(atomize_elim)(auto,case_tac b,auto)
termination by(lexicographic_order)
lemma slice_edges_Append:
"[|slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'|]
==> slice_edges S cs (as@asx) = as'@asx'"
proof(induct as arbitrary:cs as')
case Nil thus ?case by simp
next
case (Cons x xs)
note IH = `!!cs as'. [|slice_edges S cs xs = as';
slice_edges S (upd_cs cs xs) asx = asx'|]
==> slice_edges S cs (xs @ asx) = as' @ asx'`
from `slice_edges S (upd_cs cs (x # xs)) asx = asx'`
have "slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'"
by(cases "kind x")(auto,cases cs,auto)
show ?case
proof(cases "slice_edge S cs x")
case True
with `slice_edges S cs (x # xs) = as'`
have "x#slice_edges S (upd_cs cs [x]) xs = as'" by simp
then obtain xs' where "as' = x#xs'"
and "slice_edges S (upd_cs cs [x]) xs = xs'" by(cases as') auto
from IH[OF `slice_edges S (upd_cs cs [x]) xs = xs'`
`slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'`]
have "slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'" .
with True `as' = x#xs'` show ?thesis by simp
next
case False
with `slice_edges S cs (x # xs) = as'`
have "slice_edges S (upd_cs cs [x]) xs = as'" by simp
from IH[OF this `slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'`]
have "slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'" .
with False show ?thesis by simp
qed
qed
lemma slice_edges_Nil_split:
"slice_edges S cs (as@as') = []
==> slice_edges S cs as = [] ∧ slice_edges S (upd_cs cs as) as' = []"
apply(induct as arbitrary:cs)
apply clarsimp
apply(case_tac "slice_edge S cs a") apply auto
apply(case_tac "kind a") apply auto
apply(case_tac cs) apply auto
done
lemma slice_intra_edges_no_nodes_in_slice:
"[|slice_edges S cs as = []; ∀a ∈ set as. intra_kind (kind a);
∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙|]
==> ∀nx ∈ set(sourcenodes as). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct as)
case Nil thus ?case by(fastforce simp:sourcenodes_def)
next
case (Cons a' as')
note IH = ` [|slice_edges S cs as' = []; ∀a∈set as'. intra_kind (kind a);
∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙|]
==> ∀nx∈set (sourcenodes as'). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙`
from `∀a∈set (a' # as'). intra_kind (kind a)`
have "intra_kind (kind a')" and "∀a∈set as'. intra_kind (kind a)" by simp_all
from `slice_edges S cs (a' # as') = []` `intra_kind (kind a')`
`∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "sourcenode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "slice_edges S cs as' = []"
by(cases "slice_edge S cs a'",auto simp:intra_kind_def slice_edge_def)+
from IH[OF `slice_edges S cs as' = []` `∀a∈set as'. intra_kind (kind a)`
`∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙`]
have "∀nx∈set (sourcenodes as'). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙" .
with `sourcenode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙` show ?case by(simp add:sourcenodes_def)
qed
lemma silent_moves_no_slice_edges:
"[|S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s'); tl ms = targetnodes rs; length rs = length cs;
∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))|]
==> slice_edges S cs as = [] ∧ (∃rs'. tl ms' = targetnodes rs' ∧
length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as).
call_of_return_node (tl ms'!i) (sourcenode ((upd_cs cs as)!i))))"
proof(induct arbitrary:rs cs rule:silent_moves.induct)
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
from `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')` `tl ms = targetnodes rs` `length rs = length cs`
`∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
have "¬ slice_edge S cs a" by(rule silent_move_no_slice_edge)
with silent_moves_Cons show ?case
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms S ms')
note IH = `!!rs cs. [|tl ms' = targetnodes rs; length rs = length cs;
∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))|]
==> slice_edges S cs as = [] ∧ (∃rs'. tl ms'' = targetnodes rs' ∧
length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as).
call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))`
from `ms' = targetnode a # tl ms` `tl ms = targetnodes rs`
have "tl ms' = targetnodes rs" by simp
from `ms' = targetnode a # tl ms` `tl ms = targetnodes rs`
`∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
have "∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))"
by simp
from IH[OF `tl ms' = targetnodes rs` `length rs = length cs` this]
have "slice_edges S cs as = []"
and "∃rs'. tl ms'' = targetnodes rs' ∧ length rs' = length (upd_cs cs as) ∧
(∀i<length (upd_cs cs as).
call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))" by simp_all
with `intra_kind (kind a)` `¬ slice_edge S cs a`
show ?case by(fastforce simp:intra_kind_def)
next
case (silent_move_call f a s s' Q r p fs a' ms S ms')
note IH = `!!rs cs. [|tl ms' = targetnodes rs; length rs = length cs;
∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))|]
==> slice_edges S cs as = [] ∧ (∃rs'. tl ms'' = targetnodes rs' ∧
length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as).
call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))`
from `tl ms = targetnodes rs` `ms' = targetnode a # targetnode a' # tl ms`
have "tl ms' = targetnodes (a'#rs)" by(simp add:targetnodes_def)
from `length rs = length cs` have "length (a'#rs) = length (a#cs)" by simp
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`
have "call_of_return_node (targetnode a') (sourcenode a)"
by(simp add:call_of_return_node_def) blast
with `∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
`ms' = targetnode a # targetnode a' # tl ms`
have "∀i<length (a#cs).
call_of_return_node (tl ms' ! i) (sourcenode ((a#cs) ! i))"
by auto (case_tac i,auto)
from IH[OF `tl ms' = targetnodes (a'#rs)` `length (a'#rs) = length (a#cs)` this]
have "slice_edges S (a # cs) as = []"
and "∃rs'. tl ms'' = targetnodes rs' ∧
length rs' = length (upd_cs (a # cs) as) ∧
(∀i<length (upd_cs (a # cs) as).
call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i)))"
by simp_all
with `¬ slice_edge S cs a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` show ?case by simp
next
case (silent_move_return f a s s' Q p f' ms S ms')
note IH = `!!rs cs. [|tl ms' = targetnodes rs; length rs = length cs;
∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))|]
==> slice_edges S cs as = [] ∧ (∃rs'. tl ms'' = targetnodes rs' ∧
length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as).
call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))`
from `length s = Suc (length s')` `s' ≠ []` `length ms = length s` `ms' = tl ms`
obtain x xs where [simp]:"ms' = x#xs" by(cases ms)(auto,case_tac ms',auto)
from `ms' = tl ms` `tl ms = targetnodes rs` obtain r' rs' where "rs = r'#rs'"
and "x = targetnode r'" and "tl ms' = targetnodes rs'"
by(cases rs)(auto simp:targetnodes_def)
from `length rs = length cs` `rs = r'#rs'` obtain c' cs' where "cs = c'#cs'"
and "length rs' = length cs'" by(cases cs) auto
from `∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
`cs = c'#cs'` `ms' = tl ms`
have "∀i<length cs'. call_of_return_node (tl ms' ! i) (sourcenode (cs' ! i))"
by auto(erule_tac x="Suc i" in allE,cases "tl ms",auto)
from IH[OF `tl ms' = targetnodes rs'` `length rs' = length cs'` this]
have "slice_edges S cs' as = []" and "∃rs'. tl ms'' = targetnodes rs' ∧
length rs' = length (upd_cs cs' as) ∧ (∀i<length (upd_cs cs' as).
call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i)))"
by simp_all
with `¬ slice_edge S cs a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `cs = c'#cs'`
show ?case by simp
qed
qed fastforce
lemma observable_moves_singular_slice_edge:
"[|S,f \<turnstile> (ms,s) =as=> (ms',s'); tl ms = targetnodes rs; length rs = length cs;
∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))|]
==> slice_edges S cs as = [last as]"
proof(induct rule:observable_moves.induct)
case (observable_moves_snoc S f ms s as ms' s' a ms'' s'')
from `S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s')` `tl ms = targetnodes rs` `length rs = length cs`
`∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))`
obtain rs' where "slice_edges S cs as = []"
and "tl ms' = targetnodes rs'" and "length rs' = length (upd_cs cs as)"
and "∀i<length (upd_cs cs as).
call_of_return_node (tl ms'!i) (sourcenode ((upd_cs cs as)!i))"
by(fastforce dest!:silent_moves_no_slice_edges)
from `S,f \<turnstile> (ms',s') -a-> (ms'',s'')` this
have "slice_edge S (upd_cs cs as) a" by -(rule observable_move_slice_edge)
with `slice_edges S cs as = []` have "slice_edges S cs (as @ [a]) = []@[a]"
by(fastforce intro:slice_edges_Append)
thus ?case by simp
qed
lemma silent_moves_nonempty_nodestack_False:
assumes "S,kind \<turnstile> ([m],[cf]) =as=>⇣τ (m'#ms',s')" and "valid_node m"
and "ms' ≠ []" and "CFG_node m' ∈ sum_SDG_slice1 nx" and "nx ∈ S"
shows False
proof -
from assms(1-4) have "slice_edges S [] as ≠ []"
proof(induct ms' arbitrary:as m' s')
case (Cons mx msx)
note IH = `!!as m' s'. [|S,kind \<turnstile> ([m],[cf]) =as=>⇣τ (m' # msx,s'); valid_node m;
msx ≠ []; CFG_node m' ∈ sum_SDG_slice1 nx|]
==> slice_edges S [] as ≠ []`
from `S,kind \<turnstile> ([m],[cf]) =as=>⇣τ (m' # mx # msx,s')` `valid_node m`
`CFG_node m' ∈ sum_SDG_slice1 nx`
obtain as' a as'' where "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs"
and "call_of_return_node mx (sourcenode a)"
and "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx"
and "targetnode a -as''->⇘sl⇙* m'"
by(fastforce elim!:silent_moves_called_node_in_slice1_hd_nodestack_in_slice1
[of _ _ _ _ _ _ _ _ _ "[]" "[]"] simp:targetnodes_def valid_return_list_def)
from `S,kind \<turnstile> ([m],[cf]) =as=>⇣τ (m' # mx # msx,s')` `as = as'@a#as''`
obtain xs x where "S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (xs,x)"
and "S,kind \<turnstile> (xs,x) =a#as''=>⇣τ (m' # mx # msx,s')"
by(fastforce elim:silent_moves_split)
from `S,kind \<turnstile> (xs,x) =a#as''=>⇣τ (m' # mx # msx,s')`
obtain ys y where "S,kind \<turnstile> (xs,x) -a->⇣τ (ys,y)"
and "S,kind \<turnstile> (ys,y) =as''=>⇣τ (m' # mx # msx,s')"
by(fastforce elim:silent_moves.cases)
from `S,kind \<turnstile> (xs,x) -a->⇣τ (ys,y)` `∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs`
obtain xs' a' where "xs = sourcenode a#xs'"
and "ys = targetnode a#targetnode a'#xs'"
apply - apply(erule silent_move.cases) apply(auto simp:intra_kind_def)
by(cases xs,auto)+
from `S,kind \<turnstile> (ys,y) =as''=>⇣τ (m' # mx # msx,s')`
`ys = targetnode a#targetnode a'#xs'` `targetnode a -as''->⇘sl⇙* m'`
have "mx = targetnode a'" and "xs' = msx"
by(auto dest:silent_moves_same_level_path)
with `xs = sourcenode a#xs'` `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (xs,x)`
have "S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (sourcenode a#msx,x)" by simp
show ?case
proof(cases "msx = []")
case True
from `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (sourcenode a#msx,x)`
obtain rs' where "msx = targetnodes rs' ∧ length rs' = length (upd_cs [] as')"
by(fastforce dest!:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
simp:targetnodes_def)
with True have "upd_cs [] as' = []" by(cases rs')(auto simp:targetnodes_def)
with `CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx` `nx ∈ S`
have "slice_edge S (upd_cs [] as') a"
by(cases "kind a",auto intro:combSlice_refl
simp:slice_edge_def SDG_to_CFG_set_def HRB_slice_def)
hence "slice_edges S (upd_cs [] as') (a#as'') ≠ []" by simp
with `as = as'@a#as''` show ?thesis by(fastforce dest:slice_edges_Nil_split)
next
case False
from IH[OF `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (sourcenode a#msx,x)`
`valid_node m` this `CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx`]
have "slice_edges S [] as' ≠ []" .
with `as = as'@a#as''` show ?thesis by(fastforce dest:slice_edges_Nil_split)
qed
qed simp
moreover
from `S,kind \<turnstile> ([m],[cf]) =as=>⇣τ (m'#ms',s')` have "slice_edges S [] as = []"
by(fastforce dest!:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
simp:targetnodes_def)
ultimately show False by simp
qed
lemma transfers_intra_slice_kinds_slice_edges:
"[|∀a ∈ set as. intra_kind (kind a); ∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙|]
==> transfers (slice_kinds S (slice_edges S cs as)) s =
transfers (slice_kinds S as) s"
proof(induct as arbitrary:s)
case Nil thus ?case by(simp add:slice_kinds_def)
next
case (Cons a' as')
note IH = `!!s. [|∀a∈set as'. intra_kind (kind a);
∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙|] ==>
transfers (slice_kinds S (slice_edges S cs as')) s =
transfers (slice_kinds S as') s`
from `∀a∈set (a' # as'). intra_kind (kind a)`
have "intra_kind (kind a')" and "∀a∈set as'. intra_kind (kind a)"
by simp_all
show ?case
proof(cases "slice_edge S cs a'")
case True
with `intra_kind (kind a')`
have eq:"transfers (slice_kinds S (slice_edges S cs (a'#as'))) s
= transfers (slice_kinds S (slice_edges S cs as'))
(transfer (slice_kind S a') s)"
by(cases "kind a'")(auto simp:slice_kinds_def intra_kind_def)
have "transfers (slice_kinds S (a'#as')) s
= transfers (slice_kinds S as') (transfer (slice_kind S a') s)"
by(simp add:slice_kinds_def)
with eq IH[OF `∀a∈set as'. intra_kind (kind a)`
`∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙`,
of "transfer (slice_kind S a') s"]
show ?thesis by simp
next
case False
with `intra_kind (kind a')`
have eq:"transfers (slice_kinds S (slice_edges S cs (a'#as'))) s
= transfers (slice_kinds S (slice_edges S cs as')) s"
by(cases "kind a'")(auto simp:slice_kinds_def intra_kind_def)
from False `intra_kind (kind a')` `∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "sourcenode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce simp:slice_edge_def intra_kind_def)
with `intra_kind (kind a')` have "transfer (slice_kind S a') s = s"
by(cases s)(auto,cases "kind a'",
auto simp:slice_kind_def Let_def intra_kind_def)
hence "transfers (slice_kinds S (a'#as')) s
= transfers (slice_kinds S as') s"
by(simp add:slice_kinds_def)
with eq IH[OF `∀a∈set as'. intra_kind (kind a)`
`∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙`,of s] show ?thesis by simp
qed
qed
lemma exists_sliced_intra_path_preds:
assumes "m -as->⇣ι* m'" and "slice_edges S cs as = []"
and "m' ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
obtains as' where "m -as'->⇣ι* m'" and "preds (slice_kinds S as') (cf#cfs)"
and "slice_edges S cs as' = []"
proof(atomize_elim)
from `m -as->⇣ι* m'` have "m -as->* m'" and "∀a ∈ set as. intra_kind(kind a)"
by(simp_all add:intra_path_def)
from `slice_edges S cs as = []` `∀a ∈ set as. intra_kind(kind a)`
`∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "∀nx ∈ set(sourcenodes as). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(rule slice_intra_edges_no_nodes_in_slice)
with `m -as->⇣ι* m'` `m' ∈ ⌊HRB_slice S⌋⇘CFG⇙` have "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obs_intra_elem)
hence "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}" by(rule obs_intra_singleton_element)
from `m -as->* m'` have "valid_node m" and "valid_node m'"
by(fastforce dest:path_valid_node)+
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` `obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}`
show "∃as'. m -as'->⇣ι* m' ∧ preds (slice_kinds S as') (cf#cfs) ∧
slice_edges S cs as' = []"
proof(induct x arbitrary:m rule:nat.induct)
case zero
from `distance m m' 0` have "m = m'"
by(fastforce elim:distance.cases simp:intra_path_def)
with `valid_node m'` show ?case
by(rule_tac x="[]" in exI,
auto intro:empty_path simp:slice_kinds_def intra_path_def)
next
case (Suc x)
note IH = `!!m. [|distance m m' x; obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}|]
==> ∃as'. m -as'->⇣ι* m' ∧ preds (slice_kinds S as') (cf # cfs) ∧
slice_edges S cs as' = []`
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 nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m' x ∧
valid_edge a' ∧ intra_kind(kind a') ∧ targetnode a' = nx)"
by(auto elim:distance_successor_distance)
have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
from `valid_edge a` `m = sourcenode a` have "valid_node m" by simp
with `m ∈ ⌊HRB_slice S⌋⇘CFG⇙` have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by -(rule n_in_obs_intra)
with `obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}` have "m = m'" by simp
with `valid_node m` have "m -[]->⇣ι* m'"
by(fastforce intro:empty_path simp:intra_path_def)
with `distance m m' (Suc x)` show False
by(fastforce elim:distance.cases)
qed
from `distance (targetnode a) m' x` `m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
obtain mx where "mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce elim:distance.cases path_ex_obs_intra)
from `valid_edge a` `intra_kind(kind a)` `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a`
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by -(rule edge_obs_intra_subset,auto)
with `mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a`
`obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}`
have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by auto
hence "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
by(rule obs_intra_singleton_element)
from IH[OF `distance (targetnode a) m' x` this]
obtain as where "targetnode a -as->⇣ι* m'" and "preds (slice_kinds S as) (cf#cfs)"
and "slice_edges S cs as = []" by blast
from `targetnode a -as->⇣ι* m'` `valid_edge a` `intra_kind(kind a)`
`m = sourcenode a`
have "m -a#as->⇣ι* m'" by(fastforce intro:Cons_path simp:intra_path_def)
from `∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙` `m ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`m = sourcenode a` `intra_kind(kind a)`
have "¬ slice_edge S cs a" by(fastforce simp:slice_edge_def intra_kind_def)
with `slice_edges S cs as = []` `intra_kind(kind a)`
have "slice_edges S cs (a#as) = []" by(fastforce simp:intra_kind_def)
from `intra_kind(kind a)`
show ?case
proof(cases "kind a")
case (UpdateEdge f)
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a` have "slice_kind S a = \<Up>id"
by(fastforce intro:slice_kind_Upd)
hence "transfer (slice_kind S a) (cf#cfs) = (cf#cfs)"
and "pred (slice_kind S a) (cf#cfs)" by simp_all
with `preds (slice_kinds S as) (cf#cfs)`
have "preds (slice_kinds S (a#as)) (cf#cfs)"
by(simp add:slice_kinds_def)
with `m -a#as->⇣ι* m'` `slice_edges S cs (a#as) = []` show ?thesis
by blast
next
case (PredicateEdge Q)
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a` `distance m m' (Suc x)`
`obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}` `distance (targetnode a) m' x`
target
have "slice_kind S a = (λs. True)⇣\<surd>"
by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
hence "transfer (slice_kind S a) (cf#cfs) = (cf#cfs)"
and "pred (slice_kind S a) (cf#cfs)" by simp_all
with `preds (slice_kinds S as) (cf#cfs)`
have "preds (slice_kinds S (a#as)) (cf#cfs)"
by(simp add:slice_kinds_def)
with `m -a#as->⇣ι* m'` `slice_edges S cs (a#as) = []` show ?thesis by blast
qed (auto simp:intra_kind_def)
qed
qed
lemma slp_to_intra_path_with_slice_edges:
assumes "n -as->⇘sl⇙* n'" and "slice_edges S cs as = []"
obtains as' where "n -as'->⇣ι* n'" and "slice_edges S cs as' = []"
proof(atomize_elim)
from `n -as->⇘sl⇙* n'` have "n -as->* n'" and "same_level_path as"
by(simp_all add:slp_def)
from `same_level_path as` have "same_level_path_aux [] as" and "upd_cs [] as = []"
by(simp_all add:same_level_path_def)
from `n -as->* n'` `same_level_path_aux [] as` `upd_cs [] as = []`
`slice_edges S cs as = []`
show "∃as'. n -as'->⇣ι* n' ∧ slice_edges S cs as' = []"
proof(induct as arbitrary:n cs rule:length_induct)
fix as n cs
assume IH:"∀as''. length as'' < length as -->
(∀n''. n'' -as''->* n' --> same_level_path_aux [] as'' -->
upd_cs [] as'' = [] --> (∀cs'. slice_edges S cs' as'' = [] -->
(∃as'. n'' -as'->⇣ι* n' ∧ slice_edges S cs' as' = [])))"
and "n -as->* n'" and "same_level_path_aux [] as" and "upd_cs [] as = []"
and "slice_edges S cs as = []"
show "∃as'. n -as'->⇣ι* n' ∧ slice_edges S cs as' = []"
proof(cases as)
case Nil
with `n -as->* n'` show ?thesis by(fastforce simp:intra_path_def)
next
case (Cons a' as')
with `n -as->* n'` Cons have "n = sourcenode a'" and "valid_edge a'"
and "targetnode a' -as'->* n'"
by(auto intro:path_split_Cons)
show ?thesis
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with Cons `same_level_path_aux [] as` have "same_level_path_aux [] as'"
by(fastforce simp:intra_kind_def)
moreover
from Intra Cons `upd_cs [] as = []` have "upd_cs [] as' = []"
by(fastforce simp:intra_kind_def)
moreover
from `slice_edges S cs as = []` Cons Intra
have "slice_edges S cs as' = []" and "¬ slice_edge S cs a'"
by(cases "slice_edge S cs a'",auto simp:intra_kind_def)+
ultimately obtain as'' where "targetnode a' -as''->⇣ι* n'"
and "slice_edges S cs as'' = []"
using IH Cons `targetnode a' -as'->* n'`
by(erule_tac x="as'" in allE) auto
from `n = sourcenode a'` `valid_edge a'` Intra `targetnode a' -as''->⇣ι* n'`
have "n -a'#as''->⇣ι* n'" by(fastforce intro:Cons_path simp:intra_path_def)
moreover
from `slice_edges S cs as'' = []` `¬ slice_edge S cs a'` Intra
have "slice_edges S cs (a'#as'') = []" by(auto simp:intra_kind_def)
ultimately show ?thesis by blast
next
case (Call Q r p f)
with Cons `same_level_path_aux [] as`
have "same_level_path_aux [a'] as'" by simp
from Call Cons `upd_cs [] as = []` have "upd_cs [a'] as' = []"
by simp
hence "as' ≠ []" by fastforce
with `upd_cs [a'] as' = []` obtain xs ys where "as' = xs@ys" and "xs ≠ []"
and "upd_cs [a'] xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] --> upd_cs [a'] xs' ≠ []"
by -(erule upd_cs_empty_split,auto)
from `same_level_path_aux [a'] as'` `as' = xs@ys` `upd_cs [a'] xs = []`
have "same_level_path_aux [a'] xs" and "same_level_path_aux [] ys"
by(rule slpa_split)+
with `upd_cs [a'] xs = []` have "upd_cs ([a']@cs) xs = []@cs"
by(fastforce intro:same_level_path_upd_cs_callstack_Append)
from `slice_edges S cs as = []` Cons Call
have "slice_edges S (a'#cs) as' = []" and "¬ slice_edge S cs a'"
by(cases "slice_edge S cs a'",auto)+
from `slice_edges S (a'#cs) as' = []` `as' = xs@ys`
`upd_cs ([a']@cs) xs = []@cs`
have "slice_edges S cs ys = []"
by(fastforce dest:slice_edges_Nil_split)
from `same_level_path_aux [a'] xs` `upd_cs [a'] xs = []`
`∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] --> upd_cs [a'] xs' ≠ []`
have "last xs ∈ get_return_edges (last [a'])"
by(fastforce intro!:slpa_get_return_edges)
with `valid_edge a'` Call
obtain a where "valid_edge a" and "sourcenode a = sourcenode a'"
and "targetnode a = targetnode (last xs)" and "kind a = (λcf. False)⇣\<surd>"
by -(drule call_return_node_edge,auto)
from `targetnode a = targetnode (last xs)` `xs ≠ []`
have "targetnode a = targetnode (last (a'#xs))" by simp
from `as' = xs@ys` `xs ≠ []` Cons have "length ys < length as" by simp
from `targetnode a' -as'->* n'` `as' = xs@ys` `xs ≠ []`
have "targetnode (last (a'#xs)) -ys->* n'"
by(cases xs rule:rev_cases,auto dest:path_split)
with IH `length ys < length as` `same_level_path_aux [] ys`
`upd_cs [] ys = []` `slice_edges S cs ys = []`
obtain as'' where "targetnode (last (a'#xs)) -as''->⇣ι* n'"
and "slice_edges S cs as'' = []"
apply(erule_tac x="ys" in allE) apply clarsimp
apply(erule_tac x="targetnode (last (a'#xs))" in allE)
apply clarsimp apply(erule_tac x="cs" in allE)
by clarsimp
from `sourcenode a = sourcenode a'` `n = sourcenode a'`
`targetnode a = targetnode (last (a'#xs))` `valid_edge a`
`kind a = (λcf. False)⇣\<surd>` `targetnode (last (a'#xs)) -as''->⇣ι* n'`
have "n -a#as''->⇣ι* n'"
by(fastforce intro:Cons_path simp:intra_path_def intra_kind_def)
moreover
from `kind a = (λcf. False)⇣\<surd>` `slice_edges S cs as'' = []`
`¬ slice_edge S cs a'` `sourcenode a = sourcenode a'`
have "slice_edges S cs (a#as'') = []"
by(cases "kind a'")(auto simp:slice_edge_def)
ultimately show ?thesis by blast
next
case (Return Q p f)
with Cons `same_level_path_aux [] as` have False by simp
thus ?thesis by simp
qed
qed
qed
qed
subsection {* @{text "S,f \<turnstile> (ms,s) =as=>* (ms',s')"} : the reflexive transitive
closure of @{text "S,f \<turnstile> (ms,s) =as=> (ms',s')"} *}
inductive trans_observable_moves ::
"'node SDG_node set => ('edge => ('var,'val,'ret,'pname) edge_kind) => 'node list =>
(('var \<rightharpoonup> 'val) × 'ret) list => 'edge list => 'node list =>
(('var \<rightharpoonup> 'val) × 'ret) list => bool"
("_,_ \<turnstile> '(_,_') =_=>* '(_,_')" [51,50,0,0,50,0,0] 51)
where tom_Nil:
"length ms = length s ==> S,f \<turnstile> (ms,s) =[]=>* (ms,s)"
| tom_Cons:
"[|S,f \<turnstile> (ms,s) =as=> (ms',s'); S,f \<turnstile> (ms',s') =as'=>* (ms'',s'')|]
==> S,f \<turnstile> (ms,s) =(last as)#as'=>* (ms'',s'')"
lemma tom_split_snoc:
assumes "S,f \<turnstile> (ms,s) =as=>* (ms',s')" and "as ≠ []"
obtains asx asx' ms'' s'' where "as = asx@[last asx']"
and "S,f \<turnstile> (ms,s) =asx=>* (ms'',s'')" and "S,f \<turnstile> (ms'',s'') =asx'=> (ms',s')"
proof(atomize_elim)
from assms show "∃asx asx' ms'' s''. as = asx @ [last asx'] ∧
S,f \<turnstile> (ms,s) =asx=>* (ms'',s'') ∧ S,f \<turnstile> (ms'',s'') =asx'=> (ms',s')"
proof(induct rule:trans_observable_moves.induct)
case (tom_Cons S f ms s as ms' s' as' ms'' s'')
note IH = `as' ≠ [] ==> ∃asx asx' msx sx. as' = asx @ [last asx'] ∧
S,f \<turnstile> (ms',s') =asx=>* (msx,sx) ∧ S,f \<turnstile> (msx,sx) =asx'=> (ms'',s'')`
show ?case
proof(cases "as' = []")
case True
with `S,f \<turnstile> (ms',s') =as'=>* (ms'',s'')` have [simp]:"ms'' = ms'" "s'' = s'"
by(auto elim:trans_observable_moves.cases)
from `S,f \<turnstile> (ms,s) =as=> (ms',s')` have "length ms = length s"
by(rule observable_moves_equal_length)
hence "S,f \<turnstile> (ms,s) =[]=>* (ms,s)" by(rule tom_Nil)
with `S,f \<turnstile> (ms,s) =as=> (ms',s')` True show ?thesis by fastforce
next
case False
from IH[OF this] obtain xs xs' msx sx where "as' = xs @ [last xs']"
and "S,f \<turnstile> (ms',s') =xs=>* (msx,sx)"
and "S,f \<turnstile> (msx,sx) =xs'=> (ms'',s'')" by blast
from `S,f \<turnstile> (ms,s) =as=> (ms',s')` `S,f \<turnstile> (ms',s') =xs=>* (msx,sx)`
have "S,f \<turnstile> (ms,s) =(last as)#xs=>* (msx,sx)"
by(rule trans_observable_moves.tom_Cons)
with `S,f \<turnstile> (msx,sx) =xs'=> (ms'',s'')` `as' = xs @ [last xs']`
show ?thesis by fastforce
qed
qed simp
qed
lemma tom_preserves_stacks:
assumes "S,f \<turnstile> (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'"
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'"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m ms cs rs
rule:trans_observable_moves.induct)
case (tom_Nil sx n⇣c f)
thus ?case
apply(rule_tac x="cs" in exI)
apply(rule_tac x="rs" in exI)
by clarsimp
next
case (tom_Cons S f sx as msx' sx' 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'`
from `S,f \<turnstile> (m # ms,sx) =as=> (msx',sx')`
obtain m'' ms'' where "msx' = m''#ms''"
apply(cases msx') apply(auto elim!:observable_moves.cases observable_move.cases)
by(case_tac "msaa") auto
with `S,f \<turnstile> (m # ms,sx) =as=> (msx',sx')` `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''"
by(auto elim!:observable_moves_preserves_stack)
from IH[OF `msx' = m''#ms''` this(1-6)]
show ?case by fastforce
qed
qed
lemma vpa_trans_observable_moves:
assumes "valid_path_aux cs as" and "m -as->* m'" and "preds (kinds as) s"
and "transfers (kinds as) s = 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 "length s = Suc (length cs)"
obtains ms ms'' s'' ms' as' as''
where "S,kind \<turnstile> (m#ms,s) =slice_edges S cs as=>* (ms'',s'')"
and "S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',s')"
and "ms = targetnodes rs" and "length ms = length cs"
and "∀i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
and "slice_edges S cs as = slice_edges S cs as''"
and "m -as''@as'->* m'" and "valid_path_aux cs (as''@as')"
proof(atomize_elim)
from assms show "∃ms ms'' s'' as' ms' as''.
S,kind \<turnstile> (m # ms,s) =slice_edges S cs as=>* (ms'',s'') ∧
S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s') ∧
ms = targetnodes rs ∧ length ms = length cs ∧
(∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))) ∧
slice_edges S cs as = slice_edges S cs as'' ∧
m -as'' @ as'->* m' ∧ valid_path_aux cs (as'' @ as')"
proof(induct arbitrary:m s rs rule:vpa_induct)
case (vpa_empty cs)
from `m -[]->* m'` have [simp]:"m' = m" by fastforce
from `transfers (kinds []) s = s'` `length s = Suc (length cs)`
have [simp]:"s' = s" by(cases cs)(auto simp:kinds_def)
from `valid_call_list cs m` `valid_return_list rs m`
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)` `length rs = length cs`
have "∀i<length cs. call_of_return_node (targetnodes rs!i) (sourcenode (cs!i))"
by(rule get_return_edges_call_of_return_nodes)
with `length s = Suc (length cs)` `m -[]->* m'` `length rs = length cs` show ?case
apply(rule_tac x="targetnodes rs" in exI)
apply(rule_tac x="m#targetnodes rs" in exI)
apply(rule_tac x="s" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="targetnodes rs" in exI)
apply(rule_tac x="[]" in exI)
by(fastforce intro:tom_Nil silent_moves_Nil simp:targetnodes_def)
next
case (vpa_intra cs a as)
note IH = `!!m s rs. [|m -as->* m'; preds (kinds as) s; transfers (kinds as) s = 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; length s = Suc (length cs)|]
==> ∃ms ms'' s'' as' ms' as''.
S,kind \<turnstile> (m # ms,s) =slice_edges S cs as=>* (ms'',s'') ∧
S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s') ∧ ms = targetnodes rs ∧
length ms = length cs ∧
(∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))) ∧
slice_edges S cs as = slice_edges S cs as'' ∧
m -as'' @ as'->* m' ∧ valid_path_aux cs (as'' @ as')`
from `m -a # as->* m'` have "m = sourcenode a" and "valid_edge a"
and "targetnode a -as->* m'" by(auto elim:path_split_Cons)
from `preds (kinds (a # as)) s` have "pred (kind a) s"
and "preds (kinds as) (transfer (kind a) s)" by(auto simp:kinds_def)
from `transfers (kinds (a # as)) s = s'`
have "transfers (kinds as) (transfer (kind a) s) = s'" by(fastforce simp:kinds_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 `intra_kind (kind a)` `length s = Suc (length cs)`
have "length (transfer (kind a) s) = Suc (length cs)"
by(cases s)(auto simp:intra_kind_def)
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 IH[OF `targetnode a -as->* m'` `preds (kinds as) (transfer (kind a) s)`
`transfers (kinds as) (transfer (kind a) s) = s'`
`valid_call_list cs (targetnode a)`
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)` this `length rs = length cs`
`length (transfer (kind a) s) = Suc (length cs)`]
obtain ms ms'' s'' as' ms' as'' where "length ms = length cs"
and "S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s) =slice_edges S cs as=>*
(ms'',s'')"
and paths:"S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s')"
"ms = targetnodes rs"
"∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))"
"slice_edges S cs as = slice_edges S cs as''"
"targetnode a -as'' @ as'->* m'" "valid_path_aux cs (as'' @ as')"
by blast
from `∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))`
`length ms = length cs`
have "∀mx ∈ set ms. return_node mx"
by(auto simp:call_of_return_node_def in_set_conv_nth)
show ?case
proof(cases "(∀m ∈ set ms. ∃m'. call_of_return_node m m' ∧
m' ∈ ⌊HRB_slice S⌋⇘CFG⇙) ∧ m ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `m = sourcenode a` `length ms = length cs` `intra_kind (kind a)`
`∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))`
have "slice_edge S cs a"
by(fastforce simp:slice_edge_def in_set_conv_nth intra_kind_def)
with `intra_kind (kind a)`
have "slice_edges S cs (a#as) = a#slice_edges S cs as"
by(fastforce simp:intra_kind_def)
from True `pred (kind a) s` `valid_edge a` `intra_kind (kind a)`
`∀mx ∈ set ms. return_node mx` `length ms = length cs` `m = sourcenode a`
`length s = Suc (length cs)` `length (transfer (kind a) s) = Suc (length cs)`
have "S,kind \<turnstile> (sourcenode a#ms,s) -a-> (targetnode a#ms,transfer (kind a) s)"
by(fastforce intro!:observable_move_intra)
with `length ms = length cs` `length s = Suc (length cs)`
have "S,kind \<turnstile> (sourcenode a#ms,s) =[]@[a]=>
(targetnode a#ms,transfer (kind a) s)"
by(fastforce intro:observable_moves_snoc silent_moves_Nil)
with `S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s) =slice_edges S cs as=>*
(ms'',s'')`
have "S,kind \<turnstile> (sourcenode a#ms,s) =last [a]#slice_edges S cs as=>* (ms'',s'')"
by(fastforce intro:tom_Cons)
with `slice_edges S cs (a#as) = a#slice_edges S cs as`
have "S,kind \<turnstile> (sourcenode a#ms,s) =slice_edges S cs (a#as)=>* (ms'',s'')"
by simp
moreover
from `slice_edges S cs as = slice_edges S cs as''` `slice_edge S cs a`
`intra_kind (kind a)`
have "slice_edges S cs (a#as) = slice_edges S cs (a#as'')"
by(fastforce simp:intra_kind_def)
ultimately show ?thesis
using paths `m = sourcenode a` `valid_edge a` `intra_kind (kind a)`
`length ms = length cs` `slice_edges S cs (a#as) = a#slice_edges S cs as`
apply(rule_tac x="ms" in exI)
apply(rule_tac x="ms''" in exI)
apply(rule_tac x="s''" in exI)
apply(rule_tac x="as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="a#as''" in exI)
by(auto intro:Cons_path simp:intra_kind_def)
next
case False
with `∀mx ∈ set ms. return_node mx`
have disj:"(∃m ∈ set ms. ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:return_node_call_of_return_node)
with `m = sourcenode a` `length ms = length cs` `intra_kind (kind a)`
`∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))`
have "¬ slice_edge S cs a"
by(fastforce simp:slice_edge_def in_set_conv_nth intra_kind_def)
with `intra_kind (kind a)`
have "slice_edges S cs (a#as) = slice_edges S cs as"
by(fastforce simp:intra_kind_def)
from disj `pred (kind a) s` `valid_edge a` `intra_kind (kind a)`
`∀mx ∈ set ms. return_node mx` `length ms = length cs` `m = sourcenode a`
`length s = Suc (length cs)` `length (transfer (kind a) s) = Suc (length cs)`
have "S,kind \<turnstile> (sourcenode a#ms,s) -a->⇣τ (targetnode a#ms,transfer (kind a) s)"
by(fastforce intro!:silent_move_intra)
from `S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s) =slice_edges S cs as=>*
(ms'',s'')`
show ?thesis
proof(rule trans_observable_moves.cases)
fix msx sx n⇣c' f
assume "targetnode a # ms = msx"
and "transfer (kind a) s = sx" and "slice_edges S cs as = []"
and [simp]:"ms'' = msx" "s'' = sx" and "length msx = length sx"
from `slice_edges S cs (a#as) = slice_edges S cs as`
`slice_edges S cs as = []`
have "slice_edges S cs (a#as) = []" by simp
with `length ms = length cs` `length s = Suc (length cs)`
have "S,kind \<turnstile> (sourcenode a#ms,s) =slice_edges S cs (a#as)=>*
(sourcenode a#ms,s)"
by(fastforce intro:tom_Nil)
moreover
from `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',s')` `targetnode a # ms = msx`
`transfer (kind a) s = sx` `ms'' = msx` `s'' = sx`
`S,kind \<turnstile> (sourcenode a#ms,s) -a->⇣τ (targetnode a#ms,transfer (kind a) s)`
have "S,kind \<turnstile> (sourcenode a#ms,s) =a#as'=>⇣τ (m'#ms',s')"
by(fastforce intro:silent_moves_Cons)
from this `valid_edge a` `∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`ms = targetnodes rs` `valid_return_list rs m` `length rs = length cs`
`length s = Suc (length cs)` `m = sourcenode a`
have "sourcenode a -a#as'->* m'" and "valid_path_aux cs (a#as')"
by -(rule silent_moves_vpa_path,(fastforce simp:targetnodes_def)+)+
ultimately show ?thesis using `m = sourcenode a` `length ms = length cs`
`∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))`
`slice_edges S cs (a#as) = []` `intra_kind (kind a)`
`S,kind \<turnstile> (sourcenode a#ms,s) =a#as'=>⇣τ (m'#ms',s')`
`ms = targetnodes rs`
apply(rule_tac x="ms" in exI)
apply(rule_tac x="sourcenode a#ms" in exI)
apply(rule_tac x="s" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="[]" in exI)
by(auto simp:intra_kind_def)
next
fix S' f msx sx asx msx' sx' asx' msx'' sx''
assume [simp]:"S = S'" and "kind = f" and "targetnode a # ms = msx"
and "transfer (kind a) s = sx" and "slice_edges S cs as = last asx # asx'"
and "ms'' = msx''" and "s'' = sx''"
and "S',f \<turnstile> (msx,sx) =asx=> (msx',sx')"
and "S',f \<turnstile> (msx',sx') =asx'=>* (msx'',sx'')"
from `kind = f` have [simp]:"f = kind" by simp
from `S,kind \<turnstile> (sourcenode a#ms,s) -a->⇣τ
(targetnode a#ms,transfer (kind a) s)` `S',f \<turnstile> (msx,sx) =asx=> (msx',sx')`
`transfer (kind a) s = sx` `targetnode a # ms = msx`
have "S,kind \<turnstile> (sourcenode a#ms,s) =a#asx=> (msx',sx')"
by(fastforce intro:silent_move_observable_moves)
with `S',f \<turnstile> (msx',sx') =asx'=>* (msx'',sx'')` `ms'' = msx''` `s'' = sx''`
have "S,kind \<turnstile> (sourcenode a#ms,s) =last (a#asx)#asx'=>* (ms'',s'')"
by(fastforce intro:trans_observable_moves.tom_Cons)
moreover
from `S',f \<turnstile> (msx,sx) =asx=> (msx',sx')` have "asx ≠ []"
by(fastforce elim:observable_moves.cases)
with `slice_edges S cs (a#as) = slice_edges S cs as`
`slice_edges S cs as = last asx # asx'`
have "slice_edges S cs (a#as) = last (a#asx)#asx'" by simp
moreover
from `¬ slice_edge S cs a` `slice_edges S cs as = slice_edges S cs as''`
`intra_kind (kind a)`
have "slice_edges S cs (a # as) = slice_edges S cs (a # as'')"
by(fastforce simp:intra_kind_def)
ultimately show ?thesis using paths `m = sourcenode a` `intra_kind (kind a)`
`length ms = length cs` `ms = targetnodes rs` `valid_edge a`
apply(rule_tac x="ms" in exI)
apply(rule_tac x="ms''" in exI)
apply(rule_tac x="s''" in exI)
apply(rule_tac x="as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="a#as''" in exI)
by(auto intro:Cons_path simp:intra_kind_def)
qed
qed
next
case (vpa_Call cs a as Q r p fs)
note IH = `!!m s rs. [|m -as->* m'; preds (kinds as) s; transfers (kinds as) s = s';
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);
length s = Suc (length (a # cs))|]
==> ∃ms ms'' s'' as' ms' as''.
S,kind \<turnstile> (m # ms,s) =slice_edges S (a # cs) as=>* (ms'',s'') ∧
S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s') ∧ ms = targetnodes rs ∧
length ms = length (a # cs) ∧
(∀i<length (a # cs). call_of_return_node (ms ! i) (sourcenode ((a # cs) ! i))) ∧
slice_edges S (a # cs) as = slice_edges S (a # cs) as'' ∧
m -as'' @ as'->* m' ∧ valid_path_aux (a # cs) (as'' @ as')`
from `m -a # as->* m'` have "m = sourcenode a" and "valid_edge a"
and "targetnode a -as->* m'" by(auto elim:path_split_Cons)
from `preds (kinds (a # as)) s` have "pred (kind a) s"
and "preds (kinds as) (transfer (kind a) s)" by(auto simp:kinds_def)
from `transfers (kinds (a # as)) s = s'`
have "transfers (kinds as) (transfer (kind a) s) = s'" by(fastforce simp:kinds_def)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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 `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` obtain a' where "a' ∈ get_return_edges a"
by(fastforce dest:get_return_edge_call)
with `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'"
by(fastforce dest!:call_return_edges)
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'\<hookleftarrow>⇘p⇙f'` have "get_proc (sourcenode a') = p"
by(rule get_proc_return)
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 "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'\<hookleftarrow>⇘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 `length s = Suc (length cs)` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "length (transfer (kind a) s) = Suc (length (a#cs))"
by(cases s) auto
from IH[OF `targetnode a -as->* m'` `preds (kinds as) (transfer (kind a) s)`
`transfers (kinds as) (transfer (kind a) s) = s'`
`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)`
`length (transfer (kind a) s) = Suc (length (a#cs))`]
obtain ms ms'' s'' as' ms' as'' where "length ms = length (a#cs)"
and "S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s)
=slice_edges S (a#cs) as=>* (ms'',s'')"
and paths:"S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s')"
"ms = targetnodes (a'#rs)"
"∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))"
"slice_edges S (a#cs) as = slice_edges S (a#cs) as''"
"targetnode a -as'' @ as'->* m'" "valid_path_aux (a#cs) (as'' @ as')"
by blast
from `ms = targetnodes (a'#rs)` obtain x xs where [simp]:"ms = x#xs"
and "x = targetnode a'" and "xs = targetnodes rs"
by(cases ms)(auto simp:targetnodes_def)
from `∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))`
`length ms = length (a#cs)`
have "∀mx ∈ set xs. return_node mx"
apply(auto simp:in_set_conv_nth) apply(case_tac i)
apply(erule_tac x="Suc 0" in allE)
by(auto simp:call_of_return_node_def)
show ?case
proof(cases "(∀m ∈ set xs. ∃m'. call_of_return_node m m' ∧
m' ∈ ⌊HRB_slice S⌋⇘CFG⇙) ∧ sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))`
`length ms = length (a#cs)` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "slice_edge S cs a"
apply(auto simp:slice_edge_def in_set_conv_nth)
by(erule_tac x="Suc i" in allE) auto
with `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "slice_edges S cs (a#as) = a#slice_edges S (a#cs) as" by simp
from True `pred (kind a) s` `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`valid_edge a'` `a' ∈ get_return_edges a`
`∀mx ∈ set xs. return_node mx` `length ms = length (a#cs)` `m = sourcenode a`
`length s = Suc (length cs)`
`length (transfer (kind a) s) = Suc (length (a#cs))`
have "S,kind \<turnstile> (sourcenode a#xs,s) -a->
(targetnode a#targetnode a'#xs,transfer (kind a) s)"
by -(rule_tac a'="a'" in observable_move_call,fastforce+)
with `length ms = length (a#cs)` `length s = Suc (length cs)`
have "S,kind \<turnstile> (sourcenode a#xs,s) =[]@[a]=>
(targetnode a#targetnode a'#xs,transfer (kind a) s)"
by(fastforce intro:observable_moves_snoc silent_moves_Nil)
with `S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s)
=slice_edges S (a#cs) as=>* (ms'',s'')` `x = targetnode a'`
have "S,kind \<turnstile> (sourcenode a#xs,s) =last [a]#slice_edges S (a#cs) as=>*
(ms'',s'')"
by -(rule tom_Cons,auto)
with `slice_edges S cs (a#as) = a#slice_edges S (a#cs) as`
have "S,kind \<turnstile> (sourcenode a#xs,s) =slice_edges S cs (a#as)=>* (ms'',s'')"
by simp
moreover
from `slice_edges S (a#cs) as = slice_edges S (a#cs) as''`
`slice_edge S cs a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "slice_edges S cs (a#as) = slice_edges S cs (a#as'')" by simp
ultimately show ?thesis
using paths `m = sourcenode a` `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`length ms = length (a#cs)` `xs = targetnodes rs`
`slice_edges S cs (a#as) = a#slice_edges S (a#cs) as`
apply(rule_tac x="xs" in exI)
apply(rule_tac x="ms''" in exI)
apply(rule_tac x="s''" in exI)
apply(rule_tac x="as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="a#as''" in exI)
by(auto intro:Cons_path simp:targetnodes_def)
next
case False
with `∀mx ∈ set xs. return_node mx`
have disj:"(∃m ∈ set xs. ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:return_node_call_of_return_node)
with `∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))`
`length ms = length (a#cs)` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "¬ slice_edge S cs a"
apply(auto simp:slice_edge_def in_set_conv_nth)
by(erule_tac x="Suc i" in allE) auto
with `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "slice_edges S cs (a#as) = slice_edges S (a#cs) as" by simp
from disj `pred (kind a) s` `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`valid_edge a'` `a' ∈ get_return_edges a`
`∀mx ∈ set xs. return_node mx` `length ms = length (a#cs)` `m = sourcenode a`
`length s = Suc (length cs)`
`length (transfer (kind a) s) = Suc (length (a#cs))`
have "S,kind \<turnstile> (sourcenode a#xs,s) -a->⇣τ
(targetnode a#targetnode a'#xs,transfer (kind a) s)"
by -(rule_tac a'="a'" in silent_move_call,fastforce+)
from `S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s)
=slice_edges S (a#cs) as=>* (ms'',s'')`
show ?thesis
proof(rule trans_observable_moves.cases)
fix msx sx S' f
assume "targetnode a # ms = msx"
and "transfer (kind a) s = sx" and "slice_edges S (a#cs) as = []"
and [simp]:"ms'' = msx" "s'' = sx" and "length msx = length sx"
from `slice_edges S cs (a#as) = slice_edges S (a#cs) as`
`slice_edges S (a#cs) as = []`
have "slice_edges S cs (a#as) = []" by simp
with `length ms = length (a#cs)` `length s = Suc (length cs)`
have "S,kind \<turnstile> (sourcenode a#xs,s) =slice_edges S cs (a#as)=>*
(sourcenode a#xs,s)"
by(fastforce intro:tom_Nil)
moreover
from `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',s')` `targetnode a # ms = msx`
`transfer (kind a) s = sx` `ms'' = msx` `s'' = sx` `x = targetnode a'`
`S,kind \<turnstile> (sourcenode a#xs,s) -a->⇣τ
(targetnode a#targetnode a'#xs,transfer (kind a) s)`
have "S,kind \<turnstile> (sourcenode a#xs,s) =a#as'=>⇣τ (m'#ms',s')"
by(auto intro:silent_moves_Cons)
from this `valid_edge a`
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`xs = targetnodes rs` `valid_return_list rs m` `length rs = length cs`
`length s = Suc (length cs)` `m = sourcenode a`
have "sourcenode a -a#as'->* m'" and "valid_path_aux cs (a#as')"
by -(rule silent_moves_vpa_path,(fastforce simp:targetnodes_def)+)+
ultimately show ?thesis using `m = sourcenode a` `length ms = length (a#cs)`
`∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))`
`slice_edges S cs (a#as) = []` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`S,kind \<turnstile> (sourcenode a#xs,s) =a#as'=>⇣τ (m'#ms',s')`
`xs = targetnodes rs`
apply(rule_tac x="xs" in exI)
apply(rule_tac x="sourcenode a#xs" in exI)
apply(rule_tac x="s" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="[]" in exI)
by auto
next
fix S' f msx sx asx msx' sx' asx' msx'' sx''
assume [simp]:"S = S'" and "kind = f" and "targetnode a # ms = msx"
and "transfer (kind a) s = sx"
and "slice_edges S (a#cs) as = last asx # asx'"
and "ms'' = msx''" and "s'' = sx''"
and "S',f \<turnstile> (msx,sx) =asx=> (msx',sx')"
and "S',f \<turnstile> (msx',sx') =asx'=>* (msx'',sx'')"
from `kind = f` have [simp]:"f = kind" by simp
from `S,kind \<turnstile> (sourcenode a#xs,s) -a->⇣τ
(targetnode a#targetnode a'#xs,transfer (kind a) s)`
`S',f \<turnstile> (msx,sx) =asx=> (msx',sx')` `x = targetnode a'`
`transfer (kind a) s = sx` `targetnode a # ms = msx`
have "S,kind \<turnstile> (sourcenode a#xs,s) =a#asx=> (msx',sx')"
by(auto intro:silent_move_observable_moves)
with `S',f \<turnstile> (msx',sx') =asx'=>* (msx'',sx'')` `ms'' = msx''` `s'' = sx''`
have "S,kind \<turnstile> (sourcenode a#xs,s) =last (a#asx)#asx'=>* (ms'',s'')"
by(fastforce intro:trans_observable_moves.tom_Cons)
moreover
from `S',f \<turnstile> (msx,sx) =asx=> (msx',sx')` have "asx ≠ []"
by(fastforce elim:observable_moves.cases)
with `slice_edges S cs (a#as) = slice_edges S (a#cs) as`
`slice_edges S (a#cs) as = last asx # asx'`
have "slice_edges S cs (a#as) = last (a#asx)#asx'" by simp
moreover
from `¬ slice_edge S cs a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`slice_edges S (a#cs) as = slice_edges S (a#cs) as''`
have "slice_edges S cs (a # as) = slice_edges S cs (a # as'')" by simp
ultimately show ?thesis using paths `m = sourcenode a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`length ms = length (a#cs)` `xs = targetnodes rs` `valid_edge a`
apply(rule_tac x="xs" in exI)
apply(rule_tac x="ms''" in exI)
apply(rule_tac x="s''" in exI)
apply(rule_tac x="as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="a#as''" in exI)
by(auto intro:Cons_path simp:targetnodes_def)
qed
qed
next
case (vpa_ReturnEmpty cs a as Q p f)
from `preds (kinds (a # as)) s` `length s = Suc (length cs)` `kind a = Q\<hookleftarrow>⇘p⇙f`
`cs = []`
have False by(cases s)(auto simp:kinds_def)
thus ?case by simp
next
case (vpa_ReturnCons cs a as Q p f c' cs')
note IH = `!!m s rs. [|m -as->* m'; preds (kinds as) s; transfers (kinds as) s = 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'; length s = Suc (length cs')|]
==> ∃ms ms'' s'' as' ms' as''.
S,kind \<turnstile> (m # ms,s) =slice_edges S cs' as=>* (ms'',s'') ∧
S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s') ∧ ms = targetnodes rs ∧
length ms = length cs' ∧
(∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))) ∧
slice_edges S cs' as = slice_edges S cs' as'' ∧
m -as'' @ as'->* m' ∧ valid_path_aux cs' (as'' @ as')`
from `m -a # as->* m'` have "m = sourcenode a" and "valid_edge a"
and "targetnode a -as->* m'" by(auto elim:path_split_Cons)
from `preds (kinds (a # as)) s` have "pred (kind a) s"
and "preds (kinds as) (transfer (kind a) s)" by(auto simp:kinds_def)
from `transfers (kinds (a # as)) s = s'`
have "transfers (kinds as) (transfer (kind a) s) = s'" by(fastforce simp:kinds_def)
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(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 `length s = Suc (length cs)` `cs = c' # cs'` `kind a = Q\<hookleftarrow>⇘p⇙f`
have "length (transfer (kind a) s) = Suc (length cs')"
by(cases s)(auto,case_tac list,auto)
from IH[OF `targetnode a -as->* m'` `preds (kinds as) (transfer (kind a) s)`
`transfers (kinds as) (transfer (kind a) s) = s'`
`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'` this]
obtain ms ms'' s'' as' ms' as'' where "length ms = length cs'"
and "S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s)
=slice_edges S cs' as=>* (ms'',s'')"
and paths:"S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s')"
"ms = targetnodes rs'"
"∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))"
"slice_edges S cs' as = slice_edges S cs' as''"
"targetnode a -as'' @ as'->* m'" "valid_path_aux cs' (as'' @ as')"
by blast
from `∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))`
`length ms = length cs'`
have "∀mx ∈ set ms. return_node mx"
by(auto simp:in_set_conv_nth call_of_return_node_def)
from `valid_edge a` `valid_edge c'` `a ∈ get_return_edges c'`
have "return_node (targetnode a)" by(fastforce simp:return_node_def)
with `valid_edge c'` `valid_edge a` `a ∈ get_return_edges c'`
have "call_of_return_node (targetnode a) (sourcenode c')"
by(simp add:call_of_return_node_def) blast
show ?case
proof(cases "(∀m ∈ set (targetnode a#ms). ∃m'. call_of_return_node m m' ∧
m' ∈ ⌊HRB_slice S⌋⇘CFG⇙)")
case True
then obtain x where "call_of_return_node (targetnode a) x"
and "x ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
with `call_of_return_node (targetnode a) (sourcenode c')`
have "sourcenode c' ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
with True `∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))`
`length ms = length cs'` `cs = c' # cs'` `kind a = Q\<hookleftarrow>⇘p⇙f`
have "slice_edge S cs a"
apply(auto simp:slice_edge_def in_set_conv_nth)
by(erule_tac x="i" in allE) auto
with `kind a = Q\<hookleftarrow>⇘p⇙f` `cs = c' # cs'`
have "slice_edges S cs (a#as) = a#slice_edges S cs' as" by simp
from True `pred (kind a) s` `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f`
`∀mx ∈ set ms. return_node mx` `length ms = length cs'`
`length s = Suc (length cs)` `m = sourcenode a`
`length (transfer (kind a) s) = Suc (length cs')`
`return_node (targetnode a)` `cs = c' # cs'`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) -a->
(targetnode a#ms,transfer (kind a) s)"
by(auto intro!:observable_move_return)
with `length ms = length cs'` `length s = Suc (length cs)` `cs = c' # cs'`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) =[]@[a]=>
(targetnode a#ms,transfer (kind a) s)"
by(fastforce intro:observable_moves_snoc silent_moves_Nil)
with `S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s)
=slice_edges S cs' as=>* (ms'',s'')`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s)
=last [a]#slice_edges S cs' as=>* (ms'',s'')"
by -(rule tom_Cons,auto)
with `slice_edges S cs (a#as) = a#slice_edges S cs' as`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) =slice_edges S cs (a#as)=>*
(ms'',s'')" by simp
moreover
from `slice_edges S cs' as = slice_edges S cs' as''`
`slice_edge S cs a` `kind a = Q\<hookleftarrow>⇘p⇙f` `cs = c' # cs'`
have "slice_edges S cs (a#as) = slice_edges S cs (a#as'')" by simp
ultimately show ?thesis
using paths `m = sourcenode a` `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f`
`length ms = length cs'` `ms = targetnodes rs'` `cs = c' # cs'`
`slice_edges S cs (a#as) = a#slice_edges S cs' as`
`a ∈ get_return_edges c'`
`call_of_return_node (targetnode a) (sourcenode c')`
apply(rule_tac x="targetnode a#ms" in exI)
apply(rule_tac x="ms''" in exI)
apply(rule_tac x="s''" in exI)
apply(rule_tac x="as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="a#as''" in exI)
apply(auto intro:Cons_path simp:targetnodes_def)
by(case_tac i) auto
next
case False
with `∀mx ∈ set ms. return_node mx` `return_node (targetnode a)`
have "∃m ∈ set (targetnode a # ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:return_node_call_of_return_node)
with `∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))`
`length ms = length cs'` `cs = c' # cs'` `kind a = Q\<hookleftarrow>⇘p⇙f`
`call_of_return_node (targetnode a) (sourcenode c')`
have "¬ slice_edge S cs a"
apply(auto simp:slice_edge_def in_set_conv_nth)
by(erule_tac x="i" in allE) auto
with `kind a = Q\<hookleftarrow>⇘p⇙f` `cs = c' # cs'`
have "slice_edges S cs (a#as) = slice_edges S cs' as" by simp
from `pred (kind a) s` `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f`
`∀mx ∈ set ms. return_node mx` `length ms = length cs'`
`length s = Suc (length cs)` `m = sourcenode a`
`length (transfer (kind a) s) = Suc (length cs')`
`return_node (targetnode a)` `cs = c' # cs'`
`∃m ∈ set (targetnode a # ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) -a->⇣τ
(targetnode a#ms,transfer (kind a) s)"
by(auto intro!:silent_move_return)
from `S,kind \<turnstile> (targetnode a # ms,transfer (kind a) s)
=slice_edges S cs' as=>* (ms'',s'')`
show ?thesis
proof(rule trans_observable_moves.cases)
fix msx sx S' f'
assume "targetnode a # ms = msx"
and "transfer (kind a) s = sx" and "slice_edges S cs' as = []"
and [simp]:"ms'' = msx" "s'' = sx" and "length msx = length sx"
from `slice_edges S cs (a#as) = slice_edges S cs' as`
`slice_edges S cs' as = []`
have "slice_edges S cs (a#as) = []" by simp
with `length ms = length cs'` `length s = Suc (length cs)` `cs = c' # cs'`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) =slice_edges S cs (a#as)=>*
(sourcenode a#targetnode a#ms,s)"
by(fastforce intro:tom_Nil)
moreover
from `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',s')` `targetnode a # ms = msx`
`transfer (kind a) s = sx` `ms'' = msx` `s'' = sx`
`S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) -a->⇣τ
(targetnode a#ms,transfer (kind a) s)`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) =a#as'=>⇣τ (m'#ms',s')"
by(auto intro:silent_moves_Cons)
from this `valid_edge a`
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`valid_return_list rs m` `length rs = length cs`
`length s = Suc (length cs)` `m = sourcenode a`
`ms = targetnodes rs'` `rs = r'#rs'` `cs = c' # cs'`
have "sourcenode a -a#as'->* m'" and "valid_path_aux cs (a#as')"
by -(rule silent_moves_vpa_path,(fastforce simp:targetnodes_def)+)+
ultimately show ?thesis using `m = sourcenode a` `length ms = length cs'`
`∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))`
`slice_edges S cs (a#as) = []` `kind a = Q\<hookleftarrow>⇘p⇙f`
`S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) =a#as'=>⇣τ (m'#ms',s')`
`ms = targetnodes rs'` `rs = r'#rs'` `cs = c' # cs'`
`call_of_return_node (targetnode a) (sourcenode c')`
apply(rule_tac x="targetnode a#ms" in exI)
apply(rule_tac x="sourcenode a#targetnode a#ms" in exI)
apply(rule_tac x="s" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="[]" in exI)
apply(auto simp:targetnodes_def)
by(case_tac i) auto
next
fix S' f' msx sx asx msx' sx' asx' msx'' sx''
assume [simp]:"S = S'" and "kind = f'" and "targetnode a # ms = msx"
and "transfer (kind a) s = sx"
and "slice_edges S cs' as = last asx # asx'"
and "ms'' = msx''" and "s'' = sx''"
and "S',f' \<turnstile> (msx,sx) =asx=> (msx',sx')"
and "S',f' \<turnstile> (msx',sx') =asx'=>* (msx'',sx'')"
from `kind = f'` have [simp]:"f' = kind" by simp
from `S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) -a->⇣τ
(targetnode a#ms,transfer (kind a) s)`
`S',f' \<turnstile> (msx,sx) =asx=> (msx',sx')`
`transfer (kind a) s = sx` `targetnode a # ms = msx`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) =a#asx=> (msx',sx')"
by(auto intro:silent_move_observable_moves)
with `S',f' \<turnstile> (msx',sx') =asx'=>* (msx'',sx'')` `ms'' = msx''` `s'' = sx''`
have "S,kind \<turnstile> (sourcenode a#targetnode a#ms,s) =last (a#asx)#asx'=>*
(ms'',s'')"
by(fastforce intro:trans_observable_moves.tom_Cons)
moreover
from `S',f' \<turnstile> (msx,sx) =asx=> (msx',sx')` have "asx ≠ []"
by(fastforce elim:observable_moves.cases)
with `slice_edges S cs (a#as) = slice_edges S cs' as`
`slice_edges S cs' as = last asx # asx'`
have "slice_edges S cs (a#as) = last (a#asx)#asx'" by simp
moreover
from `¬ slice_edge S cs a` `kind a = Q\<hookleftarrow>⇘p⇙f`
`slice_edges S cs' as = slice_edges S cs' as''` `cs = c' # cs'`
have "slice_edges S cs (a # as) = slice_edges S cs (a # as'')" by simp
ultimately show ?thesis using paths `m = sourcenode a` `kind a = Q\<hookleftarrow>⇘p⇙f`
`length ms = length cs'` `ms = targetnodes rs'` `valid_edge a`
`rs = r'#rs'` `cs = c' # cs'` `r' ∈ get_return_edges c'`
`call_of_return_node (targetnode a) (sourcenode c')`
apply(rule_tac x="targetnode a#ms" in exI)
apply(rule_tac x="ms''" in exI)
apply(rule_tac x="s''" in exI)
apply(rule_tac x="as'" in exI)
apply(rule_tac x="ms'" in exI)
apply(rule_tac x="a#as''" in exI)
apply(auto intro:Cons_path simp:targetnodes_def)
by(case_tac i) auto
qed
qed
qed
qed
lemma valid_path_trans_observable_moves:
assumes "m -as->⇣\<surd>* m'" and "preds (kinds as) [cf]"
and "transfers (kinds as) [cf] = s'"
obtains ms'' s'' ms' as' as''
where "S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as=>* (ms'',s'')"
and "S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',s')"
and "slice_edges S [] as = slice_edges S [] as''"
and "m -as''@as'->⇣\<surd>* m'"
proof(atomize_elim)
from `m -as->⇣\<surd>* m'` have "valid_path_aux [] as" and "m -as->* m'"
by(simp_all add:vp_def valid_path_def)
from this `preds (kinds as) [cf]` `transfers (kinds as) [cf] = s'`
show "∃ms'' s'' as' ms' as''.
S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as=>* (ms'',s'') ∧
S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m' # ms',s') ∧
slice_edges S [] as = slice_edges S [] as'' ∧ m -as'' @ as'->⇣\<surd>* m'"
by -(erule vpa_trans_observable_moves[of _ _ _ _ _ _ "[]" S],
auto simp:valid_call_list_def valid_return_list_def vp_def valid_path_def)
qed
lemma WS_weak_sim_trans:
assumes "((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S"
and "S,kind \<turnstile> (ms⇣1,s⇣1) =as=>* (ms⇣1',s⇣1')" and "as ≠ []"
shows "((ms⇣1',s⇣1'),(ms⇣1',transfers (slice_kinds S as) s⇣2)) ∈ WS S ∧
S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>* (ms⇣1',transfers (slice_kinds S as) s⇣2)"
proof -
obtain f where "f = kind" by simp
with `S,kind \<turnstile> (ms⇣1,s⇣1) =as=>* (ms⇣1',s⇣1')`
have "S,f \<turnstile> (ms⇣1,s⇣1) =as=>* (ms⇣1',s⇣1')" by simp
from `S,f \<turnstile> (ms⇣1,s⇣1) =as=>* (ms⇣1',s⇣1')` `((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S`
`as ≠ []` `f = kind`
show ?thesis
proof(induct arbitrary:ms⇣2 s⇣2 rule:trans_observable_moves.induct)
case tom_Nil thus ?case by simp
next
case (tom_Cons S f ms s as ms' s' as' ms'' s'')
note IH = `!!ms⇣2 s⇣2. [|((ms',s'),(ms⇣2,s⇣2)) ∈ WS S; as' ≠ []; f = kind|]
==> ((ms'',s''),(ms'',transfers (slice_kinds S as') s⇣2)) ∈ WS S ∧
S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as'=>* (ms'',transfers (slice_kinds S as') s⇣2)`
from `S,f \<turnstile> (ms,s) =as=> (ms',s')` have "s' ≠ []"
by(fastforce elim:observable_moves.cases observable_move.cases)
from `S,f \<turnstile> (ms,s) =as=> (ms',s')`
obtain asx ax msx sx where "S,f \<turnstile> (ms,s) =asx=>⇣τ (msx,sx)"
and "S,f \<turnstile> (msx,sx) -ax-> (ms',s')" and "as = asx@[ax]"
by(fastforce elim:observable_moves.cases)
from `S,f \<turnstile> (ms,s) =asx=>⇣τ (msx,sx)` `((ms,s),(ms⇣2,s⇣2)) ∈ WS S` `f = kind`
have "((msx,sx),(ms⇣2,s⇣2)) ∈ WS S" by(fastforce intro:WS_silent_moves)
from `((msx,sx),(ms⇣2,s⇣2)) ∈ WS S` `S,f \<turnstile> (msx,sx) -ax-> (ms',s')` `s' ≠ []`
`f = kind`
obtain asx' where "((ms',s'),(ms',transfer (slice_kind S ax) s⇣2)) ∈ WS S"
and "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =asx'@[ax]=>
(ms',transfer (slice_kind S ax) s⇣2)"
by(fastforce elim:WS_observable_move)
show ?case
proof(cases "as' = []")
case True
with `S,f \<turnstile> (ms',s') =as'=>* (ms'',s'')` have "ms' = ms'' ∧ s' = s''"
by(fastforce elim:trans_observable_moves.cases dest:observable_move_notempty)
from `((ms',s'),(ms',transfer (slice_kind S ax) s⇣2)) ∈ WS S`
have "length ms' = length (transfer (slice_kind S ax) s⇣2)"
by(fastforce elim:WS.cases)
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =asx'@[ax]=>
(ms',transfer (slice_kind S ax) s⇣2)`
have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =(last (asx'@[ax]))#[]=>*
(ms',transfer (slice_kind S ax) s⇣2)"
by(fastforce intro:trans_observable_moves.intros)
with `((ms',s'),(ms',transfer (slice_kind S ax) s⇣2)) ∈ WS S` `as = asx@[ax]`
`ms' = ms'' ∧ s' = s''` True
show ?thesis by(fastforce simp:slice_kinds_def)
next
case False
from IH[OF `((ms',s'),(ms',transfer (slice_kind S ax) s⇣2)) ∈ WS S` this
`f = kind`]
have "((ms'',s''),(ms'',transfers (slice_kinds S as')
(transfer (slice_kind S ax) s⇣2))) ∈ WS S"
and "S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s⇣2) =as'=>*
(ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s⇣2))"
by simp_all
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =asx'@[ax]=>
(ms',transfer (slice_kind S ax) s⇣2)`
have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =(last (asx'@[ax]))#as'=>*
(ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s⇣2))"
by(fastforce intro:trans_observable_moves.tom_Cons)
with `((ms'',s''),(ms'',transfers (slice_kinds S as')
(transfer (slice_kind S ax) s⇣2))) ∈ WS S` False `as = asx@[ax]`
show ?thesis by(fastforce simp:slice_kinds_def)
qed
qed
qed
lemma stacks_rewrite:
assumes "valid_call_list cs m" and "valid_return_list rs m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
and "length rs = length cs" and "ms = targetnodes rs"
shows "∀i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
proof
fix i show "i < length cs -->
call_of_return_node (ms ! i) (sourcenode (cs ! i))"
proof
assume "i < length cs"
with `∀i < length rs. rs!i ∈ get_return_edges (cs!i)` `length rs = length cs`
have "rs!i ∈ get_return_edges (cs!i)" by fastforce
from `valid_return_list rs m` have "∀r ∈ set rs. valid_edge r"
by(rule valid_return_list_valid_edges)
with `i < length cs` `length rs = length cs`
have "valid_edge (rs!i)" by(simp add:all_set_conv_all_nth)
from `valid_call_list cs m` have "∀c ∈ set cs. valid_edge c"
by(rule valid_call_list_valid_edges)
with `i < length cs` have "valid_edge (cs!i)" by(simp add:all_set_conv_all_nth)
with `valid_edge (rs!i)` `rs!i ∈ get_return_edges (cs!i)` `ms = targetnodes rs`
`i < length cs` `length rs = length cs`
show "call_of_return_node (ms ! i) (sourcenode (cs ! i))"
by(fastforce simp:call_of_return_node_def return_node_def targetnodes_def)
qed
qed
lemma slice_tom_preds_vp:
assumes "S,slice_kind S \<turnstile> (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"
and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
obtains as' cs' rs' where "preds (slice_kinds S as') s"
and "slice_edges S cs as' = as" and "m -as'->* m'" and "valid_path_aux cs as'"
and "upd_cs cs as' = cs'" 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'" and "transfers (slice_kinds S as') s ≠ []"
and "transfers (slice_kinds S (slice_edges S cs as')) s =
transfers (slice_kinds S as') s"
proof(atomize_elim)
from assms show "∃as' cs' rs'. preds (slice_kinds S as') s ∧
slice_edges S cs as' = as ∧ m -as'->* m' ∧ valid_path_aux cs as' ∧
upd_cs cs as' = cs' ∧ 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' ∧
transfers (slice_kinds S as') s ≠ [] ∧
transfers (slice_kinds S (slice_edges S cs as')) s =
transfers (slice_kinds S as') s"
proof(induct S "slice_kind S" "m#ms" s as "m'#ms'" s'
arbitrary:m ms cs rs rule:trans_observable_moves.induct)
case (tom_Nil s n⇣c)
from `length (m' # ms') = length s` have "s ≠ []" by(cases s) auto
have "preds (slice_kinds S []) s" by(fastforce simp:slice_kinds_def)
moreover
have "slice_edges S cs [] = []" by simp
moreover
from `valid_node m'` have "m' -[]->* m'" by(fastforce intro:empty_path)
moreover
have "valid_path_aux cs []" by simp
moreover
have "upd_cs cs [] = cs" by simp
ultimately show ?case using `valid_call_list cs m'` `valid_return_list rs m'`
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)` `length rs = length cs`
`ms' = targetnodes rs` `s ≠ []` `valid_node m'`
apply(rule_tac x="[]" in exI)
apply(rule_tac x="cs" in exI)
apply(rule_tac x="rs" in exI)
by(clarsimp simp:slice_kinds_def)
next
case (tom_Cons S s as 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;
∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙|]
==> ∃as'' cs' rs'. preds (slice_kinds S as'') s' ∧
slice_edges S cs as'' = as' ∧ m -as''->* m' ∧ valid_path_aux cs as'' ∧
upd_cs cs as'' = cs' ∧ 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' ∧
transfers (slice_kinds S as'') s' ≠ [] ∧
transfers (slice_kinds S (slice_edges S cs as'')) s' =
transfers (slice_kinds S as'') s'`
note callstack = `∀mx∈set ms.
∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
from `S,slice_kind S \<turnstile> (m # ms,s) =as=> (msx',s')`
obtain asx ax xs s'' where "as = asx@[ax]"
and "S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (xs,s'')"
and "S,slice_kind S \<turnstile> (xs,s'') -ax-> (msx',s')"
by(fastforce elim:observable_moves.cases)
from `S,slice_kind S \<turnstile> (xs,s'') -ax-> (msx',s')`
obtain xs' ms'' where [simp]:"xs = sourcenode ax#xs'" "msx' = targetnode ax#ms''"
by(cases xs)(auto elim!:observable_move.cases,case_tac list,auto)
from `S,slice_kind S \<turnstile> (m # ms,s) =as=> (msx',s')` tom_Cons
obtain cs'' rs'' where results:"valid_node (targetnode ax)"
"valid_call_list cs'' (targetnode ax)"
"∀i < length rs''. rs''!i ∈ get_return_edges (cs''!i)"
"valid_return_list rs'' (targetnode ax)" "length rs'' = length cs''"
"ms'' = targetnodes rs''" and "upd_cs cs as = cs''"
by(auto elim!:observable_moves_preserves_stack)
from `S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (xs,s'')` callstack
have "∀a ∈ set asx. intra_kind (kind a)"
by simp(rule silent_moves_slice_intra_path)
with `S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (xs,s'')`
have [simp]:"xs' = ms" by(fastforce dest:silent_moves_intra_path)
from `S,slice_kind S \<turnstile> (xs,s'') -ax-> (msx',s')`
have "∀mx ∈ set ms''. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:observable_set_stack_in_slice)
from IH[OF `msx' = targetnode ax#ms''` results this]
obtain asx' cs' rs' where "preds (slice_kinds S asx') s'"
and "slice_edges S cs'' asx' = as'" and "targetnode ax -asx'->* m'"
and "valid_path_aux cs'' asx'" and "upd_cs cs'' asx' = cs'"
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'" and "transfers (slice_kinds S asx') s' ≠ []"
and trans_eq:"transfers (slice_kinds S (slice_edges S cs'' asx')) s' =
transfers (slice_kinds S asx') s'"
by blast
from `S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (xs,s'')`
have "preds (slice_kinds S asx) s" and "transfers (slice_kinds S asx) s = s''"
by(auto intro:silent_moves_preds_transfers simp:slice_kinds_def)
from `S,slice_kind S \<turnstile> (xs,s'') -ax-> (msx',s')`
have "pred (slice_kind S ax) s''" and "transfer (slice_kind S ax) s'' = s'"
by(auto elim:observable_move.cases)
with `preds (slice_kinds S asx) s` `as = asx@[ax]`
`transfers (slice_kinds S asx) s = s''`
have "preds (slice_kinds S as) s" by(simp add:preds_split slice_kinds_def)
from `transfers (slice_kinds S asx) s = s''`
`transfer (slice_kind S ax) s'' = s'` `as = asx@[ax]`
have "transfers (slice_kinds S as) s = s'"
by(simp add:transfers_split slice_kinds_def)
with `preds (slice_kinds S asx') s'` `preds (slice_kinds S as) s`
have "preds (slice_kinds S (as@asx')) s" by(simp add:preds_split slice_kinds_def)
moreover
from `valid_call_list cs m` `valid_return_list rs m`
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)` `length rs = length cs`
`ms = targetnodes rs`
have "∀i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
by(rule stacks_rewrite)
with `S,slice_kind S \<turnstile> (m # ms,s) =as=> (msx',s')` `ms = targetnodes rs`
`length rs = length cs`
have "slice_edges S cs as = [last as]"
by(fastforce elim:observable_moves_singular_slice_edge)
with `slice_edges S cs'' asx' = as'` `upd_cs cs as = cs''`
have "slice_edges S cs (as@asx') = [last as]@as'"
by(fastforce intro:slice_edges_Append)
moreover
from `S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (xs,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`
have "m -asx->* sourcenode ax" by(fastforce intro:silent_moves_vpa_path)
from `S,slice_kind S \<turnstile> (xs,s'') -ax-> (msx',s')` have "valid_edge ax"
by(fastforce elim:observable_move.cases)
hence "sourcenode ax -[ax]->* targetnode ax" by(rule path_edge)
with `m -asx->* sourcenode ax` `as = asx@[ax]`
have "m -as->* targetnode ax" by(fastforce intro:path_Append)
with `targetnode ax -asx'->* m'` have "m -as@asx'->* m'"
by -(rule path_Append)
moreover
from `∀a ∈ set asx. intra_kind (kind a)` have "valid_path_aux cs asx"
by(rule valid_path_aux_intra_path)
from `∀a ∈ set asx. intra_kind (kind a)` have "upd_cs cs asx = cs"
by(rule upd_cs_intra_path)
from `m -asx->* sourcenode ax` `∀a ∈ set asx. intra_kind (kind a)`
have "get_proc m = get_proc (sourcenode ax)"
by(fastforce intro:intra_path_get_procs simp:intra_path_def)
with `valid_return_list rs m` have "valid_return_list rs (sourcenode ax)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
with `S,slice_kind S \<turnstile> (xs,s'') -ax-> (msx',s')` `valid_edge ax`
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)` `ms = targetnodes rs`
`length rs = length cs`
have "valid_path_aux cs [ax]"
by(auto intro!:observable_move_vpa_path simp del:valid_path_aux.simps)
with `valid_path_aux cs asx` `upd_cs cs asx = cs` `as = asx@[ax]`
have "valid_path_aux cs as" by(fastforce intro:valid_path_aux_Append)
with `upd_cs cs as = cs''` `valid_path_aux cs'' asx'`
have "valid_path_aux cs (as@asx')" by(fastforce intro:valid_path_aux_Append)
moreover
from `upd_cs cs as = cs''` `upd_cs cs'' asx' = cs'`
have "upd_cs cs (as@asx') = cs'" by(rule upd_cs_Append)
moreover
from `transfers (slice_kinds S as) s = s'`
`transfers (slice_kinds S asx') s' ≠ []`
have "transfers (slice_kinds S (as@asx')) s ≠ []"
by(simp add:slice_kinds_def transfers_split)
moreover
from `S,slice_kind S \<turnstile> (m # ms,s) =as=> (msx',s')`
have "transfers (map (slice_kind S) as) s = s'"
by simp(rule observable_moves_preds_transfers)
from `S,slice_kind S \<turnstile> (m # ms,s) =as=> (msx',s')` `ms = targetnodes rs`
`length rs = length cs` `∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`valid_call_list cs m` `valid_return_list rs m`
have "slice_edges S cs as = [last as]"
by(fastforce intro!:observable_moves_singular_slice_edge
[OF _ _ _ stacks_rewrite])
from `S,slice_kind S \<turnstile> (m#ms,s) =asx=>⇣τ (xs,s'')` callstack
have "s = s''" by(fastforce intro:silent_moves_slice_keeps_state)
with `S,slice_kind S \<turnstile> (xs,s'') -ax-> (msx',s')`
have "transfer (slice_kind S ax) s = s'" by(fastforce elim:observable_move.cases)
with `slice_edges S cs as = [last as]` `as = asx@[ax]`
have "s' = transfers (slice_kinds S (slice_edges S cs as)) s"
by(simp add:slice_kinds_def)
from `upd_cs cs as = cs''`
have "slice_edges S cs (as @ asx') =
(slice_edges S cs as)@(slice_edges S cs'' asx')"
by(fastforce intro:slice_edges_Append)
hence trans_eq':"transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s =
transfers (slice_kinds S (slice_edges S cs'' asx'))
(transfers (slice_kinds S (slice_edges S cs as)) s)"
by(simp add:slice_kinds_def transfers_split)
from `s' = transfers (slice_kinds S (slice_edges S cs as)) s`
`transfers (map (slice_kind S) as) s = s'`
have "transfers (map (slice_kind S) (slice_edges S cs as)) s =
transfers (map (slice_kind S) as) s"
by(simp add:slice_kinds_def)
with trans_eq trans_eq'
`s' = transfers (slice_kinds S (slice_edges S cs as)) s`
have "transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s =
transfers (slice_kinds S (as @ asx')) s"
by(simp add:slice_kinds_def transfers_split)
ultimately show ?case
using `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'`
apply(rule_tac x="as@asx'" in exI)
apply(rule_tac x="cs'" in exI)
apply(rule_tac x="rs'" in exI)
by clarsimp
qed
qed
subsection {* The fundamental property of static interprocedural slicing *}
theorem fundamental_property_of_static_slicing:
assumes "m -as->⇣\<surd>* m'" and "preds (kinds as) [cf]" and "CFG_node m' ∈ S"
obtains as' where "preds (slice_kinds S as') [cf]"
and "∀V ∈ Use m'. state_val (transfers (slice_kinds S as') [cf]) V =
state_val (transfers (kinds as) [cf]) V"
and "slice_edges S [] as = slice_edges S [] as'"
and "transfers (kinds as) [cf] ≠ []" and "m -as'->⇣\<surd>* m'"
proof(atomize_elim)
from `m -as->⇣\<surd>* m'` `preds (kinds as) [cf]` obtain ms'' s'' ms' as' as''
where "S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as=>*
(ms'',s'')"
and "S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])"
and "slice_edges S [] as = slice_edges S [] as''"
and "m -as''@as'->⇣\<surd>* m'"
by(auto elim:valid_path_trans_observable_moves[of _ _ _ _ _ "S"])
from `m -as->⇣\<surd>* m'` have "valid_node m" and "valid_node m'"
by(auto intro:path_valid_node simp:vp_def)
with `CFG_node m' ∈ S` have "CFG_node m' ∈ HRB_slice S"
by -(rule HRB_slice_refl)
from `valid_node m` `CFG_node m' ∈ S` have "(([m],[cf]),([m],[cf])) ∈ WS S"
by(fastforce intro:WSI)
{ fix V assume "V ∈ Use m'"
with `valid_node m'` have "V ∈ Use⇘SDG⇙ (CFG_node m')"
by(fastforce intro:CFG_Use_SDG_Use)
moreover
from `valid_node m'`
have "parent_node (CFG_node m') -[]->⇣ι* parent_node (CFG_node m')"
by(fastforce intro:empty_path simp:intra_path_def)
ultimately have "V ∈ rv S (CFG_node m')"
using `CFG_node m' ∈ HRB_slice S` `CFG_node m' ∈ S`
by(fastforce intro:rvI simp:sourcenodes_def) }
hence "∀V ∈ Use m'. V ∈ rv S (CFG_node m')" by simp
show "∃as'. preds (slice_kinds S as') [cf] ∧
(∀V∈Use m'. state_val (transfers (slice_kinds S as') [cf]) V =
state_val (transfers (kinds as) [cf]) V) ∧
slice_edges S [] as = slice_edges S [] as' ∧
transfers (kinds as) [cf] ≠ [] ∧ m -as'->⇣\<surd>* m'"
proof(cases "slice_edges S [] as = []")
case True
hence "preds (slice_kinds S []) [cf]"
and "slice_edges S [] [] = slice_edges S [] as"
by(simp_all add:slice_kinds_def)
with `S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as=>* (ms'',s'')`
have [simp]:"ms'' = [m]" "s'' = [cf]" by(auto elim:trans_observable_moves.cases)
with `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
have "S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])"
by simp
with `valid_node m` have "m -as'->* m'" and "valid_path_aux [] as'"
by(auto intro:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ "[]"]
simp:targetnodes_def valid_return_list_def)
hence "m -as'->⇣\<surd>* m'" by(simp add:vp_def valid_path_def)
from `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
have "slice_edges S [] as' = []"
by(fastforce dest:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
simp:targetnodes_def)
from `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
`valid_node m` `valid_node m'` `CFG_node m' ∈ S`
have returns:"∀mx ∈ set ms'.
∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by -(erule silent_moves_called_node_in_slice1_nodestack_in_slice1
[of _ _ _ _ _ _ _ _ _ "[]" "[]"],
auto intro:refl_slice1 simp:targetnodes_def valid_return_list_def)
from `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
`(([m],[cf]),([m],[cf])) ∈ WS S`
have WS:"((m'#ms',transfers (kinds as) [cf]),([m],[cf])) ∈ WS S"
by(rule WS_silent_moves)
hence "transfers (kinds as) [cf] ≠ []" by(auto elim!:WS.cases)
with WS returns `transfers (kinds as) [cf] ≠ []`
have "∀V ∈ rv S (CFG_node m').
state_val (transfers (kinds as) [cf]) V = fst cf V"
apply - apply(erule WS.cases) apply clarsimp
by(case_tac msx)(auto simp:hd_conv_nth)
with `∀V ∈ Use m'. V ∈ rv S (CFG_node m')`
have Uses:"∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V"
by simp
have [simp]:"ms' = []"
proof(rule ccontr)
assume "ms' ≠ []"
with `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
`valid_node m` `valid_node m'` `CFG_node m' ∈ S`
show False
by(fastforce elim:silent_moves_nonempty_nodestack_False intro:refl_slice1)
qed
with `S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
have "S,kind \<turnstile> ([m],[cf]) =as'=>⇣τ ([m'],transfers (kinds as) [cf])"
by simp
with `valid_node m` have "m -as'->⇘sl⇙* m'" by(fastforce dest:silent_moves_slp)
from this `slice_edges S [] as' = []`
obtain asx where "m -asx->⇣ι* m'" and "slice_edges S [] asx = []"
by(erule slp_to_intra_path_with_slice_edges)
with `CFG_node m' ∈ HRB_slice S`
obtain asx' where "m -asx'->⇣ι* m'"
and "preds (slice_kinds S asx') [cf]"
and "slice_edges S [] asx' = []"
by -(erule exists_sliced_intra_path_preds,auto simp:SDG_to_CFG_set_def)
from `m -asx'->⇣ι* m'` have "m -asx'->⇣\<surd>* m'" by(rule intra_path_vp)
from Uses `slice_edges S [] asx' = []`
have "hd (transfers (slice_kinds S
(slice_edges S [] asx')) [cf]) = cf" by(simp add:slice_kinds_def)
from `m -asx'->⇣ι* m'` `CFG_node m' ∈ S`
have "transfers (slice_kinds S (slice_edges S [] asx')) [cf] =
transfers (slice_kinds S asx') [cf]"
by(fastforce intro:transfers_intra_slice_kinds_slice_edges simp:intra_path_def)
with `hd (transfers (slice_kinds S (slice_edges S [] asx')) [cf]) = cf`
have "hd (transfers (slice_kinds S asx') [cf]) = cf" by simp
with Uses have "∀V∈Use m'. state_val (transfers (slice_kinds S asx') [cf]) V =
state_val (transfers (kinds as) [cf]) V" by simp
with `m -asx'->⇣\<surd>* m'` `preds (slice_kinds S asx') [cf]`
`slice_edges S [] asx' = []` `transfers (kinds as) [cf] ≠ []` True
show ?thesis by fastforce
next
case False
with `(([m],[cf]),([m],[cf])) ∈ WS S`
`S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as=>* (ms'',s'')`
have WS:"((ms'',s''),(ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf]))
∈ WS S"
and tom:"S,slice_kind S \<turnstile> ([m],[cf]) =slice_edges S [] as=>*
(ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf])"
by(fastforce dest:WS_weak_sim_trans)+
from WS obtain mx msx where [simp]:"ms'' = mx#msx" and "valid_node mx"
by -(erule WS.cases,cases ms'',auto)
from `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])` WS
have WS':"((m'#ms',transfers (kinds as) [cf]),
(mx#msx,transfers (slice_kinds S (slice_edges S [] as)) [cf])) ∈ WS S"
by simp(rule WS_silent_moves)
from tom `valid_node m`
obtain asx csx rsx where "preds (slice_kinds S asx) [cf]"
and "slice_edges S [] asx = slice_edges S [] as"
and "m -asx->⇣\<surd>* mx" and "transfers (slice_kinds S asx) [cf] ≠ []"
and "upd_cs [] asx = csx" and stack:"valid_node mx" "valid_call_list csx mx"
"∀i < length rsx. rsx!i ∈ get_return_edges (csx!i)"
"valid_return_list rsx mx" "length rsx = length csx"
"msx = targetnodes rsx"
and trans_eq:"transfers (slice_kinds S
(slice_edges S [] asx)) [cf] =
transfers (slice_kinds S asx) [cf]"
by(auto elim:slice_tom_preds_vp[of _ _ _ _ _ _ _ _ "[]" "[]"]
simp:valid_call_list_def valid_return_list_def targetnodes_def
vp_def valid_path_def)
from `transfers (slice_kinds S asx) [cf] ≠ []`
obtain cf' cfs' where eq:"transfers (slice_kinds S asx) [cf] =
cf'#cfs'" by(cases "transfers (slice_kinds S asx) [cf]") auto
from WS' have callstack:"∀mx ∈ set msx. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce elim:WS.cases)
with `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
`valid_node m'` stack `CFG_node m' ∈ S`
have callstack':"∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by simp(erule silent_moves_called_node_in_slice1_nodestack_in_slice1
[of _ _ _ _ _ _ _ _ _ rsx csx],auto intro:refl_slice1)
with `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
stack callstack
have "mx -as'->⇘sl⇙* m'" and "msx = ms'" by(auto dest!:silent_moves_slp)
from `S,kind \<turnstile> (ms'',s'') =as'=>⇣τ (m'#ms',transfers (kinds as) [cf])`
stack
have "slice_edges S csx as' = []"
by(auto dest:silent_moves_no_slice_edges[OF _ _ _ stacks_rewrite])
with `mx -as'->⇘sl⇙* m'` obtain asx'' where "mx -asx''->⇣ι* m'"
and "slice_edges S csx asx'' = []"
by(erule slp_to_intra_path_with_slice_edges)
from stack have "∀i<length csx. call_of_return_node (msx!i) (sourcenode (csx!i))"
by -(rule stacks_rewrite)
with callstack `msx = targetnodes rsx` `length rsx = length csx`
have "∀c∈set csx. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(auto simp:all_set_conv_all_nth targetnodes_def)
with `mx -asx''->⇣ι* m'` `slice_edges S csx asx'' = []` `valid_node m'`
eq `CFG_node m' ∈ S`
obtain asx' where "mx -asx'->⇣ι* m'"
and "preds (slice_kinds S asx') (cf'#cfs')"
and "slice_edges S csx asx' = []"
by -(erule exists_sliced_intra_path_preds,
auto intro:HRB_slice_refl simp:SDG_to_CFG_set_def)
with eq have "preds (slice_kinds S asx')
(transfers (slice_kinds S asx) [cf])" by simp
with `preds (slice_kinds S asx) [cf]`
have "preds (slice_kinds S (asx@asx')) [cf]"
by(simp add:slice_kinds_def preds_split)
from `m -asx->⇣\<surd>* mx` `mx -asx'->⇣ι* m'` have "m -asx@asx'->⇣\<surd>* m'"
by(fastforce elim:vp_slp_Append intra_path_slp)
from `upd_cs [] asx = csx` `slice_edges S csx asx' = []`
have "slice_edges S [] (asx@asx') =
(slice_edges S [] asx)@[]"
by(fastforce intro:slice_edges_Append)
from `mx -asx'->⇣ι* m'` `∀c∈set csx. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have trans_eq':"transfers (slice_kinds S (slice_edges S csx asx'))
(transfers (slice_kinds S asx) [cf]) =
transfers (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])"
by(fastforce intro:transfers_intra_slice_kinds_slice_edges simp:intra_path_def)
from `upd_cs [] asx = csx`
have "slice_edges S [] (asx@asx') =
(slice_edges S [] asx)@(slice_edges S csx asx')"
by(fastforce intro:slice_edges_Append)
hence "transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf] =
transfers (slice_kinds S (slice_edges S csx asx'))
(transfers (slice_kinds S (slice_edges S [] asx)) [cf])"
by(simp add:slice_kinds_def transfers_split)
with trans_eq have "transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf] =
transfers (slice_kinds S (slice_edges S csx asx'))
(transfers (slice_kinds S asx) [cf])" by simp
with trans_eq' have trans_eq'':
"transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf] =
transfers (slice_kinds S (asx@asx')) [cf]"
by(simp add:slice_kinds_def transfers_split)
from WS' obtain x xs where "m'#ms' = xs@x#msx"
and "xs ≠ [] --> (∃mx'. call_of_return_node x mx' ∧
mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
and rest:"∀i < length (mx#msx). ∀V ∈ rv S (CFG_node ((x#msx)!i)).
(fst ((transfers (kinds as) [cf])!(length xs + i))) V =
(fst ((transfers (slice_kinds S
(slice_edges S [] as)) [cf])!i)) V"
"transfers (kinds as) [cf] ≠ []"
"transfers (slice_kinds S
(slice_edges S [] as)) [cf] ≠ []"
by(fastforce elim:WS.cases)
from `m'#ms' = xs@x#msx` `xs ≠ [] --> (∃mx'. call_of_return_node x mx' ∧
mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)` callstack'
have [simp]:"xs = []" "x = m'" "ms' = msx" by(cases xs,auto)+
from rest have "∀V ∈ rv S (CFG_node m').
state_val (transfers (kinds as) [cf]) V =
state_val (transfers (slice_kinds S (slice_edges S [] as)) [cf]) V"
by(fastforce dest:hd_conv_nth)
with `∀V ∈ Use m'. V ∈ rv S (CFG_node m')`
`slice_edges S [] asx = slice_edges S [] as`
have "∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V =
state_val (transfers (slice_kinds S (slice_edges S [] asx)) [cf]) V"
by simp
with `slice_edges S [] (asx@asx') = (slice_edges S [] asx)@[]`
have "∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V =
state_val (transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf]) V"
by simp
with trans_eq'' have "∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V =
state_val (transfers (slice_kinds S (asx@asx')) [cf]) V"
by simp
with `preds (slice_kinds S (asx@asx')) [cf]`
`m -asx@asx'->⇣\<surd>* m'` `slice_edges S [] (asx@asx') =
(slice_edges S [] asx)@[]` `transfers (kinds as) [cf] ≠ []`
`slice_edges S [] asx = slice_edges S [] as`
show ?thesis by fastforce
qed
qed
end
subsection {* The fundamental property of static interprocedural slicing related to the semantics *}
locale SemanticsProperty = SDG sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses +
CFG_semantics_wf sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main sem identifies
for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
and kind :: "'edge => ('var,'val,'ret,'pname) edge_kind"
and valid_edge :: "'edge => bool"
and Entry :: "'node" ("'('_Entry'_')") and get_proc :: "'node => 'pname"
and get_return_edges :: "'edge => 'edge set"
and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
and Exit::"'node" ("'('_Exit'_')")
and Def :: "'node => 'var set" and Use :: "'node => 'var set"
and ParamDefs :: "'node => 'var list" and ParamUses :: "'node => 'var set list"
and sem :: "'com => ('var \<rightharpoonup> 'val) list => 'com => ('var \<rightharpoonup> 'val) list => bool"
("((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [0,0,0,0] 81)
and identifies :: "'node => 'com => bool" ("_ \<triangleq> _" [51,0] 80)
begin
theorem fundamental_property_of_path_slicing_semantically:
assumes "m \<triangleq> c" and "⟨c,[cf]⟩ => ⟨c',s'⟩"
obtains m' as cfs' where "m -as->⇣\<surd>* m'" and "m' \<triangleq> c'"
and "preds (slice_kinds {CFG_node m'} as) [(cf,undefined)]"
and "∀V ∈ Use m'.
state_val (transfers (slice_kinds {CFG_node m'} as) [(cf,undefined)]) V =
state_val cfs' V" and "map fst cfs' = s'"
proof(atomize_elim)
from `m \<triangleq> c` `⟨c,[cf]⟩ => ⟨c',s'⟩` obtain m' as cfs' where "m -as->⇣\<surd>* m'"
and "transfers (kinds as) [(cf,undefined)] = cfs'"
and "preds (kinds as) [(cf,undefined)]" and "m' \<triangleq> c'" and "map fst cfs' = s'"
by(fastforce dest:fundamental_property)
from `m -as->⇣\<surd>* m'` `preds (kinds as) [(cf,undefined)]` obtain as'
where "preds (slice_kinds {CFG_node m'} as') [(cf,undefined)]"
and vals:"∀V ∈ Use m'. state_val (transfers (slice_kinds {CFG_node m'} as')
[(cf,undefined)]) V = state_val (transfers (kinds as) [(cf,undefined)]) V"
and "m -as'->⇣\<surd>* m'"
by -(erule fundamental_property_of_static_slicing,auto)
from `transfers (kinds as) [(cf,undefined)] = cfs'` vals have "∀V ∈ Use m'.
state_val (transfers (slice_kinds {CFG_node m'} as') [(cf,undefined)]) V =
state_val cfs' V" by simp
with `preds (slice_kinds {CFG_node m'} as') [(cf,undefined)]` `m -as'->⇣\<surd>* m'`
`m' \<triangleq> c'` `map fst cfs' = s'`
show "∃as m' cfs'. m -as->⇣\<surd>* m' ∧ m' \<triangleq> c' ∧
preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] ∧
(∀V∈Use m'. state_val (transfers (slice_kinds {CFG_node m'} as)
[(cf, undefined)]) V = state_val cfs' V) ∧ map fst cfs' = s'"
by blast
qed
end
end