# Theory Slice

```section ‹Static backward slice›

theory Slice imports SCDObservable Distance begin

context SDG begin

subsection ‹Preliminary definitions on the parameter nodes for defining
sliced call and return edges›

fun csppa :: "'node ⇒ 'node SDG_node set ⇒ nat ⇒
((('var ⇀ 'val) ⇒ 'val option) list) ⇒ ((('var ⇀ 'val) ⇒ 'val option) list)"
where "csppa m S x [] = []"
| "csppa m S x (f#fs) =
(if Formal_in(m,x) ∉ S then Map.empty else f)#csppa m S (Suc x) fs"

definition cspp :: "'node ⇒ 'node SDG_node set ⇒
((('var ⇀ 'val) ⇒ 'val option) list) ⇒ ((('var ⇀ 'val) ⇒ 'val option) list)"
where "cspp m S fs ≡ csppa m S 0 fs"

lemma [simp]: "length (csppa m S x fs) = length fs"
by(induct fs arbitrary:x)(auto)

lemma [simp]: "length (cspp m S fs) = length fs"

lemma csppa_Formal_in_notin_slice:
"⟦x < length fs; Formal_in(m,x + i) ∉ S⟧
⟹ (csppa m S i fs)!x = Map.empty"
by(induct fs arbitrary:i x,auto simp:nth_Cons')

lemma csppa_Formal_in_in_slice:
"⟦x < length fs; Formal_in(m,x + i) ∈ S⟧
⟹ (csppa m S i fs)!x = fs!x"
by(induct fs arbitrary:i x,auto simp:nth_Cons')

definition map_merge :: "('var ⇀ 'val) ⇒ ('var ⇀ 'val) ⇒ (nat ⇒ bool) ⇒
'var list ⇒ ('var ⇀ 'val)"
where "map_merge f g Q xs ≡ (λV. if (∃i. i < length xs ∧ xs!i = V ∧ Q i) then g V
else f V)"

definition rspp :: "'node ⇒ 'node SDG_node set ⇒ 'var list ⇒
('var ⇀ 'val) ⇒ ('var ⇀ 'val) ⇒ ('var ⇀ 'val)"
where "rspp m S xs f g ≡ map_merge f (Map.empty(ParamDefs m [:=] map g xs))
(λi. Actual_out(m,i) ∈ S) (ParamDefs m)"

lemma rspp_Actual_out_in_slice:
assumes "x < length (ParamDefs (targetnode a))" and "valid_edge a"
and "length (ParamDefs (targetnode a)) = length xs"
and "Actual_out (targetnode a,x) ∈ S"
shows "(rspp (targetnode a) S xs f g) ((ParamDefs (targetnode a))!x) = g(xs!x)"
proof -
from ‹valid_edge a› have "distinct(ParamDefs (targetnode a))"
by(rule distinct_ParamDefs)
from ‹x < length (ParamDefs (targetnode a))›
‹length (ParamDefs (targetnode a)) = length xs›
‹distinct(ParamDefs (targetnode a))›
have "(Map.empty(ParamDefs (targetnode a) [:=] map g xs))
((ParamDefs (targetnode a))!x) = (map g xs)!x"
by(fastforce intro:fun_upds_nth)
with ‹Actual_out(targetnode a,x) ∈ S› ‹x < length (ParamDefs (targetnode a))›
‹length (ParamDefs (targetnode a)) = length xs› show ?thesis
by(fastforce simp:rspp_def map_merge_def)
qed

lemma rspp_Actual_out_notin_slice:
assumes "x < length (ParamDefs (targetnode a))" and "valid_edge a"
and "length (ParamDefs (targetnode a)) = length xs"
and "Actual_out((targetnode a),x) ∉ S"
shows "(rspp (targetnode a) S xs f g) ((ParamDefs (targetnode a))!x) =
f((ParamDefs (targetnode a))!x)"
proof -
from ‹valid_edge a› have "distinct(ParamDefs (targetnode a))"
by(rule distinct_ParamDefs)
from ‹x < length (ParamDefs (targetnode a))›
‹length (ParamDefs (targetnode a)) = length xs›
‹distinct(ParamDefs (targetnode a))›
have "(Map.empty(ParamDefs (targetnode a) [:=] map g xs))
((ParamDefs (targetnode a))!x) = (map g xs)!x"
by(fastforce intro:fun_upds_nth)
with ‹Actual_out((targetnode a),x) ∉ S› ‹distinct(ParamDefs (targetnode a))›
‹x < length (ParamDefs (targetnode a))›
show ?thesis by(fastforce simp:rspp_def map_merge_def nth_eq_iff_index_eq)
qed

subsection ‹Defining the sliced edge kinds›

primrec slice_kind_aux :: "'node ⇒ 'node ⇒ 'node SDG_node set ⇒
('var,'val,'ret,'pname) edge_kind ⇒ ('var,'val,'ret,'pname) edge_kind"
where "slice_kind_aux m m' S ⇑f = (if m ∈ ⌊S⌋⇘CFG⇙ then ⇑f else ⇑id)"
| "slice_kind_aux m m' S (Q)⇩√ = (if m ∈ ⌊S⌋⇘CFG⇙ then (Q)⇩√ else
(if obs_intra m ⌊S⌋⇘CFG⇙ = {} then
(let mex = (THE mex. method_exit mex ∧ get_proc m = get_proc mex) in
(if (∃x. distance m' mex x ∧ distance m mex (x + 1) ∧
(m' = (SOME mx'. ∃a'. m = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx')))
then (λcf. True)⇩√ else (λcf. False)⇩√))
else (let mx = THE mx. mx ∈ obs_intra m ⌊S⌋⇘CFG⇙ in
(if (∃x. distance m' mx x ∧ distance m mx (x + 1) ∧
(m' = (SOME mx'. ∃a'. m = sourcenode a' ∧
distance (targetnode a') mx x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx')))
then (λcf. True)⇩√ else (λcf. False)⇩√))))"
| "slice_kind_aux m m' S (Q:r↪⇘p⇙fs) = (if m ∈ ⌊S⌋⇘CFG⇙ then (Q:r↪⇘p⇙(cspp m' S fs))
else ((λcf. False):r↪⇘p⇙fs))"
| "slice_kind_aux m m' S (Q↩⇘p⇙f) = (if m ∈ ⌊S⌋⇘CFG⇙ then
(let outs = THE outs. ∃ins. (p,ins,outs) ∈ set procs in
(Q↩⇘p⇙(λcf cf'. rspp m' S outs cf' cf)))
else ((λcf. True)↩⇘p⇙(λcf cf'. cf')))"

definition slice_kind :: "'node SDG_node set ⇒ 'edge ⇒
('var,'val,'ret,'pname) edge_kind"
where "slice_kind S a ≡
slice_kind_aux (sourcenode a) (targetnode a) (HRB_slice S) (kind a)"

definition slice_kinds :: "'node SDG_node set ⇒ 'edge list ⇒
('var,'val,'ret,'pname) edge_kind list"
where "slice_kinds S as ≡ map (slice_kind S) as"

lemma slice_intra_kind_in_slice:
"⟦sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙; intra_kind (kind a)⟧
⟹ slice_kind S a = kind a"
by(fastforce simp:intra_kind_def slice_kind_def)

lemma slice_kind_Upd:
"⟦sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙; kind a = ⇑f⟧ ⟹ slice_kind S a = ⇑id"

lemma slice_kind_Pred_empty_obs_nearer_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "method_exit mex" and "get_proc (sourcenode a) = get_proc mex"
and "distance (targetnode a) mex x" and "distance (sourcenode a) mex (x + 1)"
and "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
shows "slice_kind S a = (λs. True)⇩√"
proof -
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
have "slice_kind S a =
(if (∃x. distance (targetnode a) mex x ∧ distance (sourcenode a) mex (x + 1) ∧
(targetnode a = (SOME mx'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx'))) then (λcf. True)⇩√ else (λcf. False)⇩√)"
with ‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
‹targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')›
show ?thesis by fastforce
qed

lemma slice_kind_Pred_empty_obs_nearer_not_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "method_exit mex" and "get_proc (sourcenode a) = get_proc mex"
and "distance (targetnode a) mex x" and "distance (sourcenode a) mex (x + 1)"
and "targetnode a ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
have "slice_kind S a =
(if (∃x. distance (targetnode a) mex x ∧ distance (sourcenode a) mex (x + 1) ∧
(targetnode a = (SOME mx'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧ valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = mx'))) then (λcf. True)⇩√ else (λcf. False)⇩√)"
with ‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
‹targetnode a ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')›
show ?thesis by(auto dest:distance_det)
qed

lemma slice_kind_Pred_empty_obs_not_nearer:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
and "method_exit mex" and "get_proc (sourcenode a) = get_proc mex"
and dist:"distance (sourcenode a) mex (x + 1)" "¬ distance (targetnode a) mex x"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
moreover
from dist have "¬ (∃x. distance (targetnode a) mex x ∧
distance (sourcenode a) mex (x + 1))"
by(fastforce dest:distance_det)
ultimately show ?thesis using assms by(auto simp:slice_kind_def Let_def)
qed

lemma slice_kind_Pred_obs_nearer_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
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' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
shows "slice_kind S a = (λs. True)⇩√"
proof -
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m = (THE m. m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(rule obs_intra_the_element[THEN sym])
with assms show ?thesis by(auto simp:slice_kind_def Let_def)
qed

lemma slice_kind_Pred_obs_nearer_not_SOME:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
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' ∧ intra_kind(kind a') ∧
targetnode a' = nx')"
shows "slice_kind S a = (λs. False)⇩√"
proof -
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m = (THE m. m ∈ obs_intra (sourcenode a) (⌊HRB_slice S⌋⇘CFG⇙))"
by(rule obs_intra_the_element[THEN sym])
with assms show ?thesis by(auto dest:distance_det simp:slice_kind_def Let_def)
qed

lemma slice_kind_Pred_obs_not_nearer:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = (Q)⇩√"
and in_obs:"m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
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_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(rule obs_intra_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 ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√› in_obs the show ?thesis
by(auto simp:slice_kind_def Let_def)
qed

lemma kind_Predicate_notin_slice_slice_kind_Predicate:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a" and "kind a = (Q)⇩√"
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_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
then obtain as where "sourcenode a -as→⇩√* (_Exit_)" by(fastforce dest:Exit_path)
then obtain as' mex where "sourcenode a -as'→⇩ι* mex" and "method_exit mex"
by -(erule valid_Exit_path_intra_path)
from ‹sourcenode a -as'→⇩ι* mex› have "get_proc (sourcenode a) = get_proc mex"
by(rule intra_path_get_procs)
show ?thesis
proof(cases "∃x. distance (targetnode a) mex x ∧
distance (sourcenode a) mex (x + 1)")
case True
then obtain x where "distance (targetnode a) mex x"
and "distance (sourcenode a) mex (x + 1)" by blast
show ?thesis
proof(cases "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')")
case True
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
have "slice_kind S a = (λs. True)⇩√"
by(rule slice_kind_Pred_empty_obs_nearer_SOME)
thus ?thesis by simp
next
case False
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}›
‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
‹distance (targetnode a) mex x› ‹distance (sourcenode a) mex (x + 1)›
have "slice_kind S a = (λs. False)⇩√"
by(rule slice_kind_Pred_empty_obs_nearer_not_SOME)
thus ?thesis by simp
qed
next
case False
from ‹method_exit mex› ‹get_proc (sourcenode a) = get_proc mex›
have "mex = (THE mex. method_exit mex ∧ get_proc (sourcenode a) = get_proc mex)"
by(auto intro!:the_equality[THEN sym] intro:method_exit_unique)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}› False
have "slice_kind S a = (λs. False)⇩√"
by(auto simp:slice_kind_def Let_def)
thus ?thesis by simp
qed
next
case False
then obtain m where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" 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' ∧ intra_kind(kind a') ∧
targetnode a' = n')")
case True
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹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 ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹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_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m = (THE m. m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(rule obs_intra_the_element[THEN sym])
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = (Q)⇩√› False
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "slice_kind S a = (λs. False)⇩√"
by(auto simp:slice_kind_def Let_def)
thus ?thesis by simp
qed
qed
qed

lemma slice_kind_Call:
"⟦sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙; kind a = Q:r↪⇘p⇙fs⟧
⟹ slice_kind S a = (λcf. False):r↪⇘p⇙fs"

lemma slice_kind_Call_in_slice:
"⟦sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙; kind a = Q:r↪⇘p⇙fs⟧
⟹ slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"

lemma slice_kind_Call_in_slice_Formal_in_not:
assumes "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = Q:r↪⇘p⇙fs"
and "∀x < length fs. Formal_in(targetnode a,x) ∉ HRB_slice S"
shows "slice_kind S a = Q:r↪⇘p⇙replicate (length fs) Map.empty"
proof -
from ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = Q:r↪⇘p⇙fs›
have "slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
from ‹∀x < length fs. Formal_in(targetnode a,x) ∉ HRB_slice S›
have "cspp (targetnode a) (HRB_slice S) fs = replicate (length fs) Map.empty"
by(fastforce intro:nth_equalityI csppa_Formal_in_notin_slice simp:cspp_def)
with ‹slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)›
show ?thesis by simp
qed

lemma slice_kind_Call_in_slice_Formal_in_also:
assumes "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "kind a = Q:r↪⇘p⇙fs"
and "∀x < length fs. Formal_in(targetnode a,x) ∈ HRB_slice S"
shows "slice_kind S a = Q:r↪⇘p⇙fs"
proof -
from ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = Q:r↪⇘p⇙fs›
have "slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)"
from ‹∀x < length fs. Formal_in(targetnode a,x) ∈ HRB_slice S›
have "cspp (targetnode a) (HRB_slice S) fs = fs"
by(fastforce intro:nth_equalityI csppa_Formal_in_in_slice simp:cspp_def)
with ‹slice_kind S a = Q:r↪⇘p⇙(cspp (targetnode a) (HRB_slice S) fs)›
show ?thesis by simp
qed

lemma slice_kind_Call_intra_notin_slice:
assumes "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a"
and "intra_kind (kind a)" and "valid_edge a'" and "kind a' = Q:r↪⇘p⇙fs"
and "sourcenode a' = sourcenode a"
shows "slice_kind S a = (λs. True)⇩√"
proof -
from ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs› obtain a''
where "a'' ∈ get_return_edges a'"
by(fastforce dest:get_return_edge_call)
with ‹valid_edge a'› obtain ax where "valid_edge ax"
and "sourcenode ax = sourcenode a'" and " targetnode ax = targetnode a''"
and "kind ax = (λcf. False)⇩√"
by(fastforce dest:call_return_node_edge)
from ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs›
have "∃!a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a' ∧
intra_kind(kind a'')"
by(rule call_only_one_intra_edge)
with ‹valid_edge a› ‹sourcenode a' = sourcenode a› ‹intra_kind (kind a)›
have all:"∀a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a' ∧
intra_kind(kind a'') ⟶ a'' = a" by fastforce
with ‹valid_edge ax› ‹sourcenode ax = sourcenode a'› ‹kind ax = (λcf. False)⇩√›
have [simp]:"ax = a" by(fastforce simp:intra_kind_def)
show ?thesis
proof(cases "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
then obtain asx where "sourcenode a -asx→⇩√* (_Exit_)" by(fastforce dest:Exit_path)
then obtain as pex where "sourcenode a-as→⇩ι* pex" and "method_exit pex"
by -(erule valid_Exit_path_intra_path)
from ‹sourcenode a-as→⇩ι* pex› have "get_proc (sourcenode a) = get_proc pex"
by(rule intra_path_get_procs)
from ‹sourcenode a-as→⇩ι* pex› obtain x where "distance (sourcenode a) pex x"
and "x ≤ length as" by(erule every_path_distance)
from ‹method_exit pex› have "sourcenode a ≠ pex"
proof(rule method_exit_cases)
assume "pex = (_Exit_)"
show ?thesis
proof
assume "sourcenode a = pex"
with ‹pex = (_Exit_)› have "sourcenode a = (_Exit_)" by simp
with ‹valid_edge a› show False by(rule Exit_source)
qed
next
fix ax Qx px fx
assume "pex = sourcenode ax" and "valid_edge ax" and "kind ax = Qx↩⇘px⇙fx"
hence "∀a'. valid_edge a' ∧ sourcenode a' = sourcenode ax ⟶
(∃Qx' fx'. kind a' = Qx'↩⇘px⇙fx')" by -(rule return_edges_only)
with ‹valid_edge a› ‹intra_kind (kind a)› ‹pex = sourcenode ax›
show ?thesis by(fastforce simp:intra_kind_def)
qed
have "x ≠ 0"
proof
assume "x = 0"
with ‹distance (sourcenode a) pex x› have "sourcenode a = pex"
by(fastforce elim:distance.cases simp:intra_path_def)
with ‹sourcenode a ≠ pex› show False by simp
qed
with ‹distance (sourcenode a) pex x› obtain ax' where "valid_edge ax'"
and "sourcenode a = sourcenode ax'" and "intra_kind(kind ax')"
and "distance (targetnode ax') pex (x - 1)"
and Some:"targetnode ax' = (SOME nx. ∃a'. sourcenode ax' = sourcenode a' ∧
distance (targetnode a') pex (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
by(erule distance_successor_distance)
from ‹valid_edge ax'› ‹sourcenode a = sourcenode ax'› ‹intra_kind(kind ax')›
‹sourcenode a' = sourcenode a› all
have [simp]:"ax' = a" by fastforce
from ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind ax = (λcf. False)⇩√›
True ‹method_exit pex› ‹get_proc (sourcenode a) = get_proc pex› ‹x ≠ 0›
‹distance (targetnode ax') pex (x - 1)› ‹distance (sourcenode a) pex x› Some
show ?thesis by(fastforce elim:slice_kind_Pred_empty_obs_nearer_SOME)
next
case False
then obtain m where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
then obtain as where "sourcenode a-as→⇩ι* m" and "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by -(erule obs_intraE)
from ‹sourcenode a-as→⇩ι* m› obtain x where "distance (sourcenode a) m x"
and "x ≤ length as" by(erule every_path_distance)
from ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m ∈ ⌊HRB_slice S⌋⇘CFG⇙›
have "sourcenode a ≠ m" by fastforce
have "x ≠ 0"
proof
assume "x = 0"
with ‹distance (sourcenode a) m x› have "sourcenode a = m"
by(fastforce elim:distance.cases simp:intra_path_def)
with ‹sourcenode a ≠ m› show False by simp
qed
with ‹distance (sourcenode a) m x› obtain ax' where "valid_edge ax'"
and "sourcenode a = sourcenode ax'" and "intra_kind(kind ax')"
and "distance (targetnode ax') m (x - 1)"
and Some:"targetnode ax' = (SOME nx. ∃a'. sourcenode ax' = sourcenode a' ∧
distance (targetnode a') m (x - 1) ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
by(erule distance_successor_distance)
from ‹valid_edge ax'› ‹sourcenode a = sourcenode ax'› ‹intra_kind(kind ax')›
‹sourcenode a' = sourcenode a› all
have [simp]:"ax' = a" by fastforce
from ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind ax = (λcf. False)⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹x ≠ 0›
‹distance (targetnode ax') m (x - 1)› ‹distance (sourcenode a) m x› Some
show ?thesis by(fastforce elim:slice_kind_Pred_obs_nearer_SOME)
qed
qed

lemma slice_kind_Return:
"⟦sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙; kind a = Q↩⇘p⇙f⟧
⟹ slice_kind S a = (λcf. True)↩⇘p⇙(λcf cf'. cf')"

lemma slice_kind_Return_in_slice:
"⟦sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙; valid_edge a; kind a = Q↩⇘p⇙f;
(p,ins,outs) ∈ set procs⟧
⟹ slice_kind S a = Q↩⇘p⇙(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"

lemma length_transfer_kind_slice_kind:
assumes "valid_edge a" and "length s⇩1 = length s⇩2"
and "transfer (kind a) s⇩1 = s⇩1'" and "transfer (slice_kind S a) s⇩2 = s⇩2'"
shows "length s⇩1' = length s⇩2'"
proof(cases "kind a" rule:edge_kind_cases)
case Intra
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with Intra assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_intra_kind_in_slice simp:intra_kind_def)+
next
case False
with Intra assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Upd
elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)+
qed
next
case (Call Q r p fs)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
with Call assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Call_in_slice)+
next
case False
with Call assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Call)+
qed
next
case (Return Q p f)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
case True
from Return ‹valid_edge a› obtain a' Q' r fs
where "valid_edge a'" and "kind a' = Q':r↪⇘p⇙fs"
by -(drule return_needs_call,auto)
then obtain ins outs where "(p,ins,outs) ∈ set procs"
by(fastforce dest!:callee_in_procs)
with True ‹valid_edge a› Return assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Return_in_slice split:list.split)+
next
case False
with Return assms show ?thesis
by(cases s⇩1)(cases s⇩2,auto dest:slice_kind_Return split:list.split)+
qed
qed

subsection ‹The sliced graph of a deterministic CFG is still deterministic›

lemma only_one_SOME_edge:
assumes "valid_edge a" and "intra_kind(kind a)" and "distance (targetnode a) mex x"
shows "∃!a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
proof(rule ex_ex1I)
show "∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
proof -
have "(∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')) =
(∃n'. ∃a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧ targetnode a' = n')"
apply(unfold some_eq_ex[of "λn'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n'"])
by simp
also have "…"
using ‹valid_edge a› ‹intra_kind(kind a)› ‹distance (targetnode a) mex x›
by blast
finally show ?thesis .
qed
next
fix a' ax
assume "sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
and "sourcenode a = sourcenode ax ∧ distance (targetnode ax) mex x ∧
valid_edge ax ∧ intra_kind(kind ax) ∧
targetnode ax = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind 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 "intra_kind (kind a)"
and "intra_kind (kind 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)
show ?thesis
proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
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 ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
thus ?thesis
proof(cases "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}")
case True
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹slice_kind S a = (λs. True)⇩√›
‹kind a = (Q)⇩√›
obtain mex x where mex:"mex = (THE mex. method_exit mex ∧
get_proc (sourcenode a) = get_proc mex)"
and dist:"distance (targetnode a) mex x" "distance (sourcenode a) mex (x + 1)"
and target:"targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
from ‹valid_edge a› ‹intra_kind (kind a)› ‹distance (targetnode a) mex x›
have ex1:"∃!a'. sourcenode a = sourcenode a' ∧ distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by(rule only_one_SOME_edge)
have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
proof(rule ccontr)
assume "¬ targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') mex x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by simp
with ex1 target ‹sourcenode a = sourcenode a'› ‹valid_edge a› ‹valid_edge a'›
‹intra_kind(kind a)› ‹intra_kind(kind a')› ‹distance (targetnode a) mex x›
have "a = a'" by fastforce
with ‹targetnode a ≠ targetnode a'› show False by simp
qed
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› True ‹kind a' = (Q')⇩√›
‹sourcenode a = sourcenode a'› mex dist
show ?thesis by(auto dest:distance_det
simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
next
case False
hence "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}" .
then obtain m where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by auto
hence "m = (THE m. m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙)"
by(auto dest:obs_intra_the_element)
with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}›
‹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' ∧ intra_kind(kind 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 ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a' = (Q')⇩√›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹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› ‹intra_kind(kind 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' ∧ intra_kind(kind a') ∧
targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = nx)"
by -(rule only_one_SOME_dist_edge)
have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind 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' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
distance (targetnode a') m x ∧
valid_edge a' ∧ intra_kind(kind a') ∧
targetnode a' = n')"
by simp
with ex1 target ‹sourcenode a = sourcenode a'›
‹valid_edge a› ‹valid_edge a'› ‹intra_kind(kind a)› ‹intra_kind(kind 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 ∉ ⌊HRB_slice S⌋⇘CFG⇙›
‹kind a' = (Q')⇩√› ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹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 "intra_kind (kind a)" and "intra_kind (kind 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)
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 ∈ ⌊HRB_slice S⌋⇘CFG⇙")
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'› ‹intra_kind (kind a)› ‹intra_kind (kind 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)⇩√"