Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory WeakSimulationheader {* \isaheader{The weak simulation} *}
theory WeakSimulation imports Slice begin
context SDG begin
lemma call_node_notin_slice_return_node_neither:
assumes "call_of_return_node n n'" and "n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
shows "n ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof -
from `call_of_return_node n n'` obtain a a' where "return_node n"
and "valid_edge a" and "n' = sourcenode a"
and "valid_edge a'" and "a' ∈ get_return_edges a"
and "n = targetnode a'" by(fastforce simp:call_of_return_node_def)
from `valid_edge a` `a' ∈ get_return_edges a` obtain Q p r fs
where "kind a = Q:r\<hookrightarrow>⇘p⇙fs" by(fastforce dest!:only_call_get_return_edges)
with `valid_edge a` `a' ∈ get_return_edges a` obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'"
by(fastforce dest!:call_return_edges)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges a`
have "CFG_node (sourcenode a) s-p->⇘sum⇙ CFG_node (targetnode a')"
by(fastforce intro:sum_SDG_call_summary_edge)
show ?thesis
proof
assume "n ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with `n = targetnode a'` have "CFG_node (targetnode a') ∈ HRB_slice S"
by(simp add:SDG_to_CFG_set_def)
hence "CFG_node (sourcenode a) ∈ HRB_slice S"
proof(induct "CFG_node (targetnode a')" rule:HRB_slice_cases)
case (phase1 nx)
with `CFG_node (sourcenode a) s-p->⇘sum⇙ CFG_node (targetnode a')`
show ?case by(fastforce intro:combine_SDG_slices.combSlice_refl sum_slice1
simp:HRB_slice_def)
next
case (phase2 nx n' n'' p')
from `CFG_node (targetnode a') ∈ sum_SDG_slice2 n'`
`CFG_node (sourcenode a) s-p->⇘sum⇙ CFG_node (targetnode a')` `valid_edge a`
have "CFG_node (sourcenode a) ∈ sum_SDG_slice2 n'"
by(fastforce intro:sum_slice2)
with `n' ∈ sum_SDG_slice1 nx` `n'' s-p'->⇘ret⇙ CFG_node (parent_node n')` `nx ∈ S`
show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
simp:HRB_slice_def)
qed
with `n' ∉ ⌊HRB_slice S⌋⇘CFG⇙` `n' = sourcenode a` show False
by(simp add:SDG_to_CFG_set_def HRB_slice_def)
qed
qed
lemma edge_obs_intra_slice_eq:
assumes "valid_edge a" and "intra_kind (kind a)" and "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
shows "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
proof -
from assms have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_subset)
from `valid_edge a` have "valid_node (sourcenode a)" by simp
{ fix x assume "x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
and "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
have "∃as. targetnode a -as->⇣ι* x"
proof(cases "method_exit x")
case True
from `valid_edge a` have "valid_node (targetnode a)" by simp
then obtain asx where "targetnode a -asx->⇣\<surd>* (_Exit_)"
by(fastforce dest:Exit_path)
then obtain as pex where "targetnode a -as->⇣ι* pex" and "method_exit pex"
by -(erule valid_Exit_path_intra_path)
hence "get_proc pex = get_proc (targetnode a)"
by -(rule intra_path_get_procs[THEN sym])
also from `valid_edge a` `intra_kind (kind a)`
have "… = get_proc (sourcenode a)"
by -(rule get_proc_intra[THEN sym])
also from `x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙` True
have "… = get_proc x"
by(fastforce elim:obs_intraE intro:intra_path_get_procs)
finally have "pex = x" using `method_exit pex` True
by -(rule method_exit_unique)
with `targetnode a -as->⇣ι* pex` show ?thesis by fastforce
next
case False
with `x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "x postdominates (sourcenode a)" by(rule obs_intra_postdominate)
with `valid_edge a` `intra_kind (kind a)` `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "x postdominates (targetnode a)"
by(fastforce elim:postdominate_inner_path_targetnode path_edge obs_intraE
simp:intra_path_def sourcenodes_def)
thus ?thesis by(fastforce elim:postdominate_implies_inner_path)
qed
then obtain as where "targetnode a -as->⇣ι* x" by blast
from `x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
have "x ∈ ⌊HRB_slice S⌋⇘CFG⇙" by -(erule obs_intraE)
have "∃x' ∈ ⌊HRB_slice S⌋⇘CFG⇙. ∃as'. targetnode a -as'->⇣ι* x' ∧
(∀a' ∈ set (sourcenodes as'). a' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
proof(cases "∃a' ∈ set (sourcenodes as). a' ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
then obtain zs z zs' where "sourcenodes as = zs@z#zs'"
and "z ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "∀z' ∈ set zs. z' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(erule split_list_first_propE)
then obtain ys y ys'
where "sourcenodes ys = zs" and "as = ys@y#ys'"
and "sourcenode y = z"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from `targetnode a -as->⇣ι* x` `as = ys@y#ys'`
have "targetnode a -ys@y#ys'->* x" and "∀y' ∈ set ys. intra_kind (kind y')"
by(simp_all add:intra_path_def)
from `targetnode a -ys@y#ys'->* x` have "targetnode a -ys->* sourcenode y"
by(rule path_split)
with `∀y' ∈ set ys. intra_kind (kind y')` `sourcenode y = z`
`∀z' ∈ set zs. z' ∉ ⌊HRB_slice S⌋⇘CFG⇙` `z ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`sourcenodes ys = zs`
show ?thesis by(fastforce simp:intra_path_def)
next
case False
with `targetnode a -as->⇣ι* x` `x ∈ ⌊HRB_slice S⌋⇘CFG⇙`
show ?thesis by fastforce
qed
hence "∃y. y ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obs_intra_elem)
with `obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}`
have False by simp }
with `obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙` `valid_node (sourcenode a)`
show ?thesis by(cases "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
(auto dest!:obs_intra_singleton_disj)
qed
lemma intra_edge_obs_slice:
assumes "ms ≠ []" and "ms'' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a"
and "intra_kind (kind a)"
and disj:"(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "hd ms = sourcenode a" and "ms' = targetnode a#tl ms"
and "∀n ∈ set (tl ms'). return_node n"
shows "ms'' ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙"
proof -
from `ms'' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙` `∀n ∈ set (tl ms'). return_node n`
obtain msx m msx' mx m' where "ms' = msx@m#msx'" and "ms'' = mx#msx'"
and "mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
and "∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
and imp:"∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
--> (∃x'' ∈ set (xs'@[m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
show ?thesis
proof(cases msx)
case Nil
with `∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
disj `ms' = msx@m#msx'` `hd ms = sourcenode a` `ms' = targetnode a#tl ms`
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by(cases ms) auto
from `ms' = msx@m#msx'` `ms' = targetnode a#tl ms` Nil
have "m = targetnode a" by simp
with `valid_edge a` `intra_kind (kind a)` `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙`
have "mx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:edge_obs_intra_subset)
from `ms' = msx@m#msx'` Nil `ms' = targetnode a # tl ms`
`hd ms = sourcenode a` `ms ≠ []`
have "ms = []@sourcenode a#msx'" by(cases ms) auto
with `ms'' = mx#msx'` `mx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙`
`∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙` Nil
show ?thesis by(fastforce intro!:obsI)
next
case (Cons x xs)
with `ms' = msx@m#msx'` `ms' = targetnode a # tl ms`
have "msx = targetnode a#xs" by simp
from Cons `ms' = msx@m#msx'` `ms' = targetnode a # tl ms` `hd ms = sourcenode a`
have "ms = (sourcenode a#xs)@m#msx'" by(cases ms) auto
from disj `ms = (sourcenode a#xs)@m#msx'`
`∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have disj2:"(∃m ∈ set (xs@[m]). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce
hence "∀zs z zs'. sourcenode a#xs = zs@z#zs' ∧ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
--> (∃z'' ∈ set (zs'@[m]). ∃mx. call_of_return_node z'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
proof(cases "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `hd ms = sourcenode a` have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `valid_edge a` `intra_kind (kind a)`
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with imp `msx = targetnode a#xs` show ?thesis
by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
next
case False
with `hd ms = sourcenode a` `valid_edge a`
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
from False disj2
have "∃m ∈ set (xs@[m]). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by simp
with imp `obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}`
`msx = targetnode a#xs` show ?thesis
by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
qed
with `ms' = msx@m#msx'` `ms' = targetnode a # tl ms` `hd ms = sourcenode a`
`ms'' = mx#msx'` `mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙`
`∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`ms = (sourcenode a#xs)@m#msx'`
show ?thesis by(simp del:obs.simps)(rule obsI,auto)
qed
qed
subsection {* Silent moves *}
inductive silent_move ::
"'node SDG_node set => ('edge => ('var,'val,'ret,'pname) edge_kind) => 'node list =>
(('var \<rightharpoonup> 'val) × 'ret) list => 'edge => 'node list => (('var \<rightharpoonup> 'val) × 'ret) list => bool"
("_,_ \<turnstile> '(_,_') -_->⇣τ '(_,_')" [51,50,0,0,50,0,0] 51)
where silent_move_intra:
"[|pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
length s' = length s; length ms = length s;
hd ms = sourcenode a; ms' = (targetnode a)#tl ms|]
==> S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')"
| silent_move_call:
"[|pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs;
valid_edge a'; a' ∈ get_return_edges a;
(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
length ms = length s; length s' = Suc(length s);
hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms|]
==> S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')"
| silent_move_return:
"[|pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>⇘p⇙f';
∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙;
∀m ∈ set (tl ms). return_node m; length ms = length s; length s = Suc(length s');
s' ≠ []; hd ms = sourcenode a; hd(tl ms) = targetnode a; ms' = tl ms|]
==> S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')"
lemma silent_move_valid_nodes:
"[|S,f \<turnstile> (ms,s) -a->⇣τ (ms',s'); ∀m ∈ set ms'. valid_node m|]
==> ∀m ∈ set ms. valid_node m"
by(induct rule:silent_move.induct)(case_tac ms,auto)+
lemma silent_move_return_node:
"S,f \<turnstile> (ms,s) -a->⇣τ (ms',s') ==> ∀m ∈ set (tl ms'). return_node m"
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms n⇣c ms')
thus ?case by simp
next
case (silent_move_call f a s s' Q r p fs a' ms n⇣c ms')
from `valid_edge a'` `valid_edge a` `a' ∈ get_return_edges a`
have "return_node (targetnode a')" by(fastforce simp:return_node_def)
with `∀m∈set (tl ms). return_node m` `ms' = targetnode a # targetnode a' # tl ms`
show ?case by simp
next
case (silent_move_return f a s s' Q p f' ms n⇣c ms')
thus ?case by(cases "tl ms") auto
qed
lemma silent_move_equal_length:
assumes "S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')`
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms n⇣c ms')
from `pred (f a) s` obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from `length ms = length s` `ms' = targetnode a # tl ms`
`length s' = length s` show ?case by simp
next
case (silent_move_call f a s s' Q r p fs a' ms n⇣c ms')
from `pred (f a) s` obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from `length ms = length s` `length s' = Suc (length s)`
`ms' = targetnode a # targetnode a' # tl ms` show ?case by simp
next
case (silent_move_return f a s s' Q p f' ms n⇣c ms')
from `length ms = length s` `length s = Suc (length s')` `ms' = tl ms` `s' ≠ []`
show ?case by simp
qed
thus "length ms = length s" and "length ms' = length s'" by simp_all
qed
lemma silent_move_obs_slice:
"[|S,kind \<turnstile> (ms,s) -a->⇣τ (ms',s'); msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙;
∀n ∈ set (tl ms'). return_node n|]
==> msx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct S f≡"kind" ms s a ms' s' rule:silent_move.induct)
case (silent_move_intra a s s' ms n⇣c ms')
from `pred (kind a) s` `length ms = length s` have "ms ≠ []"
by(cases s) auto
with silent_move_intra show ?case by -(rule intra_edge_obs_slice)
next
case (silent_move_call a s s' Q r p fs a' ms S ms')
note disj = `(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙`
from `valid_edge a'` `valid_edge a` `a' ∈ get_return_edges a`
have "return_node (targetnode a')" by(fastforce simp:return_node_def)
with `valid_edge a` `a' ∈ get_return_edges a` `valid_edge a'`
have "call_of_return_node (targetnode a') (sourcenode a)"
by(simp add:call_of_return_node_def) blast
from `pred (kind a) s` `length ms = length s`
have "ms ≠ []" by(cases s) auto
from disj
show ?case
proof
assume "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with `hd ms = sourcenode a` have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `call_of_return_node (targetnode a') (sourcenode a)`
`ms' = targetnode a # targetnode a' # tl ms`
have "∃n' ∈ set (tl ms'). ∃nx. call_of_return_node n' nx ∧ nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce
with `msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙` `ms' = targetnode a # targetnode a' # tl ms`
have "msx ∈ obs (targetnode a' # tl ms) ⌊HRB_slice S⌋⇘CFG⇙" by simp
from `valid_edge a` `a' ∈ get_return_edges a`
obtain a'' where "valid_edge a''" and [simp]:"sourcenode a'' = sourcenode a"
and [simp]:"targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
by -(drule call_return_node_edge,auto simp:intra_kind_def)
from `∀m∈set (tl ms'). return_node m` `ms' = targetnode a # targetnode a' # tl ms`
have "∀m∈set (tl ms). return_node m" by simp
with `ms ≠ []` `msx ∈ obs (targetnode a'#tl ms) ⌊HRB_slice S⌋⇘CFG⇙`
`valid_edge a''` `intra_kind(kind a'')` disj
`hd ms = sourcenode a`
show ?case by -(rule intra_edge_obs_slice,fastforce+)
next
assume "∃m∈set (tl ms).
∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with `ms ≠ []` `msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙`
`ms' = targetnode a # targetnode a' # tl ms`
show ?thesis by(cases ms) auto
qed
next
case (silent_move_return a s s' Q p f' ms S ms')
from `length ms = length s` `length s = Suc (length s')` `s' ≠ []`
have "ms ≠ []" and "tl ms ≠ []" by(auto simp:length_Suc_conv)
from `∃m∈set (tl ms).
∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`tl ms ≠ []` `hd (tl ms) = targetnode a`
have "(∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
(∃m∈set (tl (tl ms)). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(cases "tl ms") auto
hence "obs ms ⌊HRB_slice S⌋⇘CFG⇙ = obs (tl ms) ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume "∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
from `tl ms ≠ []` have "hd (tl ms) ∈ set (tl ms)" by simp
with `hd (tl ms) = targetnode a` have "targetnode a ∈ set (tl ms)" by simp
with `ms ≠ []`
`∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have "∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙" by(cases ms) auto
with `ms ≠ []` show ?thesis by(cases ms) auto
next
assume "∃m∈set (tl (tl ms)). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
with `ms ≠ []` `tl ms ≠ []` show ?thesis
by(cases ms,auto simp:Let_def)(case_tac list,auto)+
qed
with `ms' = tl ms` `msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙` show ?case by simp
qed
lemma silent_move_empty_obs_slice:
assumes "S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')" and "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}"
shows "obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(rule ccontr)
assume "obs ms ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
then obtain xs where "xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')`
have "∀m ∈ set (tl ms). return_node m"
by(fastforce elim!:silent_move.cases simp:call_of_return_node_def)
with `xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙`
obtain msx m msx' m' where assms:"ms = msx@m#msx'" "xs = m'#msx'"
"m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
"∀mx ∈ set msx'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
"∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
--> (∃x'' ∈ set (xs'@[m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
from `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')` `obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}` assms
show False
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms S ms')
note disj = `(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙`
note msx = `∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} -->
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
note msx' = `∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
show False
proof(cases msx)
case Nil
with `ms = msx @ m # msx'` `hd ms = sourcenode a` have [simp]:"m = sourcenode a"
and "tl ms = msx'" by simp_all
from Nil `ms' = targetnode a # tl ms` `ms = msx @ m # msx'`
have "ms' = msx @ targetnode a # msx'" by simp
from msx' disj `tl ms = msx'` `hd ms = sourcenode a`
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
with `valid_edge a` `intra_kind (kind a)`
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by(rule edge_obs_intra_slice_eq)
with `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙`
have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by simp
from msx Nil have "∀xs x xs'. msx = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} -->
(∃x''∈set (xs' @ [targetnode a]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" by simp
with `m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙` msx'
`ms' = msx @ targetnode a # msx'`
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
with `obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}` show False by simp
next
case (Cons y ys)
with `ms = msx @ m # msx'` `ms' = targetnode a # tl ms` `hd ms = sourcenode a`
have "ms' = targetnode a # ys @ m # msx'" and "y = sourcenode a"
and "tl ms = ys @ m # msx'" by simp_all
{ fix x assume "x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from `valid_edge a` have "valid_node (sourcenode a)" by simp
from this True
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
thus ?thesis by simp
next
case False
from `valid_edge a` `intra_kind (kind a)` False
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with `x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙` show ?thesis
by fastforce
qed }
with msx Cons `y = sourcenode a`
have "∀xs x xs'. targetnode a # ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} --> (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
apply clarsimp apply(case_tac xs) apply auto
apply(erule_tac x="[]" in allE) apply clarsimp
apply(erule_tac x="sourcenode a # list" in allE) apply auto
done
with `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙` msx'
`ms' = targetnode a # ys @ m # msx'`
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
with `obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}` show False by simp
qed
next
case (silent_move_call f a s s' Q r p fs a' ms S ms')
note disj = `(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙`
note msx = `∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} -->
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
note msx' = `∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
from `valid_edge a` `a' ∈ get_return_edges a` obtain a'' where "valid_edge a''"
and "sourcenode a'' = sourcenode a" and "targetnode a'' = targetnode a'"
and "intra_kind (kind a'')"
by(fastforce dest:call_return_node_edge simp:intra_kind_def)
from `valid_edge a'` `valid_edge a` `a' ∈ get_return_edges a`
have "call_of_return_node (targetnode a') (sourcenode a)"
by(fastforce simp:call_of_return_node_def return_node_def)
show False
proof(cases msx)
case Nil
with `ms = msx @ m # msx'` `hd ms = sourcenode a` have [simp]:"m = sourcenode a"
and "tl ms = msx'" by simp_all
from Nil `ms' = targetnode a # targetnode a' # tl ms` `ms = msx @ m # msx'`
have "ms' = targetnode a # targetnode a' # msx'" by simp
from msx' disj `tl ms = msx'` `hd ms = sourcenode a`
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from `valid_edge a''` `intra_kind (kind a'')` `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`sourcenode a'' = sourcenode a` `targetnode a'' = targetnode a'`
have "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:edge_obs_intra_slice_eq)
with `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙`
have "m' ∈ obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙" by simp
from this msx' have "m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obsI)
from `call_of_return_node (targetnode a') (sourcenode a)`
`sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have "∃m' ∈ set (targetnode a'#msx').
∃mx. call_of_return_node m' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce
with `m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙`
have "m'#msx' ∈ obs (targetnode a#targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
by simp
with `ms' = targetnode a # targetnode a' # msx'` `obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}`
show False by simp
next
case (Cons y ys)
with `ms = msx @ m # msx'` `ms' = targetnode a # targetnode a' # tl ms`
`hd ms = sourcenode a`
have "ms' = targetnode a # targetnode a' # ys @ m # msx'"
and "y = sourcenode a" and "tl ms = ys @ m # msx'" by simp_all
show False
proof(cases "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} -->
(∃x''∈set (targetnode a' # ys @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
case True
hence imp:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} -->
(∃x''∈set (targetnode a' # ys @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" .
show False
proof(cases "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} -->
(∃x''∈set (ys @ [m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
case True
with imp msx Cons `y = sourcenode a`
have "∀xs x xs'. targetnode a # targetnode a' # ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} --> (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
apply clarsimp apply(case_tac xs) apply fastforce
apply(case_tac list) apply fastforce apply clarsimp
apply(erule_tac x="sourcenode a # lista" in allE) apply auto
done
with `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙` msx'
`ms' = targetnode a # targetnode a' # ys @ m # msx'`
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
with `obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}` show False by simp
next
case False
hence "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
and all:"∀x''∈set (ys @ [m]). ∀mx. call_of_return_node x'' mx -->
mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce+
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from `valid_edge a` have "valid_node (sourcenode a)" by simp
from this True
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
thus ?thesis by simp
next
case False
with `sourcenode a'' = sourcenode a`
have "sourcenode a'' ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `valid_edge a''` `intra_kind (kind a'')`
have "obs_intra (targetnode a'') ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a'') ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with `obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}`
`sourcenode a'' = sourcenode a` `targetnode a'' = targetnode a'`
show ?thesis by fastforce
qed
with msx Cons `y = sourcenode a` all
show False by simp blast
qed
next
case False
hence "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
and all:"∀x''∈set (targetnode a' # ys @ [m]).
∀mx. call_of_return_node x'' mx --> mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce+
with Cons `y = sourcenode a` msx
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}" by auto blast
from `call_of_return_node (targetnode a') (sourcenode a)` all
have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from `valid_edge a` have "valid_node (sourcenode a)" by simp
from this `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
with `obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}` show False by simp
qed
qed
next
case (silent_move_return f a s s' Q p f' ms S ms')
note msx = `∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} -->
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
note msx' = `∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
show False
proof(cases msx)
case Nil
with `ms = msx @ m # msx'` `hd ms = sourcenode a` have "tl ms = msx'" by simp
with `∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙`
msx'
show False by fastforce
next
case (Cons y ys)
with `ms = msx @ m # msx'` `hd ms = sourcenode a` `ms' = tl ms`
have "ms' = ys @ m # msx'" and "y = sourcenode a" by simp_all
from msx Cons have "∀xs x xs'. ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} --> (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by auto (erule_tac x="y # xs" in allE,auto)
with `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙` msx' `ms' = ys @ m # msx'`
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
with `obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}` show False by simp
qed
qed
qed
inductive silent_moves ::
"'node SDG_node set => ('edge => ('var,'val,'ret,'pname) edge_kind) => 'node list =>
(('var \<rightharpoonup> 'val) × 'ret) list => 'edge list => 'node list => (('var \<rightharpoonup> 'val) × 'ret) list => bool"
("_,_ \<turnstile> '(_,_') =_=>⇣τ '(_,_')" [51,50,0,0,50,0,0] 51)
where silent_moves_Nil: "length ms = length s ==> S,f \<turnstile> (ms,s) =[]=>⇣τ (ms,s)"
| silent_moves_Cons:
"[|S,f \<turnstile> (ms,s) -a->⇣τ (ms',s'); S,f \<turnstile> (ms',s') =as=>⇣τ (ms'',s'')|]
==> S,f \<turnstile> (ms,s) =a#as=>⇣τ (ms'',s'')"
lemma silent_moves_equal_length:
assumes "S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from `S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s')`
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule:silent_moves.induct)
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
from `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')`
have "length ms = length s" and "length ms' = length s'"
by(rule silent_move_equal_length)+
with `length ms' = length s' ∧ length ms'' = length s''`
show ?case by simp
qed simp
thus "length ms = length s" "length ms' = length s'" by simp_all
qed
lemma silent_moves_Append:
"[|S,f \<turnstile> (ms,s) =as=>⇣τ (ms'',s''); S,f \<turnstile> (ms'',s'') =as'=>⇣τ (ms',s')|]
==> S,f \<turnstile> (ms,s) =as@as'=>⇣τ (ms',s')"
by(induct rule:silent_moves.induct)(auto intro:silent_moves.intros)
lemma silent_moves_split:
assumes "S,f \<turnstile> (ms,s) =as@as'=>⇣τ (ms',s')"
obtains ms'' s'' where "S,f \<turnstile> (ms,s) =as=>⇣τ (ms'',s'')"
and "S,f \<turnstile> (ms'',s'') =as'=>⇣τ (ms',s')"
proof(atomize_elim)
from `S,f \<turnstile> (ms,s) =as@as'=>⇣τ (ms',s')`
show "∃ms'' s''. S,f \<turnstile> (ms,s) =as=>⇣τ (ms'',s'') ∧ S,f \<turnstile> (ms'',s'') =as'=>⇣τ (ms',s')"
proof(induct as arbitrary:ms s)
case Nil
from `S,f \<turnstile> (ms,s) =[] @ as'=>⇣τ (ms',s')` have "length ms = length s"
by(fastforce intro:silent_moves_equal_length)
hence "S,f \<turnstile> (ms,s) =[]=>⇣τ (ms,s)" by(rule silent_moves_Nil)
with `S,f \<turnstile> (ms,s) =[] @ as'=>⇣τ (ms',s')` show ?case by fastforce
next
case (Cons ax asx)
note IH = `!!ms s. S,f \<turnstile> (ms,s) =asx @ as'=>⇣τ (ms',s') ==>
∃ms'' s''. S,f \<turnstile> (ms,s) =asx=>⇣τ (ms'',s'') ∧ S,f \<turnstile> (ms'',s'') =as'=>⇣τ (ms',s')`
from `S,f \<turnstile> (ms,s) =(ax # asx) @ as'=>⇣τ (ms',s')`
obtain msx sx where "S,f \<turnstile> (ms,s) -ax->⇣τ (msx,sx)"
and "S,f \<turnstile> (msx,sx) =asx @ as'=>⇣τ (ms',s')"
by(auto elim:silent_moves.cases)
from IH[OF this(2)] obtain ms'' s'' where "S,f \<turnstile> (msx,sx) =asx=>⇣τ (ms'',s'')"
and "S,f \<turnstile> (ms'',s'') =as'=>⇣τ (ms',s')" by blast
from `S,f \<turnstile> (ms,s) -ax->⇣τ (msx,sx)` `S,f \<turnstile> (msx,sx) =asx=>⇣τ (ms'',s'')`
have "S,f \<turnstile> (ms,s) =ax#asx=>⇣τ (ms'',s'')" by(rule silent_moves_Cons)
with `S,f \<turnstile> (ms'',s'') =as'=>⇣τ (ms',s')` show ?case by blast
qed
qed
lemma valid_nodes_silent_moves:
"[|S,f\<turnstile> (ms,s) =as'=>⇣τ (ms',s'); ∀m ∈ set ms. valid_node m|]
==> ∀m ∈ set ms'. valid_node m"
proof(induct rule:silent_moves.induct)
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
note IH = `∀m∈set ms'. valid_node m ==> ∀m∈set ms''. valid_node m`
from `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')` `∀m∈set ms. valid_node m`
have "∀m∈set ms'. valid_node m"
apply - apply(erule silent_move.cases) apply auto
by(cases ms,auto dest:get_return_edges_valid)+
from IH[OF this] show ?case .
qed simp
lemma return_nodes_silent_moves:
"[|S,f \<turnstile> (ms,s) =as'=>⇣τ (ms',s'); ∀m ∈ set (tl ms). return_node m|]
==> ∀m ∈ set (tl ms'). return_node m"
by(induct rule:silent_moves.induct,auto dest:silent_move_return_node)
lemma silent_moves_intra_path:
"[|S,f \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s'); ∀a ∈ set as. intra_kind(kind a)|]
==> ms = ms' ∧ get_proc m = get_proc m'"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m
rule:silent_moves.induct)
case (silent_moves_Cons S f sx a msx' sx' as s'')
thus ?case
proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
case (silent_move_intra f a s s' n⇣c msx')
note IH = `!!m. [|msx' = m # ms; ∀a∈set as. intra_kind (kind a)|]
==> ms = ms' ∧ get_proc m = get_proc m'`
from `msx' = targetnode a # tl (m # ms)`
have "msx' = targetnode a # ms" by simp
from `∀a∈set (a # as). intra_kind (kind a)` have "∀a∈set as. intra_kind (kind a)"
by simp
from IH[OF `msx' = targetnode a # ms` this]
have "ms = ms'" and "get_proc (targetnode a) = get_proc m'" by simp_all
moreover
from `valid_edge a` `intra_kind (kind a)`
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
moreover
from `hd (m # ms) = sourcenode a` have "m = sourcenode a" by simp
ultimately show ?case using `ms = ms'` by simp
qed (auto simp:intra_kind_def)
qed simp
lemma silent_moves_nodestack_notempty:
"[|S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s'); ms ≠ []|] ==> ms' ≠ []"
apply(induct S f ms s as ms' s' rule:silent_moves.induct) apply auto
apply(erule silent_move.cases) apply auto
apply(case_tac "tl msa") by auto
lemma silent_moves_obs_slice:
"[|S,kind \<turnstile> (ms,s) =as=>⇣τ (ms',s'); mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙;
∀n ∈ set (tl ms'). return_node n|]
==> mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀n ∈ set (tl ms). return_node n)"
proof(induct S f≡"kind" ms s as ms' s' rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S ms s a ms' s' as ms'' s'')
note IH = `[|mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙; ∀m∈set (tl ms''). return_node m|]
==> mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀m∈set (tl ms'). return_node m)`
from IH[OF `mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙` `∀m∈set (tl ms''). return_node m`]
have "mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" and "∀m∈set (tl ms'). return_node m"
by simp_all
with `S,kind \<turnstile> (ms,s) -a->⇣τ (ms',s')`
have "mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce intro:silent_move_obs_slice)
moreover
from `S,kind \<turnstile> (ms,s) -a->⇣τ (ms',s')` have "∀m∈set (tl ms). return_node m"
by(fastforce elim:silent_move.cases)
ultimately show ?case by simp
qed
lemma silent_moves_empty_obs_slice:
"[|S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s'); obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}|]
==> obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
note IH = `obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {} ==> obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}`
from IH[OF `obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {}`]
have "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}" by simp
with `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')`
show ?case by -(rule silent_move_empty_obs_slice,fastforce)
qed
lemma silent_moves_preds_transfers:
assumes "S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s')"
shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
from `S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s')`
have "preds (map f as) s ∧ transfers (map f as) s = s'"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
from `S,f \<turnstile> (ms,s) -a->⇣τ (ms',s')`
have "pred (f a) s" and "transfer (f a) s = s'" by(auto elim:silent_move.cases)
with `preds (map f as) s' ∧ transfers (map f as) s' = s''`
show ?case by fastforce
qed
thus "preds (map f as) s" and "transfers (map f as) s = s'" by simp_all
qed
lemma silent_moves_intra_path_obs:
assumes "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙" and "length s = length (m#msx')"
and "∀m ∈ set msx'. return_node m"
obtains as' where "S,slice_kind S \<turnstile> (m#msx',s) =as'=>⇣τ (m'#msx',s)"
proof(atomize_elim)
from `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙`
obtain as where "m -as->⇣ι* m'" and "m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by -(erule obs_intraE)
from `m -as->⇣ι* m'` obtain x where "distance m m' x" and "x ≤ length as"
by(erule every_path_distance)
from `distance m m' x` `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙`
`length s = length (m#msx')` `∀m ∈ set msx'. return_node m`
show "∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)"
proof(induct x arbitrary:m s rule:nat.induct)
fix m fix s::"(('var \<rightharpoonup> 'val) × 'ret) list"
assume "distance m m' 0" and "length s = length (m#msx')"
then obtain as' where "m -as'->⇣ι* m'" and "length as' = 0"
by(auto elim:distance.cases)
hence "m -[]->⇣ι* m'" by(cases as) auto
hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
with `length s = length (m#msx')`[THEN sym]
have "S,slice_kind S \<turnstile> (m#msx',s) =[]=>⇣τ (m#msx',s)"
by -(rule silent_moves_Nil)
thus "∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)" by simp blast
next
fix x m fix s::"(('var \<rightharpoonup> 'val) × 'ret) list"
assume "distance m m' (Suc x)" and "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
and IH:"!!m s. [|distance m m' x; m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙;
length s = length (m#msx'); ∀m ∈ set msx'. return_node m|]
==> ∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)"
from `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙` have "valid_node m"
by(rule in_obs_intra_valid)
with `distance m m' (Suc x)` have "m ≠ m'"
by(fastforce elim:distance.cases dest:empty_path simp:intra_path_def)
have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume isin:"m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with `valid_node m` have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(fastforce intro!:n_in_obs_intra)
with `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙` `m ≠ m'` show False by simp
qed
from `distance m m' (Suc x)` obtain a where "valid_edge a" and "m = sourcenode a"
and "intra_kind(kind a)" and "distance (targetnode a) m' x"
and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m' x ∧
valid_edge a' ∧ intra_kind (kind a') ∧
targetnode a' = mx)"
by -(erule distance_successor_distance,simp+)
from `m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙`
have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
by(rule obs_intra_singleton_element)
with `valid_edge a` `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a` `intra_kind(kind a)`
have disj:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {} ∨
obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
by -(drule_tac S="⌊HRB_slice S⌋⇘CFG⇙" in edge_obs_intra_subset,auto)
from `intra_kind(kind a)` `length s = length (m#msx')` `m ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`m = sourcenode a`
have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
by(cases s)
(auto split:split_if_asm simp add:Let_def slice_kind_def intra_kind_def)
from `distance (targetnode a) m' x` obtain asx where "targetnode a -asx->⇣ι* m'"
and "length asx = x" and "∀as'. targetnode a -as'->⇣ι* m' --> x ≤ length as'"
by(auto elim:distance.cases)
from `targetnode a -asx->⇣ι* m'` `m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
obtain mx where "mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(erule path_ex_obs_intra)
with disj have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from IH[OF `distance (targetnode a) m' x` this length
`∀m ∈ set msx'. return_node m`]
obtain asx' where moves:"S,slice_kind S \<turnstile>
(targetnode a#msx',transfer (slice_kind S a) s) =asx'=>⇣τ
(m'#msx',transfer (slice_kind S a) s)" by blast
have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
proof(cases "kind a")
fix f assume "kind a = \<Up>f"
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a` have "slice_kind S a = \<Up>id"
by(fastforce intro:slice_kind_Upd)
with `length s = length (m#msx')` show ?thesis by(cases s) auto
next
fix Q assume "kind a = (Q)⇣\<surd>"
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a`
`m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙` `distance (targetnode a) m' x`
`distance m m' (Suc x)` target
have "slice_kind S a = (λs. True)⇣\<surd>"
by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
with `length s = length (m#msx')` show ?thesis by(cases s) auto
next
fix Q r p fs assume "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
with `intra_kind(kind a)` have False by(simp add:intra_kind_def)
thus ?thesis by simp
next
fix Q p f assume "kind a = Q\<hookleftarrow>⇘p⇙f"
with `intra_kind(kind a)` have False by(simp add:intra_kind_def)
thus ?thesis by simp
qed
hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
by simp_all
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a` `valid_edge a`
`intra_kind(kind a)` `length s = length (m#msx')` `∀m ∈ set msx'. return_node m`
have "S,slice_kind S \<turnstile> (sourcenode a#msx',s) -a->⇣τ
(targetnode a#msx',transfer (slice_kind S a) s)"
by(fastforce intro:silent_move_intra)
with moves `transfer (slice_kind S a) s = s` `m = sourcenode a`
have "S,slice_kind S \<turnstile> (m#msx',s) =a#asx'=>⇣τ (m'#msx',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)" by blast
qed
qed
lemma silent_moves_intra_path_no_obs:
assumes "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}" and "method_exit m'"
and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')"
and "∀m ∈ set msx'. return_node m"
obtains as where "S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)"
proof(atomize_elim)
from `method_exit m'` `get_proc m = get_proc m'` `valid_node m`
obtain as where "m -as->⇣ι* m'" by(erule intra_path_to_matching_method_exit)
then obtain x where "distance m m' x" and "x ≤ length as"
by(erule every_path_distance)
from `distance m m' x` `m -as->⇣ι* m'` `obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}`
`length s = length (m#msx')` `∀m ∈ set msx'. return_node m`
show "∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)"
proof(induct x arbitrary:m as s rule:nat.induct)
fix m fix s::"(('var \<rightharpoonup> 'val) × 'ret) list"
assume "distance m m' 0" and "length s = length (m#msx')"
then obtain as' where "m -as'->⇣ι* m'" and "length as' = 0"
by(auto elim:distance.cases)
hence "m -[]->⇣ι* m'" by(cases as) auto
hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
with `length s = length (m#msx')`[THEN sym]
have "S,slice_kind S \<turnstile> (m#msx',s) =[]=>⇣τ (m#msx',s)"
by(fastforce intro:silent_moves_Nil)
thus "∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)" by simp blast
next
fix x m as fix s::"(('var \<rightharpoonup> 'val) × 'ret) list"
assume "distance m m' (Suc x)" and "m -as->⇣ι* m'"
and "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
and IH:"!!m as s. [|distance m m' x; m -as->⇣ι* m';
obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}; length s = length (m#msx');
∀m ∈ set msx'. return_node m|]
==> ∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)"
from `m -as->⇣ι* m'` have "valid_node m"
by(fastforce intro:path_valid_node simp:intra_path_def)
from `m -as->⇣ι* m'` have "get_proc m = get_proc m'" by(rule intra_path_get_procs)
have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with `valid_node m` have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(fastforce intro!:n_in_obs_intra)
with `obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}` show False by simp
qed
from `distance m m' (Suc x)` obtain a where "valid_edge a" and "m = sourcenode a"
and "intra_kind(kind a)" and "distance (targetnode a) m' x"
and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m' x ∧
valid_edge a' ∧ intra_kind (kind a') ∧
targetnode a' = mx)"
by -(erule distance_successor_distance,simp+)
from `intra_kind(kind a)` `length s = length (m#msx')` `m ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`m = sourcenode a`
have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
by(cases s)
(auto split:split_if_asm simp add:Let_def slice_kind_def intra_kind_def)
from `distance (targetnode a) m' x` obtain asx where "targetnode a -asx->⇣ι* m'"
and "length asx = x" and "∀as'. targetnode a -as'->⇣ι* m' --> x ≤ length as'"
by(auto elim:distance.cases)
from `valid_edge a` `intra_kind(kind a)` `m ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`m = sourcenode a` `obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}`
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
by(fastforce dest:edge_obs_intra_subset)
from IH[OF `distance (targetnode a) m' x` `targetnode a -asx->⇣ι* m'` this
length `∀m ∈ set msx'. return_node m`] obtain as'
where moves:"S,slice_kind S \<turnstile>
(targetnode a#msx',transfer (slice_kind S a) s) =as'=>⇣τ
(m'#msx',transfer (slice_kind S a) s)" by blast
have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
proof(cases "kind a")
fix f assume "kind a = \<Up>f"
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a` have "slice_kind S a = \<Up>id"
by(fastforce intro:slice_kind_Upd)
with `length s = length (m#msx')` show ?thesis by(cases s) auto
next
fix Q assume "kind a = (Q)⇣\<surd>"
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a`
`obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}` `distance (targetnode a) m' x`
`distance m m' (Suc x)` `method_exit m'` `get_proc m = get_proc m'` target
have "slice_kind S a = (λs. True)⇣\<surd>"
by(fastforce intro:slice_kind_Pred_empty_obs_nearer_SOME)
with `length s = length (m#msx')` show ?thesis by(cases s) auto
next
fix Q r p fs assume "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
with `intra_kind(kind a)` have False by(simp add:intra_kind_def)
thus ?thesis by simp
next
fix Q p f assume "kind a = Q\<hookleftarrow>⇘p⇙f"
with `intra_kind(kind a)` have False by(simp add:intra_kind_def)
thus ?thesis by simp
qed
hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
by simp_all
with `m ∉ ⌊HRB_slice S⌋⇘CFG⇙` `m = sourcenode a` `valid_edge a`
`intra_kind(kind a)` `length s = length (m#msx')` `∀m ∈ set msx'. return_node m`
have "S,slice_kind S \<turnstile> (sourcenode a#msx',s) -a->⇣τ
(targetnode a#msx',transfer (slice_kind S a) s)"
by(fastforce intro:silent_move_intra)
with moves `transfer (slice_kind S a) s = s` `m = sourcenode a`
have "S,slice_kind S \<turnstile> (m#msx',s) =a#as'=>⇣τ (m'#msx',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S \<turnstile> (m#msx',s) =as=>⇣τ (m'#msx',s)" by blast
qed
qed
lemma silent_moves_vpa_path:
assumes "S,f \<turnstile> (m#ms,s) =as=>⇣τ (m'#ms',s')" and "valid_node m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
and "ms = targetnodes rs" and "valid_return_list rs m"
and "length rs = length cs"
shows "m -as->* m'" and "valid_path_aux cs as"
proof -
from assms have "m -as->* m' ∧ valid_path_aux cs as"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m cs ms rs
rule:silent_moves.induct)
case (silent_moves_Nil msx sx n⇣c f)
from `valid_node m'` have "m' -[]->* m'"
by (rule empty_path)
thus ?case by fastforce
next
case (silent_moves_Cons S f sx a msx' sx' as s'')
thus ?case
proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
case (silent_move_intra f a sx sx' n⇣c msx')
note IH = `!!m cs ms rs. [|msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs|]
==> m -as->* m' ∧ valid_path_aux cs as`
from `msx' = targetnode a # tl (m # ms)`
have "msx' = targetnode a # ms" by simp
from `valid_edge a` `intra_kind (kind a)`
have "get_proc (sourcenode a) = get_proc (targetnode a)"
by(rule get_proc_intra)
with `valid_return_list rs m` `hd (m # ms) = sourcenode a`
have "valid_return_list rs (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
from `valid_edge a` have "valid_node (targetnode a)" by simp
from IH[OF `msx' = targetnode a # ms` this
`∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`ms = targetnodes rs` `valid_return_list rs (targetnode a)`
`length rs = length cs`]
have "targetnode a -as->* m'" and "valid_path_aux cs as" by simp_all
from `valid_edge a` `targetnode a -as->* m'`
`hd (m # ms) = sourcenode a`
have "m -a#as->* m'" by(fastforce intro:Cons_path)
moreover
from `intra_kind (kind a)` `valid_path_aux cs as`
have "valid_path_aux cs (a # as)" by(fastforce simp:intra_kind_def)
ultimately show ?case by simp
next
case (silent_move_call f a sx sx' Q r p fs a' n⇣c msx')
note IH = `!!m cs ms rs. [|msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs|]
==> m -as->* m' ∧ valid_path_aux cs as`
from `valid_edge a` have "valid_node (targetnode a)" by simp
from `length rs = length cs`
have "length (a'#rs) = length (a#cs)" by simp
from `msx' = targetnode a # targetnode a' # tl (m # ms)`
have "msx' = targetnode a # targetnode a' # ms" by simp
from `ms = targetnodes rs` have "targetnode a' # ms = targetnodes (a' # rs)"
by(simp add:targetnodes_def)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` have "get_proc (targetnode a) = p"
by(rule get_proc_call)
from `valid_edge a` `a' ∈ get_return_edges a` have "valid_edge a'"
by(rule get_return_edges_valid)
from `valid_edge a` `kind a = Q:r\<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` `a' ∈ get_return_edges a`
have "get_proc (sourcenode a) = get_proc (targetnode a')"
by(rule get_proc_get_return_edge)
with `valid_return_list rs m` `hd (m # ms) = sourcenode a`
`get_proc (targetnode a) = p` `valid_edge a'` `kind a' = Q'\<hookleftarrow>⇘p⇙f'`
have "valid_return_list (a' # rs) (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE) apply clarsimp
by(case_tac list)(auto simp:targetnodes_def)
from `∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`a' ∈ get_return_edges a`
have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
by auto(case_tac i,auto)
from IH[OF `msx' = targetnode a # targetnode a' # ms` `valid_node (targetnode a)` this
`targetnode a' # ms = targetnodes (a' # rs)`
`valid_return_list (a' # rs) (targetnode a)` `length (a'#rs) = length (a#cs)`]
have "targetnode a -as->* m'" and "valid_path_aux (a # cs) as" by simp_all
from `valid_edge a` `targetnode a -as->* m'`
`hd (m # ms) = sourcenode a`
have "m -a#as->* m'" by(fastforce intro:Cons_path)
moreover
from `valid_path_aux (a # cs) as` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "valid_path_aux cs (a # as)" by simp
ultimately show ?case by simp
next
case (silent_move_return f a sx sx' Q p f' n⇣c msx')
note IH = `!!m cs ms rs. [|msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs|]
==> m -as->* m' ∧ valid_path_aux cs as`
from `valid_edge a` have "valid_node (targetnode a)" by simp
from `length (m # ms) = length sx` `length sx = Suc (length sx')`
`sx' ≠ []`
obtain x xs where "ms = x#xs" by(cases ms) auto
with `ms = targetnodes rs` obtain r' rs' where "rs = r'#rs'"
and "x = targetnode r'" and "xs = targetnodes rs'"
by(auto simp:targetnodes_def)
with `length rs = length cs` obtain c' cs' where "cs = c'#cs'"
and "length rs' = length cs'"
by(cases cs) auto
from `ms = x#xs` `length (m # ms) = length sx`
`length sx = Suc (length sx')`
have "length sx' = Suc (length xs)" by simp
from `ms = x#xs` `msx' = tl (m # ms)` `hd (tl (m # ms)) = targetnode a`
`length (m # ms) = length sx` `length sx = Suc (length sx')` `sx' ≠ []`
have "msx' = targetnode a#xs" by simp
from `∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`rs = r'#rs'` `cs = c'#cs'`
have "r' ∈ get_return_edges c'" by fastforce
from `ms = x#xs` `hd (tl (m # ms)) = targetnode a`
have "x = targetnode a" by simp
with `valid_return_list rs m` `rs = r'#rs'` `x = targetnode r'`
have "valid_return_list rs' (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="r'#cs'" in allE) apply clarsimp
by(case_tac cs')(auto simp:targetnodes_def)
from `∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)`
`rs = r'#rs'` `cs = c'#cs'`
have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
and "r' ∈ get_return_edges c'" by auto
from IH[OF `msx' = targetnode a#xs` `valid_node (targetnode a)`
`∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)` `xs = targetnodes rs'`
`valid_return_list rs' (targetnode a)` `length rs' = length cs'`]
have "targetnode a -as->* m'" and "valid_path_aux cs' as" by simp_all
from `valid_edge a` `targetnode a -as->* m'`
`hd (m # ms) = sourcenode a`
have "m -a#as->* m'" by(fastforce intro:Cons_path)
moreover
from `ms = x#xs` `hd (tl (m # ms)) = targetnode a`
have "x = targetnode a" by simp
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
have "method_exit (sourcenode a)" by(fastforce simp:method_exit_def)
from `valid_return_list rs m` `hd (m # ms) = sourcenode a`
`rs = r'#rs'`
have "get_proc (sourcenode a) = get_proc (sourcenode r') ∧
method_exit (sourcenode r') ∧ valid_edge r'"
apply(clarsimp simp:valid_return_list_def method_exit_def)
apply(erule_tac x="[]" in allE)
by(auto dest:get_proc_return)
hence "get_proc (sourcenode a) = get_proc (sourcenode r')"
and "method_exit (sourcenode r')" and "valid_edge r'" by simp_all
with `method_exit (sourcenode a)` have "sourcenode r' = sourcenode a"
by(fastforce intro:method_exit_unique)
with `valid_edge a` `valid_edge r'` `x = targetnode r'` `x = targetnode a`
have "r' = a" by(fastforce intro:edge_det)
with `r' ∈ get_return_edges c'` `valid_path_aux cs' as` `cs = c'#cs'`
`kind a = Q\<hookleftarrow>⇘p⇙f'`
have "valid_path_aux cs (a # as)" by simp
ultimately show ?case by simp
qed
qed
thus "m -as->* m'" and "valid_path_aux cs as" by simp_all
qed
subsection {* Observable moves *}
inductive observable_move ::
"'node SDG_node set => ('edge => ('var,'val,'ret,'pname) edge_kind) => 'node list =>
(('var \<rightharpoonup> 'val) × 'ret) list => 'edge => 'node list => (('var \<rightharpoonup> 'val) × 'ret) list => bool"
("_,_ \<turnstile> '(_,_') -_-> '(_,_')" [51,50,0,0,50,0,0] 51)
where observable_move_intra:
"[|pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length s' = length s; length ms = length s;
hd ms = sourcenode a; ms' = (targetnode a)#tl ms|]
==> S,f \<turnstile> (ms,s) -a-> (ms',s')"
| observable_move_call:
"[|pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs;
valid_edge a'; a' ∈ get_return_edges a;
∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length ms = length s; length s' = Suc(length s);
hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms|]
==> S,f \<turnstile> (ms,s) -a-> (ms',s')"
| observable_move_return:
"[|pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>⇘p⇙f';
∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
length ms = length s; length s = Suc(length s'); s' ≠ [];
hd ms = sourcenode a; hd(tl ms) = targetnode a; ms' = tl ms|]
==> S,f \<turnstile> (ms,s) -a-> (ms',s')"
inductive 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 observable_moves_snoc:
"[|S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s'); S,f \<turnstile> (ms',s') -a-> (ms'',s'')|]
==> S,f \<turnstile> (ms,s) =as@[a]=> (ms'',s'')"
lemma observable_move_equal_length:
assumes "S,f \<turnstile> (ms,s) -a-> (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from `S,f \<turnstile> (ms,s) -a-> (ms',s')`
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule:observable_move.induct)
case (observable_move_intra f a s s' ms S ms')
from `pred (f a) s` obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from `length ms = length s` `ms' = targetnode a # tl ms`
`length s' = length s` show ?case by simp
next
case (observable_move_call f a s s' Q r p fs a' ms S ms')
from `pred (f a) s` obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from `length ms = length s` `length s' = Suc (length s)`
`ms' = targetnode a # targetnode a' # tl ms` show ?case by simp
next
case (observable_move_return f a s s' Q p f' ms S ms')
from `length ms = length s` `length s = Suc (length s')` `ms' = tl ms` `s' ≠ []`
show ?case by simp
qed
thus "length ms = length s" and "length ms' = length s'" by simp_all
qed
lemma observable_moves_equal_length:
assumes "S,f \<turnstile> (ms,s) =as=> (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
using `S,f \<turnstile> (ms,s) =as=> (ms',s')`
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') -a-> (ms'',s'')`
have "length ms' = length s'" "length ms'' = length s''"
by(rule observable_move_equal_length)+
moreover
from `S,f \<turnstile> (ms,s) =as=>⇣τ (ms',s')`
have "length ms = length s" and "length ms' = length s'"
by(rule silent_moves_equal_length)+
ultimately show "length ms = length s" "length ms'' = length s''" by simp_all
qed
lemma observable_move_notempty:
"[|S,f \<turnstile> (ms,s) =as=> (ms',s'); as = []|] ==> False"
by(induct rule:observable_moves.induct,simp)
lemma silent_move_observable_moves:
"[|S,f \<turnstile> (ms'',s'') =as=> (ms',s'); S,f \<turnstile> (ms,s) -a->⇣τ (ms'',s'')|]
==> S,f \<turnstile> (ms,s) =a#as=> (ms',s')"
proof(induct rule:observable_moves.induct)
case (observable_moves_snoc S f msx sx as ms' s' a' ms'' s'')
from `S,f \<turnstile> (ms,s) -a->⇣τ (msx,sx)` `S,f \<turnstile> (msx,sx) =as=>⇣τ (ms',s')`
have "S,f \<turnstile> (ms,s) =a#as=>⇣τ (ms',s')" by(fastforce intro:silent_moves_Cons)
with `S,f \<turnstile> (ms',s') -a'-> (ms'',s'')`
have "S,f \<turnstile> (ms,s) =(a#as)@[a']=> (ms'',s'')"
by(fastforce intro:observable_moves.observable_moves_snoc)
thus ?case by simp
qed
lemma silent_append_observable_moves:
"[|S,f \<turnstile> (ms,s) =as=>⇣τ (ms'',s''); S,f \<turnstile> (ms'',s'') =as'=> (ms',s')|]
==> S,f \<turnstile> (ms,s) =as@as'=> (ms',s')"
by(induct rule:silent_moves.induct)(auto elim:silent_move_observable_moves)
lemma observable_moves_preds_transfers:
assumes "S,f \<turnstile> (ms,s) =as=> (ms',s')"
shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
from `S,f \<turnstile> (ms,s) =as=> (ms',s')`
have "preds (map f as) s ∧ transfers (map f as) s = s'"
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')`
have "preds (map f as) s" and "transfers (map f as) s = s'"
by(rule silent_moves_preds_transfers)+
from `S,f \<turnstile> (ms',s') -a-> (ms'',s'')`
have "pred (f a) s'" and "transfer (f a) s' = s''"
by(auto elim:observable_move.cases)
with `preds (map f as) s` `transfers (map f as) s = s'`
show ?case by(simp add:preds_split transfers_split)
qed
thus "preds (map f as) s" and "transfers (map f as) s = s'" by simp_all
qed
lemma observable_move_vpa_path:
"[|S,f \<turnstile> (m#ms,s) -a-> (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|] ==> valid_path_aux cs [a]"
proof(induct S f "m#ms" s a "m'#ms'" s' rule:observable_move.induct)
case (observable_move_return f a sx sx' Q p f' n⇣c)
from `length (m # ms) = length sx` `length sx = Suc (length sx')`
`sx' ≠ []`
obtain x xs where "ms = x#xs" by(cases ms) auto
with `ms = targetnodes rs` obtain r' rs' where "rs = r'#rs'"
and "x = targetnode r'" and "xs = targetnodes rs'"
by(auto simp:targetnodes_def)
with `length rs = length cs` obtain c' cs' where "cs = c'#cs'"
and "length rs' = length cs'"
by(cases cs) auto
from `∀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 `ms = x#xs` `hd (tl (m # ms)) = targetnode a`
have "x = targetnode a" by simp
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
have "method_exit (sourcenode a)" by(fastforce simp:method_exit_def)
from `valid_return_list rs m` `hd (m # ms) = sourcenode a`
`rs = r'#rs'`
have "get_proc (sourcenode a) = get_proc (sourcenode r') ∧
method_exit (sourcenode r') ∧ valid_edge r'"
apply(clarsimp simp:valid_return_list_def method_exit_def)
apply(erule_tac x="[]" in allE)
by(auto dest:get_proc_return)
hence "get_proc (sourcenode a) = get_proc (sourcenode r')"
and "method_exit (sourcenode r')" and "valid_edge r'" by simp_all
with `method_exit (sourcenode a)` have "sourcenode r' = sourcenode a"
by(fastforce intro:method_exit_unique)
with `valid_edge a` `valid_edge r'` `x = targetnode r'` `x = targetnode a`
have "r' = a" by(fastforce intro:edge_det)
with `r' ∈ get_return_edges c'` `cs = c'#cs'` `kind a = Q\<hookleftarrow>⇘p⇙f'`
show ?case by simp
qed(auto simp:intra_kind_def)
subsection {* Relevant variables *}
inductive_set relevant_vars ::
"'node SDG_node set => 'node SDG_node => 'var set" ("rv _")
for S :: "'node SDG_node set" and n :: "'node SDG_node"
where rvI:
"[|parent_node n -as->⇣ι* parent_node n'; n' ∈ HRB_slice S; V ∈ Use⇘SDG⇙ n';
∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''|]
==> V ∈ rv S n"
lemma rvE:
assumes rv:"V ∈ rv S n"
obtains as n' where "parent_node n -as->⇣ι* parent_node n'"
and "n' ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ n'"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''"
using rv
by(atomize_elim,auto elim!:relevant_vars.cases)
lemma rv_parent_node:
"parent_node n = parent_node n' ==> rv (S::'node SDG_node set) n = rv S n'"
by(fastforce elim:rvE intro:rvI)
lemma obs_intra_empty_rv_empty:
assumes "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}" shows "rv S (CFG_node m) = {}"
proof(rule ccontr)
assume "rv S (CFG_node m) ≠ {}"
then obtain x where "x ∈ rv S (CFG_node m)" by fastforce
then obtain n' as where "m -as->⇣ι* parent_node n'" and "n' ∈ HRB_slice S"
by(fastforce elim:rvE)
hence "parent_node n' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:valid_SDG_node_in_slice_parent_node_in_slice
simp:SDG_to_CFG_set_def)
with `m -as->⇣ι* parent_node n'` obtain mx where "mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
by(erule path_ex_obs_intra)
with `obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}` show False by simp
qed
lemma eq_obs_intra_in_rv:
assumes obs_eq:"obs_intra (parent_node n) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (parent_node n') ⌊HRB_slice S⌋⇘CFG⇙"
and "x ∈ rv S n" shows "x ∈ rv S n'"
proof -
from `x ∈ rv S n` obtain as n''
where "parent_node n -as->⇣ι* parent_node n''" and "n'' ∈ HRB_slice S"
and "x ∈ Use⇘SDG⇙ n''"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> x ∉ Def⇘SDG⇙ n''"
by(erule rvE)
from `parent_node n -as->⇣ι* parent_node n''` have "valid_node (parent_node n'')"
by(fastforce dest:path_valid_node simp:intra_path_def)
from `parent_node n -as->⇣ι* parent_node n''` `n'' ∈ HRB_slice S`
have "∃nx as' as''. parent_node nx ∈ obs_intra (parent_node n) ⌊HRB_slice S⌋⇘CFG⇙ ∧
parent_node n -as'->⇣ι* parent_node nx ∧
parent_node nx -as''->⇣ι* parent_node n'' ∧ as = as'@as''"
proof(cases "∀nx. parent_node nx ∈ set (sourcenodes as) --> nx ∉ HRB_slice S")
case True
with `parent_node n -as->⇣ι* parent_node n''` `n'' ∈ HRB_slice S`
have "parent_node n'' ∈ obs_intra (parent_node n) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obs_intra_elem valid_SDG_node_in_slice_parent_node_in_slice
simp:SDG_to_CFG_set_def)
with `parent_node n -as->⇣ι* parent_node n''` `valid_node (parent_node n'')`
show ?thesis by(fastforce intro:empty_path simp:intra_path_def)
next
case False
hence "∃nx. parent_node nx ∈ set (sourcenodes as) ∧ nx ∈ HRB_slice S" by simp
hence "∃mx ∈ set (sourcenodes as). ∃nx. mx = parent_node nx ∧ nx ∈ HRB_slice S"
by fastforce
then obtain mx ms ms' where "sourcenodes as = ms@mx#ms'"
and "∃nx. mx = parent_node nx ∧ nx ∈ HRB_slice S"
and all:"∀x ∈ set ms. ¬ (∃nx. x = parent_node nx ∧ nx ∈ HRB_slice S)"
by(fastforce elim!:split_list_first_propE)
then obtain nx' where "mx = parent_node nx'" and "nx' ∈ HRB_slice S" by blast
from `sourcenodes as = ms@mx#ms'`
obtain as' a' as'' where "ms = sourcenodes as'"
and [simp]:"as = as'@a'#as''" and "sourcenode a' = mx"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from all `ms = sourcenodes as'`
have "∀nx∈set (sourcenodes as'). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce simp:SDG_to_CFG_set_def)
from `parent_node n -as->⇣ι* parent_node n''` `sourcenode a' = mx`
have "parent_node n -as'->⇣ι* mx" and "valid_edge a'" and "intra_kind(kind a')"
and "targetnode a' -as''->⇣ι* parent_node n''"
by(fastforce dest:path_split simp:intra_path_def)+
with `sourcenode a' = mx` have "mx -a'#as''->⇣ι* parent_node n''"
by(fastforce intro:Cons_path simp:intra_path_def)
from `parent_node n -as'->⇣ι* mx` `mx = parent_node nx'` `nx' ∈ HRB_slice S`
`∀nx∈set (sourcenodes as'). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙` `ms = sourcenodes as'`
have "mx ∈ obs_intra (parent_node n) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obs_intra_elem valid_SDG_node_in_slice_parent_node_in_slice
simp:SDG_to_CFG_set_def)
with `parent_node n -as'->⇣ι* mx` `mx -a'#as''->⇣ι* parent_node n''`
`mx = parent_node nx'`
show ?thesis by simp blast
qed
then obtain nx as' as''
where "parent_node nx ∈ obs_intra (parent_node n) ⌊HRB_slice S⌋⇘CFG⇙"
and "parent_node n -as'->⇣ι* parent_node nx"
and "parent_node nx -as''->⇣ι* parent_node n''" and [simp]:"as = as'@as''"
by blast
from `parent_node nx ∈ obs_intra (parent_node n) ⌊HRB_slice S⌋⇘CFG⇙` obs_eq
have "parent_node nx ∈ obs_intra (parent_node n') ⌊HRB_slice S⌋⇘CFG⇙" by auto
then obtain asx where "parent_node n' -asx->⇣ι* parent_node nx"
and "∀ni ∈ set(sourcenodes asx). ni ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "parent_node nx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(erule obs_intraE)
from `∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> x ∉ Def⇘SDG⇙ n''`
have "∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes as'')
--> x ∉ Def⇘SDG⇙ ni"
by(auto simp:sourcenodes_def)
from `∀ni ∈ set(sourcenodes asx). ni ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`parent_node n' -asx->⇣ι* parent_node nx`
have "∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes asx)
--> x ∉ Def⇘SDG⇙ ni"
proof(induct asx arbitrary:n')
case Nil thus ?case by(simp add:sourcenodes_def)
next
case (Cons ax' asx')
note IH = `!!n'. [|∀ni∈set (sourcenodes asx'). ni ∉ ⌊HRB_slice S⌋⇘CFG⇙;
parent_node n' -asx'->⇣ι* parent_node nx|]
==> ∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes asx')
--> x ∉ Def⇘SDG⇙ ni`
from `parent_node n' -ax'#asx'->⇣ι* parent_node nx`
have "parent_node n' -[]@ax'#asx'->* parent_node nx"
and "∀a ∈ set (ax'#asx'). intra_kind(kind a)" by(simp_all add:intra_path_def)
hence "targetnode ax' -asx'->* parent_node nx" and "valid_edge ax'"
and "parent_node n' = sourcenode ax'" by(fastforce dest:path_split)+
with `∀a ∈ set (ax'#asx'). intra_kind(kind a)`
have path:"parent_node (CFG_node (targetnode ax')) -asx'->⇣ι* parent_node nx"
by(simp add:intra_path_def)
from `∀ni∈set (sourcenodes (ax'#asx')). ni ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have all:"∀ni∈set (sourcenodes asx'). ni ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "sourcenode ax' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(auto simp:sourcenodes_def)
from IH[OF all path]
have "∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes asx')
--> x ∉ Def⇘SDG⇙ ni" .
with `∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes as'')
--> x ∉ Def⇘SDG⇙ ni`
have all:"∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes (asx'@as''))
--> x ∉ Def⇘SDG⇙ ni"
by(auto simp:sourcenodes_def)
from `parent_node n' -ax'#asx'->⇣ι* parent_node nx`
`parent_node nx -as''->⇣ι* parent_node n''`
have path:"parent_node n' -ax'#asx'@as''->⇣ι* parent_node n''"
by(fastforce intro:path_Append[of _ "ax'#asx'",simplified] simp:intra_path_def)
have "∀nx'. parent_node nx' = sourcenode ax' --> x ∉ Def⇘SDG⇙ nx'"
proof
fix nx'
show "parent_node nx' = sourcenode ax' --> x ∉ Def⇘SDG⇙ nx'"
proof
assume "parent_node nx' = sourcenode ax'"
show "x ∉ Def⇘SDG⇙ nx'"
proof
assume "x ∈ Def⇘SDG⇙ nx'"
from `parent_node n' = sourcenode ax'` `parent_node nx' = sourcenode ax'`
have "parent_node nx' = parent_node n'" by simp
with `x ∈ Def⇘SDG⇙ nx'` `x ∈ Use⇘SDG⇙ n''` all path
have "nx' influences x in n''" by(fastforce simp:data_dependence_def)
hence "nx' s-x->⇘dd⇙ n''" by(rule sum_SDG_ddep_edge)
with `n'' ∈ HRB_slice S` have "nx' ∈ HRB_slice S"
by(fastforce elim:combine_SDG_slices.cases
intro:combine_SDG_slices.intros ddep_slice1 ddep_slice2
simp:HRB_slice_def)
hence "CFG_node (parent_node nx') ∈ HRB_slice S"
by(rule valid_SDG_node_in_slice_parent_node_in_slice)
with `sourcenode ax' ∉ ⌊HRB_slice S⌋⇘CFG⇙` `parent_node n' = sourcenode ax'`
`parent_node nx' = sourcenode ax'` show False
by(simp add:SDG_to_CFG_set_def)
qed
qed
qed
with all show ?case by(auto simp add:sourcenodes_def)
qed
with `∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes as'')
--> x ∉ Def⇘SDG⇙ ni`
have all:"∀ni. valid_SDG_node ni ∧ parent_node ni ∈ set (sourcenodes (asx@as''))
--> x ∉ Def⇘SDG⇙ ni"
by(auto simp:sourcenodes_def)
with `parent_node n' -asx->⇣ι* parent_node nx`
`parent_node nx -as''->⇣ι* parent_node n''`
have "parent_node n' -asx@as''->⇣ι* parent_node n''"
by(fastforce intro:path_Append simp:intra_path_def)
from this `n'' ∈ HRB_slice S` `x ∈ Use⇘SDG⇙ n''` all
show "x ∈ rv S n'" by(rule rvI)
qed
lemma closed_eq_obs_eq_rvs:
fixes S :: "'node SDG_node set"
assumes obs_eq:"obs_intra (parent_node n) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (parent_node n') ⌊HRB_slice S⌋⇘CFG⇙"
shows "rv S n = rv S n'"
proof
show "rv S n ⊆ rv S n'"
proof
fix x assume "x ∈ rv S n"
with obs_eq show "x ∈ rv S n'" by(rule eq_obs_intra_in_rv)
qed
next
show "rv S n' ⊆ rv S n"
proof
fix x assume "x ∈ rv S n'"
with obs_eq[THEN sym] show "x ∈ rv S n" by(rule eq_obs_intra_in_rv)
qed
qed
lemma closed_eq_obs_eq_rvs':
fixes S :: "'node SDG_node set"
assumes obs_eq:"obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = obs_intra m' ⌊HRB_slice S⌋⇘CFG⇙"
shows "rv S (CFG_node m) = rv S (CFG_node m')"
proof
show "rv S (CFG_node m) ⊆ rv S (CFG_node m')"
proof
fix x assume "x ∈ rv S (CFG_node m)"
with obs_eq show "x ∈ rv S (CFG_node m')"
by -(rule eq_obs_intra_in_rv,auto)
qed
next
show "rv S (CFG_node m') ⊆ rv S (CFG_node m)"
proof
fix x assume "x ∈ rv S (CFG_node m')"
with obs_eq[THEN sym] show "x ∈ rv S (CFG_node m)"
by -(rule eq_obs_intra_in_rv,auto)
qed
qed
lemma rv_branching_edges_slice_kinds_False:
assumes "valid_edge a" and "valid_edge ax"
and "sourcenode a = sourcenode ax" and "targetnode a ≠ targetnode ax"
and "intra_kind (kind a)" and "intra_kind (kind ax)"
and "preds (slice_kinds S (a#as)) s"
and "preds (slice_kinds S (ax#asx)) s'"
and "length s = length s'" and "snd (hd s) = snd (hd s')"
and "∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V"
shows False
proof -
from `valid_edge a` `valid_edge ax` `sourcenode a = sourcenode ax`
`targetnode a ≠ targetnode ax` `intra_kind (kind a)` `intra_kind (kind ax)`
obtain Q Q' where "kind a = (Q)⇣\<surd>" and "kind ax = (Q')⇣\<surd>"
and "∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s)"
by(auto dest:deterministic)
from `valid_edge a` `valid_edge ax` `sourcenode a = sourcenode ax`
`targetnode a ≠ targetnode ax` `intra_kind (kind a)` `intra_kind (kind ax)`
obtain P P' where "slice_kind S a = (P)⇣\<surd>"
and "slice_kind S ax = (P')⇣\<surd>"
and "∀s. (P s --> ¬ P' s) ∧ (P' s --> ¬ P s)"
by -(erule slice_deterministic,auto)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `intra_kind (kind a)`
have "slice_kind S a = kind a" by -(rule slice_intra_kind_in_slice)
with `preds (slice_kinds S (a#as)) s` `kind a = (Q)⇣\<surd>`
`slice_kind S a = (P)⇣\<surd>` have "pred (kind a) s"
by(simp add:slice_kinds_def)
from True `sourcenode a = sourcenode ax` `intra_kind (kind ax)`
have "slice_kind S ax = kind ax"
by(fastforce intro:slice_intra_kind_in_slice)
with `preds (slice_kinds S (ax#asx)) s'` `kind ax = (Q')⇣\<surd>`
`slice_kind S ax = (P')⇣\<surd>` have "pred (kind ax) s'"
by(simp add:slice_kinds_def)
with `kind ax = (Q')⇣\<surd>` have "Q' (fst (hd s'))" by(cases s') auto
from `valid_edge a` have "sourcenode a -[]->⇣ι* sourcenode a"
by(fastforce intro:empty_path simp:intra_path_def)
with True `valid_edge a`
have "∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))"
by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def SDG_to_CFG_set_def)
with `∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V`
have "∀V ∈ Use (sourcenode a). state_val s V = state_val s' V" by blast
with `valid_edge a` `pred (kind a) s` `pred (kind ax) s'` `length s = length s'`
`snd (hd s) = snd (hd s')`
have "pred (kind a) s'" by(auto intro:CFG_edge_Uses_pred_equal)
with `kind a = (Q)⇣\<surd>` have "Q (fst (hd s'))" by(cases s') auto
with `Q' (fst (hd s'))` `∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s)`
have False by simp
thus ?thesis by simp
next
case False
with `kind a = (Q)⇣\<surd>` `slice_kind S a = (P)⇣\<surd>` `valid_edge a`
have "P = (λs. False) ∨ P = (λs. True)"
by(fastforce elim:kind_Predicate_notin_slice_slice_kind_Predicate)
with `slice_kind S a = (P)⇣\<surd>`
`preds (slice_kinds S (a#as)) s`
have "P = (λs. True)" by(cases s)(auto simp:slice_kinds_def)
from `sourcenode a = sourcenode ax` False
have "sourcenode ax ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `kind ax = (Q')⇣\<surd>` `slice_kind S ax = (P')⇣\<surd>` `valid_edge ax`
have "P' = (λs. False) ∨ P' = (λs. True)"
by(fastforce elim:kind_Predicate_notin_slice_slice_kind_Predicate)
with `slice_kind S ax = (P')⇣\<surd>`
`preds (slice_kinds S (ax#asx)) s'`
have "P' = (λs. True)" by(cases s')(auto simp:slice_kinds_def)
with `P = (λs. True)` `∀s. (P s --> ¬ P' s) ∧ (P' s --> ¬ P s)`
have False by blast
thus ?thesis by simp
qed
qed
lemma rv_edge_slice_kinds:
assumes "valid_edge a" and "intra_kind (kind a)"
and "∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V"
and "preds (slice_kinds S (a#as)) s" and "preds (slice_kinds S (a#asx)) s'"
shows "∀V∈rv S (CFG_node (targetnode a)).
state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a))"
from `preds (slice_kinds S (a#as)) s`
have "s ≠ []" by(cases s,auto simp:slice_kinds_def)
from `preds (slice_kinds S (a#asx)) s'`
have "s' ≠ []" by(cases s',auto simp:slice_kinds_def)
show "state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V"
proof(cases "V ∈ Def (sourcenode a)")
case True
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `intra_kind (kind a)` have "slice_kind S a = kind a"
by -(rule slice_intra_kind_in_slice)
with `preds (slice_kinds S (a#as)) s` have "pred (kind a) s"
by(simp add:slice_kinds_def)
from `slice_kind S a = kind a`
`preds (slice_kinds S (a#asx)) s'`
have "pred (kind a) s'" by(simp add:slice_kinds_def)
from `valid_edge a` have "sourcenode a -[]->⇣ι* sourcenode a"
by(fastforce intro:empty_path simp:intra_path_def)
with True `valid_edge a`
have "∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))"
by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def SDG_to_CFG_set_def)
with `∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V`
have "∀V ∈ Use (sourcenode a). state_val s V = state_val s' V" by blast
from `valid_edge a` this `pred (kind a) s` `pred (kind a) s'`
`intra_kind (kind a)`
have "∀V ∈ Def (sourcenode a).
state_val (transfer (kind a) s) V = state_val (transfer (kind a) s') V"
by -(rule CFG_intra_edge_transfer_uses_only_Use,auto)
with `V ∈ Def (sourcenode a)` `slice_kind S a = kind a`
show ?thesis by simp
next
case False
from `V ∈ rv S (CFG_node (targetnode a))`
obtain xs nx where "targetnode a -xs->⇣ι* parent_node nx"
and "nx ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ nx"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes xs)
--> V ∉ Def⇘SDG⇙ n''" by(fastforce elim:rvE)
from `valid_edge a` have "valid_node (sourcenode a)" by simp
from `valid_edge a` `targetnode a -xs->⇣ι* parent_node nx` `intra_kind (kind a)`
have "sourcenode a -a#xs ->⇣ι* parent_node nx"
by(fastforce intro:path.Cons_path simp:intra_path_def)
with `V ∈ Def (sourcenode a)` `V ∈ Use⇘SDG⇙ nx` `valid_node (sourcenode a)`
`∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes xs)
--> V ∉ Def⇘SDG⇙ n''`
have "(CFG_node (sourcenode a)) influences V in nx"
by(fastforce intro:CFG_Def_SDG_Def simp:data_dependence_def)
hence "(CFG_node (sourcenode a)) s-V->⇘dd⇙ nx" by(rule sum_SDG_ddep_edge)
from `nx ∈ HRB_slice S` `(CFG_node (sourcenode a)) s-V->⇘dd⇙ nx`
have "CFG_node (sourcenode a) ∈ HRB_slice S"
proof(induct rule:HRB_slice_cases)
case (phase1 n nx')
with `(CFG_node (sourcenode a)) s-V->⇘dd⇙ nx` show ?case
by(fastforce intro:intro:ddep_slice1 combine_SDG_slices.combSlice_refl
simp:HRB_slice_def)
next
case (phase2 nx' n' n'' p n)
from `(CFG_node (sourcenode a)) s-V->⇘dd⇙ n` `n ∈ sum_SDG_slice2 n'`
have "CFG_node (sourcenode a) ∈ sum_SDG_slice2 n'" by(rule ddep_slice2)
with phase2 show ?thesis
by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
simp:HRB_slice_def)
qed
with False have False by(simp add:SDG_to_CFG_set_def)
thus ?thesis by simp
qed
next
case False
from `V ∈ rv S (CFG_node (targetnode a))`
obtain xs nx where "targetnode a -xs->⇣ι* parent_node nx"
and "nx ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ nx"
and all:"∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes xs)
--> V ∉ Def⇘SDG⇙ n''" by(fastforce elim:rvE)
from `valid_edge a` have "valid_node (sourcenode a)" by simp
from `valid_edge a` `targetnode a -xs->⇣ι* parent_node nx` `intra_kind (kind a)`
have "sourcenode a -a#xs ->⇣ι* parent_node nx"
by(fastforce intro:path.Cons_path simp:intra_path_def)
from False all
have "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (a#xs))
--> V ∉ Def⇘SDG⇙ n''"
by(fastforce dest:SDG_Def_parent_Def simp:sourcenodes_def)
with `sourcenode a -a#xs ->⇣ι* parent_node nx` `nx ∈ HRB_slice S`
`V ∈ Use⇘SDG⇙ nx`
have "V ∈ rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
from `intra_kind (kind a)` show ?thesis
proof(cases "kind a")
case(UpdateEdge f)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with `intra_kind (kind a)` have "slice_kind S a = kind a"
by(fastforce intro:slice_intra_kind_in_slice)
from UpdateEdge `s ≠ []` have "pred (kind a) s" by(cases s) auto
with `valid_edge a` `V ∉ Def (sourcenode a)` `intra_kind (kind a)`
have "state_val (transfer (kind a) s) V = state_val s V"
by(fastforce intro:CFG_intra_edge_no_Def_equal)
from UpdateEdge `s' ≠ []` have "pred (kind a) s'" by(cases s') auto
with `valid_edge a` `V ∉ Def (sourcenode a)` `intra_kind (kind a)`
have "state_val (transfer (kind a) s') V = state_val s' V"
by(fastforce intro:CFG_intra_edge_no_Def_equal)
with `∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V`
`state_val (transfer (kind a) s) V = state_val s V`
`V ∈ rv S (CFG_node (sourcenode a))` `slice_kind S a = kind a`
show ?thesis by fastforce
next
case False
with UpdateEdge have "slice_kind S a = \<Up>id"
by -(rule slice_kind_Upd)
with `∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V`
`V ∈ rv S (CFG_node (sourcenode a))` `s ≠ []` `s' ≠ []`
show ?thesis by(cases s,auto,cases s',auto)
qed
next
case (PredicateEdge Q)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with PredicateEdge `intra_kind (kind a)`
have "slice_kind S a = (Q)⇣\<surd>"
by(simp add:slice_intra_kind_in_slice)
with `∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V`
`V ∈ rv S (CFG_node (sourcenode a))` `s ≠ []` `s' ≠ []`
show ?thesis by(cases s,auto,cases s',auto)
next
case False
with PredicateEdge `valid_edge a`
obtain Q' where "slice_kind S a = (Q')⇣\<surd>"
by -(erule kind_Predicate_notin_slice_slice_kind_Predicate)
with`∀V∈rv S (CFG_node (sourcenode a)). state_val s V = state_val s' V`
`V ∈ rv S (CFG_node (sourcenode a))` `s ≠ []` `s' ≠ []`
show ?thesis by(cases s,auto,cases s',auto)
qed
qed (auto simp:intra_kind_def)
qed
qed
subsection {* The weak simulation relational set @{text WS} *}
inductive_set WS :: "'node SDG_node set => (('node list × (('var \<rightharpoonup> 'val) × 'ret) list) ×
('node list × (('var \<rightharpoonup> 'val) × 'ret) list)) set"
for S :: "'node SDG_node set"
where WSI: "[|∀m ∈ set ms. valid_node m; ∀m' ∈ set ms'. valid_node m';
length ms = length s; length ms' = length s'; s ≠ []; s' ≠ []; ms = msx@mx#tl ms';
get_proc mx = get_proc (hd ms');
∀m ∈ set (tl ms'). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
∀i < length ms'. snd (s!(length msx + i)) = snd (s'!i);
∀m ∈ set (tl ms). return_node m;
∀i < length ms'. ∀V ∈ rv S (CFG_node ((mx#tl ms')!i)).
(fst (s!(length msx + i))) V = (fst (s'!i)) V;
obs ms ⌊HRB_slice S⌋⇘CFG⇙ = obs ms' ⌊HRB_slice S⌋⇘CFG⇙|]
==> ((ms,s),(ms',s')) ∈ WS S"
lemma WS_silent_move:
assumes "S,kind \<turnstile> (ms⇣1,s⇣1) -a->⇣τ (ms⇣1',s⇣1')" and "((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S"
shows "((ms⇣1',s⇣1'),(ms⇣2,s⇣2)) ∈ WS S"
proof -
from `((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S` obtain msx mx
where WSE:"∀m ∈ set ms⇣1. valid_node m" "∀m ∈ set ms⇣2. valid_node m"
"length ms⇣1 = length s⇣1" "length ms⇣2 = length s⇣2" "s⇣1 ≠ []" "s⇣2 ≠ []"
"ms⇣1 = msx@mx#tl ms⇣2" "get_proc mx = get_proc (hd ms⇣2)"
"∀m ∈ set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
"msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
"∀m ∈ set (tl ms⇣1). return_node m"
"∀i < length ms⇣2. snd (s⇣1!(length msx + i)) = snd (s⇣2!i)"
"∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V"
"obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce elim:WS.cases)
{ assume "∀m ∈ set (tl ms⇣1'). return_node m"
have "obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙"
proof(cases "obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
with `S,kind \<turnstile> (ms⇣1,s⇣1) -a->⇣τ (ms⇣1',s⇣1')` have "obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = {}"
by(rule silent_move_empty_obs_slice)
with `obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
`obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = {}`
show ?thesis by simp
next
case False
from this `∀m ∈ set (tl ms⇣1'). return_node m`
obtain ms' where "obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = {ms'}"
by(fastforce dest:obs_singleton_element)
hence "ms' ∈ obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from `S,kind \<turnstile> (ms⇣1,s⇣1) -a->⇣τ (ms⇣1',s⇣1')` `ms' ∈ obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙`
`∀m ∈ set (tl ms⇣1'). return_node m`
have "ms' ∈ obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce intro:silent_move_obs_slice)
from this `∀m ∈ set (tl ms⇣1). return_node m`
have "obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = {ms'}" by(rule obs_singleton_element)
with `obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = {ms'}`
`obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
show ?thesis by simp
qed }
with `S,kind \<turnstile> (ms⇣1,s⇣1) -a->⇣τ (ms⇣1',s⇣1')` WSE
show ?thesis
proof(induct S f≡"kind" ms⇣1 s⇣1 a ms⇣1' s⇣1' rule:silent_move.induct)
case (silent_move_intra a s⇣1 s⇣1' ms⇣1 S ms⇣1')
note obs_eq = `∀a∈set (tl ms⇣1'). return_node a ==>
obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
from `s⇣1 ≠ []` `s⇣2 ≠ []` obtain cf⇣1 cfs⇣1 cf⇣2 cfs⇣2 where [simp]:"s⇣1 = cf⇣1#cfs⇣1"
and [simp]:"s⇣2 = cf⇣2#cfs⇣2" by(cases s⇣1,auto,cases s⇣2,fastforce+)
from `transfer (kind a) s⇣1 = s⇣1'` `intra_kind (kind a)`
obtain cf⇣1' where [simp]:"s⇣1' = cf⇣1'#cfs⇣1"
by(cases cf⇣1,cases "kind a",auto simp:intra_kind_def)
from `∀m ∈ set ms⇣1. valid_node m` `ms⇣1' = targetnode a # tl ms⇣1` `valid_edge a`
have "∀m ∈ set ms⇣1'. valid_node m" by(cases ms⇣1) auto
from `length ms⇣1 = length s⇣1` `length s⇣1' = length s⇣1`
`ms⇣1' = targetnode a # tl ms⇣1`
have "length ms⇣1' = length s⇣1'" by(cases ms⇣1) auto
from `∀m ∈ set (tl ms⇣1). return_node m` `ms⇣1' = targetnode a # tl ms⇣1`
have "∀m ∈ set (tl ms⇣1'). return_node m" by simp
from obs_eq[OF this] have "obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙" .
from `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` `length ms⇣2 = length s⇣2`
have "∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V"
by(cases ms⇣2) auto
show ?case
proof(cases msx)
case Nil
with `ms⇣1 = msx@mx#tl ms⇣2` `hd ms⇣1 = sourcenode a`
have [simp]:"mx = sourcenode a" and [simp]:"tl ms⇣1 = tl ms⇣2" by simp_all
from `∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`(∃m∈set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms⇣1 ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have "hd ms⇣1 ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
with `hd ms⇣1 = sourcenode a` have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
from `ms⇣1' = targetnode a # tl ms⇣1` have "ms⇣1' = [] @ targetnode a # tl ms⇣2"
by simp
from `valid_edge a` `intra_kind(kind a)`
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
with `get_proc mx = get_proc (hd ms⇣2)`
have "get_proc (targetnode a) = get_proc (hd ms⇣2)" by simp
from `transfer (kind a) s⇣1 = s⇣1'` `intra_kind (kind a)`
have "snd cf⇣1' = snd cf⇣1" by(auto simp:intra_kind_def)
with `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)` Nil
have "∀i<length ms⇣2. snd (s⇣1' ! i) = snd (s⇣2 ! i)"
by auto(case_tac i,auto)
have "∀V ∈ rv S (CFG_node (targetnode a)). fst cf⇣1' V = fst cf⇣2 V"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a))"
from `valid_edge a` `intra_kind (kind a)` `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
hence "rv S (CFG_node (targetnode a)) = rv S (CFG_node (sourcenode a))"
by(rule closed_eq_obs_eq_rvs')
with `V ∈ rv S (CFG_node (targetnode a))`
have "V ∈ rv S (CFG_node (sourcenode a))" by simp
then obtain as n' where "sourcenode a -as->⇣ι* parent_node n'"
and "n' ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ n'"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''"
by(fastforce elim:rvE)
with `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙` `valid_edge a`
have "V ∉ Def⇘SDG⇙ (CFG_node (sourcenode a))"
apply(clarsimp simp:intra_path_def)
apply(erule path.cases)
by(auto dest:valid_SDG_node_in_slice_parent_node_in_slice
simp:sourcenodes_def SDG_to_CFG_set_def)
from `valid_edge a` have "valid_node (sourcenode a)" by simp
with `V ∉ Def⇘SDG⇙ (CFG_node (sourcenode a))` have "V ∉ Def (sourcenode a)"
by(fastforce intro:CFG_Def_SDG_Def valid_SDG_CFG_node)
with `valid_edge a` `intra_kind (kind a)` `pred (kind a) s⇣1`
have "state_val (transfer (kind a) s⇣1) V = state_val s⇣1 V"
by(fastforce intro:CFG_intra_edge_no_Def_equal)
with `transfer (kind a) s⇣1 = s⇣1'` have "fst cf⇣1' V = fst cf⇣1 V" by simp
from `V ∈ rv S (CFG_node (sourcenode a))` `msx = []`
`∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V`
have "fst cf⇣1 V = fst cf⇣2 V" by simp
with `fst cf⇣1' V = fst cf⇣1 V` show "fst cf⇣1' V = fst cf⇣2 V" by simp
qed
with `∀i<length ms⇣2. ∀V∈rv S (CFG_node ((mx # tl ms⇣2) ! i)).
(fst (s⇣1 ! (length msx + i))) V = (fst (s⇣2 ! i)) V` Nil
have "∀i<length ms⇣2. ∀V∈rv S (CFG_node ((targetnode a # tl ms⇣2) ! i)).
(fst (s⇣1' ! (length [] + i))) V = (fst (s⇣2 ! i)) V"
by auto (case_tac i,auto)
with `∀m ∈ set ms⇣1'. valid_node m` `∀m ∈ set ms⇣2. valid_node m`
`length ms⇣1' = length s⇣1'` `length ms⇣2 = length s⇣2`
`ms⇣1' = [] @ targetnode a # tl ms⇣2`
`get_proc (targetnode a) = get_proc (hd ms⇣2)`
`∀m ∈ set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀m ∈ set (tl ms⇣1). return_node m`
`obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
`∀i<length ms⇣2. snd (s⇣1' ! i) = snd (s⇣2 ! i)`
show ?thesis by(auto intro!:WSI)
next
case (Cons mx' msx')
with `ms⇣1 = msx@mx#tl ms⇣2` `hd ms⇣1 = sourcenode a`
have [simp]:"mx' = sourcenode a" and [simp]:"tl ms⇣1 = msx'@mx#tl ms⇣2"
by simp_all
from `ms⇣1' = targetnode a # tl ms⇣1` have "ms⇣1' = ((targetnode a)#msx')@mx#tl ms⇣2"
by simp
from `∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V` Cons
have rv:"∀V∈rv S (CFG_node mx).
(fst (s⇣1' ! length (targetnode a#msx'))) V = state_val s⇣2 V" by fastforce
from `ms⇣1 = msx@mx#tl ms⇣2` Cons `ms⇣1' = targetnode a # tl ms⇣1`
have "ms⇣1' = ((targetnode a)#msx')@mx#tl ms⇣2" by simp
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)` Cons
have "∀i<length ms⇣2. snd (s⇣1' ! (length msx + i)) = snd (s⇣2 ! i)" by fastforce
from `∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V` Cons
have "∀V∈rv S (CFG_node mx). (fst (s⇣1' ! length msx)) V = state_val s⇣2 V"
by simp
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` Cons
have "∀i<length ms⇣2. ∀V∈rv S (CFG_node ((mx # tl ms⇣2)!i)).
(fst (s⇣1'!(length (targetnode a # msx') + i))) V = (fst (s⇣2!i)) V"
by clarsimp
with `∀m∈set ms⇣1'. valid_node m` `∀m∈set ms⇣2. valid_node m`
`length ms⇣1' = length s⇣1'` `length ms⇣2 = length s⇣2`
`ms⇣1' = ((targetnode a)#msx')@mx#tl ms⇣2`
`∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀m ∈ set (tl ms⇣1'). return_node m` `get_proc mx = get_proc (hd ms⇣2)`
`msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
`obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙` Cons
`∀i<length ms⇣2. snd (s⇣1' ! (length msx + i)) = snd (s⇣2 ! i)`
show ?thesis by -(rule WSI,clarsimp+,fastforce,clarsimp+)
qed
next
case (silent_move_call a s⇣1 s⇣1' Q r p fs a' ms⇣1 S ms⇣1')
note obs_eq = `∀a∈set (tl ms⇣1'). return_node a ==>
obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
from `s⇣1 ≠ []` `s⇣2 ≠ []` obtain cf⇣1 cfs⇣1 cf⇣2 cfs⇣2 where [simp]:"s⇣1 = cf⇣1#cfs⇣1"
and [simp]:"s⇣2 = cf⇣2#cfs⇣2" by(cases s⇣1,auto,cases s⇣2,fastforce+)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
obtain ins outs where "(p,ins,outs) ∈ set procs"
by(fastforce dest!:callee_in_procs)
with `transfer (kind a) s⇣1 = s⇣1'` `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have [simp]:"s⇣1' = (Map.empty(ins [:=] params fs (fst cf⇣1)), r) # cf⇣1 # cfs⇣1"
by simp(unfold formal_in_THE,simp)
from `length ms⇣1 = length s⇣1` `ms⇣1' = targetnode a # targetnode a' # tl ms⇣1`
have "length ms⇣1' = length s⇣1'" by simp
from `valid_edge a` `a' ∈ get_return_edges a` have "valid_edge a'"
by(rule get_return_edges_valid)
with `∀m∈set ms⇣1. valid_node m` `valid_edge a`
`ms⇣1' = targetnode a # targetnode a' # tl ms⇣1`
have "∀m∈set ms⇣1'. valid_node m" by(cases ms⇣1) auto
from `valid_edge a'` `valid_edge a` `a' ∈ get_return_edges a`
have "return_node (targetnode a')" by(fastforce simp:return_node_def)
with `valid_edge a` `a' ∈ get_return_edges a` `valid_edge a'`
have "call_of_return_node (targetnode a') (sourcenode a)"
by(simp add:call_of_return_node_def) blast
from `∀m ∈ set (tl ms⇣1). return_node m` `return_node (targetnode a')`
`ms⇣1' = targetnode a # targetnode a' # tl ms⇣1`
have "∀m ∈ set (tl ms⇣1'). return_node m" by simp
from obs_eq[OF this] have "obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙" .
from `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` `length ms⇣2 = length s⇣2`
have "∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V"
by(erule_tac x="0" in allE) auto
show ?case
proof(cases msx)
case Nil
with `ms⇣1 = msx@mx#tl ms⇣2` `hd ms⇣1 = sourcenode a`
have [simp]:"mx = sourcenode a" and [simp]:"tl ms⇣1 = tl ms⇣2" by simp_all
from `∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`(∃m∈set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms⇣1 ∉ ⌊HRB_slice S⌋⇘CFG⇙`
have "hd ms⇣1 ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
with `hd ms⇣1 = sourcenode a` have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
from `valid_edge a` `a' ∈ get_return_edges a`
obtain a'' where "valid_edge a''" and "sourcenode a'' = sourcenode a"
and "targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
by -(drule call_return_node_edge,auto 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)
with `sourcenode a'' = sourcenode a` `targetnode a'' = targetnode a'`
`get_proc mx = get_proc (hd ms⇣2)`
have "get_proc (targetnode a') = get_proc (hd ms⇣2)" by simp
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges a`
have "CFG_node (sourcenode a) s-p->⇘sum⇙ CFG_node (targetnode a')"
by(fastforce intro:sum_SDG_call_summary_edge)
have "targetnode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume "targetnode a' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
hence "CFG_node (targetnode a') ∈ HRB_slice S" by(simp add:SDG_to_CFG_set_def)
hence "CFG_node (sourcenode a) ∈ HRB_slice S"
proof(induct "CFG_node (targetnode a')" rule:HRB_slice_cases)
case (phase1 nx)
with `CFG_node (sourcenode a) s-p->⇘sum⇙ CFG_node (targetnode a')`
show ?case by(fastforce intro:combine_SDG_slices.combSlice_refl sum_slice1
simp:HRB_slice_def)
next
case (phase2 nx n' n'' p')
from `CFG_node (targetnode a') ∈ sum_SDG_slice2 n'`
`CFG_node (sourcenode a) s-p->⇘sum⇙ CFG_node (targetnode a')` `valid_edge a`
have "CFG_node (sourcenode a) ∈ sum_SDG_slice2 n'"
by(fastforce intro:sum_slice2)
with `n' ∈ sum_SDG_slice1 nx` `n'' s-p'->⇘ret⇙ CFG_node (parent_node n')`
`nx ∈ S`
show ?case
by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
simp:HRB_slice_def)
qed
with `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙` show False
by(simp add:SDG_to_CFG_set_def HRB_slice_def)
qed
from `ms⇣1' = targetnode a # targetnode a' # tl ms⇣1`
have "ms⇣1' = [targetnode a] @ targetnode a' # tl ms⇣2" by simp
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)` Nil
have "∀i<length ms⇣2. snd (s⇣1' ! (length [targetnode a] + i)) = snd (s⇣2 ! i)"
by fastforce
have "∀V∈rv S (CFG_node (targetnode a')). (fst (s⇣1' ! 1)) V = state_val s⇣2 V"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a'))"
from `valid_edge a` `a' ∈ get_return_edges a`
obtain a'' where edge:"valid_edge a''" "sourcenode a'' = sourcenode a"
"targetnode a'' = targetnode a'" "intra_kind(kind a'')"
by -(drule call_return_node_edge,auto simp:intra_kind_def)
from `V ∈ rv S (CFG_node (targetnode a'))`
obtain as n' where "targetnode a' -as->⇣ι* parent_node n'"
and "n' ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ n'"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''"
by(fastforce elim:rvE)
from `targetnode a' -as->⇣ι* parent_node n'` edge
have "sourcenode a -a''#as->⇣ι* parent_node n'"
by(fastforce intro:Cons_path simp:intra_path_def)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "V ∉ Def (sourcenode a)"
by(fastforce dest:call_source_Def_empty)
with `∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''` `sourcenode a'' = sourcenode a`
have "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (a''#as))
--> V ∉ Def⇘SDG⇙ n''"
by(fastforce dest:SDG_Def_parent_Def simp:sourcenodes_def)
with `sourcenode a -a''#as->⇣ι* parent_node n'` `n' ∈ HRB_slice S`
`V ∈ Use⇘SDG⇙ n'`
have "V ∈ rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
from `∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V` Nil
have "∀V∈rv S (CFG_node (sourcenode a)). fst cf⇣1 V = fst cf⇣2 V" by simp
with `V ∈ rv S (CFG_node (sourcenode a))` have "fst cf⇣1 V = fst cf⇣2 V" by simp
thus "(fst (s⇣1' ! 1)) V = state_val s⇣2 V" by simp
qed
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` Nil
have "∀i<length ms⇣2. ∀V∈rv S (CFG_node ((targetnode a' # tl ms⇣2)!i)).
(fst (s⇣1'!(length [targetnode a] + i))) V = (fst (s⇣2!i)) V"
by clarsimp(case_tac i,auto)
with `∀m∈set ms⇣1'. valid_node m` `∀m∈set ms⇣2. valid_node m`
`length ms⇣1' = length s⇣1'` `length ms⇣2 = length s⇣2`
`∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`ms⇣1' = [targetnode a] @ targetnode a' # tl ms⇣2`
`targetnode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙` `return_node (targetnode a')`
`obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
`get_proc (targetnode a') = get_proc (hd ms⇣2)`
`∀m ∈ set (tl ms⇣1'). return_node m` `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`call_of_return_node (targetnode a') (sourcenode a)`
`∀i<length ms⇣2. snd (s⇣1' ! (length [targetnode a] + i)) = snd (s⇣2 ! i)`
show ?thesis by(auto intro!:WSI)
next
case (Cons mx' msx')
with `ms⇣1 = msx@mx#tl ms⇣2` `hd ms⇣1 = sourcenode a`
have [simp]:"mx' = sourcenode a" and [simp]:"tl ms⇣1 = msx'@mx#tl ms⇣2"
by simp_all
from `ms⇣1' = targetnode a # targetnode a' # tl ms⇣1`
have "ms⇣1' = (targetnode a # targetnode a' # msx')@mx#tl ms⇣2"
by simp
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)` Cons
have "∀i<length ms⇣2.
snd (s⇣1' ! (length (targetnode a # targetnode a' # msx') + i)) = snd (s⇣2 ! i)"
by fastforce
from `∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V` Cons
have "∀V∈rv S (CFG_node mx).
(fst (s⇣1' ! length(targetnode a # targetnode a' # msx'))) V = state_val s⇣2 V"
by simp
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` Cons
have "∀i<length ms⇣2. ∀V∈rv S (CFG_node ((mx # tl ms⇣2)!i)).
(fst (s⇣1'!(length (targetnode a # targetnode a' # msx') + i))) V =
(fst (s⇣2!i)) V"
by clarsimp
with `∀m∈set ms⇣1'. valid_node m` `∀m∈set ms⇣2. valid_node m`
`length ms⇣1' = length s⇣1'` `length ms⇣2 = length s⇣2`
`ms⇣1' = (targetnode a # targetnode a' # msx')@mx#tl ms⇣2`
`return_node (targetnode a')`
`∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
`obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙` Cons
`get_proc mx = get_proc (hd ms⇣2)` `∀m ∈ set (tl ms⇣1'). return_node m`
`∀i<length ms⇣2.
snd (s⇣1' ! (length (targetnode a # targetnode a' # msx') + i)) = snd (s⇣2 ! i)`
show ?thesis by -(rule WSI,clarsimp+,fastforce,clarsimp+)
qed
next
case (silent_move_return a s⇣1 s⇣1' Q p f' ms⇣1 S ms⇣1')
note obs_eq = `∀a∈set (tl ms⇣1'). return_node a ==>
obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
from `transfer (kind a) s⇣1 = s⇣1'` `kind a = Q\<hookleftarrow>⇘p⇙f'` `s⇣1 ≠ []` `s⇣1' ≠ []`
obtain cf⇣1 cfx⇣1 cfs⇣1 cf⇣1' where [simp]:"s⇣1 = cf⇣1#cfx⇣1#cfs⇣1"
and "s⇣1' = (f' (fst cf⇣1) (fst cfx⇣1),snd cfx⇣1)#cfs⇣1"
by(cases s⇣1,auto,case_tac list,fastforce+)
from `s⇣2 ≠ []` obtain cf⇣2 cfs⇣2 where [simp]:"s⇣2 = cf⇣2#cfs⇣2" by(cases s⇣2) auto
from `length ms⇣1 = length s⇣1` have "ms⇣1 ≠ []" and "tl ms⇣1 ≠ []" by(cases ms⇣1,auto)+
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
obtain a' Q' r' fs' where "valid_edge a'" and "kind a' = Q':r'\<hookrightarrow>⇘p⇙fs'"
and "a ∈ get_return_edges a'"
by -(drule return_needs_call,auto)
then obtain ins outs where "(p,ins,outs) ∈ set procs"
by(fastforce dest!:callee_in_procs)
with `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
have "f' (fst cf⇣1) (fst cfx⇣1) =
(fst cfx⇣1)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs)"
by(rule CFG_return_edge_fun)
with `s⇣1' = (f' (fst cf⇣1) (fst cfx⇣1),snd cfx⇣1)#cfs⇣1`
have [simp]:"s⇣1' = ((fst cfx⇣1)
(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs),snd cfx⇣1)#cfs⇣1" by simp
from `∀m∈set ms⇣1. valid_node m` `ms⇣1' = tl ms⇣1` have "∀m∈set ms⇣1'. valid_node m"
by(cases ms⇣1) auto
from `length ms⇣1 = length s⇣1` `ms⇣1' = tl ms⇣1`
have "length ms⇣1' = length s⇣1'" by simp
from `∀m∈set (tl ms⇣1). return_node m` `ms⇣1' = tl ms⇣1` `ms⇣1 ≠ []` `tl ms⇣1 ≠ []`
have "∀m∈set (tl ms⇣1'). return_node m" by(cases ms⇣1)(auto,cases ms⇣1',auto)
from obs_eq[OF this] have "obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙" .
show ?case
proof(cases msx)
case Nil
with `ms⇣1 = msx@mx#tl ms⇣2` `hd ms⇣1 = sourcenode a`
have "mx = sourcenode a" and "tl ms⇣1 = tl ms⇣2" by simp_all
with `∃m∈set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙`
`∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have False by fastforce
thus ?thesis by simp
next
case (Cons mx' msx')
with `ms⇣1 = msx@mx#tl ms⇣2` `hd ms⇣1 = sourcenode a`
have [simp]:"mx' = sourcenode a" and [simp]:"tl ms⇣1 = msx'@mx#tl ms⇣2"
by simp_all
from `ms⇣1' = tl ms⇣1` have "ms⇣1' = msx'@mx#tl ms⇣2" by simp
with `ms⇣1 = msx@mx#tl ms⇣2` `∀m∈set (tl ms⇣1). return_node m` Cons
have "∀m∈set (tl ms⇣1'). return_node m"
by(cases msx') auto
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)` Cons
have "∀i<length ms⇣2. snd (s⇣1' ! (length msx' + i)) = snd (s⇣2 ! i)"
by auto(case_tac i,auto,cases msx',auto)
from `∀i<length ms⇣2. ∀V∈rv S (CFG_node ((mx # tl ms⇣2) ! i)).
(fst (s⇣1 ! (length msx + i))) V = (fst (s⇣2 ! i)) V`
`length ms⇣2 = length s⇣2` `s⇣2 ≠ []`
have "∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V"
by fastforce
have "∀V∈rv S (CFG_node mx). (fst (s⇣1' ! length msx')) V = state_val s⇣2 V"
proof(cases msx')
case Nil
with `∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V`
`msx = mx'#msx'`
have rv:"∀V∈rv S (CFG_node mx). fst cfx⇣1 V = fst cf⇣2 V" by fastforce
from Nil `tl ms⇣1 = msx'@mx#tl ms⇣2` `hd (tl ms⇣1) = targetnode a`
have [simp]:"mx = targetnode a" by simp
from Cons
`msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
obtain mx'' where "call_of_return_node mx mx''" and "mx'' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by blast
hence "mx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by(rule call_node_notin_slice_return_node_neither)
have "∀V∈rv S (CFG_node mx).
(fst cfx⇣1)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs) V = fst cf⇣2 V"
proof
fix V assume "V∈rv S (CFG_node mx)"
show "(fst cfx⇣1)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs) V =
fst cf⇣2 V"
proof(cases "V ∈ set (ParamDefs (targetnode a))")
case True
with `valid_edge a` have "V ∈ Def (targetnode a)"
by(fastforce intro:ParamDefs_in_Def)
with `valid_edge a` have "V ∈ Def⇘SDG⇙ (CFG_node (targetnode a))"
by(auto intro!:CFG_Def_SDG_Def)
from `V∈rv S (CFG_node mx)` obtain as n'
where "targetnode a -as->⇣ι* parent_node n'"
and "n' ∈ HRB_slice S" "V ∈ Use⇘SDG⇙ n'"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''" by(fastforce elim:rvE)
from `targetnode a -as->⇣ι* parent_node n'` `n' ∈ HRB_slice S`
`mx ∉ ⌊HRB_slice S⌋⇘CFG⇙`
obtain ax asx where "as = ax#asx"
by(auto simp:intra_path_def)(erule path.cases,
auto dest:valid_SDG_node_in_slice_parent_node_in_slice
simp:SDG_to_CFG_set_def)
with `targetnode a -as->⇣ι* parent_node n'`
have "targetnode a = sourcenode ax" and "valid_edge ax"
by(auto elim:path.cases simp:intra_path_def)
with `∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''` `as = ax#asx` `V ∈ Def⇘SDG⇙ (CFG_node (targetnode a))`
have False by(fastforce simp:sourcenodes_def)
thus ?thesis by simp
next
case False
with `V∈rv S (CFG_node mx)` rv show ?thesis
by(fastforce dest:fun_upds_notin[of _ _ "fst cfx⇣1"])
qed
qed
with Nil `msx = mx'#msx'` show ?thesis by fastforce
next
case Cons
with `∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V`
`msx = mx'#msx'`
show ?thesis by fastforce
qed
with `∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V` Cons
have "∀V∈rv S (CFG_node mx). (fst (s⇣1' ! length msx')) V = state_val s⇣2 V"
by(cases msx') auto
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` Cons
have "∀i<length ms⇣2. ∀V∈rv S (CFG_node ((mx # tl ms⇣2) ! i)).
(fst (s⇣1' ! (length msx' + i))) V = (fst (s⇣2 ! i)) V"
by clarsimp(case_tac i,auto)
with `∀m∈set ms⇣1'. valid_node m` `∀m∈set ms⇣2. valid_node m`
`length ms⇣1' = length s⇣1'` `length ms⇣2 = length s⇣2`
`ms⇣1' = msx'@mx#tl ms⇣2` `get_proc mx = get_proc (hd ms⇣2)`
`∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
`∀m∈set (tl ms⇣1'). return_node m` Cons `get_proc mx = get_proc (hd ms⇣2)`
`∀m∈set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`obs ms⇣1' ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
`∀i<length ms⇣2. snd (s⇣1' ! (length msx' + i)) = snd (s⇣2 ! i)`
show ?thesis by(auto intro!:WSI)
qed
qed
qed
lemma WS_silent_moves:
"[|S,kind \<turnstile> (ms⇣1,s⇣1) =as=>⇣τ (ms⇣1',s⇣1'); ((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S|]
==> ((ms⇣1',s⇣1'),(ms⇣2,s⇣2)) ∈ WS S"
by(induct S f≡"kind" ms⇣1 s⇣1 as ms⇣1' s⇣1' rule:silent_moves.induct,
auto dest:WS_silent_move)
lemma WS_observable_move:
assumes "((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S"
and "S,kind \<turnstile> (ms⇣1,s⇣1) -a-> (ms⇣1',s⇣1')" and "s⇣1' ≠ []"
obtains as where "((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S a) s⇣2)) ∈ WS S"
and "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as@[a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)"
proof(atomize_elim)
from `((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S` obtain msx mx
where assms:"∀m ∈ set ms⇣1. valid_node m" "∀m ∈ set ms⇣2. valid_node m"
"length ms⇣1 = length s⇣1" "length ms⇣2 = length s⇣2" "s⇣1 ≠ []" "s⇣2 ≠ []"
"ms⇣1 = msx@mx#tl ms⇣2" "get_proc mx = get_proc (hd ms⇣2)"
"∀m ∈ set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
"msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
"∀m ∈ set (tl ms⇣1). return_node m"
"∀i < length ms⇣2. snd (s⇣1!(length msx + i)) = snd (s⇣2!i)"
"∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V"
"obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce elim:WS.cases)
from `S,kind \<turnstile> (ms⇣1,s⇣1) -a-> (ms⇣1',s⇣1')` assms
show "∃as. ((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S a) s⇣2)) ∈ WS S ∧
S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as @ [a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)"
proof(induct S f≡"kind" ms⇣1 s⇣1 a ms⇣1' s⇣1' rule:observable_move.induct)
case (observable_move_intra a s⇣1 s⇣1' ms⇣1 S ms⇣1')
from `s⇣1 ≠ []` `s⇣2 ≠ []` obtain cf⇣1 cfs⇣1 cf⇣2 cfs⇣2 where [simp]:"s⇣1 = cf⇣1#cfs⇣1"
and [simp]:"s⇣2 = cf⇣2#cfs⇣2" by(cases s⇣1,auto,cases s⇣2,fastforce+)
from `length ms⇣1 = length s⇣1` `s⇣1 ≠ []` have [simp]:"ms⇣1 ≠ []" by(cases ms⇣1) auto
from `length ms⇣2 = length s⇣2` `s⇣2 ≠ []` have [simp]:"ms⇣2 ≠ []" by(cases ms⇣2) auto
from `∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`hd ms⇣1 = sourcenode a` `ms⇣1 = msx@mx#tl ms⇣2`
`msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
have [simp]:"mx = sourcenode a" "msx = []" and [simp]:"tl ms⇣2 = tl ms⇣1"
by(cases msx,auto)+
hence "length ms⇣1 = length ms⇣2" by(cases ms⇣2) auto
with `length ms⇣1 = length s⇣1` `length ms⇣2 = length s⇣2`
have "length s⇣1 = length s⇣2" by simp
from `hd ms⇣1 ∈ ⌊HRB_slice S⌋⇘CFG⇙` `hd ms⇣1 = sourcenode a`
have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `valid_edge a`
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
from `∀m ∈ set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}`
`hd ms⇣1 = sourcenode a`
have "(hd ms⇣1#tl ms⇣1) ∈ obs ([]@hd ms⇣1#tl ms⇣1) ⌊HRB_slice S⌋⇘CFG⇙"
by(cases ms⇣1)(auto intro!:obsI)
hence "ms⇣1 ∈ obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
have "ms⇣1 ∈ obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙" by simp
from `ms⇣2 ≠ []` `length ms⇣2 = length s⇣2` have "length s⇣2 = length (hd ms⇣2#tl ms⇣2)"
by(fastforce dest!:hd_Cons_tl)
from `∀m ∈ set (tl ms⇣1). return_node m` have "∀m ∈ set (tl ms⇣2). return_node m"
by simp
with `ms⇣1 ∈ obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
have "hd ms⇣1 ∈ obs_intra (hd ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙"
proof(rule obsE)
fix nsx n nsx' n'
assume "ms⇣2 = nsx @ n # nsx'" and "ms⇣1 = n' # nsx'"
and "n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
from `ms⇣2 = nsx @ n # nsx'` `ms⇣1 = n' # nsx'` `tl ms⇣2 = tl ms⇣1`
have [simp]:"nsx = []" by(cases nsx) auto
with `ms⇣2 = nsx @ n # nsx'` have [simp]:"n = hd ms⇣2" by simp
from `ms⇣1 = n' # nsx'` have [simp]:"n' = hd ms⇣1" by simp
with `n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙` show ?thesis by simp
qed
with `length s⇣2 = length (hd ms⇣2#tl ms⇣2)` `∀m ∈ set (tl ms⇣2). return_node m`
obtain as where "S,slice_kind S \<turnstile> (hd ms⇣2#tl ms⇣2,s⇣2) =as=>⇣τ (hd ms⇣1#tl ms⇣1,s⇣2)"
by(fastforce elim:silent_moves_intra_path_obs[of _ _ _ s⇣2 "tl ms⇣2"])
with `ms⇣2 ≠ []` have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)"
by(fastforce dest!:hd_Cons_tl)
from `valid_edge a` have "valid_node (sourcenode a)" by simp
hence "sourcenode a -[]->⇣ι* sourcenode a"
by(fastforce intro:empty_path simp:intra_path_def)
with `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "∀V. V ∈ Use⇘SDG⇙ (CFG_node (sourcenode a))
--> V ∈ rv S (CFG_node (sourcenode a))"
by auto(rule rvI,auto simp:SDG_to_CFG_set_def sourcenodes_def)
with `valid_node (sourcenode a)`
have "∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))"
by(fastforce intro:CFG_Use_SDG_Use)
from `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` `length ms⇣2 = length s⇣2`
have "∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V"
by(cases ms⇣2) auto
with `∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))`
have "∀V ∈ Use (sourcenode a). fst cf⇣1 V = fst cf⇣2 V" by fastforce
moreover
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)`
have "snd (hd s⇣1) = snd (hd s⇣2)" by(erule_tac x="0" in allE) auto
ultimately have "pred (kind a) s⇣2"
using `valid_edge a` `pred (kind a) s⇣1` `length s⇣1 = length s⇣2`
by(fastforce intro:CFG_edge_Uses_pred_equal)
from `ms⇣1' = targetnode a # tl ms⇣1` `length s⇣1' = length s⇣1`
`length ms⇣1 = length s⇣1` have "length ms⇣1' = length s⇣1'" by simp
from `transfer (kind a) s⇣1 = s⇣1'` `intra_kind (kind a)`
obtain cf⇣1' where [simp]:"s⇣1' = cf⇣1'#cfs⇣1"
by(cases cf⇣1,cases "kind a",auto simp:intra_kind_def)
from `intra_kind (kind a)` `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `pred (kind a) s⇣2`
have "pred (slice_kind S a) s⇣2" by(simp add:slice_intra_kind_in_slice)
from `valid_edge a` `length s⇣1 = length s⇣2` `transfer (kind a) s⇣1 = s⇣1'`
have "length s⇣1' = length (transfer (slice_kind S a) s⇣2)"
by(fastforce intro:length_transfer_kind_slice_kind)
with `length s⇣1 = length s⇣2`
have "length s⇣2 = length (transfer (slice_kind S a) s⇣2)" by simp
with `pred (slice_kind S a) s⇣2` `valid_edge a` `intra_kind (kind a)`
`∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`hd ms⇣1 ∈ ⌊HRB_slice S⌋⇘CFG⇙` `hd ms⇣1 = sourcenode a`
`length ms⇣1 = length s⇣1` `length s⇣1 = length s⇣2`
`ms⇣1' = targetnode a # tl ms⇣1` `∀m ∈ set (tl ms⇣2). return_node m`
have "S,slice_kind S \<turnstile> (ms⇣1,s⇣2) -a-> (ms⇣1',transfer (slice_kind S a) s⇣2)"
by(auto intro:observable_move.observable_move_intra)
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)`
have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as@[a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)"
by(rule observable_moves_snoc)
from `∀m ∈ set ms⇣1. valid_node m` `ms⇣1' = targetnode a # tl ms⇣1` `valid_edge a`
have "∀m ∈ set ms⇣1'. valid_node m" by(cases ms⇣1) auto
from `∀m ∈ set (tl ms⇣2). return_node m` `ms⇣1' = targetnode a # tl ms⇣1`
`ms⇣1' = targetnode a # tl ms⇣1`
have "∀m ∈ set (tl ms⇣1'). return_node m" by fastforce
from `ms⇣1' = targetnode a # tl ms⇣1` `tl ms⇣2 = tl ms⇣1`
have "ms⇣1' = [] @ targetnode a # tl ms⇣2" by simp
from `intra_kind (kind a)` `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have cf2':"∃cf⇣2'. transfer (slice_kind S a) s⇣2 = cf⇣2'#cfs⇣2 ∧ snd cf⇣2' = snd cf⇣2"
by(cases cf⇣2)(auto dest:slice_intra_kind_in_slice simp:intra_kind_def)
from `transfer (kind a) s⇣1 = s⇣1'` `intra_kind (kind a)`
have "snd cf⇣1' = snd cf⇣1" by(auto simp:intra_kind_def)
with `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)`
`snd (hd s⇣1) = snd (hd s⇣2)` `ms⇣1' = [] @ targetnode a # tl ms⇣2`
cf2' `length ms⇣1 = length ms⇣2`
have "∀i<length ms⇣1'. snd (s⇣1' ! i) = snd (transfer (slice_kind S a) s⇣2 ! i)"
by auto(case_tac i,auto)
have "∀V ∈ rv S (CFG_node (targetnode a)).
fst cf⇣1' V = state_val (transfer (slice_kind S a) s⇣2) V"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a))"
show "fst cf⇣1' V = state_val (transfer (slice_kind S a) s⇣2) V"
proof(cases "V ∈ Def (sourcenode a)")
case True
from `intra_kind (kind a)` have "(∃f. kind a = \<Up>f) ∨ (∃Q. kind a = (Q)⇣\<surd>)"
by(simp add:intra_kind_def)
thus ?thesis
proof
assume "∃f. kind a = \<Up>f"
then obtain f' where "kind a = \<Up>f'" by blast
with `transfer (kind a) s⇣1 = s⇣1'`
have "s⇣1' = (f' (fst cf⇣1),snd cf⇣1) # cfs⇣1" by simp
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = \<Up>f'`
have "slice_kind S a = \<Up>f'"
by(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
hence "transfer (slice_kind S a) s⇣2 = (f' (fst cf⇣2),snd cf⇣2) # cfs⇣2" by simp
from `valid_edge a` `∀V ∈ Use (sourcenode a). fst cf⇣1 V = fst cf⇣2 V`
`intra_kind (kind a)` `pred (kind a) s⇣1` `pred (kind a) s⇣2`
have "∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s⇣1) V =
state_val (transfer (kind a) s⇣2) V"
by -(erule CFG_intra_edge_transfer_uses_only_Use,auto)
with `kind a = \<Up>f'` `s⇣1' = (f' (fst cf⇣1),snd cf⇣1) # cfs⇣1` True
`transfer (slice_kind S a) s⇣2 = (f' (fst cf⇣2),snd cf⇣2) # cfs⇣2`
show ?thesis by simp
next
assume "∃Q. kind a = (Q)⇣\<surd>"
then obtain Q where "kind a = (Q)⇣\<surd>" by blast
with `transfer (kind a) s⇣1 = s⇣1'` have "s⇣1' = cf⇣1 # cfs⇣1" by simp
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = (Q)⇣\<surd>`
have "slice_kind S a = (Q)⇣\<surd>"
by(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
hence "transfer (slice_kind S a) s⇣2 = s⇣2" by simp
from `valid_edge a` `∀V ∈ Use (sourcenode a). fst cf⇣1 V = fst cf⇣2 V`
`intra_kind (kind a)` `pred (kind a) s⇣1` `pred (kind a) s⇣2`
have "∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s⇣1) V =
state_val (transfer (kind a) s⇣2) V"
by -(erule CFG_intra_edge_transfer_uses_only_Use,auto simp:intra_kind_def)
with True `kind a = (Q)⇣\<surd>` `s⇣1' = cf⇣1 # cfs⇣1`
`transfer (slice_kind S a) s⇣2 = s⇣2`
show ?thesis by simp
qed
next
case False
with `valid_edge a` `intra_kind (kind a)` `pred (kind a) s⇣1`
have "state_val (transfer (kind a) s⇣1) V = state_val s⇣1 V"
by(fastforce intro:CFG_intra_edge_no_Def_equal)
with `transfer (kind a) s⇣1 = s⇣1'` have "fst cf⇣1' V = fst cf⇣1 V" by simp
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `intra_kind (kind a)`
have "slice_kind S a = kind a" by(fastforce intro:slice_intra_kind_in_slice)
from False `valid_edge a` `pred (kind a) s⇣2` `intra_kind (kind a)`
have "state_val (transfer (kind a) s⇣2) V = state_val s⇣2 V"
by(fastforce intro:CFG_intra_edge_no_Def_equal)
with `slice_kind S a = kind a`
have "state_val (transfer (slice_kind S a) s⇣2) V = fst cf⇣2 V" by simp
from `V ∈ rv S (CFG_node (targetnode a))` obtain as' nx
where "targetnode a -as'->⇣ι* parent_node nx"
and "nx ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ nx"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as')
--> V ∉ Def⇘SDG⇙ n''"
by(fastforce elim:rvE)
with `∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as')
--> V ∉ Def⇘SDG⇙ n''` False
have all:"∀n''. valid_SDG_node n'' ∧
parent_node n'' ∈ set (sourcenodes (a#as')) --> V ∉ Def⇘SDG⇙ n''"
by(fastforce dest:SDG_Def_parent_Def simp:sourcenodes_def)
from `valid_edge a` `targetnode a -as'->⇣ι* parent_node nx`
`intra_kind (kind a)`
have "sourcenode a -a#as'->⇣ι* parent_node nx"
by(fastforce intro:Cons_path simp:intra_path_def)
with `nx ∈ HRB_slice S` `V ∈ Use⇘SDG⇙ nx` all
have "V ∈ rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
with `∀V ∈ rv S (CFG_node mx). (fst (s⇣1!(length msx))) V = state_val s⇣2 V`
`state_val (transfer (slice_kind S a) s⇣2) V = fst cf⇣2 V`
`fst cf⇣1' V = fst cf⇣1 V`
show ?thesis by fastforce
qed
qed
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` cf2'
`ms⇣1' = [] @ targetnode a # tl ms⇣2`
`length ms⇣1 = length s⇣1` `length ms⇣2 = length s⇣2` `length s⇣1 = length s⇣2`
have "∀i<length ms⇣1'. ∀V∈rv S (CFG_node ((targetnode a # tl ms⇣1')!i)).
(fst (s⇣1'!(length [] + i))) V = (fst (transfer (slice_kind S a) s⇣2 ! i)) V"
by clarsimp(case_tac i,auto)
with `∀m ∈ set ms⇣2. valid_node m` `∀m ∈ set ms⇣1'. valid_node m`
`length ms⇣2 = length s⇣2` `length s⇣1' = length (transfer (slice_kind S a) s⇣2)`
`length ms⇣1' = length s⇣1'` `∀m ∈ set (tl ms⇣1'). return_node m`
`ms⇣1' = [] @ targetnode a # tl ms⇣2` `get_proc mx = get_proc (hd ms⇣2)`
`∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀i<length ms⇣1'. snd (s⇣1' ! i) = snd (transfer (slice_kind S a) s⇣2 ! i)`
have "((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S a) s⇣2)) ∈ WS S"
by(fastforce intro!:WSI)
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as@[a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)`
show ?case by blast
next
case (observable_move_call a s⇣1 s⇣1' Q r p fs a' ms⇣1 S ms⇣1')
from `s⇣1 ≠ []` `s⇣2 ≠ []` obtain cf⇣1 cfs⇣1 cf⇣2 cfs⇣2 where [simp]:"s⇣1 = cf⇣1#cfs⇣1"
and [simp]:"s⇣2 = cf⇣2#cfs⇣2" by(cases s⇣1,auto,cases s⇣2,fastforce+)
from `length ms⇣1 = length s⇣1` `s⇣1 ≠ []` have [simp]:"ms⇣1 ≠ []" by(cases ms⇣1) auto
from `length ms⇣2 = length s⇣2` `s⇣2 ≠ []` have [simp]:"ms⇣2 ≠ []" by(cases ms⇣2) auto
from `∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`hd ms⇣1 = sourcenode a` `ms⇣1 = msx@mx#tl ms⇣2`
`msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
have [simp]:"mx = sourcenode a" "msx = []" and [simp]:"tl ms⇣2 = tl ms⇣1"
by(cases msx,auto)+
hence "length ms⇣1 = length ms⇣2" by(cases ms⇣2) auto
with `length ms⇣1 = length s⇣1` `length ms⇣2 = length s⇣2`
have "length s⇣1 = length s⇣2" by simp
from `hd ms⇣1 ∈ ⌊HRB_slice S⌋⇘CFG⇙` `hd ms⇣1 = sourcenode a`
have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `valid_edge a`
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
from `∀m ∈ set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}`
`hd ms⇣1 = sourcenode a`
have "(hd ms⇣1#tl ms⇣1) ∈ obs ([]@hd ms⇣1#tl ms⇣1) ⌊HRB_slice S⌋⇘CFG⇙"
by(cases ms⇣1)(auto intro!:obsI)
hence "ms⇣1 ∈ obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙" by simp
with `obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
have "ms⇣1 ∈ obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙" by simp
from `ms⇣2 ≠ []` `length ms⇣2 = length s⇣2` have "length s⇣2 = length (hd ms⇣2#tl ms⇣2)"
by(fastforce dest!:hd_Cons_tl)
from `∀m ∈ set (tl ms⇣1). return_node m` have "∀m ∈ set (tl ms⇣2). return_node m"
by simp
with `ms⇣1 ∈ obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
have "hd ms⇣1 ∈ obs_intra (hd ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙"
proof(rule obsE)
fix nsx n nsx' n'
assume "ms⇣2 = nsx @ n # nsx'" and "ms⇣1 = n' # nsx'"
and "n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
from `ms⇣2 = nsx @ n # nsx'` `ms⇣1 = n' # nsx'` `tl ms⇣2 = tl ms⇣1`
have [simp]:"nsx = []" by(cases nsx) auto
with `ms⇣2 = nsx @ n # nsx'` have [simp]:"n = hd ms⇣2" by simp
from `ms⇣1 = n' # nsx'` have [simp]:"n' = hd ms⇣1" by simp
with `n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙` show ?thesis by simp
qed
with `length s⇣2 = length (hd ms⇣2#tl ms⇣2)` `∀m ∈ set (tl ms⇣2). return_node m`
obtain as where "S,slice_kind S \<turnstile> (hd ms⇣2#tl ms⇣2,s⇣2) =as=>⇣τ (hd ms⇣1#tl ms⇣1,s⇣2)"
by(fastforce elim:silent_moves_intra_path_obs[of _ _ _ s⇣2 "tl ms⇣2"])
with `ms⇣2 ≠ []` have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)"
by(fastforce dest!:hd_Cons_tl)
from `valid_edge a` have "valid_node (sourcenode a)" by simp
hence "sourcenode a -[]->⇣ι* sourcenode a"
by(fastforce intro:empty_path simp:intra_path_def)
with `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "∀V. V ∈ Use⇘SDG⇙ (CFG_node (sourcenode a))
--> V ∈ rv S (CFG_node (sourcenode a))"
by auto(rule rvI,auto simp:SDG_to_CFG_set_def sourcenodes_def)
with `valid_node (sourcenode a)`
have "∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))"
by(fastforce intro:CFG_Use_SDG_Use)
from `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` `length ms⇣2 = length s⇣2`
have "∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V"
by(cases ms⇣2) auto
with `∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))`
have "∀V ∈ Use (sourcenode a). fst cf⇣1 V = fst cf⇣2 V" by fastforce
moreover
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)`
have "snd (hd s⇣1) = snd (hd s⇣2)" by(erule_tac x="0" in allE) auto
ultimately have "pred (kind a) s⇣2"
using `valid_edge a` `pred (kind a) s⇣1` `length s⇣1 = length s⇣2`
by(fastforce intro:CFG_edge_Uses_pred_equal)
from `ms⇣1' = (targetnode a)#(targetnode a')#tl ms⇣1` `length s⇣1' = Suc(length s⇣1)`
`length ms⇣1 = length s⇣1` have "length ms⇣1' = length s⇣1'" by simp
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` obtain ins outs
where "(p,ins,outs) ∈ set procs" by(fastforce dest!:callee_in_procs)
with `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "(THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins"
by(rule formal_in_THE)
with `transfer (kind a) s⇣1 = s⇣1'` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have [simp]:"s⇣1' = (empty(ins [:=] params fs (fst cf⇣1)),r)#cf⇣1#cfs⇣1" by simp
from `valid_edge a'` `a' ∈ get_return_edges a` `valid_edge 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
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `pred (kind a) s⇣2` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "pred (slice_kind S a) s⇣2" by(fastforce dest:slice_kind_Call_in_slice)
from `valid_edge a` `length s⇣1 = length s⇣2` `transfer (kind a) s⇣1 = s⇣1'`
have "length s⇣1' = length (transfer (slice_kind S a) s⇣2)"
by(fastforce intro:length_transfer_kind_slice_kind)
with `pred (slice_kind S a) s⇣2` `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`hd ms⇣1 ∈ ⌊HRB_slice S⌋⇘CFG⇙` `hd ms⇣1 = sourcenode a`
`length ms⇣1 = length s⇣1` `length s⇣1 = length s⇣2` `valid_edge a'`
`ms⇣1' = (targetnode a)#(targetnode a')#tl ms⇣1` `a' ∈ get_return_edges a`
`∀m ∈ set (tl ms⇣2). return_node m`
have "S,slice_kind S \<turnstile> (ms⇣1,s⇣2) -a-> (ms⇣1',transfer (slice_kind S a) s⇣2)"
by(auto intro:observable_move.observable_move_call)
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)`
have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as@[a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)"
by(rule observable_moves_snoc)
from `∀m ∈ set ms⇣1. valid_node m` `ms⇣1' = (targetnode a)#(targetnode a')#tl ms⇣1`
`valid_edge a` `valid_edge a'`
have "∀m ∈ set ms⇣1'. valid_node m" by(cases ms⇣1) auto
from `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have cf2':"∃cf⇣2'. transfer (slice_kind S a) s⇣2 = cf⇣2'#s⇣2 ∧ snd cf⇣2' = r"
by(auto dest:slice_kind_Call_in_slice)
with `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)`
`length ms⇣1' = length s⇣1'` `msx = []` `length ms⇣1 = length ms⇣2`
`length ms⇣1 = length s⇣1`
have "∀i<length ms⇣1'. snd (s⇣1' ! i) = snd (transfer (slice_kind S a) s⇣2 ! i)"
by auto(case_tac i,auto)
have "∀V ∈ rv S (CFG_node (targetnode a')).
V ∈ rv S (CFG_node (sourcenode a))"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a'))"
then obtain as n' where "targetnode a' -as->⇣ι* parent_node n'"
and "n' ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ n'"
and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''" by(fastforce elim:rvE)
from `valid_edge a` `a' ∈ get_return_edges a`
obtain a'' where "valid_edge a''" and "sourcenode a'' = sourcenode a"
and "targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
by -(drule call_return_node_edge,auto simp:intra_kind_def)
with `targetnode a' -as->⇣ι* parent_node n'`
have "sourcenode a -a''#as->⇣ι* parent_node n'"
by(fastforce intro:Cons_path simp:intra_path_def)
from `sourcenode a'' = sourcenode a` `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "∀n''. valid_SDG_node n'' ∧ parent_node n'' = sourcenode a''
--> V ∉ Def⇘SDG⇙ n''"
by(fastforce dest:SDG_Def_parent_Def call_source_Def_empty)
with `∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as)
--> V ∉ Def⇘SDG⇙ n''`
have "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (a''#as))
--> V ∉ Def⇘SDG⇙ n''" by(fastforce simp:sourcenodes_def)
with `sourcenode a -a''#as->⇣ι* parent_node n'` `n' ∈ HRB_slice S`
`V ∈ Use⇘SDG⇙ n'`
show "V ∈ rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
qed
have "∀V ∈ rv S (CFG_node (targetnode a)).
(empty(ins [:=] params fs (fst cf⇣1))) V =
state_val (transfer (slice_kind S a) s⇣2) V"
proof
fix V assume "V ∈ rv S (CFG_node (targetnode a))"
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`(THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins`
have eq:"fst (hd (transfer (slice_kind S a) s⇣2)) =
empty(ins [:=] params (cspp (targetnode a) (HRB_slice S) fs) (fst cf⇣2))"
by(auto dest:slice_kind_Call_in_slice)
show "(empty(ins [:=] params fs (fst cf⇣1))) V =
state_val (transfer (slice_kind S a) s⇣2) V"
proof(cases "V ∈ set ins")
case True
then obtain i where "V = ins!i" and "i < length ins"
by(auto simp:in_set_conv_nth)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `(p,ins,outs) ∈ set procs`
`i < length ins`
have "valid_SDG_node (Formal_in (targetnode a,i))" by fastforce
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` have "get_proc(targetnode a) = p"
by(rule get_proc_call)
with `valid_SDG_node (Formal_in (targetnode a,i))`
`(p,ins,outs) ∈ set procs` `V = ins!i`
have "V ∈ Def⇘SDG⇙ (Formal_in (targetnode a,i))"
by(fastforce intro:Formal_in_SDG_Def)
from `V ∈ rv S (CFG_node (targetnode a))` obtain as' nx
where "targetnode a -as'->⇣ι* parent_node nx"
and "nx ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ nx"
and "∀n''. valid_SDG_node n'' ∧
parent_node n'' ∈ set (sourcenodes as') --> V ∉ Def⇘SDG⇙ n''"
by(fastforce elim:rvE)
with `valid_SDG_node (Formal_in (targetnode a,i))`
`V ∈ Def⇘SDG⇙ (Formal_in (targetnode a,i))`
have "targetnode a = parent_node nx"
apply(auto simp:intra_path_def sourcenodes_def)
apply(erule path.cases) apply fastforce
apply(erule_tac x="Formal_in (targetnode a,i)" in allE) by fastforce
with `V ∈ Use⇘SDG⇙ nx` have "V ∈ Use (targetnode a)"
by(fastforce intro:SDG_Use_parent_Use)
with `valid_edge a` have "V ∈ Use⇘SDG⇙ (CFG_node (targetnode a))"
by(auto intro!:CFG_Use_SDG_Use)
from `targetnode a = parent_node nx`[THEN sym] `valid_edge a`
have "parent_node (Formal_in (targetnode a,i)) -[]->⇣ι* parent_node nx"
by(fastforce intro:empty_path simp:intra_path_def)
with `V ∈ Def⇘SDG⇙ (Formal_in (targetnode a,i))`
`V ∈ Use⇘SDG⇙ (CFG_node (targetnode a))` `targetnode a = parent_node nx`
have "Formal_in (targetnode a,i) influences V in (CFG_node (targetnode a))"
by(fastforce simp:data_dependence_def sourcenodes_def)
hence ddep:"Formal_in (targetnode a,i) s-V->⇘dd⇙ (CFG_node (targetnode a))"
by(rule sum_SDG_ddep_edge)
from `targetnode a = parent_node nx` `nx ∈ HRB_slice S`
have "CFG_node (targetnode a) ∈ HRB_slice S"
by(fastforce dest:valid_SDG_node_in_slice_parent_node_in_slice)
hence "Formal_in (targetnode a,i) ∈ HRB_slice S"
proof(induct "CFG_node (targetnode a)" rule:HRB_slice_cases)
case (phase1 nx)
with ddep show ?case
by(fastforce intro:ddep_slice1 combine_SDG_slices.combSlice_refl
simp:HRB_slice_def)
next
case (phase2 nx n' n'' p)
from `CFG_node (targetnode a) ∈ sum_SDG_slice2 n'` ddep
have "Formal_in (targetnode a,i) ∈ sum_SDG_slice2 n'"
by(fastforce intro:ddep_slice2)
with `n'' s-p->⇘ret⇙ CFG_node (parent_node n')` `n' ∈ sum_SDG_slice1 nx`
`nx ∈ S`
show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node simp:HRB_slice_def)
qed
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have slice_kind:"slice_kind S a =
Q:r\<hookrightarrow>⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
by(rule slice_kind_Call_in_slice)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `(p,ins,outs) ∈ set procs`
have "length fs = length ins" by(rule CFG_call_edge_length)
from `Formal_in (targetnode a,i) ∈ HRB_slice S`
`length fs = length ins` `i < length ins`
have cspp:"(cspp (targetnode a) (HRB_slice S) fs)!i = fs!i"
by(fastforce intro:csppa_Formal_in_in_slice simp:cspp_def)
from `i < length ins` `length fs = length ins`
have "(params (cspp (targetnode a) (HRB_slice S) fs) (fst cf⇣2))!i =
((cspp (targetnode a) (HRB_slice S) fs)!i) (fst cf⇣2)"
by(fastforce intro:params_nth)
with cspp
have eq:"(params (cspp (targetnode a) (HRB_slice S) fs) (fst cf⇣2))!i =
(fs!i) (fst cf⇣2)" by simp
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `(p,ins,outs) ∈ set procs`
have "(THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins"
by(rule formal_in_THE)
with slice_kind
have "fst (hd (transfer (slice_kind S a) s⇣2)) =
empty(ins [:=] params (cspp (targetnode a) (HRB_slice S) fs) (fst cf⇣2))"
by simp
moreover
from `(p,ins,outs) ∈ set procs` have "distinct ins"
by(rule distinct_formal_ins)
ultimately have "state_val (transfer (slice_kind S a) s⇣2) V =
(params (cspp (targetnode a) (HRB_slice S) fs) (fst cf⇣2))!i"
using `V = ins!i` `i < length ins` `length fs = length ins`
by(fastforce intro:fun_upds_nth)
with eq
have 2:"state_val (transfer (slice_kind S a) s⇣2) V = (fs!i) (fst cf⇣2)"
by simp
from `V = ins!i` `i < length ins` `length fs = length ins`
`distinct ins`
have "empty(ins [:=] params fs (fst cf⇣1)) V = (params fs (fst cf⇣1))!i"
by(fastforce intro:fun_upds_nth)
with `i < length ins` `length fs = length ins`
have 1:"empty(ins [:=] params fs (fst cf⇣1)) V = (fs!i) (fst cf⇣1)"
by(fastforce intro:params_nth)
from `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V`
have rv:"∀V∈rv S (CFG_node (sourcenode a)). fst cf⇣1 V = fst cf⇣2 V"
by(erule_tac x="0" in allE) auto
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `(p,ins,outs) ∈ set procs`
`i < length ins` have "∀V∈(ParamUses (sourcenode a)!i).
V ∈ Use⇘SDG⇙ (Actual_in (sourcenode a,i))"
by(fastforce intro:Actual_in_SDG_Use)
with `valid_edge a` have "∀V∈(ParamUses (sourcenode a)!i).
V ∈ Use⇘SDG⇙ (CFG_node (sourcenode a))"
by(auto intro!:CFG_Use_SDG_Use dest:SDG_Use_parent_Use)
moreover
from `valid_edge a` have "parent_node (CFG_node (sourcenode a)) -[]->⇣ι*
parent_node (CFG_node (sourcenode a))"
by(fastforce intro:empty_path simp:intra_path_def)
ultimately
have "∀V∈(ParamUses (sourcenode a)!i). V ∈ rv S (CFG_node (sourcenode a))"
using `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `valid_edge a`
by(fastforce intro:rvI simp:SDG_to_CFG_set_def sourcenodes_def)
with rv have "∀V ∈ (ParamUses (sourcenode a))!i. fst cf⇣1 V = fst cf⇣2 V"
by fastforce
with `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `i < length ins`
`(p,ins,outs) ∈ set procs` `pred (kind a) s⇣1` `pred (kind a) s⇣2`
have "(params fs (fst cf⇣1))!i = (params fs (fst cf⇣2))!i"
by(fastforce dest!:CFG_call_edge_params)
moreover
from `i < length ins` `length fs = length ins`
have "(params fs (fst cf⇣1))!i = (fs!i) (fst cf⇣1)"
and "(params fs (fst cf⇣2))!i = (fs!i) (fst cf⇣2)"
by(auto intro:params_nth)
ultimately show ?thesis using 1 2 by simp
next
case False
with eq show ?thesis by(fastforce simp:fun_upds_notin)
qed
qed
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` cf2' `tl ms⇣2 = tl ms⇣1`
`length ms⇣2 = length s⇣2` `length ms⇣1 = length s⇣1` `length s⇣1 = length s⇣2`
`ms⇣1' = (targetnode a)#(targetnode a')#tl ms⇣1`
`∀V ∈ rv S (CFG_node (targetnode a')). V ∈ rv S (CFG_node (sourcenode a))`
have "∀i<length ms⇣1'. ∀V∈rv S (CFG_node ((targetnode a # tl ms⇣1')!i)).
(fst (s⇣1'!(length [] + i))) V = (fst (transfer (slice_kind S a) s⇣2!i)) V"
apply clarsimp apply(case_tac i) apply auto
apply(erule_tac x="nat" in allE)
apply(case_tac nat) apply auto done
with `∀m ∈ set ms⇣2. valid_node m` `∀m ∈ set ms⇣1'. valid_node m`
`length ms⇣2 = length s⇣2` `length s⇣1' = length (transfer (slice_kind S a) s⇣2)`
`length ms⇣1' = length s⇣1'` `ms⇣1' = (targetnode a)#(targetnode a')#tl ms⇣1`
`get_proc mx = get_proc (hd ms⇣2)` `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`return_node (targetnode a')` `∀m ∈ set (tl ms⇣1). return_node m`
`call_of_return_node (targetnode a') (sourcenode a)`
`∀i<length ms⇣1'. snd (s⇣1' ! i) = snd (transfer (slice_kind S a) s⇣2 ! i)`
have "((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S a) s⇣2)) ∈ WS S"
by(fastforce intro!:WSI)
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as@[a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)`
show ?case by blast
next
case (observable_move_return a s⇣1 s⇣1' Q p f' ms⇣1 S ms⇣1')
from `s⇣1 ≠ []` `s⇣2 ≠ []` obtain cf⇣1 cfs⇣1 cf⇣2 cfs⇣2 where [simp]:"s⇣1 = cf⇣1#cfs⇣1"
and [simp]:"s⇣2 = cf⇣2#cfs⇣2" by(cases s⇣1,auto,cases s⇣2,fastforce+)
from `length ms⇣1 = length s⇣1` `s⇣1 ≠ []` have [simp]:"ms⇣1 ≠ []" by(cases ms⇣1) auto
from `length ms⇣2 = length s⇣2` `s⇣2 ≠ []` have [simp]:"ms⇣2 ≠ []" by(cases ms⇣2) auto
from `∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`hd ms⇣1 = sourcenode a` `ms⇣1 = msx@mx#tl ms⇣2`
`msx ≠ [] --> (∃mx'. call_of_return_node mx mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)`
have [simp]:"mx = sourcenode a" "msx = []" and [simp]:"tl ms⇣2 = tl ms⇣1"
by(cases msx,auto)+
hence "length ms⇣1 = length ms⇣2" by(cases ms⇣2) auto
with `length ms⇣1 = length s⇣1` `length ms⇣2 = length s⇣2`
have "length s⇣1 = length s⇣2" by simp
have "∃as. S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)"
proof(cases "obs_intra (hd ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
from `valid_edge a` `hd ms⇣1 = sourcenode a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
have "method_exit (hd ms⇣1)" by(fastforce simp:method_exit_def)
from `∀m∈set ms⇣2. valid_node m` have "valid_node (hd ms⇣2)" by(cases ms⇣2) auto
then obtain asx where "hd ms⇣2 -asx->⇣\<surd>* (_Exit_)" by(fastforce dest!:Exit_path)
then obtain as pex where "hd ms⇣2 -as->⇣ι* pex" and "method_exit pex"
by(fastforce elim:valid_Exit_path_intra_path)
from `hd ms⇣2 -as->⇣ι* pex` have "get_proc (hd ms⇣2) = get_proc pex"
by(rule intra_path_get_procs)
with `get_proc mx = get_proc (hd ms⇣2)`
have "get_proc mx = get_proc pex" by simp
with `method_exit (hd ms⇣1)` ` hd ms⇣1 = sourcenode a` `method_exit pex`
have [simp]:"pex = hd ms⇣1" by(fastforce intro:method_exit_unique)
from `obs_intra (hd ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙ = {}` `method_exit pex`
`get_proc (hd ms⇣2) = get_proc pex` `valid_node (hd ms⇣2)`
`length ms⇣2 = length s⇣2` `∀m∈set (tl ms⇣1). return_node m` `ms⇣2 ≠ []`
obtain as'
where "S,slice_kind S \<turnstile> (hd ms⇣2#tl ms⇣2,s⇣2) =as'=>⇣τ (hd ms⇣1#tl ms⇣1,s⇣2)"
by(fastforce elim!:silent_moves_intra_path_no_obs[of _ _ _ s⇣2 "tl ms⇣2"]
dest:hd_Cons_tl)
with `ms⇣2 ≠ []` have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as'=>⇣τ (ms⇣1,s⇣2)"
by(fastforce dest!:hd_Cons_tl)
thus ?thesis by blast
next
case False
then obtain x where "x ∈ obs_intra (hd ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
hence "obs_intra (hd ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙ = {x}"
by(rule obs_intra_singleton_element)
with `∀m ∈ set (tl ms⇣2). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "x#tl ms⇣1 ∈ obs ([]@hd ms⇣2#tl ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obsI)
with `ms⇣2 ≠ []` have "x#tl ms⇣1 ∈ obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:hd_Cons_tl simp del:obs.simps)
with `obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙ = obs ms⇣2 ⌊HRB_slice S⌋⇘CFG⇙`
have "x#tl ms⇣1 ∈ obs ms⇣1 ⌊HRB_slice S⌋⇘CFG⇙" by simp
from this `∀m∈set (tl ms⇣1). return_node m`
have "x ∈ obs_intra (hd ms⇣1) ⌊HRB_slice S⌋⇘CFG⇙"
proof(rule obsE)
fix nsx n nsx' n'
assume "ms⇣1 = nsx @ n # nsx'" and "x # tl ms⇣1 = n' # nsx'"
and "n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
from `ms⇣1 = nsx @ n # nsx'` `x # tl ms⇣1 = n' # nsx'` `tl ms⇣2 = tl ms⇣1`
have [simp]:"nsx = []" by(cases nsx) auto
with `ms⇣1 = nsx @ n # nsx'` have [simp]:"n = hd ms⇣1" by simp
from `x # tl ms⇣1 = n' # nsx'` have [simp]:"n' = x" by simp
with `n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙` show ?thesis by simp
qed
{ fix m as assume "hd ms⇣1 -as->⇣ι* m"
hence "hd ms⇣1 -as->* m" and "∀a ∈ set as. intra_kind (kind a)"
by(simp_all add:intra_path_def)
hence "m = hd ms⇣1"
proof(induct "hd ms⇣1" as m rule:path.induct)
case (Cons_path m'' as' m' a')
from `∀a∈set (a' # as'). intra_kind (kind a)`
have "intra_kind (kind a')" by simp
with `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `valid_edge a'`
`sourcenode a' = hd ms⇣1` `hd ms⇣1 = sourcenode a`
have False by(fastforce dest:return_edges_only simp:intra_kind_def)
thus ?case by simp
qed simp }
with `x ∈ obs_intra (hd ms⇣1) ⌊HRB_slice S⌋⇘CFG⇙`
have "x = hd ms⇣1" by(fastforce elim:obs_intraE)
with `x ∈ obs_intra (hd ms⇣2) ⌊HRB_slice S⌋⇘CFG⇙` `length ms⇣2 = length s⇣2`
`∀m∈set (tl ms⇣1). return_node m` `ms⇣2 ≠ []`
obtain as where "S,slice_kind S \<turnstile> (hd ms⇣2#tl ms⇣2,s⇣2) =as=>⇣τ (hd ms⇣1#tl ms⇣1,s⇣2)"
by(fastforce elim!:silent_moves_intra_path_obs[of _ _ _ s⇣2 "tl ms⇣2"]
dest:hd_Cons_tl)
with `ms⇣2 ≠ []` have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)"
by(fastforce dest!:hd_Cons_tl)
thus ?thesis by blast
qed
then obtain as where "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)" by blast
from `ms⇣1' = tl ms⇣1` `length s⇣1 = Suc(length s⇣1')`
`length ms⇣1 = length s⇣1` have "length ms⇣1' = length s⇣1'" by simp
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` obtain a'' Q' r' fs' where "valid_edge a''"
and "kind a'' = Q':r'\<hookrightarrow>⇘p⇙fs'" and "a ∈ get_return_edges a''"
by -(drule return_needs_call,auto)
then obtain ins outs where "(p,ins,outs) ∈ set procs"
by(fastforce dest!:callee_in_procs)
from `length s⇣1 = Suc(length s⇣1')` `s⇣1' ≠ []`
obtain cfx cfsx where [simp]:"cfs⇣1 = cfx#cfsx" by(cases cfs⇣1) auto
with `length s⇣1 = length s⇣2` obtain cfx' cfsx' where [simp]:"cfs⇣2 = cfx'#cfsx'"
by(cases cfs⇣2) auto
from `length ms⇣1 = length s⇣1` have "tl ms⇣1 = []@hd(tl ms⇣1)#tl(tl ms⇣1)"
by(auto simp:length_Suc_conv)
from `kind a = Q\<hookleftarrow>⇘p⇙f'` `transfer (kind a) s⇣1 = s⇣1'`
have "s⇣1' = (f' (fst cf⇣1) (fst cfx),snd cfx)#cfsx" by simp
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `(p,ins,outs) ∈ set procs`
have "f' (fst cf⇣1) (fst cfx) =
(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs)"
by(rule CFG_return_edge_fun)
with `s⇣1' = (f' (fst cf⇣1) (fst cfx),snd cfx)#cfsx`
have [simp]:"s⇣1' =
((fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs),snd cfx)#cfsx"
by simp
have "pred (slice_kind S a) s⇣2"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from `valid_edge a` have "valid_node (sourcenode a)" by simp
hence "sourcenode a -[]->⇣ι* sourcenode a"
by(fastforce intro:empty_path simp:intra_path_def)
with `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "∀V. V ∈ Use⇘SDG⇙ (CFG_node (sourcenode a))
--> V ∈ rv S (CFG_node (sourcenode a))"
by auto(rule rvI,auto simp:SDG_to_CFG_set_def sourcenodes_def)
with `valid_node (sourcenode a)`
have "∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))"
by(fastforce intro:CFG_Use_SDG_Use)
from `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` `length ms⇣2 = length s⇣2`
have "∀V∈rv S (CFG_node mx). (fst (s⇣1 ! length msx)) V = state_val s⇣2 V"
by(cases ms⇣2) auto
with `∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node (sourcenode a))`
have "∀V ∈ Use (sourcenode a). fst cf⇣1 V = fst cf⇣2 V" by fastforce
moreover
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)`
have "snd (hd s⇣1) = snd (hd s⇣2)" by(erule_tac x="0" in allE) auto
ultimately have "pred (kind a) s⇣2"
using `valid_edge a` `pred (kind a) s⇣1` `length s⇣1 = length s⇣2`
by(fastforce intro:CFG_edge_Uses_pred_equal)
with `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `(p,ins,outs) ∈ set procs`
`sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙`
show ?thesis by(fastforce dest:slice_kind_Return_in_slice)
next
case False
with `kind a = Q\<hookleftarrow>⇘p⇙f'` have "slice_kind S a = (λcf. True)\<hookleftarrow>⇘p⇙(λcf cf'. cf')"
by -(rule slice_kind_Return)
thus ?thesis by simp
qed
from `valid_edge a` `length s⇣1 = length s⇣2` `transfer (kind a) s⇣1 = s⇣1'`
have "length s⇣1' = length (transfer (slice_kind S a) s⇣2)"
by(fastforce intro:length_transfer_kind_slice_kind)
with `pred (slice_kind S a) s⇣2` `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
`∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`hd ms⇣1 = sourcenode a`
`length ms⇣1 = length s⇣1` `length s⇣1 = length s⇣2`
`ms⇣1' = tl ms⇣1` `hd(tl ms⇣1) = targetnode a` `∀m ∈ set (tl ms⇣1). return_node m`
have "S,slice_kind S \<turnstile> (ms⇣1,s⇣2) -a-> (ms⇣1',transfer (slice_kind S a) s⇣2)"
by(fastforce intro!:observable_move.observable_move_return)
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as=>⇣τ (ms⇣1,s⇣2)`
have "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as@[a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)"
by(rule observable_moves_snoc)
from `∀m ∈ set ms⇣1. valid_node m` `ms⇣1' = tl ms⇣1`
have "∀m ∈ set ms⇣1'. valid_node m" by(cases ms⇣1) auto
from `length ms⇣1' = length s⇣1'` have "ms⇣1' = []@hd ms⇣1'#tl ms⇣1'"
by(cases ms⇣1') auto
from `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)`
`length ms⇣1 = length ms⇣2` `length ms⇣1 = length s⇣1`
have "snd cfx = snd cfx'" by(erule_tac x="1" in allE) auto
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `(p,ins,outs) ∈ set procs`
have cf2':"∃cf⇣2'. transfer (slice_kind S a) s⇣2 = cf⇣2'#cfsx' ∧ snd cf⇣2' = snd cfx'"
by(cases cfx',cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙",
auto dest:slice_kind_Return slice_kind_Return_in_slice)
with `∀i<length ms⇣2. snd (s⇣1 ! (length msx + i)) = snd (s⇣2 ! i)`
`length ms⇣1' = length s⇣1'` `msx = []` `length ms⇣1 = length ms⇣2`
`length ms⇣1 = length s⇣1` `snd cfx = snd cfx'`
have "∀i<length ms⇣1'. snd (s⇣1' ! i) = snd (transfer (slice_kind S a) s⇣2 ! i)"
apply auto apply(case_tac i) apply auto
by(erule_tac x="Suc(Suc nat)" in allE) auto
from `∀m ∈ set (tl ms⇣1). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
have "∀m ∈ set (tl (tl ms⇣1)).
∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(cases "tl ms⇣1") auto
from `∀m ∈ set (tl ms⇣1). return_node m`
have "∀m ∈ set (tl (tl ms⇣1)). return_node m" by(cases "tl ms⇣1") auto
have "∀V∈rv S (CFG_node (hd (tl ms⇣1))).
(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs) V =
state_val (transfer (slice_kind S a) s⇣2) V"
proof
fix V assume "V∈rv S (CFG_node (hd (tl ms⇣1)))"
with `hd(tl ms⇣1) = targetnode a` have "V∈rv S (CFG_node (targetnode a))"
by simp
show "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs) V =
state_val (transfer (slice_kind S a) s⇣2) V"
proof(cases "V ∈ set (ParamDefs (targetnode a))")
case True
then obtain i where "V = (ParamDefs (targetnode a))!i"
and "i < length(ParamDefs (targetnode a))"
by(auto simp:in_set_conv_nth)
moreover
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `(p,ins,outs) ∈ set procs`
have length:"length(ParamDefs (targetnode a)) = length outs"
by(fastforce intro:ParamDefs_return_target_length)
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `(p,ins,outs) ∈ set procs`
`i < length(ParamDefs (targetnode a))`
`length(ParamDefs (targetnode a)) = length outs`
have "valid_SDG_node (Actual_out(targetnode a,i))" by fastforce
with `V = (ParamDefs (targetnode a))!i`
have "V ∈ Def⇘SDG⇙ (Actual_out(targetnode a,i))"
by(fastforce intro:Actual_out_SDG_Def)
from `V ∈ rv S (CFG_node (targetnode a))` obtain as' nx
where "targetnode a -as'->⇣ι* parent_node nx"
and "nx ∈ HRB_slice S" and "V ∈ Use⇘SDG⇙ nx"
and "∀n''. valid_SDG_node n'' ∧
parent_node n'' ∈ set (sourcenodes as') --> V ∉ Def⇘SDG⇙ n''"
by(fastforce elim:rvE)
with `valid_SDG_node (Actual_out(targetnode a,i))`
`V ∈ Def⇘SDG⇙ (Actual_out(targetnode a,i))`
have "targetnode a = parent_node nx"
apply(auto simp:intra_path_def sourcenodes_def)
apply(erule path.cases) apply fastforce
apply(erule_tac x="(Actual_out(targetnode a,i))" in allE) by fastforce
with `V ∈ Use⇘SDG⇙ nx` have "V ∈ Use (targetnode a)"
by(fastforce intro:SDG_Use_parent_Use)
with `valid_edge a` have "V ∈ Use⇘SDG⇙ (CFG_node (targetnode a))"
by(auto intro!:CFG_Use_SDG_Use)
from `targetnode a = parent_node nx`[THEN sym] `valid_edge a`
have "parent_node (Actual_out(targetnode a,i)) -[]->⇣ι* parent_node nx"
by(fastforce intro:empty_path simp:intra_path_def)
with `V ∈ Def⇘SDG⇙ (Actual_out(targetnode a,i))`
`V ∈ Use⇘SDG⇙ (CFG_node (targetnode a))` `targetnode a = parent_node nx`
have "Actual_out(targetnode a,i) influences V in (CFG_node (targetnode a))"
by(fastforce simp:data_dependence_def sourcenodes_def)
hence ddep:"Actual_out(targetnode a,i) s-V->⇘dd⇙ (CFG_node (targetnode a))"
by(rule sum_SDG_ddep_edge)
from `targetnode a = parent_node nx` `nx ∈ HRB_slice S`
have "CFG_node (targetnode a) ∈ HRB_slice S"
by(fastforce dest:valid_SDG_node_in_slice_parent_node_in_slice)
hence "Actual_out(targetnode a,i) ∈ HRB_slice S"
proof(induct "CFG_node (targetnode a)" rule:HRB_slice_cases)
case (phase1 nx')
with ddep show ?case
by(fastforce intro: ddep_slice1 combine_SDG_slices.combSlice_refl
simp:HRB_slice_def)
next
case (phase2 nx' n' n'' p)
from `CFG_node (targetnode a) ∈ sum_SDG_slice2 n'` ddep
have "Actual_out(targetnode a,i) ∈ sum_SDG_slice2 n'"
by(fastforce intro:ddep_slice2)
with `n'' s-p->⇘ret⇙ CFG_node (parent_node n')` `n' ∈ sum_SDG_slice1 nx'`
`nx' ∈ S`
show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
simp:HRB_slice_def)
qed
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `valid_edge a''`
`kind a'' = Q':r'\<hookrightarrow>⇘p⇙fs'` `a ∈ get_return_edges a''`
`CFG_node (targetnode a) ∈ HRB_slice S`
have "CFG_node (sourcenode a) ∈ HRB_slice S"
by(rule call_return_nodes_in_slice)
hence "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(simp add:SDG_to_CFG_set_def)
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
`(p,ins,outs) ∈ set procs`
have slice_kind:"slice_kind S a =
Q\<hookleftarrow>⇘p⇙(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
by(rule slice_kind_Return_in_slice)
from `Actual_out(targetnode a,i) ∈ HRB_slice S`
`i < length(ParamDefs (targetnode a))` `valid_edge a`
`V = (ParamDefs (targetnode a))!i` length
have 2:"rspp (targetnode a) (HRB_slice S) outs (fst cfx') (fst cf⇣2) V =
(fst cf⇣2)(outs!i)"
by(fastforce intro:rspp_Actual_out_in_slice)
from `i < length(ParamDefs (targetnode a))` length `valid_edge a`
have "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs)
((ParamDefs (targetnode a))!i) = (map (fst cf⇣1) outs)!i"
by(fastforce intro:fun_upds_nth distinct_ParamDefs)
with `V = (ParamDefs (targetnode a))!i`
`i < length(ParamDefs (targetnode a))` length
have 1:"(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs) V =
(fst cf⇣1)(outs!i)"
by simp
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `(p,ins,outs) ∈ set procs`
`i < length(ParamDefs (targetnode a))` length
have po:"Formal_out(sourcenode a,i) s-p:outs!i->⇘out⇙ Actual_out(targetnode a,i)"
by(fastforce intro:sum_SDG_param_out_edge)
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
have "CFG_node (sourcenode a) s-p->⇘ret⇙ CFG_node (targetnode a)"
by(fastforce intro:sum_SDG_return_edge)
from `Actual_out(targetnode a,i) ∈ HRB_slice S`
have "Formal_out(sourcenode a,i) ∈ HRB_slice S"
proof(induct "Actual_out(targetnode a,i)" rule:HRB_slice_cases)
case (phase1 nx')
let ?AO = "Actual_out(targetnode a,i)"
from `valid_SDG_node ?AO` have "?AO ∈ sum_SDG_slice2 ?AO"
by(rule refl_slice2)
with po have "Formal_out(sourcenode a,i) ∈ sum_SDG_slice2 ?AO"
by(rule param_out_slice2)
with `CFG_node (sourcenode a) s-p->⇘ret⇙ CFG_node (targetnode a)`
`Actual_out (targetnode a, i) ∈ sum_SDG_slice1 nx'` `nx' ∈ S`
show ?case
by(fastforce intro:combSlice_Return_parent_node simp:HRB_slice_def)
next
case (phase2 nx' n' n'' p)
from `Actual_out (targetnode a, i) ∈ sum_SDG_slice2 n'` po
have "Formal_out(sourcenode a,i) ∈ sum_SDG_slice2 n'"
by(fastforce intro:param_out_slice2)
with `n' ∈ sum_SDG_slice1 nx'` `n'' s-p->⇘ret⇙ CFG_node (parent_node n')`
`nx' ∈ S`
show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
simp:HRB_slice_def)
qed
with `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'` `(p,ins,outs) ∈ set procs`
`i < length(ParamDefs (targetnode a))` length
have "outs!i ∈ Use⇘SDG⇙ Formal_out(sourcenode a,i)"
by(fastforce intro!:Formal_out_SDG_Use get_proc_return)
with `valid_edge a` have "outs!i ∈ Use⇘SDG⇙ (CFG_node (sourcenode a))"
by(auto intro!:CFG_Use_SDG_Use dest:SDG_Use_parent_Use)
moreover
from `valid_edge a` have "parent_node (CFG_node (sourcenode a)) -[]->⇣ι*
parent_node (CFG_node (sourcenode a))"
by(fastforce intro:empty_path simp:intra_path_def)
ultimately have "outs!i ∈ rv S (CFG_node (sourcenode a))"
using `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `valid_edge a`
by(fastforce intro:rvI simp:SDG_to_CFG_set_def sourcenodes_def)
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V`
have "(fst cf⇣1)(outs!i) = (fst cf⇣2)(outs!i)"
by auto(erule_tac x="0" in allE,auto)
with 1 2 slice_kind show ?thesis by simp
next
case False
with `transfer (kind a) s⇣1 = s⇣1'`
have "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs) =
(fst (hd cfs⇣1))(ParamDefs (targetnode a) [:=] map (fst cf⇣1) outs)"
by(cases cfs⇣1,auto intro:CFG_return_edge_fun)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from `sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙` `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f'`
`(p,ins,outs) ∈ set procs`
have "slice_kind S a =
Q\<hookleftarrow>⇘p⇙(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
by(rule slice_kind_Return_in_slice)
with `length s⇣1' = length (transfer (slice_kind S a) s⇣2)`
`length s⇣1 = length s⇣2`
have "state_val (transfer (slice_kind S a) s⇣2) V =
rspp (targetnode a) (HRB_slice S) outs (fst cfx') (fst cf⇣2) V"
by simp
with `V ∉ set (ParamDefs (targetnode a))`
have "state_val (transfer (slice_kind S a) s⇣2) V = state_val cfs⇣2 V"
by(fastforce simp:rspp_def map_merge_def)
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V`
`hd(tl ms⇣1) = targetnode a`
`length ms⇣1 = length s⇣1` `length s⇣1 = length s⇣2`[THEN sym] False
`tl ms⇣2 = tl ms⇣1` `length ms⇣2 = length s⇣2`
`V∈rv S (CFG_node (targetnode a))`
show ?thesis by(fastforce simp:length_Suc_conv fun_upds_notin)
next
case False
from `sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙` `kind a = Q\<hookleftarrow>⇘p⇙f'`
have "slice_kind S a = (λcf. True)\<hookleftarrow>⇘p⇙(λcf cf'. cf')"
by(rule slice_kind_Return)
from `length ms⇣2 = length s⇣2` have "1 < length ms⇣2" by simp
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V`
`V∈rv S (CFG_node (hd (tl ms⇣1)))`
`ms⇣1' = tl ms⇣1` `ms⇣1' = []@hd ms⇣1'#tl ms⇣1'`
have "fst cfx V = fst cfx' V" apply auto
apply(erule_tac x="1" in allE)
by(cases "tl ms⇣1") auto
with `∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V`
`hd(tl ms⇣1) = targetnode a`
`length ms⇣1 = length s⇣1` `length s⇣1 = length s⇣2`[THEN sym] False
`tl ms⇣2 = tl ms⇣1` `length ms⇣2 = length s⇣2`
`V∈rv S (CFG_node (targetnode a))`
`V ∉ set (ParamDefs (targetnode a))`
`slice_kind S a = (λcf. True)\<hookleftarrow>⇘p⇙(λcf cf'. cf')`
show ?thesis by(auto simp:fun_upds_notin)
qed
qed
qed
with `hd(tl ms⇣1) = targetnode a` `tl ms⇣2 = tl ms⇣1` `ms⇣1' = tl ms⇣1`
`∀i < length ms⇣2. ∀V ∈ rv S (CFG_node ((mx#tl ms⇣2)!i)).
(fst (s⇣1!(length msx + i))) V = (fst (s⇣2!i)) V` `length ms⇣1' = length s⇣1'`
`length ms⇣1 = length s⇣1` `length ms⇣2 = length s⇣2` `length s⇣1 = length s⇣2` cf2'
have "∀i<length ms⇣1'. ∀V∈rv S (CFG_node ((hd (tl ms⇣1) # tl ms⇣1')!i)).
(fst (s⇣1'!(length [] + i))) V = (fst (transfer (slice_kind S a) s⇣2!i)) V"
apply(case_tac "tl ms⇣1") apply auto
apply(cases ms⇣2) apply auto
apply(case_tac i) apply auto
by(erule_tac x="Suc(Suc nat)" in allE,auto)
with `∀m ∈ set ms⇣2. valid_node m` `∀m ∈ set ms⇣1'. valid_node m`
`length ms⇣2 = length s⇣2` `length s⇣1' = length (transfer (slice_kind S a) s⇣2)`
`length ms⇣1' = length s⇣1'` `ms⇣1' = tl ms⇣1` `ms⇣1' = []@hd ms⇣1'#tl ms⇣1'`
`tl ms⇣1 = []@hd(tl ms⇣1)#tl(tl ms⇣1)`
`get_proc mx = get_proc (hd ms⇣2)`
`∀m ∈ set (tl (tl ms⇣1)). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙`
`∀m ∈ set (tl (tl ms⇣1)). return_node m`
`∀i<length ms⇣1'. snd (s⇣1' ! i) = snd (transfer (slice_kind S a) s⇣2 ! i)`
have "((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S a) s⇣2)) ∈ WS S"
by(auto intro!:WSI)
with `S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as@[a]=> (ms⇣1',transfer (slice_kind S a) s⇣2)`
show ?case by blast
qed
qed
subsection {* The weak simulation *}
definition is_weak_sim ::
"(('node list × (('var \<rightharpoonup> 'val) × 'ret) list) ×
('node list × (('var \<rightharpoonup> 'val) × 'ret) list)) set => 'node SDG_node set => bool"
where "is_weak_sim R S ≡
∀ms⇣1 s⇣1 ms⇣2 s⇣2 ms⇣1' s⇣1' as.
((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ R ∧ S,kind \<turnstile> (ms⇣1,s⇣1) =as=> (ms⇣1',s⇣1') ∧ s⇣1' ≠ []
--> (∃ms⇣2' s⇣2' as'. ((ms⇣1',s⇣1'),(ms⇣2',s⇣2')) ∈ R ∧
S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as'=> (ms⇣2',s⇣2'))"
lemma WS_weak_sim:
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 "s⇣1' ≠ []"
obtains as' where "((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S (last as)) s⇣2)) ∈ WS S"
and "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as'@[last as]=>
(ms⇣1',transfer (slice_kind S (last as)) s⇣2)"
proof(atomize_elim)
from `S,kind \<turnstile> (ms⇣1,s⇣1) =as=> (ms⇣1',s⇣1')` obtain ms' s' as' a'
where "S,kind \<turnstile> (ms⇣1,s⇣1) =as'=>⇣τ (ms',s')"
and "S,kind \<turnstile> (ms',s') -a'-> (ms⇣1',s⇣1')" and "as = as'@[a']"
by(fastforce elim:observable_moves.cases)
from `S,kind \<turnstile> (ms',s') -a'-> (ms⇣1',s⇣1')`
have "∀m ∈ set (tl ms'). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
and "∀n ∈ set (tl ms'). return_node n" and "ms' ≠ []"
by(auto elim:observable_move.cases simp:call_of_return_node_def)
from `S,kind \<turnstile> (ms⇣1,s⇣1) =as'=>⇣τ (ms',s')` `((ms⇣1,s⇣1),(ms⇣2,s⇣2)) ∈ WS S`
have "((ms',s'),(ms⇣2,s⇣2)) ∈ WS S" by(rule WS_silent_moves)
with `S,kind \<turnstile> (ms',s') -a'-> (ms⇣1',s⇣1')` `s⇣1' ≠ []`
obtain as'' where "((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S a') s⇣2)) ∈ WS S"
and "S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as''@[a']=>
(ms⇣1',transfer (slice_kind S a') s⇣2)"
by(fastforce elim:WS_observable_move)
with `((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S a') s⇣2)) ∈ WS S` `as = as'@[a']`
show "∃as'. ((ms⇣1',s⇣1'),(ms⇣1',transfer (slice_kind S (last as)) s⇣2)) ∈ WS S ∧
S,slice_kind S \<turnstile> (ms⇣2,s⇣2) =as'@[last as]=>
(ms⇣1',transfer (slice_kind S (last as)) s⇣2)"
by fastforce
qed
text {* The following lemma states the correctness of static intraprocedural slicing:\\
the simulation @{text "WS S"} is a desired weak simulation *}
theorem WS_is_weak_sim:"is_weak_sim (WS S) S"
by(fastforce elim:WS_weak_sim simp:is_weak_sim_def)
end
end