# Theory Slice

```section ‹Static backward slice›

theory Slice
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"

lemma slice_kind_Upd:
"⟦sourcenode a ∉ backward_slice S; kind a = ⇑f⟧ ⟹ slice_kind S a = ⇑id"

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)⇩√"

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)⇩√"

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)"
with det have "Q' = (λs. False)" by(simp add:fun_eq_iff)
with True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'› show ?thesis
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)⇩√"
from True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'›
have "slice_kind S a' = (Q')⇩√"
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)⇩√"
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)⇩√"
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'›
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›
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"
from ‹slice_kind S a = kind a› ‹preds (slice_kinds S (a#asx)) s'›
have "pred (kind a) s'"
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'"
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)⇩√"
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"
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'"
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)"
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"
from ‹n⇩1 ∈ (backward_slice S)› obtain s⇩2'
where "transfer (slice_kind S a) s⇩2 = s⇩2'"
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›
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›
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```