Theory Slicing.Slice
section ‹Static backward slice›
theory Slice
imports Observable Distance DataDependence "../Basic/SemanticsCFG"
begin
locale BackwardSlice =
CFG_wf sourcenode targetnode kind valid_edge Entry Def Use state_val
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val" +
fixes backward_slice :: "'node set ⇒ 'node set"
assumes valid_nodes:"n ∈ backward_slice S ⟹ valid_node n"
and refl:"⟦valid_node n; n ∈ S⟧ ⟹ n ∈ backward_slice S"
and dd_closed:"⟦n' ∈ backward_slice S; n influences V in n'⟧
⟹ n ∈ backward_slice S"
and obs_finite:"finite (obs n (backward_slice S))"
and obs_singleton:"card (obs n (backward_slice S)) ≤ 1"
begin
lemma slice_n_in_obs:
"n ∈ backward_slice S ⟹ obs n (backward_slice S) = {n}"
by(fastforce intro!:n_in_obs dest:valid_nodes)
lemma obs_singleton_disj:
"(∃m. obs n (backward_slice S) = {m}) ∨ obs n (backward_slice S) = {}"
proof -
have "finite(obs n (backward_slice S))" by(rule obs_finite)
show ?thesis
proof(cases "card(obs n (backward_slice S)) = 0")
case True
with ‹finite(obs n (backward_slice S))› have "obs n (backward_slice S) = {}"
by simp
thus ?thesis by simp
next
case False
have "card(obs n (backward_slice S)) ≤ 1" by(rule obs_singleton)
with False have "card(obs n (backward_slice S)) = 1"
by simp
hence "∃m. obs n (backward_slice S) = {m}" by(fastforce dest:card_eq_SucD)
thus ?thesis by simp
qed
qed
lemma obs_singleton_element:
assumes "m ∈ obs n (backward_slice S)" shows "obs n (backward_slice S) = {m}"
proof -
have "(∃m. obs n (backward_slice S) = {m}) ∨ obs n (backward_slice S) = {}"
by(rule obs_singleton_disj)
with ‹m ∈ obs n (backward_slice S)› show ?thesis by fastforce
qed
lemma obs_the_element:
"m ∈ obs n (backward_slice S) ⟹ (THE m. m ∈ obs n (backward_slice S)) = m"
by(fastforce dest:obs_singleton_element)
subsection ‹Traversing the sliced graph›
text ‹‹slice_kind S a› conforms to @{term "kind a"} in the
sliced graph›
definition slice_kind :: "'node set ⇒ 'edge ⇒ 'state edge_kind"
where "slice_kind S a = (let S' = backward_slice S; n = sourcenode a in
(if sourcenode a ∈ S' then kind a
else (case kind a of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒
(if obs (sourcenode a) S' = {} then
(let nx = (SOME n'. ∃a'. n = sourcenode a' ∧ valid_edge a' ∧ targetnode a' = n')
in (if (targetnode a = nx) then (λs. True)⇩√ else (λs. False)⇩√))
else (let m = THE m. m ∈ obs n S' in
(if (∃x. distance (targetnode a) m x ∧ distance n m (x + 1) ∧
(targetnode a = (SOME nx'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = nx')))
then (λs. True)⇩√ else (λs. False)⇩√
))
))
))"
definition
slice_kinds :: "'node set ⇒ 'edge list ⇒ 'state edge_kind list"
where "slice_kinds S as ≡ map (slice_kind S) as"
lemma slice_kind_in_slice:
"sourcenode a ∈ backward_slice S ⟹ slice_kind S a = kind a"
by(simp add:slice_kind_def)
lemma slice_kind_Upd:
"⟦sourcenode a ∉ backward_slice S; kind a = ⇑f⟧ ⟹ slice_kind S a = ⇑id"
by(simp add:slice_kind_def)
lemma slice_kind_Pred_empty_obs_SOME:
"⟦sourcenode a ∉ backward_slice S; kind a = (Q)⇩√;
obs (sourcenode a) (backward_slice S) = {};
targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = n')⟧
⟹ slice_kind S a = (λs. True)⇩√"
by(simp add:slice_kind_def)
lemma slice_kind_Pred_empty_obs_not_SOME:
"⟦sourcenode a ∉ backward_slice S; kind a = (Q)⇩√;
obs (sourcenode a) (backward_slice S) = {};
targetnode a ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = n')⟧
⟹ slice_kind S a = (λs. False)⇩√"
by(simp add:slice_kind_def)
lemma slice_kind_Pred_obs_nearer_SOME:
assumes "sourcenode a ∉ backward_slice S" and "kind a = (Q)⇩√"
and "m ∈ obs (sourcenode a) (backward_slice S)"
and "distance (targetnode a) m x" "distance (sourcenode a) m (x + 1)"
and "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = n')"
shows "slice_kind S a = (λs. True)⇩√"
proof -
from ‹m ∈ obs (sourcenode a) (backward_slice S)›
have "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
by(rule obs_the_element[THEN sym])
with assms show ?thesis
by(fastforce simp:slice_kind_def Let_def)
qed
lemma slice_kind_Pred_obs_nearer_not_SOME:
assumes "sourcenode a ∉ backward_slice S" and "kind a = (Q)⇩√"
and "m ∈ obs (sourcenode a) (backward_slice S)"
and "distance (targetnode a) m x" "distance (sourcenode a) m (x + 1)"
and "targetnode a ≠ (SOME nx'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = nx')"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from ‹m ∈ obs (sourcenode a) (backward_slice S)›
have "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
by(rule obs_the_element[THEN sym])
with assms show ?thesis
by(fastforce dest:distance_det simp:slice_kind_def Let_def)
qed
lemma slice_kind_Pred_obs_not_nearer:
assumes "sourcenode a ∉ backward_slice S" and "kind a = (Q)⇩√"
and in_obs:"m ∈ obs (sourcenode a) (backward_slice S)"
and dist:"distance (sourcenode a) m (x + 1)"
"¬ distance (targetnode a) m x"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from in_obs have the:"m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
by(rule obs_the_element[THEN sym])
from dist have "¬ (∃x. distance (targetnode a) m x ∧
distance (sourcenode a) m (x + 1))"
by(fastforce dest:distance_det)
with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√› in_obs the show ?thesis
by(fastforce simp:slice_kind_def Let_def)
qed
lemma kind_Predicate_notin_slice_slice_kind_Predicate:
assumes "kind a = (Q)⇩√" and "sourcenode a ∉ backward_slice S"
obtains Q' where "slice_kind S a = (Q')⇩√" and "Q' = (λs. False) ∨ Q' = (λs. True)"
proof(atomize_elim)
show "∃Q'. slice_kind S a = (Q')⇩√ ∧ (Q' = (λs. False) ∨ Q' = (λs. True))"
proof(cases "obs (sourcenode a) (backward_slice S) = {}")
case True
show ?thesis
proof(cases "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')")
case True
with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
‹obs (sourcenode a) (backward_slice S) = {}›
have "slice_kind S a = (λs. True)⇩√" by(rule slice_kind_Pred_empty_obs_SOME)
thus ?thesis by simp
next
case False
with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
‹obs (sourcenode a) (backward_slice S) = {}›
have "slice_kind S a = (λs. False)⇩√"
by(rule slice_kind_Pred_empty_obs_not_SOME)
thus ?thesis by simp
qed
next
case False
then obtain m where "m ∈ obs (sourcenode a) (backward_slice S)" by blast
show ?thesis
proof(cases "∃x. distance (targetnode a) m x ∧
distance (sourcenode a) m (x + 1)")
case True
then obtain x where "distance (targetnode a) m x"
and "distance (sourcenode a) m (x + 1)" by blast
show ?thesis
proof(cases "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = n')")
case True
with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
‹m ∈ obs (sourcenode a) (backward_slice S)›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
have "slice_kind S a = (λs. True)⇩√"
by(rule slice_kind_Pred_obs_nearer_SOME)
thus ?thesis by simp
next
case False
with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
‹m ∈ obs (sourcenode a) (backward_slice S)›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
have "slice_kind S a = (λs. False)⇩√"
by(rule slice_kind_Pred_obs_nearer_not_SOME)
thus ?thesis by simp
qed
next
case False
from ‹m ∈ obs (sourcenode a) (backward_slice S)›
have "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
by(rule obs_the_element[THEN sym])
with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√› False
‹m ∈ obs (sourcenode a) (backward_slice S)›
have "slice_kind S a = (λs. False)⇩√"
by(fastforce simp:slice_kind_def Let_def)
thus ?thesis by simp
qed
qed
qed
lemma only_one_SOME_edge:
assumes "valid_edge a"
shows "∃!a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
proof(rule ex_ex1I)
show "∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
proof -
have "(∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')) =
(∃n'. ∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧ targetnode a' = n')"
apply(unfold some_eq_ex[of "λn'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n'"])
by simp
also have "…" using ‹valid_edge a› by blast
finally show ?thesis .
qed
next
fix a' ax
assume "sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
and "sourcenode a = sourcenode ax ∧ valid_edge ax ∧
targetnode ax = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
thus "a' = ax" by(fastforce intro!:edge_det)
qed
lemma slice_kind_only_one_True_edge:
assumes "sourcenode a = sourcenode a'" and "targetnode a ≠ targetnode a'"
and "valid_edge a" and "valid_edge a'" and "slice_kind S a = (λs. True)⇩√"
shows "slice_kind S a' = (λs. False)⇩√"
proof -
from assms obtain Q Q' where "kind a = (Q)⇩√"
and "kind a' = (Q')⇩√" and det:"∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
by(auto dest:deterministic)
from ‹valid_edge a› have ex1:"∃!a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
by(rule only_one_SOME_edge)
show ?thesis
proof(cases "sourcenode a ∈ backward_slice S")
case True
with ‹slice_kind S a = (λs. True)⇩√› ‹kind a = (Q)⇩√› have "Q = (λs. True)"
by(simp add:slice_kind_def Let_def)
with det have "Q' = (λs. False)" by(simp add:fun_eq_iff)
with True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'› show ?thesis
by(simp add:slice_kind_def Let_def)
next
case False
hence "sourcenode a ∉ backward_slice S" by simp
thus ?thesis
proof(cases "obs (sourcenode a) (backward_slice S) = {}")
case True
with ‹sourcenode a ∉ backward_slice S› ‹slice_kind S a = (λs. True)⇩√›
‹kind a = (Q)⇩√›
have target:"targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
proof(rule ccontr)
assume "¬ targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
by simp
with ex1 target ‹sourcenode a = sourcenode a'› ‹valid_edge a›
‹valid_edge a'› have "a = a'" by blast
with ‹targetnode a ≠ targetnode a'› show False by simp
qed
with ‹sourcenode a ∉ backward_slice S› True ‹kind a' = (Q')⇩√›
‹sourcenode a = sourcenode a'› show ?thesis
by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
next
case False
hence "obs (sourcenode a) (backward_slice S) ≠ {}" .
then obtain m where "m ∈ obs (sourcenode a) (backward_slice S)" by auto
hence "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
by(auto dest:obs_the_element)
with ‹sourcenode a ∉ backward_slice S›
‹obs (sourcenode a) (backward_slice S) ≠ {}›
‹slice_kind S a = (λs. True)⇩√› ‹kind a = (Q)⇩√›
obtain x x' where "distance (targetnode a) m x"
"distance (sourcenode a) m (x + 1)"
and target:"targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = n')"
by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
show ?thesis
proof(cases "distance (targetnode a') m x")
case False
with ‹sourcenode a ∉ backward_slice S› ‹kind a' = (Q')⇩√›
‹m ∈ obs (sourcenode a) (backward_slice S)›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
‹sourcenode a = sourcenode a'› show ?thesis
by(fastforce intro:slice_kind_Pred_obs_not_nearer)
next
case True
from ‹valid_edge a› ‹distance (targetnode a) m x›
‹distance (sourcenode a) m (x + 1)›
have ex1:"∃!a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧ valid_edge a' ∧
targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = nx)"
by(fastforce intro!:only_one_SOME_dist_edge)
have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = n')"
proof(rule ccontr)
assume "¬ targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = n')"
hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ targetnode a' = n')"
by simp
with ex1 target ‹sourcenode a = sourcenode a'›
‹valid_edge a› ‹valid_edge a'›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
have "a = a'" by auto
with ‹targetnode a ≠ targetnode a'› show False by simp
qed
with ‹sourcenode a ∉ backward_slice S›
‹kind a' = (Q')⇩√› ‹m ∈ obs (sourcenode a) (backward_slice S)›
‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
True ‹sourcenode a = sourcenode a'› show ?thesis
by(fastforce intro:slice_kind_Pred_obs_nearer_not_SOME)
qed
qed
qed
qed
lemma slice_deterministic:
assumes "valid_edge a" and "valid_edge a'"
and "sourcenode a = sourcenode a'" and "targetnode a ≠ targetnode a'"
obtains Q Q' where "slice_kind S a = (Q)⇩√" and "slice_kind S a' = (Q')⇩√"
and "∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
proof(atomize_elim)
from assms obtain Q Q'
where "kind a = (Q)⇩√" and "kind a' = (Q')⇩√"
and det:"∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
by(auto dest:deterministic)
from ‹valid_edge a› have ex1:"∃!a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
valid_edge a' ∧ targetnode a' = n')"
by(rule only_one_SOME_edge)
show "∃Q Q'. slice_kind S a = (Q)⇩√ ∧ slice_kind S a' = (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
proof(cases "sourcenode a ∈ backward_slice S")
case True
with ‹kind a = (Q)⇩√› have "slice_kind S a = (Q)⇩√"
by(simp add:slice_kind_def Let_def)
from True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'›
have "slice_kind S a' = (Q')⇩√"
by(simp add:slice_kind_def Let_def)
with ‹slice_kind S a = (Q)⇩√› det show ?thesis by blast
next
case False
with ‹kind a = (Q)⇩√›
have "slice_kind S a = (λs. True)⇩√ ∨ slice_kind S a = (λs. False)⇩√"
by(simp add:slice_kind_def Let_def)
thus ?thesis
proof
assume true:"slice_kind S a = (λs. True)⇩√"
with ‹sourcenode a = sourcenode a'› ‹targetnode a ≠ targetnode a'›
‹valid_edge a› ‹valid_edge a'›
have "slice_kind S a' = (λs. False)⇩√"
by(rule slice_kind_only_one_True_edge)
with true show ?thesis by simp
next
assume false:"slice_kind S a = (λs. False)⇩√"
from False ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'›
have "slice_kind S a' = (λs. True)⇩√ ∨ slice_kind S a' = (λs. False)⇩√"
by(simp add:slice_kind_def Let_def)
with false show ?thesis by auto
qed
qed
qed
subsection ‹Observable and silent moves›
inductive silent_move ::
"'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge ⇒
'node ⇒ 'state ⇒ bool" ("_,_ ⊢ '(_,_') -_→⇩τ '(_,_')" [51,50,0,0,50,0,0] 51)
where silent_moveI:
"⟦pred (f a) s; transfer (f a) s = s'; sourcenode a ∉ backward_slice S;
valid_edge a⟧
⟹ S,f ⊢ (sourcenode a,s) -a→⇩τ (targetnode a,s')"
inductive silent_moves ::
"'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge list ⇒
'node ⇒ 'state ⇒ bool" ("_,_ ⊢ '(_,_') =_⇒⇩τ '(_,_')" [51,50,0,0,50,0,0] 51)
where silent_moves_Nil: "S,f ⊢ (n,s) =[]⇒⇩τ (n,s)"
| silent_moves_Cons:
"⟦S,f ⊢ (n,s) -a→⇩τ (n',s'); S,f ⊢ (n',s') =as⇒⇩τ (n'',s'')⟧
⟹ S,f ⊢ (n,s) =a#as⇒⇩τ (n'',s'')"
lemma silent_moves_obs_slice:
"⟦S,f ⊢ (n,s) =as⇒⇩τ (n',s'); nx ∈ obs n' (backward_slice S)⟧
⟹ nx ∈ obs n (backward_slice S)"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f n s a n' s' as n'' s'')
from ‹nx ∈ obs n'' (backward_slice S)›
‹nx ∈ obs n'' (backward_slice S) ⟹ nx ∈ obs n' (backward_slice S)›
have obs:"nx ∈ obs n' (backward_slice S)" by simp
from ‹S,f ⊢ (n,s) -a→⇩τ (n',s')›
have "n = sourcenode a" and "n' = targetnode a" and "valid_edge a"
and "n ∉ (backward_slice S)"
by(auto elim:silent_move.cases)
hence "obs n' (backward_slice S) ⊆ obs n (backward_slice S)"
by simp(rule edge_obs_subset,simp+)
with obs show ?case by blast
qed
lemma silent_moves_preds_transfers_path:
"⟦S,f ⊢ (n,s) =as⇒⇩τ (n',s'); valid_node n⟧
⟹ preds (map f as) s ∧ transfers (map f as) s = s' ∧ n -as→* n'"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by(simp add:path.empty_path)
next
case (silent_moves_Cons S f n s a n' s' as n'' s'')
note IH = ‹valid_node n' ⟹
preds (map f as) s' ∧ transfers (map f as) s' = s'' ∧ n' -as→* n''›
from ‹S,f ⊢ (n,s) -a→⇩τ (n',s')› have "pred (f a) s" and "transfer (f a) s = s'"
and "n = sourcenode a" and "n' = targetnode a" and "valid_edge a"
by(auto elim:silent_move.cases)
from ‹n' = targetnode a› ‹valid_edge a› have "valid_node n'" by simp
from IH[OF this] have "preds (map f as) s'" and "transfers (map f as) s' = s''"
and "n' -as→* n''" by simp_all
from ‹n = sourcenode a› ‹n' = targetnode a› ‹valid_edge a› ‹n' -as→* n''›
have "n -a#as→* n''" by(fastforce intro:Cons_path)
with ‹pred (f a) s› ‹preds (map f as) s'› ‹transfer (f a) s = s'›
‹transfers (map f as) s' = s''› show ?case by simp
qed
lemma obs_silent_moves:
assumes "obs n (backward_slice S) = {n'}"
obtains as where "S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)"
proof(atomize_elim)
from ‹obs n (backward_slice S) = {n'}›
have "n' ∈ obs n (backward_slice S)" by simp
then obtain as where "n -as→* n'"
and "∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)"
and "n' ∈ (backward_slice S)" by(erule obsE)
from ‹n -as→* n'› obtain x where "distance n n' x" and "x ≤ length as"
by(erule every_path_distance)
from ‹distance n n' x› ‹n' ∈ obs n (backward_slice S)›
show "∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)"
proof(induct x arbitrary:n s rule:nat.induct)
fix n s assume "distance n n' 0"
then obtain as' where "n -as'→* n'" and "length as' = 0"
by(auto elim:distance.cases)
hence "n -[]→* n'" by(cases as) auto
hence "n = n'" by(fastforce elim:path.cases)
hence "S,slice_kind S ⊢ (n,s) =[]⇒⇩τ (n',s)" by(fastforce intro:silent_moves_Nil)
thus "∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)" by blast
next
fix x n s
assume "distance n n' (Suc x)" and "n' ∈ obs n (backward_slice S)"
and IH:"⋀n s. ⟦distance n n' x; n' ∈ obs n (backward_slice S)⟧
⟹ ∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)"
from ‹n' ∈ obs n (backward_slice S)›
have "valid_node n" by(rule in_obs_valid)
with ‹distance n n' (Suc x)›
have "n ≠ n'" by(fastforce elim:distance.cases dest:empty_path)
have "n ∉ backward_slice S"
proof
assume isin:"n ∈ backward_slice S"
with ‹valid_node n› have "obs n (backward_slice S) = {n}"
by(fastforce intro!:n_in_obs)
with ‹n' ∈ obs n (backward_slice S)› ‹n ≠ n'› show False by simp
qed
from ‹distance n n' (Suc x)› obtain a where "valid_edge a"
and "n = sourcenode a" and "distance (targetnode a) n' x"
and target:"targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ targetnode a' = nx)"
by -(erule distance_successor_distance,simp+)
from ‹n' ∈ obs n (backward_slice S)›
have "obs n (backward_slice S) = {n'}"
by(rule obs_singleton_element)
with ‹valid_edge a› ‹n ∉ backward_slice S› ‹n = sourcenode a›
have disj:"obs (targetnode a) (backward_slice S) = {} ∨
obs (targetnode a) (backward_slice S) = {n'}"
by -(drule_tac S="backward_slice S" in edge_obs_subset,auto)
from ‹distance (targetnode a) n' x› obtain asx where "targetnode a -asx→* n'"
and "length asx = x" and "∀as'. targetnode a -as'→* n' ⟶ x ≤ length as'"
by(auto elim:distance.cases)
from ‹targetnode a -asx→* n'› ‹n' ∈ (backward_slice S)›
obtain m where "∃m. m ∈ obs (targetnode a) (backward_slice S)"
by(fastforce elim:path_ex_obs)
with disj have "n' ∈ obs (targetnode a) (backward_slice S)" by fastforce
from IH[OF ‹distance (targetnode a) n' x› this,of "transfer (slice_kind S a) s"]
obtain asx' where
moves:"S,slice_kind S ⊢ (targetnode a,transfer (slice_kind S a) s) =asx'⇒⇩τ
(n',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")
case (Update f)
with ‹n ∉ backward_slice S› ‹n = sourcenode a› have "slice_kind S a = ⇑id"
by(fastforce intro:slice_kind_Upd)
thus ?thesis by simp
next
case (Predicate Q)
with ‹n ∉ backward_slice S› ‹n = sourcenode a›
‹n' ∈ obs n (backward_slice S)› ‹distance (targetnode a) n' x›
‹distance n n' (Suc x)› target
have "slice_kind S a = (λs. True)⇩√"
by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
thus ?thesis by simp
qed
hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
by simp_all
with ‹n ∉ backward_slice S› ‹n = sourcenode a› ‹valid_edge a›
have "S,slice_kind S ⊢ (sourcenode a,s) -a→⇩τ
(targetnode a,transfer (slice_kind S a) s)"
by(fastforce intro:silent_moveI)
with moves ‹transfer (slice_kind S a) s = s› ‹n = sourcenode a›
have "S,slice_kind S ⊢ (n,s) =a#asx'⇒⇩τ (n',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)" by blast
qed
qed
inductive observable_move ::
"'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge ⇒
'node ⇒ 'state ⇒ bool" ("_,_ ⊢ '(_,_') -_→ '(_,_')" [51,50,0,0,50,0,0] 51)
where observable_moveI:
"⟦pred (f a) s; transfer (f a) s = s'; sourcenode a ∈ backward_slice S;
valid_edge a⟧
⟹ S,f ⊢ (sourcenode a,s) -a→ (targetnode a,s')"
inductive observable_moves ::
"'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge list ⇒
'node ⇒ 'state ⇒ bool" ("_,_ ⊢ '(_,_') =_⇒ '(_,_')" [51,50,0,0,50,0,0] 51)
where observable_moves_snoc:
"⟦S,f ⊢ (n,s) =as⇒⇩τ (n',s'); S,f ⊢ (n',s') -a→ (n'',s'')⟧
⟹ S,f ⊢ (n,s) =as@[a]⇒ (n'',s'')"
lemma observable_move_notempty:
"⟦S,f ⊢ (n,s) =as⇒ (n',s'); as = []⟧ ⟹ False"
by(induct rule:observable_moves.induct,simp)
lemma silent_move_observable_moves:
"⟦S,f ⊢ (n'',s'') =as⇒ (n',s'); S,f ⊢ (n,s) -a→⇩τ (n'',s'')⟧
⟹ S,f ⊢ (n,s) =a#as⇒ (n',s')"
proof(induct rule:observable_moves.induct)
case (observable_moves_snoc S f nx sx as n' s' a' n'' s'')
from ‹S,f ⊢ (n,s) -a→⇩τ (nx,sx)› ‹S,f ⊢ (nx,sx) =as⇒⇩τ (n',s')›
have "S,f ⊢ (n,s) =a#as⇒⇩τ (n',s')" by(rule silent_moves_Cons)
with ‹S,f ⊢ (n',s') -a'→ (n'',s'')›
have "S,f ⊢ (n,s) =(a#as)@[a']⇒ (n'',s'')"
by -(rule observable_moves.observable_moves_snoc)
thus ?case by simp
qed
lemma observable_moves_preds_transfers_path:
"S,f ⊢ (n,s) =as⇒ (n',s')
⟹ preds (map f as) s ∧ transfers (map f as) s = s' ∧ n -as→* n'"
proof(induct rule:observable_moves.induct)
case (observable_moves_snoc S f n s as n' s' a n'' s'')
have "valid_node n"
proof(cases as)
case Nil
with ‹S,f ⊢ (n,s) =as⇒⇩τ (n',s')› have "n = n'" and "s = s'"
by(auto elim:silent_moves.cases)
with ‹S,f ⊢ (n',s') -a→ (n'',s'')› show ?thesis
by(fastforce elim:observable_move.cases)
next
case (Cons a' as')
with ‹S,f ⊢ (n,s) =as⇒⇩τ (n',s')› show ?thesis
by(fastforce elim:silent_moves.cases silent_move.cases)
qed
with ‹S,f ⊢ (n,s) =as⇒⇩τ (n',s')›
have "preds (map f as) s" and "transfers (map f as) s = s'"
and "n -as→* n'" by(auto dest:silent_moves_preds_transfers_path)
from ‹S,f ⊢ (n',s') -a→ (n'',s'')› have "pred (f a) s'"
and "transfer (f a) s' = s''" and "n' = sourcenode a" and "n'' = targetnode a"
and "valid_edge a"
by(auto elim:observable_move.cases)
from ‹n' = sourcenode a› ‹n'' = targetnode a› ‹valid_edge a›
have "n' -[a]→* n''" by(fastforce intro:path.intros)
with ‹n -as→* n'› have "n -as@[a]→* n''" by(rule path_Append)
with ‹preds (map f as) s› ‹pred (f a) s'› ‹transfer (f a) s' = s''›
‹transfers (map f as) s = s'›
show ?case by(simp add:transfers_split preds_split)
qed
subsection ‹Relevant variables›
inductive_set relevant_vars :: "'node set ⇒ 'node ⇒ 'var set" ("rv _")
for S :: "'node set" and n :: "'node"
where rvI:
"⟦n -as→* n'; n' ∈ backward_slice S; V ∈ Use n';
∀nx ∈ set(sourcenodes as). V ∉ Def nx⟧
⟹ V ∈ rv S n"
lemma rvE:
assumes rv:"V ∈ rv S n"
obtains as n' where "n -as→* n'" and "n' ∈ backward_slice S" and "V ∈ Use n'"
and "∀nx ∈ set(sourcenodes as). V ∉ Def nx"
using rv
by(atomize_elim,auto elim!:relevant_vars.cases)
lemma eq_obs_in_rv:
assumes obs_eq:"obs n (backward_slice S) = obs n' (backward_slice S)"
and "x ∈ rv S n" shows "x ∈ rv S n'"
proof -
from ‹x ∈ rv S n› obtain as m
where "n -as→* m" and "m ∈ backward_slice S" and "x ∈ Use m"
and "∀nx∈set (sourcenodes as). x ∉ Def nx"
by(erule rvE)
from ‹n -as→* m› have "valid_node m" by(fastforce dest:path_valid_node)
from ‹n -as→* m› ‹m ∈ backward_slice S›
have "∃nx as' as''. nx ∈ obs n (backward_slice S) ∧ n -as'→* nx ∧
nx -as''→* m ∧ as = as'@as''"
proof(cases "∀nx ∈ set(sourcenodes as). nx ∉ backward_slice S")
case True
with ‹n -as→* m› ‹m ∈ backward_slice S› have "m ∈ obs n (backward_slice S)"
by -(rule obs_elem)
with ‹n -as→* m› ‹valid_node m› show ?thesis by(blast intro:empty_path)
next
case False
hence "∃nx ∈ set(sourcenodes as). nx ∈ backward_slice S" by simp
then obtain nx' ns ns' where "sourcenodes as = ns@nx'#ns'"
and "nx' ∈ backward_slice S"
and "∀x ∈ set ns. x ∉ backward_slice S"
by(fastforce elim!:split_list_first_propE)
from ‹sourcenodes as = ns@nx'#ns'›
obtain as' a' as'' where "ns = sourcenodes as'"
and "as = as'@a'#as''" and "sourcenode a' = nx'"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹n -as→* m› ‹as = as'@a'#as''› ‹sourcenode a' = nx'›
have "n -as'→* nx'" and "valid_edge a'" and "targetnode a' -as''→* m"
by(fastforce dest:path_split)+
with ‹sourcenode a' = nx'› have "nx' -a'#as''→* m" by(fastforce intro:Cons_path)
from ‹n -as'→* nx'› ‹nx' ∈ backward_slice S›
‹∀x ∈ set ns. x ∉ backward_slice S› ‹ns = sourcenodes as'›
have "nx' ∈ obs n (backward_slice S)"
by(fastforce intro:obs_elem)
with ‹n -as'→* nx'› ‹nx' -a'#as''→* m› ‹as = as'@a'#as''› show ?thesis by blast
qed
then obtain nx as' as'' where "nx ∈ obs n (backward_slice S)"
and "n -as'→* nx" and "nx -as''→* m" and "as = as'@as''"
by blast
from ‹nx ∈ obs n (backward_slice S)› obs_eq
have "nx ∈ obs n' (backward_slice S)" by auto
then obtain asx where "n' -asx→* nx"
and "∀ni ∈ set(sourcenodes asx). ni ∉ backward_slice S"
and "nx ∈ backward_slice S"
by(erule obsE)
from ‹as = as'@as''› ‹∀nx∈set (sourcenodes as). x ∉ Def nx›
have "∀ni∈set (sourcenodes as''). x ∉ Def ni"
by(auto simp:sourcenodes_def)
from ‹∀ni ∈ set(sourcenodes asx). ni ∉ backward_slice S› ‹n' -asx→* nx›
have "∀ni ∈ set(sourcenodes asx). x ∉ Def 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 ∉ backward_slice S;
n' -asx'→* nx⟧
⟹ ∀ni∈set (sourcenodes asx'). x ∉ Def ni›
from ‹n' -ax'#asx'→* nx› have "n' -[]@ax'#asx'→* nx" by simp
hence "targetnode ax' -asx'→* nx" and "n' = sourcenode ax'"
by(fastforce dest:path_split)+
from ‹∀ni∈set (sourcenodes (ax'#asx')). ni ∉ backward_slice S›
have all:"∀ni∈set (sourcenodes asx'). ni ∉ backward_slice S"
and "sourcenode ax' ∉ backward_slice S"
by(auto simp:sourcenodes_def)
from IH[OF all ‹targetnode ax' -asx'→* nx›]
have "∀ni∈set (sourcenodes asx'). x ∉ Def ni" .
with ‹∀ni∈set (sourcenodes as''). x ∉ Def ni›
have "∀ni∈set (sourcenodes (asx'@as'')). x ∉ Def ni"
by(auto simp:sourcenodes_def)
from ‹n' -ax'#asx'→* nx› ‹nx -as''→* m› have "n' -(ax'#asx')@as''→* m"
by-(rule path_Append)
hence "n' -ax'#asx'@as''→* m" by simp
have "x ∉ Def (sourcenode ax')"
proof
assume "x ∈ Def (sourcenode ax')"
with ‹x ∈ Use m› ‹∀ni∈set (sourcenodes (asx'@as'')). x ∉ Def ni›
‹n' -ax'#asx'@as''→* m› ‹n' = sourcenode ax'›
have "n' influences x in m"
by(auto simp:data_dependence_def)
with ‹m ∈ backward_slice S› dd_closed have "n' ∈ backward_slice S"
by(auto simp:dd_closed)
with ‹n' = sourcenode ax'› ‹sourcenode ax' ∉ backward_slice S›
show False by simp
qed
with ‹∀ni∈set (sourcenodes (asx'@as'')). x ∉ Def ni›
show ?case by(simp add:sourcenodes_def)
qed
with ‹∀ni∈set (sourcenodes as''). x ∉ Def ni›
have "∀ni∈set (sourcenodes (asx@as'')). x ∉ Def ni"
by(auto simp:sourcenodes_def)
from ‹n' -asx→* nx› ‹nx -as''→* m› have "n' -asx@as''→* m" by(rule path_Append)
with ‹m ∈ backward_slice S› ‹x ∈ Use m›
‹∀ni∈set (sourcenodes (asx@as'')). x ∉ Def ni› show "x ∈ rv S n'" by -(rule rvI)
qed
lemma closed_eq_obs_eq_rvs:
fixes S :: "'node set"
assumes "valid_node n" and "valid_node n'"
and obs_eq:"obs n (backward_slice S) = obs n' (backward_slice S)"
shows "rv S n = rv S n'"
proof
show "rv S n ⊆ rv S n'"
proof
fix x assume "x ∈ rv S n"
with ‹valid_node n› obs_eq show "x ∈ rv S n'" by -(rule eq_obs_in_rv)
qed
next
show "rv S n' ⊆ rv S n"
proof
fix x assume "x ∈ rv S n'"
with ‹valid_node n'› obs_eq[THEN sym] show "x ∈ rv S n" by -(rule eq_obs_in_rv)
qed
qed
lemma rv_edge_slice_kinds:
assumes "valid_edge a" and "sourcenode a = n" and "targetnode a = n''"
and "∀V∈rv S n. 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 n''. 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 n''"
show "state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V"
proof(cases "V ∈ Def n")
case True
show ?thesis
proof(cases "sourcenode a ∈ backward_slice S")
case True
hence "slice_kind S a = kind a" by(rule slice_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› ‹sourcenode a = n› have "n -[]→* n"
by(fastforce intro:empty_path)
with True ‹sourcenode a = n› have "∀V ∈ Use n. V ∈ rv S n"
by(fastforce intro:rvI simp:sourcenodes_def)
with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹sourcenode a = n›
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'›
have "∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
state_val (transfer (kind a) s') V"
by(rule CFG_edge_transfer_uses_only_Use)
with ‹V ∈ Def n› ‹sourcenode a = n› ‹slice_kind S a = kind a›
show ?thesis by simp
next
case False
from ‹V ∈ rv S n''› obtain xs nx where "n'' -xs→* nx"
and "nx ∈ backward_slice S" and "V ∈ Use nx"
and "∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'" by(erule rvE)
from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''›
‹n'' -xs→* nx›
have "n -a#xs→* nx" by -(rule path.Cons_path)
with ‹V ∈ Def n› ‹V ∈ Use nx› ‹∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'›
have "n influences V in nx" by(fastforce simp:data_dependence_def)
with ‹nx ∈ backward_slice S› have "n ∈ backward_slice S"
by(rule dd_closed)
with ‹sourcenode a = n› False have False by simp
thus ?thesis by simp
qed
next
case False
from ‹V ∈ rv S n''› obtain xs nx where "n'' -xs→* nx"
and "nx ∈ backward_slice S" and "V ∈ Use nx"
and "∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'" by(erule rvE)
from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹n'' -xs→* nx›
have "n -a#xs→* nx" by -(rule path.Cons_path)
from False ‹∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'› ‹sourcenode a = n›
have "∀nx' ∈ set(sourcenodes (a#xs)). V ∉ Def nx'"
by(simp add:sourcenodes_def)
with ‹n -a#xs→* nx› ‹nx ∈ backward_slice S› ‹V ∈ Use nx›
have "V ∈ rv S n" by(rule rvI)
show ?thesis
proof(cases "kind a")
case (Predicate Q)
show ?thesis
proof(cases "sourcenode a ∈ backward_slice S")
case True
with Predicate have "slice_kind S a = (Q)⇩√"
by(simp add:slice_kind_in_slice)
with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
show ?thesis by simp
next
case False
with Predicate obtain Q' where "slice_kind S a = (Q')⇩√"
by -(erule kind_Predicate_notin_slice_slice_kind_Predicate)
with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
show ?thesis by simp
qed
next
case (Update f)
show ?thesis
proof(cases "sourcenode a ∈ backward_slice S")
case True
hence "slice_kind S a = kind a" by(rule slice_kind_in_slice)
from Update have "pred (kind a) s" by simp
with ‹valid_edge a› ‹sourcenode a = n› ‹V ∉ Def n›
have "state_val (transfer (kind a) s) V = state_val s V"
by(fastforce intro:CFG_edge_no_Def_equal)
from Update have "pred (kind a) s'" by simp
with ‹valid_edge a› ‹sourcenode a = n› ‹V ∉ Def n›
have "state_val (transfer (kind a) s') V = state_val s' V"
by(fastforce intro:CFG_edge_no_Def_equal)
with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
‹state_val (transfer (kind a) s) V = state_val s V›
‹slice_kind S a = kind a›
show ?thesis by fastforce
next
case False
with Update have "slice_kind S a = ⇑id" by -(rule slice_kind_Upd)
with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
show ?thesis by fastforce
qed
qed
qed
qed
lemma rv_branching_edges_slice_kinds_False:
assumes "valid_edge a" and "valid_edge ax"
and "sourcenode a = n" and "sourcenode ax = n"
and "targetnode a = n''" and "targetnode ax ≠ n''"
and "preds (slice_kinds S (a#as)) s" and "preds (slice_kinds S (ax#asx)) s'"
and "∀V∈rv S n. state_val s V = state_val s' V"
shows False
proof -
from ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = n› ‹sourcenode ax = n›
‹targetnode a = n''› ‹targetnode ax ≠ n''›
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 = n› ‹sourcenode ax = n›
‹targetnode a = n''› ‹targetnode ax ≠ n''›
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 ∈ backward_slice S")
case True
hence "slice_kind S a = kind a" by(rule slice_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 = n› ‹sourcenode ax = n›
have "slice_kind S ax = kind ax" by(fastforce simp:slice_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' s'" by simp
from ‹valid_edge a› ‹sourcenode a = n› have "n -[]→* n"
by(fastforce intro:empty_path)
with True ‹sourcenode a = n› have "∀V ∈ Use n. V ∈ rv S n"
by(fastforce intro:rvI simp:sourcenodes_def)
with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹sourcenode a = n›
have "∀V ∈ Use (sourcenode a). state_val s V = state_val s' V" by blast
with ‹valid_edge a› ‹pred (kind a) s› have "pred (kind a) s'"
by(rule CFG_edge_Uses_pred_equal)
with ‹kind a = (Q)⇩√› have "Q s'" by simp
with ‹Q' 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)⇩√›
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(fastforce simp:slice_kinds_def)
from ‹kind ax = (Q')⇩√› ‹slice_kind S ax = (P')⇩√›
‹sourcenode a = n› ‹sourcenode ax = n› False
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(fastforce 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
subsection ‹The set ‹WS››
inductive_set WS :: "'node set ⇒ (('node × 'state) × ('node × 'state)) set"
for S :: "'node set"
where WSI:"⟦obs n (backward_slice S) = obs n' (backward_slice S);
∀V ∈ rv S n. state_val s V = state_val s' V;
valid_node n; valid_node n'⟧
⟹ ((n,s),(n',s')) ∈ WS S"
lemma WSD:
"((n,s),(n',s')) ∈ WS S
⟹ obs n (backward_slice S) = obs n' (backward_slice S) ∧
(∀V ∈ rv S n. state_val s V = state_val s' V) ∧
valid_node n ∧ valid_node n'"
by(auto elim:WS.cases)
lemma WS_silent_move:
assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S" and "S,kind ⊢ (n⇩1,s⇩1) -a→⇩τ (n⇩1',s⇩1')"
and "obs n⇩1' (backward_slice S) ≠ {}" shows "((n⇩1',s⇩1'),(n⇩2,s⇩2)) ∈ WS S"
proof -
from ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› have "valid_node n⇩1" and "valid_node n⇩2"
by(auto dest:WSD)
from ‹S,kind ⊢ (n⇩1,s⇩1) -a→⇩τ (n⇩1',s⇩1')› have "sourcenode a = n⇩1"
and "targetnode a = n⇩1'" and "transfer (kind a) s⇩1 = s⇩1'"
and "n⇩1 ∉ backward_slice S" and "valid_edge a" and "pred (kind a) s⇩1"
by(auto elim:silent_move.cases)
from ‹targetnode a = n⇩1'› ‹valid_edge a› have "valid_node n⇩1'"
by(auto simp:valid_node_def)
have "(∃m. obs n⇩1' (backward_slice S) = {m}) ∨ obs n⇩1' (backward_slice S) = {}"
by(rule obs_singleton_disj)
with ‹obs n⇩1' (backward_slice S) ≠ {}› obtain n
where "obs n⇩1' (backward_slice S) = {n}" by fastforce
hence "n ∈ obs n⇩1' (backward_slice S)" by auto
then obtain as where "n⇩1' -as→* n"
and "∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)"
and "n ∈ (backward_slice S)" by(erule obsE)
from ‹n⇩1' -as→* n› ‹valid_edge a› ‹sourcenode a = n⇩1› ‹targetnode a = n⇩1'›
have "n⇩1 -a#as→* n" by(rule Cons_path)
moreover
from ‹∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)› ‹sourcenode a = n⇩1›
‹n⇩1 ∉ backward_slice S›
have "∀nx ∈ set(sourcenodes (a#as)). nx ∉ (backward_slice S)"
by(simp add:sourcenodes_def)
ultimately have "n ∈ obs n⇩1 (backward_slice S)" using ‹n ∈ (backward_slice S)›
by(rule obs_elem)
hence "obs n⇩1 (backward_slice S) = {n}" by(rule obs_singleton_element)
with ‹obs n⇩1' (backward_slice S) = {n}›
have "obs n⇩1 (backward_slice S) = obs n⇩1' (backward_slice S)"
by simp
with ‹valid_node n⇩1› ‹valid_node n⇩1'› have "rv S n⇩1 = rv S n⇩1'"
by(rule closed_eq_obs_eq_rvs)
from ‹n ∈ obs n⇩1 (backward_slice S)› ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S›
have "obs n⇩1 (backward_slice S) = obs n⇩2 (backward_slice S)"
and "∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V"
by(fastforce dest:WSD)+
from ‹obs n⇩1 (backward_slice S) = obs n⇩2 (backward_slice S)›
‹obs n⇩1 (backward_slice S) = {n}› ‹obs n⇩1' (backward_slice S) = {n}›
have "obs n⇩1' (backward_slice S) = obs n⇩2 (backward_slice S)" by simp
have "∀V ∈ rv S n⇩1'. state_val s⇩1' V = state_val s⇩2 V"
proof
fix V assume "V ∈ rv S n⇩1'"
with ‹rv S n⇩1 = rv S n⇩1'› have "V ∈ rv S n⇩1" by simp
then obtain as n' where "n⇩1 -as→* n'" and "n' ∈ (backward_slice S)"
and "V ∈ Use n'" and "∀nx ∈ set(sourcenodes as). V ∉ Def nx"
by(erule rvE)
with ‹n⇩1 ∉ backward_slice S› have "V ∉ Def n⇩1"
by(auto elim:path.cases simp:sourcenodes_def)
with ‹valid_edge a› ‹sourcenode a = n⇩1› ‹pred (kind a) s⇩1›
have "state_val (transfer (kind a) s⇩1) V = state_val s⇩1 V"
by(fastforce intro:CFG_edge_no_Def_equal)
with ‹transfer (kind a) s⇩1 = s⇩1'› have "state_val s⇩1' V = state_val s⇩1 V" by simp
from ‹V ∈ rv S n⇩1› ‹∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V›
have "state_val s⇩1 V = state_val s⇩2 V" by simp
with ‹state_val s⇩1' V = state_val s⇩1 V›
show "state_val s⇩1' V = state_val s⇩2 V" by simp
qed
with ‹obs n⇩1' (backward_slice S) = obs n⇩2 (backward_slice S)›
‹valid_node n⇩1'› ‹valid_node n⇩2› show ?thesis by(fastforce intro:WSI)
qed
lemma WS_silent_moves:
"⟦S,f ⊢ (n⇩1,s⇩1) =as⇒⇩τ (n⇩1',s⇩1'); ((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S; f = kind;
obs n⇩1' (backward_slice S) ≠ {}⟧
⟹ ((n⇩1',s⇩1'),(n⇩2,s⇩2)) ∈ WS S"
proof(induct rule:silent_moves.induct)
case silent_moves_Nil thus ?case by simp
next
case (silent_moves_Cons S f n s a n' s' as n'' s'')
note IH = ‹⟦((n',s'),(n⇩2,s⇩2)) ∈ WS S; f = kind; obs n'' (backward_slice S) ≠ {}⟧
⟹ ((n'',s''),(n⇩2,s⇩2)) ∈ WS S›
from ‹S,f ⊢ (n',s') =as⇒⇩τ (n'',s'')› ‹obs n'' (backward_slice S) ≠ {}›
have "obs n' (backward_slice S) ≠ {}" by(fastforce dest:silent_moves_obs_slice)
with ‹((n,s),(n⇩2,s⇩2)) ∈ WS S› ‹S,f ⊢ (n,s) -a→⇩τ (n',s')› ‹f = kind›
have "((n',s'),(n⇩2,s⇩2)) ∈ WS S" by -(rule WS_silent_move,simp+)
from IH[OF this ‹f = kind› ‹obs n'' (backward_slice S) ≠ {}›]
show ?case .
qed
lemma WS_observable_move:
assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S" and "S,kind ⊢ (n⇩1,s⇩1) -a→ (n⇩1',s⇩1')"
obtains as where "((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S a) s⇩2)) ∈ WS S"
and "S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',transfer (slice_kind S a) s⇩2)"
proof(atomize_elim)
from ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› have "valid_node n⇩1" by(auto dest:WSD)
from ‹S,kind ⊢ (n⇩1,s⇩1) -a→ (n⇩1',s⇩1')› have [simp]:"n⇩1 = sourcenode a"
and [simp]:"n⇩1' = targetnode a" and "pred (kind a) s⇩1"
and "transfer (kind a) s⇩1 = s⇩1'" and "n⇩1 ∈ (backward_slice S)"
and "valid_edge a" and "pred (kind a) s⇩1"
by(auto elim:observable_move.cases)
from ‹valid_edge a› have "valid_node n⇩1'" by(auto simp:valid_node_def)
from ‹valid_node n⇩1› ‹n⇩1 ∈ (backward_slice S)›
have "obs n⇩1 (backward_slice S) = {n⇩1}" by(rule n_in_obs)
with ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› have "obs n⇩2 (backward_slice S) = {n⇩1}"
and "∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V" by(auto dest:WSD)
from ‹valid_node n⇩1› have "n⇩1 -[]→* n⇩1" by(rule empty_path)
with ‹n⇩1 ∈ (backward_slice S)› have "∀V ∈ Use n⇩1. V ∈ rv S n⇩1"
by(fastforce intro:rvI simp:sourcenodes_def)
with ‹∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V›
have "∀V ∈ Use n⇩1. state_val s⇩1 V = state_val s⇩2 V" by blast
with ‹valid_edge a› ‹pred (kind a) s⇩1› have "pred (kind a) s⇩2"
by(fastforce intro:CFG_edge_Uses_pred_equal)
with ‹n⇩1 ∈ (backward_slice S)› have "pred (slice_kind S a) s⇩2"
by(simp add:slice_kind_in_slice)
from ‹n⇩1 ∈ (backward_slice S)› obtain s⇩2'
where "transfer (slice_kind S a) s⇩2 = s⇩2'"
by(simp add:slice_kind_in_slice)
with ‹pred (slice_kind S a) s⇩2› ‹n⇩1 ∈ (backward_slice S)› ‹valid_edge a›
have "S,slice_kind S ⊢ (n⇩1,s⇩2) -a→ (n⇩1',s⇩2')"
by(fastforce intro:observable_moveI)
from ‹obs n⇩2 (backward_slice S) = {n⇩1}›
obtain as where "S,slice_kind S ⊢ (n⇩2,s⇩2) =as⇒⇩τ (n⇩1,s⇩2)"
by(erule obs_silent_moves)
with ‹S,slice_kind S ⊢ (n⇩1,s⇩2) -a→ (n⇩1',s⇩2')›
have "S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',s⇩2')"
by -(rule observable_moves_snoc)
have "∀V ∈ rv S n⇩1'. state_val s⇩1' V = state_val s⇩2' V"
proof
fix V assume rv:"V ∈ rv S n⇩1'"
show "state_val s⇩1' V = state_val s⇩2' V"
proof(cases "V ∈ Def n⇩1")
case True
thus ?thesis
proof(cases "kind a")
case (Update f)
with ‹transfer (kind a) s⇩1 = s⇩1'› have "s⇩1' = f s⇩1" by simp
from Update[THEN sym] ‹n⇩1 ∈ (backward_slice S)›
have "slice_kind S a = ⇑f"
by(fastforce intro:slice_kind_in_slice)
with ‹transfer (slice_kind S a) s⇩2 = s⇩2'› have "s⇩2' = f s⇩2" by simp
from ‹valid_edge a› ‹∀V ∈ Use n⇩1. state_val s⇩1 V = state_val s⇩2 V›
True Update ‹s⇩1' = f s⇩1› ‹s⇩2' = f s⇩2› show ?thesis
by(fastforce dest:CFG_edge_transfer_uses_only_Use)
next
case (Predicate Q)
with ‹transfer (kind a) s⇩1 = s⇩1'› have "s⇩1' = s⇩1" by simp
from Predicate[THEN sym] ‹n⇩1 ∈ (backward_slice S)›
have "slice_kind S a = (Q)⇩√"
by(fastforce intro:slice_kind_in_slice)
with ‹transfer (slice_kind S a) s⇩2 = s⇩2'› have "s⇩2' = s⇩2" by simp
with ‹valid_edge a› ‹∀V ∈ Use n⇩1. state_val s⇩1 V = state_val s⇩2 V›
True Predicate ‹s⇩1' = s⇩1› ‹pred (kind a) s⇩1› ‹pred (kind a) s⇩2›
show ?thesis by(auto dest:CFG_edge_transfer_uses_only_Use)
qed
next
case False
with ‹valid_edge a› ‹transfer (kind a) s⇩1 = s⇩1'›[THEN sym]
‹pred (kind a) s⇩1› ‹pred (kind a) s⇩2›
have "state_val s⇩1' V = state_val s⇩1 V"
by(fastforce intro:CFG_edge_no_Def_equal)
have "state_val s⇩2' V = state_val s⇩2 V"
proof(cases "kind a")
case (Update f)
with ‹n⇩1 ∈ (backward_slice S)› have "slice_kind S a = kind a"
by(fastforce intro:slice_kind_in_slice)
with ‹valid_edge a› ‹transfer (slice_kind S a) s⇩2 = s⇩2'›[THEN sym]
False ‹pred (kind a) s⇩2›
show ?thesis by(fastforce intro:CFG_edge_no_Def_equal)
next
case (Predicate Q)
with ‹transfer (slice_kind S a) s⇩2 = s⇩2'› have "s⇩2 = s⇩2'"
by(cases "slice_kind S a",
auto split:if_split_asm simp:slice_kind_def Let_def)
thus ?thesis by simp
qed
from rv obtain as' nx where "n⇩1' -as'→* nx"
and "nx ∈ (backward_slice S)"
and "V ∈ Use nx" and "∀nx ∈ set(sourcenodes as'). V ∉ Def nx"
by(erule rvE)
from ‹∀nx ∈ set(sourcenodes as'). V ∉ Def nx› False
have "∀nx ∈ set(sourcenodes (a#as')). V ∉ Def nx"
by(auto simp:sourcenodes_def)
from ‹valid_edge a› ‹n⇩1' -as'→* nx› have "n⇩1 -a#as'→* nx"
by(fastforce intro:Cons_path)
with ‹nx ∈ (backward_slice S)› ‹V ∈ Use nx›
‹∀nx ∈ set(sourcenodes (a#as')). V ∉ Def nx›
have "V ∈ rv S n⇩1" by -(rule rvI)
with ‹∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V›
‹state_val s⇩1' V = state_val s⇩1 V› ‹state_val s⇩2' V = state_val s⇩2 V›
show ?thesis by fastforce
qed
qed
with ‹valid_node n⇩1'› have "((n⇩1',s⇩1'),(n⇩1',s⇩2')) ∈ WS S" by(fastforce intro:WSI)
with ‹S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',s⇩2')›
‹transfer (slice_kind S a) s⇩2 = s⇩2'›
show "∃as. ((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S a) s⇩2)) ∈ WS S ∧
S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',transfer (slice_kind S a) s⇩2)"
by blast
qed
definition is_weak_sim ::
"(('node × 'state) × ('node × 'state)) set ⇒ 'node set ⇒ bool"
where "is_weak_sim R S ≡
∀n⇩1 s⇩1 n⇩2 s⇩2 n⇩1' s⇩1' as. ((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ R ∧ S,kind ⊢ (n⇩1,s⇩1) =as⇒ (n⇩1',s⇩1')
⟶ (∃n⇩2' s⇩2' as'. ((n⇩1',s⇩1'),(n⇩2',s⇩2')) ∈ R ∧
S,slice_kind S ⊢ (n⇩2,s⇩2) =as'⇒ (n⇩2',s⇩2'))"
lemma WS_weak_sim:
assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S"
and "S,kind ⊢ (n⇩1,s⇩1) =as⇒ (n⇩1',s⇩1')"
shows "((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S (last as)) s⇩2)) ∈ WS S ∧
(∃as'. S,slice_kind S ⊢ (n⇩2,s⇩2) =as'@[last as]⇒
(n⇩1',transfer (slice_kind S (last as)) s⇩2))"
proof -
from ‹S,kind ⊢ (n⇩1,s⇩1) =as⇒ (n⇩1',s⇩1')› obtain a' as' n' s'
where "S,kind ⊢ (n⇩1,s⇩1) =as'⇒⇩τ (n',s')"
and "S,kind ⊢ (n',s') -a'→ (n⇩1',s⇩1')" and "as = as'@[a']"
by(fastforce elim:observable_moves.cases)
from ‹S,kind ⊢ (n',s') -a'→ (n⇩1',s⇩1')› have "obs n' (backward_slice S) = {n'}"
by(fastforce elim:observable_move.cases intro!:n_in_obs)
hence "obs n' (backward_slice S) ≠ {}" by fast
with ‹S,kind ⊢ (n⇩1,s⇩1) =as'⇒⇩τ (n',s')› ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S›
have "((n',s'),(n⇩2,s⇩2)) ∈ WS S"
by -(rule WS_silent_moves,simp+)
with ‹S,kind ⊢ (n',s') -a'→ (n⇩1',s⇩1')› obtain asx
where "((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S a') s⇩2)) ∈ WS S"
and "S,slice_kind S ⊢ (n⇩2,s⇩2) =asx@[a']⇒
(n⇩1',transfer (slice_kind S a') s⇩2)"
by(fastforce elim:WS_observable_move)
with ‹as = as'@[a']› show
"((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S (last as)) s⇩2)) ∈ WS S ∧
(∃as'. S,slice_kind S ⊢ (n⇩2,s⇩2) =as'@[last as]⇒
(n⇩1',transfer (slice_kind S (last as)) s⇩2))" by simp blast
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 dest:WS_weak_sim simp:is_weak_sim_def)
subsection ‹@{term "n -as→* n'"} and transitive closure of
@{term "S,f ⊢ (n,s) =as⇒⇩τ (n',s')"}›
inductive trans_observable_moves ::
"'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge list ⇒
'node ⇒ 'state ⇒ bool" ("_,_ ⊢ '(_,_') =_⇒* '(_,_')" [51,50,0,0,50,0,0] 51)
where tom_Nil:
"S,f ⊢ (n,s) =[]⇒* (n,s)"
| tom_Cons:
"⟦S,f ⊢ (n,s) =as⇒ (n',s'); S,f ⊢ (n',s') =as'⇒* (n'',s'')⟧
⟹ S,f ⊢ (n,s) =(last as)#as'⇒* (n'',s'')"
definition slice_edges :: "'node set ⇒ 'edge list ⇒ 'edge list"
where "slice_edges S as ≡ [a ← as. sourcenode a ∈ backward_slice S]"
lemma silent_moves_no_slice_edges:
"S,f ⊢ (n,s) =as⇒⇩τ (n',s') ⟹ slice_edges S as = []"
by(induct rule:silent_moves.induct,auto elim:silent_move.cases simp:slice_edges_def)
lemma observable_moves_last_slice_edges:
"S,f ⊢ (n,s) =as⇒ (n',s') ⟹ slice_edges S as = [last as]"
by(induct rule:observable_moves.induct,
fastforce dest:silent_moves_no_slice_edges elim:observable_move.cases
simp:slice_edges_def)
lemma slice_edges_no_nodes_in_slice:
"slice_edges S as = []
⟹ ∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)"
proof(induct as)
case Nil thus ?case by(simp add:slice_edges_def sourcenodes_def)
next
case (Cons a' as')
note IH = ‹slice_edges S as' = [] ⟹
∀nx∈set (sourcenodes as'). nx ∉ backward_slice S›
from ‹slice_edges S (a'#as') = []› have "slice_edges S as' = []"
and "sourcenode a' ∉ backward_slice S"
by(auto simp:slice_edges_def split:if_split_asm)
from IH[OF ‹slice_edges S as' = []›] ‹sourcenode a' ∉ backward_slice S›
show ?case by(simp add:sourcenodes_def)
qed
lemma sliced_path_determ:
"⟦n -as→* n'; n -as'→* n'; slice_edges S as = slice_edges S as';
preds (slice_kinds S as) s; preds (slice_kinds S as') s'; n' ∈ S;
∀V ∈ rv S n. state_val s V = state_val s' V⟧ ⟹ as = as'"
proof(induct arbitrary:as' s s' rule:path.induct)
case (empty_path n)
from ‹slice_edges S [] = slice_edges S as'›
have "∀nx ∈ set(sourcenodes as'). nx ∉ (backward_slice S)"
by(fastforce intro!:slice_edges_no_nodes_in_slice simp:slice_edges_def)
with ‹n -as'→* n› show ?case
proof(induct nx≡"n" as' nx'≡"n" rule:path.induct)
case (Cons_path n'' as a)
from ‹valid_node n› ‹n ∈ S› have "n ∈ backward_slice S" by(rule refl)
with ‹∀nx∈set (sourcenodes (a # as)). nx ∉ backward_slice S›
‹sourcenode a = n›
have False by(simp add:sourcenodes_def)
thus ?case by simp
qed simp
next
case (Cons_path n'' as n' a n)
note IH = ‹⋀as' s s'. ⟦n'' -as'→* n'; slice_edges S as = slice_edges S as';
preds (slice_kinds S as) s; preds (slice_kinds S as') s'; n' ∈ S;
∀V∈rv S n''. state_val s V = state_val s' V⟧ ⟹ as = as'›
show ?case
proof(cases as')
case Nil
with ‹n -as'→* n'› have "n = n'" by fastforce
from Nil ‹slice_edges S (a#as) = slice_edges S as'› ‹sourcenode a = n›
have "n ∉ backward_slice S" by(fastforce simp:slice_edges_def)
from ‹valid_edge a› ‹sourcenode a = n› ‹n = n'› ‹n' ∈ S›
have "n ∈ backward_slice S" by(fastforce intro:refl)
with ‹n = n'› ‹n ∉ backward_slice S› have False by simp
thus ?thesis by simp
next
case (Cons ax asx)
with ‹n -as'→* n'› have "n = sourcenode ax" and "valid_edge ax"
and "targetnode ax -asx→* n'" by(auto elim:path_split_Cons)
show ?thesis
proof(cases "targetnode ax = n''")
case True
with ‹targetnode ax -asx→* n'› have "n'' -asx→* n'" by simp
from ‹valid_edge ax› ‹valid_edge a› ‹n = sourcenode ax› ‹sourcenode a = n›
True ‹targetnode a = n''› have "ax = a" by(fastforce intro:edge_det)
from ‹slice_edges S (a#as) = slice_edges S as'› Cons
‹n = sourcenode ax› ‹sourcenode a = n›
have "slice_edges S as = slice_edges S asx"
by(cases "n ∈ backward_slice S")(auto simp:slice_edges_def)
from ‹preds (slice_kinds S (a#as)) s›
have preds1:"preds (slice_kinds S as) (transfer (slice_kind S a) s)"
by(simp add:slice_kinds_def)
from ‹preds (slice_kinds S as') s'› Cons ‹ax = a›
have preds2:"preds (slice_kinds S asx) (transfer (slice_kind S a) s')"
by(simp add:slice_kinds_def)
from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''›
‹preds (slice_kinds S (a#as)) s› ‹preds (slice_kinds S as') s'›
‹ax = a› Cons ‹∀V∈rv S n. state_val s V = state_val s' V›
have "∀V∈rv S n''. state_val (transfer (slice_kind S a) s) V =
state_val (transfer (slice_kind S a) s') V"
by -(rule rv_edge_slice_kinds,auto)
from IH[OF ‹n'' -asx→* n'› ‹slice_edges S as = slice_edges S asx›
preds1 preds2 ‹n' ∈ S› this] Cons ‹ax = a› show ?thesis by simp
next
case False
with ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = n› ‹n = sourcenode ax›
‹targetnode a = n''› ‹preds (slice_kinds S (a#as)) s›
‹preds (slice_kinds S as') s'› Cons
‹∀V∈rv S n. state_val s V = state_val s' V›
have False by -(erule rv_branching_edges_slice_kinds_False,auto)
thus ?thesis by simp
qed
qed
qed
lemma path_trans_observable_moves:
assumes "n -as→* n'" and "preds (kinds as) s" and "transfers (kinds as) s = s'"
obtains n'' s'' as' as'' where "S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')"
and "S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',s')"
and "slice_edges S as = slice_edges S as''" and "n -as''@as'→* n'"
proof(atomize_elim)
from ‹n -as→* n'› ‹preds (kinds as) s› ‹transfers (kinds as) s = s'›
show "∃n'' s'' as' as''.
S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'') ∧
S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',s') ∧ slice_edges S as = slice_edges S as'' ∧
n -as''@as'→* n'"
proof(induct arbitrary:s rule:path.induct)
case (empty_path n)
from ‹transfers (kinds []) s = s'› have "s = s'" by(simp add:kinds_def)
have "S,kind ⊢ (n,s) =[]⇒* (n,s)" by(rule tom_Nil)
have "S,kind ⊢ (n,s) =[]⇒⇩τ (n,s)" by(rule silent_moves_Nil)
with ‹S,kind ⊢ (n,s) =[]⇒* (n,s)› ‹s = s'› ‹valid_node n›
show ?case
apply(rule_tac x="n" in exI)
apply(rule_tac x="s" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="[]" in exI)
by(fastforce intro:path.empty_path simp:slice_edges_def)
next
case (Cons_path n'' as n' a n)
note IH = ‹⋀s. ⟦preds (kinds as) s; transfers (kinds as) s = s'⟧
⟹ ∃nx s'' as' as''. S,kind ⊢ (n'',s) =slice_edges S as⇒* (nx,s'') ∧
S,kind ⊢ (nx,s'') =as'⇒⇩τ (n',s') ∧
slice_edges S as = slice_edges S as'' ∧ n'' -as''@as'→* n'›
from ‹preds (kinds (a#as)) s› ‹transfers (kinds (a#as)) s = s'›
have "preds (kinds as) (transfer (kind a) s)"
"transfers (kinds as) (transfer (kind a) s) = s'" by(simp_all add:kinds_def)
from IH[OF this] obtain nx sx asx asx'
where "S,kind ⊢ (n'',transfer (kind a) s) =slice_edges S as⇒* (nx,sx)"
and "S,kind ⊢ (nx,sx) =asx⇒⇩τ (n',s')"
and "slice_edges S as = slice_edges S asx'"
and "n'' -asx'@asx→* n'"
by clarsimp
from ‹preds (kinds (a#as)) s› have "pred (kind a) s" by(simp add:kinds_def)
show ?case
proof(cases "n ∈ backward_slice S")
case True
with ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹pred (kind a) s›
have "S,kind ⊢ (n,s) -a→ (n'',transfer (kind a) s)"
by(fastforce intro:observable_moveI)
hence "S,kind ⊢ (n,s) =[]@[a]⇒ (n'',transfer (kind a) s)"
by(fastforce intro:observable_moves_snoc silent_moves_Nil)
with ‹S,kind ⊢ (n'',transfer (kind a) s) =slice_edges S as⇒* (nx,sx)›
have "S,kind ⊢ (n,s) =a#slice_edges S as⇒* (nx,sx)"
by(fastforce dest:tom_Cons)
with ‹S,kind ⊢ (nx,sx) =asx⇒⇩τ (n',s')›
‹slice_edges S as = slice_edges S asx'› ‹n'' -asx'@asx→* n'›
‹sourcenode a = n› ‹valid_edge a› ‹targetnode a = n''› True
show ?thesis
apply(rule_tac x="nx" in exI)
apply(rule_tac x="sx" in exI)
apply(rule_tac x="asx" in exI)
apply(rule_tac x="a#asx'" in exI)
by(auto intro:path.Cons_path simp:slice_edges_def)
next
case False
with ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹pred (kind a) s›
have "S,kind ⊢ (n,s) -a→⇩τ (n'',transfer (kind a) s)"
by(fastforce intro:silent_moveI)
from ‹S,kind ⊢ (n'',transfer (kind a) s) =slice_edges S as⇒* (nx,sx)›
obtain f s'' asx'' where "S,f ⊢ (n'',s'') =asx''⇒* (nx,sx)"
and "f = kind" and "s'' = transfer (kind a) s"
and "asx'' = slice_edges S as" by simp
from ‹S,f ⊢ (n'',s'') =asx''⇒* (nx,sx)› ‹f = kind›
‹asx'' = slice_edges S as› ‹s'' = transfer (kind a) s›
‹S,kind ⊢ (n,s) -a→⇩τ (n'',transfer (kind a) s)›
‹S,kind ⊢ (nx,sx) =asx⇒⇩τ (n',s')› ‹slice_edges S as = slice_edges S asx'›
‹n'' -asx'@asx→* n'› False
show ?thesis
proof(induct rule:trans_observable_moves.induct)
case (tom_Nil S f ni si)
have "S,kind ⊢ (n,s) =[]⇒* (n,s)" by(rule trans_observable_moves.tom_Nil)
from ‹S,kind ⊢ (ni,si) =asx⇒⇩τ (n',s')›
‹S,kind ⊢ (n,s) -a→⇩τ (ni,transfer (kind a) s)›
‹si = transfer (kind a) s›
have "S,kind ⊢ (n,s) =a#asx⇒⇩τ (n',s')"
by(fastforce intro:silent_moves_Cons)
with ‹valid_edge a› ‹sourcenode a = n›
have "n -a#asx→* n'" by(fastforce dest:silent_moves_preds_transfers_path)
with ‹sourcenode a = n› ‹valid_edge a› ‹targetnode a = n''›
‹[] = slice_edges S as› ‹n ∉ backward_slice S›
‹S,kind ⊢ (n,s) =a#asx⇒⇩τ (n',s')›
show ?case
apply(rule_tac x="n" in exI)
apply(rule_tac x="s" in exI)
apply(rule_tac x="a#asx" in exI)
apply(rule_tac x="[]" in exI)
by(fastforce simp:slice_edges_def intro:trans_observable_moves.tom_Nil)
next
case (tom_Cons S f ni si asi ni' si' asi' n'' s'')
from ‹S,f ⊢ (ni,si) =asi⇒ (ni',si')› have "asi ≠ []"
by(fastforce dest:observable_move_notempty)
from ‹S,kind ⊢ (n,s) -a→⇩τ (ni,transfer (kind a) s)›
have "valid_edge a" and "sourcenode a = n" and "targetnode a = ni"
by(auto elim:silent_move.cases)
from ‹S,kind ⊢ (n,s) -a→⇩τ (ni,transfer (kind a) s)› ‹f = kind›
‹si = transfer (kind a) s› ‹S,f ⊢ (ni,si) =asi⇒ (ni',si')›
have "S,f ⊢ (n,s) =a#asi⇒ (ni',si')"
by(fastforce intro:silent_move_observable_moves)
with ‹S,f ⊢ (ni',si') =asi'⇒* (n'',s'')›
have "S,f ⊢ (n,s) =(last (a#asi))#asi'⇒* (n'',s'')"
by -(rule trans_observable_moves.tom_Cons)
with ‹f = kind› ‹last asi # asi' = slice_edges S as› ‹n ∉ backward_slice S›
‹S,kind ⊢ (n'',s'') =asx⇒⇩τ (n',s')› ‹sourcenode a = n› ‹asi ≠ []›
‹ni -asx'@asx→* n'› ‹slice_edges S as = slice_edges S asx'›
‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = ni›
show ?case
apply(rule_tac x="n''" in exI)
apply(rule_tac x="s''" in exI)
apply(rule_tac x="asx" in exI)
apply(rule_tac x="a#asx'" in exI)
by(auto intro:path.Cons_path simp:slice_edges_def)
qed
qed
qed
qed
lemma WS_weak_sim_trans:
assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S"
and "S,kind ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')" and "as ≠ []"
shows "((n⇩1',s⇩1'),(n⇩1',transfers (slice_kinds S as) s⇩2)) ∈ WS S ∧
S,slice_kind S ⊢ (n⇩2,s⇩2) =as⇒* (n⇩1',transfers (slice_kinds S as) s⇩2)"
proof -
obtain f where "f = kind" by simp
with ‹S,kind ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')›
have "S,f ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')" by simp
from ‹S,f ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')› ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› ‹as ≠ []› ‹f = kind›
show "((n⇩1',s⇩1'),(n⇩1',transfers (slice_kinds S as) s⇩2)) ∈ WS S ∧
S,slice_kind S ⊢ (n⇩2,s⇩2) =as⇒* (n⇩1',transfers (slice_kinds S as) s⇩2)"
proof(induct arbitrary:n⇩2 s⇩2 rule:trans_observable_moves.induct)
case tom_Nil thus ?case by simp
next
case (tom_Cons S f n s as n' s' as' n'' s'')
note IH = ‹⋀n⇩2 s⇩2. ⟦((n',s'),(n⇩2,s⇩2)) ∈ WS S; as' ≠ []; f = kind⟧
⟹ ((n'',s''),(n'',transfers (slice_kinds S as') s⇩2)) ∈ WS S ∧
S,slice_kind S ⊢ (n⇩2,s⇩2) =as'⇒* (n'',transfers (slice_kinds S as') s⇩2)›
from ‹S,f ⊢ (n,s) =as⇒ (n',s')›
obtain asx ax nx sx where "S,f ⊢ (n,s) =asx⇒⇩τ (nx,sx)"
and "S,f ⊢ (nx,sx) -ax→ (n',s')" and "as = asx@[ax]"
by(fastforce elim:observable_moves.cases)
from ‹S,f ⊢ (nx,sx) -ax→ (n',s')› have "obs nx (backward_slice S) = {nx}"
by(fastforce intro!:n_in_obs elim:observable_move.cases)
with ‹S,f ⊢ (n,s) =asx⇒⇩τ (nx,sx)› ‹((n,s),(n⇩2,s⇩2)) ∈ WS S› ‹f = kind›
have "((nx,sx),(n⇩2,s⇩2)) ∈ WS S" by(fastforce intro:WS_silent_moves)
with ‹S,f ⊢ (nx,sx) -ax→ (n',s')› ‹f = kind›
obtain asx' where "((n',s'),(n',transfer (slice_kind S ax) s⇩2)) ∈ WS S"
and "S,slice_kind S ⊢ (n⇩2,s⇩2) =asx'@[ax]⇒
(n',transfer (slice_kind S ax) s⇩2)"
by(fastforce elim:WS_observable_move)
show ?case
proof(cases "as' = []")
case True
with ‹S,f ⊢ (n',s') =as'⇒* (n'',s'')› have "n' = n'' ∧ s' = s''"
by(fastforce elim:trans_observable_moves.cases dest:observable_move_notempty)
from ‹S,slice_kind S ⊢ (n⇩2,s⇩2) =asx'@[ax]⇒
(n',transfer (slice_kind S ax) s⇩2)›
have "S,slice_kind S ⊢ (n⇩2,s⇩2) =(last (asx'@[ax]))#[]⇒*
(n',transfer (slice_kind S ax) s⇩2)"
by(fastforce intro:trans_observable_moves.intros)
with ‹((n',s'),(n',transfer (slice_kind S ax) s⇩2)) ∈ WS S› ‹as = asx@[ax]›
‹n' = n'' ∧ s' = s''› True
show ?thesis by(fastforce simp:slice_kinds_def)
next
case False
from IH[OF ‹((n',s'),(n',transfer (slice_kind S ax) s⇩2)) ∈ WS S› this
‹f = kind›]
have "((n'',s''),(n'',transfers (slice_kinds S as')
(transfer (slice_kind S ax) s⇩2))) ∈ WS S"
and "S,slice_kind S ⊢ (n',transfer (slice_kind S ax) s⇩2)
=as'⇒* (n'',transfers (slice_kinds S as')
(transfer (slice_kind S ax) s⇩2))" by simp_all
with ‹S,slice_kind S ⊢ (n⇩2,s⇩2) =asx'@[ax]⇒
(n',transfer (slice_kind S ax) s⇩2)›
have "S,slice_kind S ⊢ (n⇩2,s⇩2) =(last (asx'@[ax]))#as'⇒*
(n'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s⇩2))"
by(fastforce intro:trans_observable_moves.tom_Cons)
with ‹((n'',s''),(n'',transfers (slice_kinds S as')
(transfer (slice_kind S ax) s⇩2))) ∈ WS S› False ‹as = asx@[ax]›
show ?thesis by(fastforce simp:slice_kinds_def)
qed
qed
qed
lemma transfers_slice_kinds_slice_edges:
"transfers (slice_kinds S (slice_edges S as)) s = transfers (slice_kinds S as) s"
proof(induct as arbitrary:s)
case Nil thus ?case by(simp add:slice_kinds_def slice_edges_def)
next
case (Cons a' as')
note IH = ‹⋀s. transfers (slice_kinds S (slice_edges S as')) s =
transfers (slice_kinds S as') s›
show ?case
proof(cases "sourcenode a' ∈ backward_slice S")
case True
hence eq:"transfers (slice_kinds S (slice_edges S (a'#as'))) s
= transfers (slice_kinds S (slice_edges S as'))
(transfer (slice_kind S a') s)"
by(simp add:slice_edges_def slice_kinds_def)
have "transfers (slice_kinds S (a'#as')) s
= transfers (slice_kinds S as') (transfer (slice_kind S a') s)"
by(simp add:slice_kinds_def)
with eq IH[of "transfer (slice_kind S a') s"] show ?thesis by simp
next
case False
hence eq:"transfers (slice_kinds S (slice_edges S (a'#as'))) s
= transfers (slice_kinds S (slice_edges S as')) s"
by(simp add:slice_edges_def slice_kinds_def)
from False have "transfer (slice_kind S a') s = s"
by(cases "kind a'",auto simp:slice_kind_def Let_def)
hence "transfers (slice_kinds S (a'#as')) s
= transfers (slice_kinds S as') s"
by(simp add:slice_kinds_def)
with eq IH[of s] show ?thesis by simp
qed
qed
lemma trans_observable_moves_preds:
assumes "S,f ⊢ (n,s) =as⇒* (n',s')" and "valid_node n"
obtains as' where "preds (map f as') s" and "slice_edges S as' = as"
and "n -as'→* n'"
proof(atomize_elim)
from ‹S,f ⊢ (n,s) =as⇒* (n',s')› ‹valid_node n›
show "∃as'. preds (map f as') s ∧ slice_edges S as' = as ∧ n -as'→* n'"
proof(induct rule:trans_observable_moves.induct)
case tom_Nil thus ?case
by(rule_tac x="[]" in exI,fastforce intro:empty_path simp:slice_edges_def)
next
case (tom_Cons S f n s as n' s' as' n'' s'')
note IH = ‹valid_node n'
⟹ ∃asx. preds (map f asx) s' ∧ slice_edges S asx = as' ∧ n' -asx→* n''›
from ‹S,f ⊢ (n,s) =as⇒ (n',s')›
have "preds (map f as) s" and "transfers (map f as) s = s'"
and "n -as→* n'"
by(fastforce dest:observable_moves_preds_transfers_path)+
from ‹n -as→* n'› have "valid_node n'" by(fastforce dest:path_valid_node)
from ‹S,f ⊢ (n,s) =as⇒ (n',s')› have "slice_edges S as = [last as]"
by(rule observable_moves_last_slice_edges)
from IH[OF ‹valid_node n'›]
obtain asx where "preds (map f asx) s'" and "slice_edges S asx = as'"
and "n' -asx→* n''"
by blast
from ‹n -as→* n'› ‹n' -asx→* n''› have "n -as@asx→* n''" by(rule path_Append)
from ‹preds (map f asx) s'› ‹transfers (map f as) s = s'›[THEN sym]
‹preds (map f as) s›
have "preds (map f (as@asx)) s" by(simp add:preds_split)
with ‹slice_edges S as = [last as]› ‹slice_edges S asx = as'›
‹n -as@asx→* n''› show ?case
by(rule_tac x="as@asx" in exI,auto simp:slice_edges_def)
qed
qed
lemma exists_sliced_path_preds:
assumes "n -as→* n'" and "slice_edges S as = []" and "n' ∈ backward_slice S"
obtains as' where "n -as'→* n'" and "preds (slice_kinds S as') s"
and "slice_edges S as' = []"
proof(atomize_elim)
from ‹slice_edges S as = []›
have "∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)"
by(rule slice_edges_no_nodes_in_slice)
with ‹n -as→* n'› ‹n' ∈ backward_slice S› have "n' ∈ obs n (backward_slice S)"
by -(rule obs_elem)
hence "obs n (backward_slice S) = {n'}" by(rule obs_singleton_element)
from ‹n -as→* n'› have "valid_node n" and "valid_node n'"
by(fastforce dest:path_valid_node)+
from ‹n -as→* n'› obtain x where "distance n n' x" and "x ≤ length as"
by(erule every_path_distance)
from ‹distance n n' x› ‹obs n (backward_slice S) = {n'}›
show "∃as'. n -as'→* n' ∧ preds (slice_kinds S as') s ∧
slice_edges S as' = []"
proof(induct x arbitrary:n rule:nat.induct)
case zero
from ‹distance n n' 0› have "n = n'" by(fastforce elim:distance.cases)
with ‹valid_node n'› show ?case
by(rule_tac x="[]" in exI,
auto intro:empty_path simp:slice_kinds_def slice_edges_def)
next
case (Suc x)
note IH = ‹⋀n. ⟦distance n n' x; obs n (backward_slice S) = {n'}⟧
⟹ ∃as'. n -as'→* n' ∧ preds (slice_kinds S as') s ∧
slice_edges S as' = []›
from ‹distance n n' (Suc x)› obtain a
where "valid_edge a" and "n = sourcenode a"
and "distance (targetnode a) n' x"
and target:"targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ targetnode a' = nx)"
by(auto elim:distance_successor_distance)
have "n ∉ backward_slice S"
proof
assume "n ∈ backward_slice S"
from ‹valid_edge a› ‹n = sourcenode a› have "valid_node n" by simp
with ‹n ∈ backward_slice S› have "obs n (backward_slice S) = {n}"
by -(rule n_in_obs)
with ‹obs n (backward_slice S) = {n'}› have "n = n'" by simp
with ‹valid_node n› have "n -[]→* n'" by(fastforce intro:empty_path)
with ‹distance n n' (Suc x)› show False
by(fastforce elim:distance.cases)
qed
from ‹distance (targetnode a) n' x› ‹n' ∈ backward_slice S›
obtain m where "m ∈ obs (targetnode a) (backward_slice S)"
by(fastforce elim:distance.cases path_ex_obs)
from ‹valid_edge a› ‹n ∉ backward_slice S› ‹n = sourcenode a›
have "obs (targetnode a) (backward_slice S) ⊆
obs (sourcenode a) (backward_slice S)"
by -(rule edge_obs_subset,auto)
with ‹m ∈ obs (targetnode a) (backward_slice S)› ‹n = sourcenode a›
‹obs n (backward_slice S) = {n'}›
have "n' ∈ obs (targetnode a) (backward_slice S)" by auto
hence "obs (targetnode a) (backward_slice S) = {n'}"
by(rule obs_singleton_element)
from IH[OF ‹distance (targetnode a) n' x› this]
obtain as where "targetnode a -as→* n'" and "preds (slice_kinds S as) s"
and "slice_edges S as = []" by blast
from ‹targetnode a -as→* n'› ‹valid_edge a› ‹n = sourcenode a›
have "n -a#as→* n'" by(fastforce intro:Cons_path)
from ‹slice_edges S as = []› ‹n ∉ backward_slice S› ‹n = sourcenode a›
have "slice_edges S (a#as) = []" by(simp add:slice_edges_def)
show ?case
proof(cases "kind a")
case (Update f)
with ‹n ∉ backward_slice S› ‹n = sourcenode a› have "slice_kind S a = ⇑id"
by(fastforce intro:slice_kind_Upd)
hence "transfer (slice_kind S a) s = s" and "pred (slice_kind S a) s"
by simp_all
with ‹preds (slice_kinds S as) s› have "preds (slice_kinds S (a#as)) s"
by(simp add:slice_kinds_def)
with ‹n -a#as→* n'› ‹slice_edges S (a#as) = []› show ?thesis
by blast
next
case (Predicate Q)
with ‹n ∉ backward_slice S› ‹n = sourcenode a› ‹distance n n' (Suc x)›
‹obs n (backward_slice S) = {n'}› ‹distance (targetnode a) n' x›
‹targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') n' x ∧
valid_edge a' ∧ targetnode a' = nx)›
have "slice_kind S a = (λs. True)⇩√"
by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
hence "transfer (slice_kind S a) s = s" and "pred (slice_kind S a) s"
by simp_all
with ‹preds (slice_kinds S as) s› have "preds (slice_kinds S (a#as)) s"
by(simp add:slice_kinds_def)
with ‹n -a#as→* n'› ‹slice_edges S (a#as) = []› show ?thesis by blast
qed
qed
qed
theorem fundamental_property_of_static_slicing:
assumes path:"n -as→* n'" and preds:"preds (kinds as) s" and "n' ∈ S"
obtains as' where "preds (slice_kinds S as') s"
and "(∀V ∈ Use n'. state_val (transfers (slice_kinds S as') s) V =
state_val (transfers (kinds as) s) V)"
and "slice_edges S as = slice_edges S as'" and "n -as'→* n'"
proof(atomize_elim)
from path preds obtain n'' s'' as' as''
where "S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')"
and "S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)"
and "slice_edges S as = slice_edges S as''"
and "n -as''@as'→* n'"
by -(erule_tac S="S" in path_trans_observable_moves,auto)
from path have "valid_node n" and "valid_node n'"
by(fastforce dest:path_valid_node)+
from ‹valid_node n› have "((n,s),(n,s)) ∈ WS S" by(fastforce intro:WSI)
from ‹valid_node n'› ‹n' ∈ S› have "obs n' (backward_slice S) = {n'}"
by(fastforce intro!:n_in_obs refl)
from ‹valid_node n'› have "n'-[]→* n'" by(fastforce intro:empty_path)
with ‹valid_node n'› ‹n' ∈ S› have "∀V ∈ Use n'. V ∈ rv S n'"
by(fastforce intro:rvI refl simp:sourcenodes_def)
show "∃as'. preds (slice_kinds S as') s ∧
(∀V ∈ Use n'. state_val (transfers (slice_kinds S as') s) V =
state_val (transfers (kinds as) s) V) ∧
slice_edges S as = slice_edges S as' ∧ n -as'→* n'"
proof(cases "slice_edges S as = []")
case True
hence "preds (slice_kinds S []) s" and "slice_edges S [] = slice_edges S as"
by(simp_all add:slice_kinds_def slice_edges_def)
from ‹S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')› True
have "n = n''" and "s = s''"
by(fastforce elim:trans_observable_moves.cases)+
with ‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
have "S,kind ⊢ (n,s) =as'⇒⇩τ (n',transfers (kinds as) s)" by simp
with ‹valid_node n› have "n -as'→* n'"
by(fastforce dest:silent_moves_preds_transfers_path)
from ‹S,kind ⊢ (n,s) =as'⇒⇩τ (n',transfers (kinds as) s)›
have "slice_edges S as' = []" by(fastforce dest:silent_moves_no_slice_edges)
with ‹n -as'→* n'› ‹valid_node n'› ‹n' ∈ S› obtain asx
where "n -asx→* n'" and "preds (slice_kinds S asx) s"
and "slice_edges S asx = []"
by -(erule exists_sliced_path_preds,auto intro:refl)
from ‹S,kind ⊢ (n,s) =as'⇒⇩τ (n',transfers (kinds as) s)›
‹((n,s),(n,s)) ∈ WS S› ‹obs n' (backward_slice S) = {n'}›
have "((n',transfers (kinds as) s),(n,s)) ∈ WS S"
by(fastforce intro:WS_silent_moves)
with True have "∀V ∈ rv S n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S (slice_edges S as)) s) V"
by(fastforce dest:WSD simp:slice_edges_def slice_kinds_def)
with ‹∀V ∈ Use n'. V ∈ rv S n'›
have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S (slice_edges S as)) s) V" by simp
with ‹slice_edges S asx = []› ‹slice_edges S [] = slice_edges S as›
have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S (slice_edges S asx)) s) V"
by(simp add:slice_edges_def)
hence "∀V ∈ Use n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S asx) s) V"
by(simp add:transfers_slice_kinds_slice_edges)
with ‹n -asx→* n'› ‹preds (slice_kinds S asx) s›
‹slice_edges S asx = []› ‹slice_edges S [] = slice_edges S as›
show ?thesis
by(rule_tac x="asx" in exI,simp add:slice_edges_def)
next
case False
with ‹S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')› ‹((n,s),(n,s)) ∈ WS S›
have "((n'',s''),(n'',transfers (slice_kinds S (slice_edges S as)) s)) ∈ WS S"
"S,slice_kind S ⊢ (n,s) =slice_edges S as⇒*
(n'',transfers (slice_kinds S (slice_edges S as)) s)"
by(fastforce dest:WS_weak_sim_trans)+
from ‹S,slice_kind S ⊢ (n,s) =slice_edges S as⇒*
(n'',transfers (slice_kinds S (slice_edges S as)) s)›
‹valid_node n›
obtain asx where "preds (slice_kinds S asx) s"
and "slice_edges S asx = slice_edges S as"
and "n -asx→* n''"
by(fastforce elim:trans_observable_moves_preds simp:slice_kinds_def)
from ‹n -asx→* n''› have "valid_node n''" by(fastforce dest:path_valid_node)
with ‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
have "n'' -as'→* n'"
by(fastforce dest:silent_moves_preds_transfers_path)
from ‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
have "slice_edges S as' = []" by(fastforce dest:silent_moves_no_slice_edges)
with ‹n'' -as'→* n'› ‹valid_node n'› ‹n' ∈ S› obtain asx'
where "n'' -asx'→* n'" and "slice_edges S asx' = []"
and "preds (slice_kinds S asx') (transfers (slice_kinds S asx) s)"
by -(erule exists_sliced_path_preds,auto intro:refl)
from ‹n -asx→* n''› ‹n'' -asx'→* n'› have "n -asx@asx'→* n'"
by(rule path_Append)
from ‹slice_edges S asx = slice_edges S as› ‹slice_edges S asx' = []›
have "slice_edges S as = slice_edges S (asx@asx')"
by(auto simp:slice_edges_def)
from ‹preds (slice_kinds S asx') (transfers (slice_kinds S asx) s)›
‹preds (slice_kinds S asx) s›
have "preds (slice_kinds S (asx@asx')) s"
by(simp add:slice_kinds_def preds_split)
from ‹obs n' (backward_slice S) = {n'}›
‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
‹((n'',s''),(n'',transfers (slice_kinds S (slice_edges S as)) s)) ∈ WS S›
have "((n',transfers (kinds as) s),
(n'',transfers (slice_kinds S (slice_edges S as)) s)) ∈ WS S"
by(fastforce intro:WS_silent_moves)
hence "∀V ∈ rv S n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S (slice_edges S as)) s) V"
by(fastforce dest:WSD)
with ‹∀V ∈ Use n'. V ∈ rv S n'› ‹slice_edges S asx = slice_edges S as›
have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S (slice_edges S asx)) s) V"
by fastforce
with ‹slice_edges S asx' = []›
have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S (slice_edges S (asx@asx'))) s) V"
by(auto simp:slice_edges_def)
hence "∀V ∈ Use n'. state_val (transfers (kinds as) s) V =
state_val (transfers (slice_kinds S (asx@asx')) s) V"
by(simp add:transfers_slice_kinds_slice_edges)
with ‹preds (slice_kinds S (asx@asx')) s› ‹n -asx@asx'→* n'›
‹slice_edges S as = slice_edges S (asx@asx')›
show ?thesis by simp blast
qed
qed
end
subsection ‹The fundamental property of (static) slicing related to the semantics›
locale BackwardSlice_wf =
BackwardSlice sourcenode targetnode kind valid_edge Entry Def Use state_val
backward_slice +
CFG_semantics_wf sourcenode targetnode kind valid_edge Entry sem identifies
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and backward_slice :: "'node set ⇒ 'node set"
and sem :: "'com ⇒ 'state ⇒ 'com ⇒ 'state ⇒ bool"
("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
and identifies :: "'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51, 0] 80)
begin
theorem fundamental_property_of_path_slicing_semantically:
assumes "n ≜ c" and "⟨c,s⟩ ⇒ ⟨c',s'⟩"
obtains n' as where "n -as→* n'" and "preds (slice_kinds {n'} as) s" and "n' ≜ c'"
and "∀V ∈ Use n'. state_val (transfers (slice_kinds {n'} as) s) V = state_val s' V"
proof(atomize_elim)
from ‹n ≜ c› ‹⟨c,s⟩ ⇒ ⟨c',s'⟩› obtain n' as where "n -as→* n'"
and "transfers (kinds as) s = s'" and "preds (kinds as) s" and "n' ≜ c'"
by(fastforce dest:fundamental_property)
from ‹n -as→* n'› ‹preds (kinds as) s› obtain as'
where "preds (slice_kinds {n'} as') s"
and vals:"∀V ∈ Use n'. state_val (transfers (slice_kinds {n'} as') s) V =
state_val (transfers (kinds as) s) V" and "n -as'→* n'"
by -(erule fundamental_property_of_static_slicing,auto)
from ‹transfers (kinds as) s = s'› vals have "∀V ∈ Use n'.
state_val (transfers (slice_kinds {n'} as') s) V = state_val s' V"
by simp
with ‹preds (slice_kinds {n'} as') s› ‹n -as'→* n'› ‹ n' ≜ c'›
show "∃as n'. n -as→* n' ∧ preds (slice_kinds {n'} as) s ∧ n' ≜ c' ∧
(∀V∈Use n'. state_val (transfers (slice_kinds {n'} as) s) V = state_val s' V)"
by blast
qed
end
end