Up to index of Isabelle/HOL/Jinja/Slicing
theory Sliceheader {* \isaheader{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 {* @{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 \<Up>f => \<Up>id | (Q)⇣\<surd> =>
(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)⇣\<surd> else (λs. False)⇣\<surd>))
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)⇣\<surd> else (λs. False)⇣\<surd>
))
))
))"
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 = \<Up>f|] ==> slice_kind S a = \<Up>id"
by(simp add:slice_kind_def)
lemma slice_kind_Pred_empty_obs_SOME:
"[|sourcenode a ∉ backward_slice S; kind a = (Q)⇣\<surd>;
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)⇣\<surd>"
by(simp add:slice_kind_def)
lemma slice_kind_Pred_empty_obs_not_SOME:
"[|sourcenode a ∉ backward_slice S; kind a = (Q)⇣\<surd>;
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)⇣\<surd>"
by(simp add:slice_kind_def)
lemma slice_kind_Pred_obs_nearer_SOME:
assumes "sourcenode a ∉ backward_slice S" and "kind a = (Q)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>"
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)⇣\<surd>` 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)⇣\<surd>" and "sourcenode a ∉ backward_slice S"
obtains Q' where "slice_kind S a = (Q')⇣\<surd>" and "Q' = (λs. False) ∨ Q' = (λs. True)"
proof(atomize_elim)
show "∃Q'. slice_kind S a = (Q')⇣\<surd> ∧ (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)⇣\<surd>`
`obs (sourcenode a) (backward_slice S) = {}`
have "slice_kind S a = (λs. True)⇣\<surd>" by(rule slice_kind_Pred_empty_obs_SOME)
thus ?thesis by simp
next
case False
with `sourcenode a ∉ backward_slice S` `kind a = (Q)⇣\<surd>`
`obs (sourcenode a) (backward_slice S) = {}`
have "slice_kind S a = (λs. False)⇣\<surd>"
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)⇣\<surd>`
`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)⇣\<surd>"
by(rule slice_kind_Pred_obs_nearer_SOME)
thus ?thesis by simp
next
case False
with `sourcenode a ∉ backward_slice S` `kind a = (Q)⇣\<surd>`
`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)⇣\<surd>"
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)⇣\<surd>` False
`m ∈ obs (sourcenode a) (backward_slice S)`
have "slice_kind S a = (λs. False)⇣\<surd>"
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)⇣\<surd>"
shows "slice_kind S a' = (λs. False)⇣\<surd>"
proof -
from assms obtain Q Q' where "kind a = (Q)⇣\<surd>"
and "kind a' = (Q')⇣\<surd>" 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)⇣\<surd>` `kind a = (Q)⇣\<surd>` 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')⇣\<surd>` `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)⇣\<surd>`
`kind a = (Q)⇣\<surd>`
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:split_if_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')⇣\<surd>`
`sourcenode a = sourcenode a'` show ?thesis
by(auto simp:slice_kind_def Let_def fun_eq_iff split:split_if_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)⇣\<surd>` `kind a = (Q)⇣\<surd>`
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:split_if_asm)
show ?thesis
proof(cases "distance (targetnode a') m x")
case False
with `sourcenode a ∉ backward_slice S` `kind a' = (Q')⇣\<surd>`
`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')⇣\<surd>` `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)⇣\<surd>" and "slice_kind S a' = (Q')⇣\<surd>"
and "∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s)"
proof(atomize_elim)
from assms obtain Q Q'
where "kind a = (Q)⇣\<surd>" and "kind a' = (Q')⇣\<surd>"
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)⇣\<surd> ∧ slice_kind S a' = (Q')⇣\<surd> ∧
(∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
proof(cases "sourcenode a ∈ backward_slice S")
case True
with `kind a = (Q)⇣\<surd>` have "slice_kind S a = (Q)⇣\<surd>"
by(simp add:slice_kind_def Let_def)
from True `kind a' = (Q')⇣\<surd>` `sourcenode a = sourcenode a'`
have "slice_kind S a' = (Q')⇣\<surd>"
by(simp add:slice_kind_def Let_def)
with `slice_kind S a = (Q)⇣\<surd>` det show ?thesis by blast
next
case False
with `kind a = (Q)⇣\<surd>`
have "slice_kind S a = (λs. True)⇣\<surd> ∨ slice_kind S a = (λs. False)⇣\<surd>"
by(simp add:slice_kind_def Let_def)
thus ?thesis
proof
assume true:"slice_kind S a = (λs. True)⇣\<surd>"
with `sourcenode a = sourcenode a'` `targetnode a ≠ targetnode a'`
`valid_edge a` `valid_edge a'`
have "slice_kind S a' = (λs. False)⇣\<surd>"
by(rule slice_kind_only_one_True_edge)
with true show ?thesis by simp
next
assume false:"slice_kind S a = (λs. False)⇣\<surd>"
from False `kind a' = (Q')⇣\<surd>` `sourcenode a = sourcenode a'`
have "slice_kind S a' = (λs. True)⇣\<surd> ∨ slice_kind S a' = (λs. False)⇣\<surd>"
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" ("_,_ \<turnstile> '(_,_') -_->⇣τ '(_,_')" [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 \<turnstile> (sourcenode a,s) -a->⇣τ (targetnode a,s')"
inductive silent_moves ::
"'node set => ('edge => 'state edge_kind) => 'node => 'state => 'edge list =>
'node => 'state => bool" ("_,_ \<turnstile> '(_,_') =_=>⇣τ '(_,_')" [51,50,0,0,50,0,0] 51)
where silent_moves_Nil: "S,f \<turnstile> (n,s) =[]=>⇣τ (n,s)"
| silent_moves_Cons:
"[|S,f \<turnstile> (n,s) -a->⇣τ (n',s'); S,f \<turnstile> (n',s') =as=>⇣τ (n'',s'')|]
==> S,f \<turnstile> (n,s) =a#as=>⇣τ (n'',s'')"
lemma silent_moves_obs_slice:
"[|S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (n,s) =[]=>⇣τ (n',s)" by(fastforce intro:silent_moves_Nil)
thus "∃as. S,slice_kind S \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 = \<Up>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)⇣\<surd>"
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 \<turnstile> (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 \<turnstile> (n,s) =a#asx'=>⇣τ (n',s)"
by(fastforce intro:silent_moves_Cons)
thus "∃as. S,slice_kind S \<turnstile> (n,s) =as=>⇣τ (n',s)" by blast
qed
qed
inductive observable_move ::
"'node set => ('edge => 'state edge_kind) => 'node => 'state => 'edge =>
'node => 'state => bool" ("_,_ \<turnstile> '(_,_') -_-> '(_,_')" [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 \<turnstile> (sourcenode a,s) -a-> (targetnode a,s')"
inductive observable_moves ::
"'node set => ('edge => 'state edge_kind) => 'node => 'state => 'edge list =>
'node => 'state => bool" ("_,_ \<turnstile> '(_,_') =_=> '(_,_')" [51,50,0,0,50,0,0] 51)
where observable_moves_snoc:
"[|S,f \<turnstile> (n,s) =as=>⇣τ (n',s'); S,f \<turnstile> (n',s') -a-> (n'',s'')|]
==> S,f \<turnstile> (n,s) =as@[a]=> (n'',s'')"
lemma observable_move_notempty:
"[|S,f \<turnstile> (n,s) =as=> (n',s'); as = []|] ==> False"
by(induct rule:observable_moves.induct,simp)
lemma silent_move_observable_moves:
"[|S,f \<turnstile> (n'',s'') =as=> (n',s'); S,f \<turnstile> (n,s) -a->⇣τ (n'',s'')|]
==> S,f \<turnstile> (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 \<turnstile> (n,s) -a->⇣τ (nx,sx)` `S,f \<turnstile> (nx,sx) =as=>⇣τ (n',s')`
have "S,f \<turnstile> (n,s) =a#as=>⇣τ (n',s')" by(rule silent_moves_Cons)
with `S,f \<turnstile> (n',s') -a'-> (n'',s'')`
have "S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (n,s) =as=>⇣τ (n',s')` have "n = n'" and "s = s'"
by(auto elim:silent_moves.cases)
with `S,f \<turnstile> (n',s') -a-> (n'',s'')` show ?thesis
by(fastforce elim:observable_move.cases)
next
case (Cons a' as')
with `S,f \<turnstile> (n,s) =as=>⇣τ (n',s')` show ?thesis
by(fastforce elim:silent_moves.cases silent_move.cases)
qed
with `S,f \<turnstile> (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 \<turnstile> (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)⇣\<surd>"
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')⇣\<surd>"
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 = \<Up>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)⇣\<surd>" and "kind ax = (Q')⇣\<surd>"
and "∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s)"
by(auto dest:deterministic)
from `valid_edge a` `valid_edge ax` `sourcenode a = n` `sourcenode ax = n`
`targetnode a = n''` `targetnode ax ≠ n''`
obtain P P' where "slice_kind S a = (P)⇣\<surd>"
and "slice_kind S ax = (P')⇣\<surd>"
and "∀s. (P s --> ¬ P' s) ∧ (P' s --> ¬ P s)"
by -(erule slice_deterministic,auto)
show ?thesis
proof(cases "sourcenode a ∈ 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)⇣\<surd>`
`slice_kind S a = (P)⇣\<surd>` 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')⇣\<surd>`
`slice_kind S ax = (P')⇣\<surd>` have "pred (kind ax) s'"
by(simp add:slice_kinds_def)
with `kind ax = (Q')⇣\<surd>` have "Q' 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)⇣\<surd>` 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)⇣\<surd>` `slice_kind S a = (P)⇣\<surd>`
have "P = (λs. False) ∨ P = (λs. True)"
by(fastforce elim:kind_Predicate_notin_slice_slice_kind_Predicate)
with `slice_kind S a = (P)⇣\<surd>` `preds (slice_kinds S (a#as)) s`
have "P = (λs. True)" by(fastforce simp:slice_kinds_def)
from `kind ax = (Q')⇣\<surd>` `slice_kind S ax = (P')⇣\<surd>`
`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')⇣\<surd>` `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 @{text 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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (n⇣2,s⇣2) =as=>⇣τ (n⇣1,s⇣2)"
by(erule obs_silent_moves)
with `S,slice_kind S \<turnstile> (n⇣1,s⇣2) -a-> (n⇣1',s⇣2')`
have "S,slice_kind S \<turnstile> (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 = \<Up>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)⇣\<surd>"
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:split_if_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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (n⇣2,s⇣2) =as'@[last as]=>
(n⇣1',transfer (slice_kind S (last as)) s⇣2))"
proof -
from `S,kind \<turnstile> (n⇣1,s⇣1) =as=> (n⇣1',s⇣1')` obtain a' as' n' s'
where "S,kind \<turnstile> (n⇣1,s⇣1) =as'=>⇣τ (n',s')"
and "S,kind \<turnstile> (n',s') -a'-> (n⇣1',s⇣1')" and "as = as'@[a']"
by(fastforce elim:observable_moves.cases)
from `S,kind \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 @{text "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 \<turnstile> (n,s) =as=>⇣τ (n',s')"} *}
inductive trans_observable_moves ::
"'node set => ('edge => 'state edge_kind) => 'node => 'state => 'edge list =>
'node => 'state => bool" ("_,_ \<turnstile> '(_,_') =_=>* '(_,_')" [51,50,0,0,50,0,0] 51)
where tom_Nil:
"S,f \<turnstile> (n,s) =[]=>* (n,s)"
| tom_Cons:
"[|S,f \<turnstile> (n,s) =as=> (n',s'); S,f \<turnstile> (n',s') =as'=>* (n'',s'')|]
==> S,f \<turnstile> (n,s) =(last as)#as'=>* (n'',s'')"
definition slice_edges :: "'node set => 'edge list => 'edge list"
where "slice_edges S as ≡ [a \<leftarrow> as. sourcenode a ∈ backward_slice S]"
lemma silent_moves_no_slice_edges:
"S,f \<turnstile> (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 \<turnstile> (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:split_if_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 \<turnstile> (n,s) =slice_edges S as=>* (n'',s'')"
and "S,kind \<turnstile> (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 \<turnstile> (n,s) =slice_edges S as=>* (n'',s'') ∧
S,kind \<turnstile> (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 \<turnstile> (n,s) =[]=>* (n,s)" by(rule tom_Nil)
have "S,kind \<turnstile> (n,s) =[]=>⇣τ (n,s)" by(rule silent_moves_Nil)
with `S,kind \<turnstile> (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 \<turnstile> (n'',s) =slice_edges S as=>* (nx,s'') ∧
S,kind \<turnstile> (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 \<turnstile> (n'',transfer (kind a) s) =slice_edges S as=>* (nx,sx)"
and "S,kind \<turnstile> (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 \<turnstile> (n,s) -a-> (n'',transfer (kind a) s)"
by(fastforce intro:observable_moveI)
hence "S,kind \<turnstile> (n,s) =[]@[a]=> (n'',transfer (kind a) s)"
by(fastforce intro:observable_moves_snoc silent_moves_Nil)
with `S,kind \<turnstile> (n'',transfer (kind a) s) =slice_edges S as=>* (nx,sx)`
have "S,kind \<turnstile> (n,s) =a#slice_edges S as=>* (nx,sx)"
by(fastforce dest:tom_Cons)
with `S,kind \<turnstile> (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 \<turnstile> (n,s) -a->⇣τ (n'',transfer (kind a) s)"
by(fastforce intro:silent_moveI)
from `S,kind \<turnstile> (n'',transfer (kind a) s) =slice_edges S as=>* (nx,sx)`
obtain f s'' asx'' where "S,f \<turnstile> (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 \<turnstile> (n'',s'') =asx''=>* (nx,sx)` `f = kind`
`asx'' = slice_edges S as` `s'' = transfer (kind a) s`
`S,kind \<turnstile> (n,s) -a->⇣τ (n'',transfer (kind a) s)`
`S,kind \<turnstile> (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 \<turnstile> (n,s) =[]=>* (n,s)" by(rule trans_observable_moves.tom_Nil)
from `S,kind \<turnstile> (ni,si) =asx=>⇣τ (n',s')`
`S,kind \<turnstile> (n,s) -a->⇣τ (ni,transfer (kind a) s)`
`si = transfer (kind a) s`
have "S,kind \<turnstile> (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 \<turnstile> (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 \<turnstile> (ni,si) =asi=> (ni',si')` have "asi ≠ []"
by(fastforce dest:observable_move_notempty)
from `S,kind \<turnstile> (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 \<turnstile> (n,s) -a->⇣τ (ni,transfer (kind a) s)` `f = kind`
`si = transfer (kind a) s` `S,f \<turnstile> (ni,si) =asi=> (ni',si')`
have "S,f \<turnstile> (n,s) =a#asi=> (ni',si')"
by(fastforce intro:silent_move_observable_moves)
with `S,f \<turnstile> (ni',si') =asi'=>* (n'',s'')`
have "S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (n⇣1,s⇣1) =as=>* (n⇣1',s⇣1')`
have "S,f \<turnstile> (n⇣1,s⇣1) =as=>* (n⇣1',s⇣1')" by simp
from `S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (n⇣2,s⇣2) =as'=>* (n'',transfers (slice_kinds S as') s⇣2)`
from `S,f \<turnstile> (n,s) =as=> (n',s')`
obtain asx ax nx sx where "S,f \<turnstile> (n,s) =asx=>⇣τ (nx,sx)"
and "S,f \<turnstile> (nx,sx) -ax-> (n',s')" and "as = asx@[ax]"
by(fastforce elim:observable_moves.cases)
from `S,f \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (n⇣2,s⇣2) =asx'@[ax]=>
(n',transfer (slice_kind S ax) s⇣2)`
have "S,slice_kind S \<turnstile> (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 \<turnstile> (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 \<turnstile> (n⇣2,s⇣2) =asx'@[ax]=>
(n',transfer (slice_kind S ax) s⇣2)`
have "S,slice_kind S \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 = \<Up>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)⇣\<surd>"
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 \<turnstile> (n,s) =slice_edges S as=>* (n'',s'')"
and "S,kind \<turnstile> (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 \<turnstile> (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 \<turnstile> (n'',s'') =as'=>⇣τ (n',transfers (kinds as) s)`
have "S,kind \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (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 \<turnstile> (n'',s'') =as'=>⇣τ (n',transfers (kinds as) s)`
have "n'' -as'->* n'"
by(fastforce dest:silent_moves_preds_transfers_path)
from `S,kind \<turnstile> (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 \<turnstile> (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" ("_ \<triangleq> _" [51, 0] 80)
begin
theorem fundamental_property_of_path_slicing_semantically:
assumes "n \<triangleq> c" and "⟨c,s⟩ => ⟨c',s'⟩"
obtains n' as where "n -as->* n'" and "preds (slice_kinds {n'} as) s" and "n' \<triangleq> c'"
and "∀V ∈ Use n'. state_val (transfers (slice_kinds {n'} as) s) V = state_val s' V"
proof(atomize_elim)
from `n \<triangleq> 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' \<triangleq> 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' \<triangleq> c'`
show "∃as n'. n -as->* n' ∧ preds (slice_kinds {n'} as) s ∧ n' \<triangleq> c' ∧
(∀V∈Use n'. state_val (transfers (slice_kinds {n'} as) s) V = state_val s' V)"
by blast
qed
end
end