Theory WeakSimulation
section ‹The weak simulation›
theory WeakSimulation imports Slice begin
context SDG begin
lemma call_node_notin_slice_return_node_neither:
assumes "call_of_return_node n n'" and "n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
shows "n ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof -
from ‹call_of_return_node n n'› obtain a a' where "return_node n"
and "valid_edge a" and "n' = sourcenode a"
and "valid_edge a'" and "a' ∈ get_return_edges a"
and "n = targetnode a'" by(fastforce simp:call_of_return_node_def)
from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q p r fs
where "kind a = Q:r↪⇘p⇙fs" by(fastforce dest!:only_call_get_return_edges)
with ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
by(fastforce dest!:call_return_edges)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
have "CFG_node (sourcenode a) s-p→⇘sum⇙ CFG_node (targetnode a')"
by(fastforce intro:sum_SDG_call_summary_edge)
show ?thesis
proof
assume "n ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹n = targetnode a'› have "CFG_node (targetnode a') ∈ HRB_slice S"
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→⇩√* (_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 ⇀ 'val) × 'ret) list ⇒ 'edge ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
(‹_,_ ⊢ '(_,_') -_→⇩τ '(_,_')› [51,50,0,0,50,0,0] 51)
where silent_move_intra:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
length s' = length s; length ms = length s;
hd ms = sourcenode a; ms' = (targetnode a)#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"
| silent_move_call:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘p⇙fs;
valid_edge a'; a' ∈ get_return_edges a;
(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
length ms = length s; length s' = Suc(length s);
hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"
| silent_move_return:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q↩⇘p⇙f';
∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙;
∀m ∈ set (tl ms). return_node m; length ms = length s; length s = Suc(length s');
s' ≠ []; hd ms = sourcenode a; hd(tl ms) = targetnode a; ms' = tl ms⟧
⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"
lemma silent_move_valid_nodes:
"⟦S,f ⊢ (ms,s) -a→⇩τ (ms',s'); ∀m ∈ set ms'. valid_node m⟧
⟹ ∀m ∈ set ms. valid_node m"
by(induct rule:silent_move.induct)(case_tac ms,auto)+
lemma silent_move_return_node:
"S,f ⊢ (ms,s) -a→⇩τ (ms',s') ⟹ ∀m ∈ set (tl ms'). return_node m"
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms n⇩c ms')
thus ?case by simp
next
case (silent_move_call f a s s' Q r p fs a' ms n⇩c ms')
from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "return_node (targetnode a')" by(fastforce simp:return_node_def)
with ‹∀m∈set (tl ms). return_node m› ‹ms' = targetnode a # targetnode a' # tl ms›
show ?case by simp
next
case (silent_move_return f a s s' Q p f' ms n⇩c ms')
thus ?case by(cases "tl ms") auto
qed
lemma silent_move_equal_length:
assumes "S,f ⊢ (ms,s) -a→⇩τ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms n⇩c ms')
from ‹pred (f a) s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from ‹length ms = length s› ‹ms' = targetnode a # tl ms›
‹length s' = length s› show ?case by simp
next
case (silent_move_call f a s s' Q r p fs a' ms n⇩c ms')
from ‹pred (f a) s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from ‹length ms = length s› ‹length s' = Suc (length s)›
‹ms' = targetnode a # targetnode a' # tl ms› show ?case by simp
next
case (silent_move_return f a s s' Q p f' ms n⇩c ms')
from ‹length ms = length s› ‹length s = Suc (length s')› ‹ms' = tl ms› ‹s' ≠ []›
show ?case by simp
qed
thus "length ms = length s" and "length ms' = length s'" by simp_all
qed
lemma silent_move_obs_slice:
"⟦S,kind ⊢ (ms,s) -a→⇩τ (ms',s'); msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙;
∀n ∈ set (tl ms'). return_node n⟧
⟹ msx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct S f≡"kind" ms s a ms' s' rule:silent_move.induct)
case (silent_move_intra a s s' ms n⇩c ms')
from ‹pred (kind a) s› ‹length ms = length s› have "ms ≠ []"
by(cases s) auto
with silent_move_intra show ?case by -(rule intra_edge_obs_slice)
next
case (silent_move_call a s s' Q r p fs a' ms S ms')
note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "return_node (targetnode a')" by(fastforce simp:return_node_def)
with ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹valid_edge a'›
have "call_of_return_node (targetnode a') (sourcenode a)"
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 ⊢ (ms,s) -a→⇩τ (ms',s')" and "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}"
shows "obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(rule ccontr)
assume "obs ms ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
then obtain xs where "xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "∀m ∈ set (tl ms). return_node m"
by(fastforce elim!:silent_move.cases simp:call_of_return_node_def)
with ‹xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙›
obtain msx m msx' m' where assms:"ms = msx@m#msx'" "xs = m'#msx'"
"m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
"∀mx ∈ set msx'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
"∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
⟶ (∃x'' ∈ set (xs'@[m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')› ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› assms
show False
proof(induct rule:silent_move.induct)
case (silent_move_intra f a s s' ms S ms')
note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
show False
proof(cases msx)
case Nil
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have [simp]:"m = sourcenode a"
and "tl ms = msx'" by simp_all
from Nil ‹ms' = targetnode a # tl ms› ‹ms = msx @ m # msx'›
have "ms' = msx @ targetnode a # msx'" by simp
from msx' disj ‹tl ms = msx'› ‹hd ms = sourcenode a›
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
with ‹valid_edge a› ‹intra_kind (kind a)›
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by(rule edge_obs_intra_slice_eq)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by simp
from msx Nil have "∀xs x xs'. msx = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [targetnode a]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" by simp
with ‹m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙› msx'
‹ms' = msx @ targetnode a # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
next
case (Cons y ys)
with ‹ms = msx @ m # msx'› ‹ms' = targetnode a # tl ms› ‹hd ms = sourcenode a›
have "ms' = targetnode a # ys @ m # msx'" and "y = sourcenode a"
and "tl ms = ys @ m # msx'" by simp_all
{ fix x assume "x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
from this True
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
thus ?thesis by simp
next
case False
from ‹valid_edge a› ‹intra_kind (kind a)› False
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with ‹x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙› show ?thesis
by fastforce
qed }
with msx Cons ‹y = sourcenode a›
have "∀xs x xs'. targetnode a # ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
apply clarsimp apply(case_tac xs) apply auto
apply(erule_tac x="[]" in allE) apply clarsimp
apply(erule_tac x="sourcenode a # list" in allE) apply auto
done
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx'
‹ms' = targetnode a # ys @ m # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
next
case (silent_move_call f a s s' Q r p fs a' ms S ms')
note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧
m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain a'' where "valid_edge a''"
and "sourcenode a'' = sourcenode a" and "targetnode a'' = targetnode a'"
and "intra_kind (kind a'')"
by(fastforce dest:call_return_node_edge simp:intra_kind_def)
from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "call_of_return_node (targetnode a') (sourcenode a)"
by(fastforce simp:call_of_return_node_def return_node_def)
show False
proof(cases msx)
case Nil
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have [simp]:"m = sourcenode a"
and "tl ms = msx'" by simp_all
from Nil ‹ms' = targetnode a # targetnode a' # tl ms› ‹ms = msx @ m # msx'›
have "ms' = targetnode a # targetnode a' # msx'" by simp
from msx' disj ‹tl ms = msx'› ‹hd ms = sourcenode a›
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from ‹valid_edge a''› ‹intra_kind (kind a'')› ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹sourcenode a'' = sourcenode a› ‹targetnode a'' = targetnode a'›
have "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce dest:edge_obs_intra_slice_eq)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
have "m' ∈ obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙" by simp
from this msx' have "m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce intro:obsI)
from ‹call_of_return_node (targetnode a') (sourcenode a)›
‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
have "∃m' ∈ set (targetnode a'#msx').
∃mx. call_of_return_node m' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce
with ‹m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙›
have "m'#msx' ∈ obs (targetnode a#targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
by simp
with ‹ms' = targetnode a # targetnode a' # msx'› ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}›
show False by simp
next
case (Cons y ys)
with ‹ms = msx @ m # msx'› ‹ms' = targetnode a # targetnode a' # tl ms›
‹hd ms = sourcenode a›
have "ms' = targetnode a # targetnode a' # ys @ m # msx'"
and "y = sourcenode a" and "tl ms = ys @ m # msx'" by simp_all
show False
proof(cases "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (targetnode a' # ys @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
case True
hence imp:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (targetnode a' # ys @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" .
show False
proof(cases "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (ys @ [m]). ∃mx. call_of_return_node x'' mx ∧
mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
case True
with imp msx Cons ‹y = sourcenode a›
have "∀xs x xs'. targetnode a # targetnode a' # ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
apply clarsimp apply(case_tac xs) apply fastforce
apply(case_tac list) apply fastforce apply clarsimp
apply(erule_tac x="sourcenode a # lista" in allE) apply auto
done
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx'
‹ms' = targetnode a # targetnode a' # ys @ m # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
next
case False
hence "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
and all:"∀x''∈set (ys @ [m]). ∀mx. call_of_return_node x'' mx ⟶
mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce+
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
from this True
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
thus ?thesis by simp
next
case False
with ‹sourcenode a'' = sourcenode a›
have "sourcenode a'' ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with ‹valid_edge a''› ‹intra_kind (kind a'')›
have "obs_intra (targetnode a'') ⌊HRB_slice S⌋⇘CFG⇙ =
obs_intra (sourcenode a'') ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_slice_eq)
with ‹obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}›
‹sourcenode a'' = sourcenode a› ‹targetnode a'' = targetnode a'›
show ?thesis by fastforce
qed
with msx Cons ‹y = sourcenode a› all
show False by simp blast
qed
next
case False
hence "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
and all:"∀x''∈set (targetnode a' # ys @ [m]).
∀mx. call_of_return_node x'' mx ⟶ mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by fastforce+
with Cons ‹y = sourcenode a› msx
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}" by auto blast
from ‹call_of_return_node (targetnode a') (sourcenode a)› all
have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
from this ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙›
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(rule n_in_obs_intra)
with ‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
qed
next
case (silent_move_return f a s s' Q p f' ms S ms')
note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
(∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧
mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
show False
proof(cases msx)
case Nil
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have "tl ms = msx'" by simp
with ‹∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
msx'
show False by fastforce
next
case (Cons y ys)
with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› ‹ms' = tl ms›
have "ms' = ys @ m # msx'" and "y = sourcenode a" by simp_all
from msx Cons have "∀xs x xs'. ys = xs@x#xs' ∧
obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ (∃x''∈set (xs' @ [m]).
∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by auto (erule_tac x="y # xs" in allE,auto)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx' ‹ms' = ys @ m # msx'›
have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
qed
qed
inductive silent_moves ::
"'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒
(('var ⇀ 'val) × 'ret) list ⇒ 'edge list ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
(‹_,_ ⊢ '(_,_') =_⇒⇩τ '(_,_')› [51,50,0,0,50,0,0] 51)
where silent_moves_Nil: "length ms = length s ⟹ S,f ⊢ (ms,s) =[]⇒⇩τ (ms,s)"
| silent_moves_Cons:
"⟦S,f ⊢ (ms,s) -a→⇩τ (ms',s'); S,f ⊢ (ms',s') =as⇒⇩τ (ms'',s'')⟧
⟹ S,f ⊢ (ms,s) =a#as⇒⇩τ (ms'',s'')"
lemma silent_moves_equal_length:
assumes "S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from ‹S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')›
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule:silent_moves.induct)
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "length ms = length s" and "length ms' = length s'"
by(rule silent_move_equal_length)+
with ‹length ms' = length s' ∧ length ms'' = length s''›
show ?case by simp
qed simp
thus "length ms = length s" "length ms' = length s'" by simp_all
qed
lemma silent_moves_Append:
"⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s''); S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')⟧
⟹ S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')"
by(induct rule:silent_moves.induct)(auto intro:silent_moves.intros)
lemma silent_moves_split:
assumes "S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')"
obtains ms'' s'' where "S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s'')"
and "S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')"
proof(atomize_elim)
from ‹S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')›
show "∃ms'' s''. S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s'') ∧ S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')"
proof(induct as arbitrary:ms s)
case Nil
from ‹S,f ⊢ (ms,s) =[] @ as'⇒⇩τ (ms',s')› have "length ms = length s"
by(fastforce intro:silent_moves_equal_length)
hence "S,f ⊢ (ms,s) =[]⇒⇩τ (ms,s)" by(rule silent_moves_Nil)
with ‹S,f ⊢ (ms,s) =[] @ as'⇒⇩τ (ms',s')› show ?case by fastforce
next
case (Cons ax asx)
note IH = ‹⋀ms s. S,f ⊢ (ms,s) =asx @ as'⇒⇩τ (ms',s') ⟹
∃ms'' s''. S,f ⊢ (ms,s) =asx⇒⇩τ (ms'',s'') ∧ S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')›
from ‹S,f ⊢ (ms,s) =(ax # asx) @ as'⇒⇩τ (ms',s')›
obtain msx sx where "S,f ⊢ (ms,s) -ax→⇩τ (msx,sx)"
and "S,f ⊢ (msx,sx) =asx @ as'⇒⇩τ (ms',s')"
by(auto elim:silent_moves.cases)
from IH[OF this(2)] obtain ms'' s'' where "S,f ⊢ (msx,sx) =asx⇒⇩τ (ms'',s'')"
and "S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')" by blast
from ‹S,f ⊢ (ms,s) -ax→⇩τ (msx,sx)› ‹S,f ⊢ (msx,sx) =asx⇒⇩τ (ms'',s'')›
have "S,f ⊢ (ms,s) =ax#asx⇒⇩τ (ms'',s'')" by(rule silent_moves_Cons)
with ‹S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')› show ?case by blast
qed
qed
lemma valid_nodes_silent_moves:
"⟦S,f⊢ (ms,s) =as'⇒⇩τ (ms',s'); ∀m ∈ set ms. valid_node m⟧
⟹ ∀m ∈ set ms'. valid_node m"
proof(induct rule:silent_moves.induct)
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
note IH = ‹∀m∈set ms'. valid_node m ⟹ ∀m∈set ms''. valid_node m›
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')› ‹∀m∈set ms. valid_node m›
have "∀m∈set ms'. valid_node m"
apply - apply(erule silent_move.cases) apply auto
by(cases ms,auto dest:get_return_edges_valid)+
from IH[OF this] show ?case .
qed simp
lemma return_nodes_silent_moves:
"⟦S,f ⊢ (ms,s) =as'⇒⇩τ (ms',s'); ∀m ∈ set (tl ms). return_node m⟧
⟹ ∀m ∈ set (tl ms'). return_node m"
by(induct rule:silent_moves.induct,auto dest:silent_move_return_node)
lemma silent_moves_intra_path:
"⟦S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s'); ∀a ∈ set as. intra_kind(kind a)⟧
⟹ ms = ms' ∧ get_proc m = get_proc m'"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m
rule:silent_moves.induct)
case (silent_moves_Cons S f sx a msx' sx' as s'')
thus ?case
proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
case (silent_move_intra f a s s' n⇩c msx')
note IH = ‹⋀m. ⟦msx' = m # ms; ∀a∈set as. intra_kind (kind a)⟧
⟹ ms = ms' ∧ get_proc m = get_proc m'›
from ‹msx' = targetnode a # tl (m # ms)›
have "msx' = targetnode a # ms" by simp
from ‹∀a∈set (a # as). intra_kind (kind a)› have "∀a∈set as. intra_kind (kind a)"
by simp
from IH[OF ‹msx' = targetnode a # ms› this]
have "ms = ms'" and "get_proc (targetnode a) = get_proc m'" by simp_all
moreover
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
moreover
from ‹hd (m # ms) = sourcenode a› have "m = sourcenode a" by simp
ultimately show ?case using ‹ms = ms'› by simp
qed (auto simp:intra_kind_def)
qed simp
lemma silent_moves_nodestack_notempty:
"⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); ms ≠ []⟧ ⟹ ms' ≠ []"
apply(induct S f ms s as ms' s' rule:silent_moves.induct) apply auto
apply(erule silent_move.cases) apply auto
apply(case_tac "tl msa") by auto
lemma silent_moves_obs_slice:
"⟦S,kind ⊢ (ms,s) =as⇒⇩τ (ms',s'); mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙;
∀n ∈ set (tl ms'). return_node n⟧
⟹ mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀n ∈ set (tl ms). return_node n)"
proof(induct S f≡"kind" ms s as ms' s' rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S ms s a ms' s' as ms'' s'')
note IH = ‹⟦mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙; ∀m∈set (tl ms''). return_node m⟧
⟹ mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀m∈set (tl ms'). return_node m)›
from IH[OF ‹mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙› ‹∀m∈set (tl ms''). return_node m›]
have "mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" and "∀m∈set (tl ms'). return_node m"
by simp_all
with ‹S,kind ⊢ (ms,s) -a→⇩τ (ms',s')›
have "mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce intro:silent_move_obs_slice)
moreover
from ‹S,kind ⊢ (ms,s) -a→⇩τ (ms',s')› have "∀m∈set (tl ms). return_node m"
by(fastforce elim:silent_move.cases)
ultimately show ?case by simp
qed
lemma silent_moves_empty_obs_slice:
"⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}⟧
⟹ obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
note IH = ‹obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {} ⟹ obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}›
from IH[OF ‹obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {}›]
have "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}" by simp
with ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
show ?case by -(rule silent_move_empty_obs_slice,fastforce)
qed
lemma silent_moves_preds_transfers:
assumes "S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')"
shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
from ‹S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')›
have "preds (map f as) s ∧ transfers (map f as) s = s'"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
have "pred (f a) s" and "transfer (f a) s = s'" by(auto elim:silent_move.cases)
with ‹preds (map f as) s' ∧ transfers (map f as) s' = s''›
show ?case by fastforce
qed
thus "preds (map f as) s" and "transfers (map f as) s = s'" by simp_all
qed
lemma silent_moves_intra_path_obs:
assumes "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙" and "length s = length (m#msx')"
and "∀m ∈ set msx'. return_node m"
obtains as' where "S,slice_kind S ⊢ (m#msx',s) =as'⇒⇩τ (m'#msx',s)"
proof(atomize_elim)
from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
obtain as where "m -as→⇩ι* m'" and "m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by -(erule obs_intraE)
from ‹m -as→⇩ι* m'› obtain x where "distance m m' x" and "x ≤ length as"
by(erule every_path_distance)
from ‹distance m m' x› ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
show "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
proof(induct x arbitrary:m s rule:nat.induct)
fix m fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' 0" and "length s = length (m#msx')"
then obtain as' where "m -as'→⇩ι* m'" and "length as' = 0"
by(auto elim:distance.cases)
hence "m -[]→⇩ι* m'" by(cases as) auto
hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
with ‹length s = length (m#msx')›[THEN sym]
have "S,slice_kind S ⊢ (m#msx',s) =[]⇒⇩τ (m#msx',s)"
by -(rule silent_moves_Nil)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by simp blast
next
fix x m fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' (Suc x)" and "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
and IH:"⋀m s. ⟦distance m m' x; m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙;
length s = length (m#msx'); ∀m ∈ set msx'. return_node m⟧
⟹ ∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› have "valid_node m"
by(rule in_obs_intra_valid)
with ‹distance m m' (Suc x)› have "m ≠ m'"
by(fastforce elim:distance.cases dest:empty_path simp:intra_path_def)
have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume isin:"m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(fastforce intro!:n_in_obs_intra)
with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› ‹m ≠ m'› show False by simp
qed
from ‹distance m m' (Suc x)› obtain a where "valid_edge a" and "m = sourcenode a"
and "intra_kind(kind a)" and "distance (targetnode a) m' x"
and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m' x ∧
valid_edge a' ∧ intra_kind (kind a') ∧
targetnode a' = mx)"
by -(erule distance_successor_distance,simp+)
from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
by(rule obs_intra_singleton_element)
with ‹valid_edge a› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹intra_kind(kind a)›
have disj:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {} ∨
obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
by -(drule_tac S="⌊HRB_slice S⌋⇘CFG⇙" in edge_obs_intra_subset,auto)
from ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹m = sourcenode a›
have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
by(cases s)
(auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
from ‹distance (targetnode a) m' x› obtain asx where "targetnode a -asx→⇩ι* m'"
and "length asx = x" and "∀as'. targetnode a -as'→⇩ι* m' ⟶ x ≤ length as'"
by(auto elim:distance.cases)
from ‹targetnode a -asx→⇩ι* m'› ‹m' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
obtain mx where "mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(erule path_ex_obs_intra)
with disj have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
from IH[OF ‹distance (targetnode a) m' x› this length
‹∀m ∈ set msx'. return_node m›]
obtain asx' where moves:"S,slice_kind S ⊢
(targetnode a#msx',transfer (slice_kind S a) s) =asx'⇒⇩τ
(m'#msx',transfer (slice_kind S a) s)" by blast
have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
proof(cases "kind a")
fix f assume "kind a = ⇑f"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› have "slice_kind S a = ⇑id"
by(fastforce intro:slice_kind_Upd)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q assume "kind a = (Q)⇩√"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› ‹distance (targetnode a) m' x›
‹distance m m' (Suc x)› target
have "slice_kind S a = (λs. True)⇩√"
by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q r p fs assume "kind a = Q:r↪⇘p⇙fs"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
next
fix Q p f assume "kind a = Q↩⇘p⇙f"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
qed
hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
by simp_all
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹valid_edge a›
‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
have "S,slice_kind S ⊢ (sourcenode a#msx',s) -a→⇩τ
(targetnode a#msx',transfer (slice_kind S a) s)"
by(fastforce intro:silent_move_intra)
with moves ‹transfer (slice_kind S a) s = s› ‹m = sourcenode a›
have "S,slice_kind S ⊢ (m#msx',s) =a#asx'⇒⇩τ (m'#msx',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by blast
qed
qed
lemma silent_moves_intra_path_no_obs:
assumes "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}" and "method_exit m'"
and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')"
and "∀m ∈ set msx'. return_node m"
obtains as where "S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
proof(atomize_elim)
from ‹method_exit m'› ‹get_proc m = get_proc m'› ‹valid_node m›
obtain as where "m -as→⇩ι* m'" by(erule intra_path_to_matching_method_exit)
then obtain x where "distance m m' x" and "x ≤ length as"
by(erule every_path_distance)
from ‹distance m m' x› ‹m -as→⇩ι* m'› ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}›
‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
show "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
proof(induct x arbitrary:m as s rule:nat.induct)
fix m fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' 0" and "length s = length (m#msx')"
then obtain as' where "m -as'→⇩ι* m'" and "length as' = 0"
by(auto elim:distance.cases)
hence "m -[]→⇩ι* m'" by(cases as) auto
hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
with ‹length s = length (m#msx')›[THEN sym]
have "S,slice_kind S ⊢ (m#msx',s) =[]⇒⇩τ (m#msx',s)"
by(fastforce intro:silent_moves_Nil)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by simp blast
next
fix x m as fix s::"(('var ⇀ 'val) × 'ret) list"
assume "distance m m' (Suc x)" and "m -as→⇩ι* m'"
and "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
and IH:"⋀m as s. ⟦distance m m' x; m -as→⇩ι* m';
obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}; length s = length (m#msx');
∀m ∈ set msx'. return_node m⟧
⟹ ∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
from ‹m -as→⇩ι* m'› have "valid_node m"
by(fastforce intro:path_valid_node simp:intra_path_def)
from ‹m -as→⇩ι* m'› have "get_proc m = get_proc m'" by(rule intra_path_get_procs)
have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof
assume "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(fastforce intro!:n_in_obs_intra)
with ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
qed
from ‹distance m m' (Suc x)› obtain a where "valid_edge a" and "m = sourcenode a"
and "intra_kind(kind a)" and "distance (targetnode a) m' x"
and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m' x ∧
valid_edge a' ∧ intra_kind (kind a') ∧
targetnode a' = mx)"
by -(erule distance_successor_distance,simp+)
from ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹m = sourcenode a›
have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
by(cases s)
(auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
from ‹distance (targetnode a) m' x› obtain asx where "targetnode a -asx→⇩ι* m'"
and "length asx = x" and "∀as'. targetnode a -as'→⇩ι* m' ⟶ x ≤ length as'"
by(auto elim:distance.cases)
from ‹valid_edge a› ‹intra_kind(kind a)› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹m = sourcenode a› ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}›
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
by(fastforce dest:edge_obs_intra_subset)
from IH[OF ‹distance (targetnode a) m' x› ‹targetnode a -asx→⇩ι* m'› this
length ‹∀m ∈ set msx'. return_node m›] obtain as'
where moves:"S,slice_kind S ⊢
(targetnode a#msx',transfer (slice_kind S a) s) =as'⇒⇩τ
(m'#msx',transfer (slice_kind S a) s)" by blast
have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
proof(cases "kind a")
fix f assume "kind a = ⇑f"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› have "slice_kind S a = ⇑id"
by(fastforce intro:slice_kind_Upd)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q assume "kind a = (Q)⇩√"
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}› ‹distance (targetnode a) m' x›
‹distance m m' (Suc x)› ‹method_exit m'› ‹get_proc m = get_proc m'› target
have "slice_kind S a = (λs. True)⇩√"
by(fastforce intro:slice_kind_Pred_empty_obs_nearer_SOME)
with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
next
fix Q r p fs assume "kind a = Q:r↪⇘p⇙fs"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
next
fix Q p f assume "kind a = Q↩⇘p⇙f"
with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
thus ?thesis by simp
qed
hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
by simp_all
with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹valid_edge a›
‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
have "S,slice_kind S ⊢ (sourcenode a#msx',s) -a→⇩τ
(targetnode a#msx',transfer (slice_kind S a) s)"
by(fastforce intro:silent_move_intra)
with moves ‹transfer (slice_kind S a) s = s› ‹m = sourcenode a›
have "S,slice_kind S ⊢ (m#msx',s) =a#as'⇒⇩τ (m'#msx',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by blast
qed
qed
lemma silent_moves_vpa_path:
assumes "S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
and "ms = targetnodes rs" and "valid_return_list rs m"
and "length rs = length cs"
shows "m -as→* m'" and "valid_path_aux cs as"
proof -
from assms have "m -as→* m' ∧ valid_path_aux cs as"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m cs ms rs
rule:silent_moves.induct)
case (silent_moves_Nil msx sx n⇩c f)
from ‹valid_node m'› have "m' -[]→* m'"
by (rule empty_path)
thus ?case by fastforce
next
case (silent_moves_Cons S f sx a msx' sx' as s'')
thus ?case
proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
case (silent_move_intra f a sx sx' n⇩c msx')
note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs⟧
⟹ m -as→* m' ∧ valid_path_aux cs as›
from ‹msx' = targetnode a # tl (m # ms)›
have "msx' = targetnode a # ms" by simp
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)"
by(rule get_proc_intra)
with ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
have "valid_return_list rs (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from IH[OF ‹msx' = targetnode a # ms› this
‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹ms = targetnodes rs› ‹valid_return_list rs (targetnode a)›
‹length rs = length cs›]
have "targetnode a -as→* m'" and "valid_path_aux cs as" by simp_all
from ‹valid_edge a› ‹targetnode a -as→* m'›
‹hd (m # ms) = sourcenode a›
have "m -a#as→* m'" by(fastforce intro:Cons_path)
moreover
from ‹intra_kind (kind a)› ‹valid_path_aux cs as›
have "valid_path_aux cs (a # as)" by(fastforce simp:intra_kind_def)
ultimately show ?case by simp
next
case (silent_move_call f a sx sx' Q r p fs a' n⇩c msx')
note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs⟧
⟹ m -as→* m' ∧ valid_path_aux cs as›
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from ‹length rs = length cs›
have "length (a'#rs) = length (a#cs)" by simp
from ‹msx' = targetnode a # targetnode a' # tl (m # ms)›
have "msx' = targetnode a # targetnode a' # ms" by simp
from ‹ms = targetnodes rs› have "targetnode a' # ms = targetnodes (a' # rs)"
by(simp add:targetnodes_def)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
by(rule get_return_edges_valid)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
from ‹valid_edge a› ‹a' ∈ get_return_edges a›
have "get_proc (sourcenode a) = get_proc (targetnode a')"
by(rule get_proc_get_return_edge)
with ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
‹get_proc (targetnode a) = p› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
have "valid_return_list (a' # rs) (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE) apply clarsimp
by(case_tac list)(auto simp:targetnodes_def)
from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹a' ∈ get_return_edges a›
have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
by auto(case_tac i,auto)
from IH[OF ‹msx' = targetnode a # targetnode a' # ms› ‹valid_node (targetnode a)› this
‹targetnode a' # ms = targetnodes (a' # rs)›
‹valid_return_list (a' # rs) (targetnode a)› ‹length (a'#rs) = length (a#cs)›]
have "targetnode a -as→* m'" and "valid_path_aux (a # cs) as" by simp_all
from ‹valid_edge a› ‹targetnode a -as→* m'›
‹hd (m # ms) = sourcenode a›
have "m -a#as→* m'" by(fastforce intro:Cons_path)
moreover
from ‹valid_path_aux (a # cs) as› ‹kind a = Q:r↪⇘p⇙fs›
have "valid_path_aux cs (a # as)" by simp
ultimately show ?case by simp
next
case (silent_move_return f a sx sx' Q p f' n⇩c msx')
note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
ms = targetnodes rs; valid_return_list rs m;
length rs = length cs⟧
⟹ m -as→* m' ∧ valid_path_aux cs as›
from ‹valid_edge a› have "valid_node (targetnode a)" by simp
from ‹length (m # ms) = length sx› ‹length sx = Suc (length sx')›
‹sx' ≠ []›
obtain x xs where "ms = x#xs" by(cases ms) auto
with ‹ms = targetnodes rs› obtain r' rs' where "rs = r'#rs'"
and "x = targetnode r'" and "xs = targetnodes rs'"
by(auto simp:targetnodes_def)
with ‹length rs = length cs› obtain c' cs' where "cs = c'#cs'"
and "length rs' = length cs'"
by(cases cs) auto
from ‹ms = x#xs› ‹length (m # ms) = length sx›
‹length sx = Suc (length sx')›
have "length sx' = Suc (length xs)" by simp
from ‹ms = x#xs› ‹msx' = tl (m # ms)› ‹hd (tl (m # ms)) = targetnode a›
‹length (m # ms) = length sx› ‹length sx = Suc (length sx')› ‹sx' ≠ []›
have "msx' = targetnode a#xs" by simp
from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹rs = r'#rs'› ‹cs = c'#cs'›
have "r' ∈ get_return_edges c'" by fastforce
from ‹ms = x#xs› ‹hd (tl (m # ms)) = targetnode a›
have "x = targetnode a" by simp
with ‹valid_return_list rs m› ‹rs = r'#rs'› ‹x = targetnode r'›
have "valid_return_list rs' (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="r'#cs'" in allE) apply clarsimp
by(case_tac cs')(auto simp:targetnodes_def)
from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
‹rs = r'#rs'› ‹cs = c'#cs'›
have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
and "r' ∈ get_return_edges c'" by auto
from IH[OF ‹msx' = targetnode a#xs› ‹valid_node (targetnode a)›
‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)› ‹xs = targetnodes rs'›
‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'›]
have "targetnode a -as→* m'" and "valid_path_aux cs' as" by simp_all
from ‹valid_edge a› ‹targetnode a -as→* m'›
‹hd (m # ms) = sourcenode a›
have "m -a#as→* m'" by(fastforce intro:Cons_path)
moreover
from ‹ms = x#xs› ‹hd (tl (m # ms)) = targetnode a›
have "x = targetnode a" by simp
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
have "method_exit (sourcenode a)" by(fastforce simp:method_exit_def)
from ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
‹rs = r'#rs'›
have "get_proc (sourcenode a) = get_proc (sourcenode r') ∧
method_exit (sourcenode r') ∧ valid_edge r'"
apply(clarsimp simp:valid_return_list_def method_exit_def)
apply(erule_tac x="[]" in allE)
by(auto dest:get_proc_return)
hence "get_proc (sourcenode a) = get_proc (sourcenode r')"
and "method_exit (sourcenode r')" and "valid_edge r'" by simp_all
with ‹method_exit (sourcenode a)› have "sourcenode r' = sourcenode a"
by(fastforce intro:method_exit_unique)
with ‹valid_edge a› ‹valid_edge r'› ‹x = targetnode r'› ‹x = targetnode a›
have "r' = a" by(fastforce intro:edge_det)
with ‹r' ∈ get_return_edges c'› ‹valid_path_aux cs' as› ‹cs = c'#cs'›
‹kind a = Q↩⇘p⇙f'›
have "valid_path_aux cs (a # as)" by simp
ultimately show ?case by simp
qed
qed
thus "m -as→* m'" and "valid_path_aux cs as" by simp_all
qed
subsection ‹Observable moves›
inductive observable_move ::
"'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒
(('var ⇀ 'val) × 'ret) list ⇒ 'edge ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
(‹_,_ ⊢ '(_,_') -_→ '(_,_')› [51,50,0,0,50,0,0] 51)
where observable_move_intra:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length s' = length s; length ms = length s;
hd ms = sourcenode a; ms' = (targetnode a)#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→ (ms',s')"
| observable_move_call:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘p⇙fs;
valid_edge a'; a' ∈ get_return_edges a;
∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length ms = length s; length s' = Suc(length s);
hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms⟧
⟹ S,f ⊢ (ms,s) -a→ (ms',s')"
| observable_move_return:
"⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q↩⇘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 ⊢ (ms,s) -a→ (ms',s')"
inductive observable_moves ::
"'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒
(('var ⇀ 'val) × 'ret) list ⇒ 'edge list ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
(‹_,_ ⊢ '(_,_') =_⇒ '(_,_')› [51,50,0,0,50,0,0] 51)
where observable_moves_snoc:
"⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); S,f ⊢ (ms',s') -a→ (ms'',s'')⟧
⟹ S,f ⊢ (ms,s) =as@[a]⇒ (ms'',s'')"
lemma observable_move_equal_length:
assumes "S,f ⊢ (ms,s) -a→ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
proof -
from ‹S,f ⊢ (ms,s) -a→ (ms',s')›
have "length ms = length s ∧ length ms' = length s'"
proof(induct rule: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 ⊢ (ms,s) =as⇒ (ms',s')"
shows "length ms = length s" and "length ms' = length s'"
using ‹S,f ⊢ (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 ⊢ (ms',s') -a→ (ms'',s'')›
have "length ms' = length s'" "length ms'' = length s''"
by(rule observable_move_equal_length)+
moreover
from ‹S,f ⊢ (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 ⊢ (ms,s) =as⇒ (ms',s'); as = []⟧ ⟹ False"
by(induct rule:observable_moves.induct,simp)
lemma silent_move_observable_moves:
"⟦S,f ⊢ (ms'',s'') =as⇒ (ms',s'); S,f ⊢ (ms,s) -a→⇩τ (ms'',s'')⟧
⟹ S,f ⊢ (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 ⊢ (ms,s) -a→⇩τ (msx,sx)› ‹S,f ⊢ (msx,sx) =as⇒⇩τ (ms',s')›
have "S,f ⊢ (ms,s) =a#as⇒⇩τ (ms',s')" by(fastforce intro:silent_moves_Cons)
with ‹S,f ⊢ (ms',s') -a'→ (ms'',s'')›
have "S,f ⊢ (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 ⊢ (ms,s) =as⇒⇩τ (ms'',s''); S,f ⊢ (ms'',s'') =as'⇒ (ms',s')⟧
⟹ S,f ⊢ (ms,s) =as@as'⇒ (ms',s')"
by(induct rule:silent_moves.induct)(auto elim:silent_move_observable_moves)
lemma observable_moves_preds_transfers:
assumes "S,f ⊢ (ms,s) =as⇒ (ms',s')"
shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
from ‹S,f ⊢ (ms,s) =as⇒ (ms',s')›
have "preds (map f as) s ∧ transfers (map f as) s = s'"
proof(induct rule:observable_moves.induct)
case (observable_moves_snoc S f ms s as ms' s' a ms'' s'')
from ‹S,f ⊢ (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 ⊢ (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 ⊢ (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↩⇘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↩⇘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→⇩d⇩d 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)⇩√" and "kind ax = (Q')⇩√"
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)⇩√"
and "slice_kind S ax = (P')⇩√"
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)⇩√›
‹slice_kind S a = (P)⇩√› 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')⇩√›
‹slice_kind S ax = (P')⇩√› have "pred (kind ax) s'"
by(simp add:slice_kinds_def)
with ‹kind ax = (Q')⇩√› 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)⇩√› 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)⇩√› ‹slice_kind S a = (P)⇩√› ‹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)⇩√›
‹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')⇩√› ‹slice_kind S ax = (P')⇩√› ‹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')⇩√›
‹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→⇩d⇩d nx" by(rule sum_SDG_ddep_edge)
from ‹nx ∈ HRB_slice S› ‹(CFG_node (sourcenode a)) s-V→⇩d⇩d 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→⇩d⇩d 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→⇩d⇩d 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 = ⇑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)⇩√"
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')⇩√"
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 ‹WS››
inductive_set WS :: "'node SDG_node set ⇒ (('node list × (('var ⇀ 'val) × 'ret) list) ×
('node list × (('var ⇀ '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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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↪⇘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↪⇘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↪⇘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↪⇘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↩⇘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↩⇘p⇙f'›
obtain a' Q' r' fs' where "valid_edge a'" and "kind a' = Q':r'↪⇘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↩⇘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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (ms⇩2,s⇩2) =as⇒⇩τ (ms⇩1,s⇩2)›
have "S,slice_kind S ⊢ (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 = ⇑f) ∨ (∃Q. kind a = (Q)⇩√)"
by(simp add:intra_kind_def)
thus ?thesis
proof
assume "∃f. kind a = ⇑f"
then obtain f' where "kind a = ⇑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 = ⇑f'›
have "slice_kind S a = ⇑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 = ⇑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)⇩√"
then obtain Q where "kind a = (Q)⇩√" 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)⇩√›
have "slice_kind S a = (Q)⇩√"
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)⇩√› ‹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 ⊢ (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 ⊢ (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 ⊢ (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↪⇘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↪⇘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↪⇘p⇙fs›
have [simp]:"s⇩1' = (Map.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↪⇘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↪⇘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 ⊢ (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 ⊢ (ms⇩2,s⇩2) =as⇒⇩τ (ms⇩1,s⇩2)›
have "S,slice_kind S ⊢ (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↪⇘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↪⇘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)).
(Map.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↪⇘p⇙fs›
‹(THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins›
have eq:"fst (hd (transfer (slice_kind S a) s⇩2)) =
Map.empty(ins [:=] params (cspp (targetnode a) (HRB_slice S) fs) (fst cf⇩2))"
by(auto dest:slice_kind_Call_in_slice)
show "(Map.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↪⇘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↪⇘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→⇩d⇩d (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↪⇘p⇙fs›
have slice_kind:"slice_kind S a =
Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
by(rule slice_kind_Call_in_slice)
from ‹valid_edge a› ‹kind a = Q:r↪⇘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↪⇘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)) =
Map.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 "Map.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:"Map.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↪⇘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↪⇘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 ⊢ (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 ⊢ (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↩⇘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→⇩√* (_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 ⊢ (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 ⊢ (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↩⇘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 ⊢ (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 ⊢ (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 ⊢ (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↩⇘p⇙f'› obtain a'' Q' r' fs' where "valid_edge a''"
and "kind a'' = Q':r'↪⇘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↩⇘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↩⇘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↩⇘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↩⇘p⇙f'› have "slice_kind S a = (λcf. True)↩⇘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↩⇘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 ⊢ (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 ⊢ (ms⇩2,s⇩2) =as⇒⇩τ (ms⇩1,s⇩2)›
have "S,slice_kind S ⊢ (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↩⇘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↩⇘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↩⇘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→⇩d⇩d (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↩⇘p⇙f'› ‹valid_edge a''›
‹kind a'' = Q':r'↪⇘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↩⇘p⇙f'›
‹(p,ins,outs) ∈ set procs›
have slice_kind:"slice_kind S a =
Q↩⇘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↩⇘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↩⇘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↩⇘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↩⇘p⇙f'›
‹(p,ins,outs) ∈ set procs›
have "slice_kind S a =
Q↩⇘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↩⇘p⇙f'›
have "slice_kind S a = (λcf. True)↩⇘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)↩⇘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 ⊢ (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 ⇀ 'val) × 'ret) list) ×
('node list × (('var ⇀ '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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (ms⇩2,s⇩2) =as'@[last as]⇒
(ms⇩1',transfer (slice_kind S (last as)) s⇩2)"
proof(atomize_elim)
from ‹S,kind ⊢ (ms⇩1,s⇩1) =as⇒ (ms⇩1',s⇩1')› obtain ms' s' as' a'
where "S,kind ⊢ (ms⇩1,s⇩1) =as'⇒⇩τ (ms',s')"
and "S,kind ⊢ (ms',s') -a'→ (ms⇩1',s⇩1')" and "as = as'@[a']"
by(fastforce elim:observable_moves.cases)
from ‹S,kind ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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 ⊢ (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 ‹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