Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory Observableheader {* \isaheader{Observable Sets of Nodes} *}
theory Observable imports ReturnAndCallNodes begin
context CFG begin
subsection {* Intraprocedural observable sets *}
inductive_set obs_intra :: "'node => 'node set => 'node set"
for n::"'node" and S::"'node set"
where obs_intra_elem:
"[|n -as->⇣ι* n'; ∀nx ∈ set(sourcenodes as). nx ∉ S; n' ∈ S|] ==> n' ∈ obs_intra n S"
lemma obs_intraE:
assumes "n' ∈ obs_intra n S"
obtains as where "n -as->⇣ι* n'" and "∀nx ∈ set(sourcenodes as). nx ∉ S" and "n' ∈ S"
using `n' ∈ obs_intra n S`
by(fastforce elim:obs_intra.cases)
lemma n_in_obs_intra:
assumes "valid_node n" and "n ∈ S" shows "obs_intra n S = {n}"
proof -
from `valid_node n` have "n -[]->* n" by(rule empty_path)
hence "n -[]->⇣ι* n" by(simp add:intra_path_def)
with `n ∈ S` have "n ∈ obs_intra n S"
by(fastforce elim:obs_intra_elem simp:sourcenodes_def)
{ fix n' assume "n' ∈ obs_intra n S"
have "n' = n"
proof(rule ccontr)
assume "n' ≠ n"
from `n' ∈ obs_intra n S` obtain as where "n -as->⇣ι* n'"
and "∀nx ∈ set(sourcenodes as). nx ∉ S"
and "n' ∈ S" by(fastforce elim:obs_intra.cases)
from `n -as->⇣ι* n'` have "n -as->* n'" by(simp add:intra_path_def)
from this `∀nx ∈ set(sourcenodes as). nx ∉ S` `n' ≠ n` `n ∈ S`
show False
proof(induct rule:path.induct)
case (Cons_path n'' as n' a n)
from `∀nx∈set (sourcenodes (a#as)). nx ∉ S` `sourcenode a = n`
have "n ∉ S" by(simp add:sourcenodes_def)
with `n ∈ S` show False by simp
qed simp
qed }
with `n ∈ obs_intra n S` show ?thesis by fastforce
qed
lemma in_obs_intra_valid:
assumes "n' ∈ obs_intra n S" shows "valid_node n" and "valid_node n'"
using `n' ∈ obs_intra n S`
by(auto elim!:obs_intraE intro:path_valid_node simp:intra_path_def)
lemma edge_obs_intra_subset:
assumes "valid_edge a" and "intra_kind (kind a)" and "sourcenode a ∉ S"
shows "obs_intra (targetnode a) S ⊆ obs_intra (sourcenode a) S"
proof
fix n assume "n ∈ obs_intra (targetnode a) S"
then obtain as where "targetnode a -as->⇣ι* n"
and all:"∀nx ∈ set(sourcenodes as). nx ∉ S" and "n ∈ S" by(erule obs_intraE)
from `valid_edge a` `intra_kind (kind a)` `targetnode a -as->⇣ι* n`
have "sourcenode a -[a]@as->⇣ι* n" by(fastforce intro:Cons_path simp:intra_path_def)
moreover
from all `sourcenode a ∉ S` have "∀nx ∈ set(sourcenodes (a#as)). nx ∉ S"
by(simp add:sourcenodes_def)
ultimately show "n ∈ obs_intra (sourcenode a) S" using `n ∈ S`
by(fastforce intro:obs_intra_elem)
qed
lemma path_obs_intra_subset:
assumes "n -as->⇣ι* n'" and "∀n' ∈ set(sourcenodes as). n' ∉ S"
shows "obs_intra n' S ⊆ obs_intra n S"
proof -
from `n -as->⇣ι* n'` have "n -as->* n'" and "∀a ∈ set as. intra_kind (kind a)"
by(simp_all add:intra_path_def)
from this `∀n' ∈ set(sourcenodes as). n' ∉ S` show ?thesis
proof(induct rule:path.induct)
case (Cons_path n'' as n' a n)
note IH = `[|∀a∈set as. intra_kind (kind a); ∀n'∈set (sourcenodes as). n' ∉ S|]
==> obs_intra n' S ⊆ obs_intra n'' S`
from `∀n'∈set (sourcenodes (a#as)). n' ∉ S`
have all:"∀n'∈set (sourcenodes as). n' ∉ S" and "sourcenode a ∉ S"
by(simp_all add:sourcenodes_def)
from `∀a ∈ set (a#as). intra_kind (kind a)`
have "intra_kind (kind a)" and "∀a ∈ set as. intra_kind (kind a)"
by(simp_all add:intra_path_def)
from IH[OF `∀a ∈ set as. intra_kind (kind a)` all]
have "obs_intra n' S ⊆ obs_intra n'' S" .
from `valid_edge a` `intra_kind (kind a)` `targetnode a = n''`
`sourcenode a = n` `sourcenode a ∉ S`
have "obs_intra n'' S ⊆ obs_intra n S" by(fastforce dest:edge_obs_intra_subset)
with `obs_intra n' S ⊆ obs_intra n'' S` show ?case by fastforce
qed simp
qed
lemma path_ex_obs_intra:
assumes "n -as->⇣ι* n'" and "n' ∈ S"
obtains m where "m ∈ obs_intra n S"
proof(atomize_elim)
show "∃m. m ∈ obs_intra n S"
proof(cases "∀nx ∈ set(sourcenodes as). nx ∉ S")
case True
with `n -as->⇣ι* n'` `n' ∈ S` have "n' ∈ obs_intra n S" by -(rule obs_intra_elem)
thus ?thesis by fastforce
next
case False
hence "∃nx ∈ set(sourcenodes as). nx ∈ S" by fastforce
then obtain nx ns ns' where "sourcenodes as = ns@nx#ns'"
and "nx ∈ S" and "∀n' ∈ set ns. n' ∉ 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)
with `n -as->⇣ι* n'` have "n -as'->⇣ι* nx"
by(fastforce dest:path_split simp:intra_path_def)
with `nx ∈ S` `∀n' ∈ set ns. n' ∉ S` `ns = sourcenodes as'`
have "nx ∈ obs_intra n S" by(fastforce intro:obs_intra_elem)
thus ?thesis by fastforce
qed
qed
subsection {* Interprocedural observable sets restricted to the slice *}
fun obs :: "'node list => 'node set => 'node list set"
where "obs [] S = {}"
| "obs (n#ns) S = (let S' = obs_intra n S in
(if (S' = {} ∨ (∃n' ∈ set ns. ∃nx. call_of_return_node n' nx ∧ nx ∉ S))
then obs ns S else (λnx. nx#ns) ` S'))"
lemma obsI:
assumes "n' ∈ obs_intra n S"
and "∀nx ∈ set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
shows "[|ns = nsx@n#nsx'; ∀xs x xs'. nsx = xs@x#xs' ∧ obs_intra x S ≠ {}
--> (∃x'' ∈ set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)|]
==> n'#nsx' ∈ obs ns S"
proof(induct ns arbitrary:nsx)
case (Cons x xs)
note IH = `!!nsx. [|xs = nsx@n#nsx';
∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)|]
==> n'#nsx' ∈ obs xs S`
note nsx = `∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)`
show ?case
proof(cases nsx)
case Nil
with `x#xs = nsx@n#nsx'` have "n = x" and "xs = nsx'" by simp_all
with `n' ∈ obs_intra n S`
`∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S`
show ?thesis by(fastforce simp:Let_def)
next
case (Cons z zs)
with `x#xs = nsx@n#nsx'` have [simp]:"x = z" "xs = zs@n#nsx'" by simp_all
from nsx Cons
have "∀xs x xs'. zs = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
by clarsimp(erule_tac x="z#xs" in allE,auto)
from IH[OF `xs = zs@n#nsx'` this] have "n'#nsx' ∈ obs xs S" by simp
show ?thesis
proof(cases "obs_intra z S = {}")
case True
with Cons `n'#nsx' ∈ obs xs S` show ?thesis by(simp add:Let_def)
next
case False
from nsx Cons
have "obs_intra z S ≠ {} -->
(∃x''∈set (zs @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
by clarsimp(erule_tac x="[]" in allE,auto)
with False have "∃x''∈set (zs @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S"
by simp
with `xs = zs@n#nsx'`
have "∃n' ∈ set xs. ∃nx. call_of_return_node n' nx ∧ nx ∉ S" by fastforce
with Cons `n'#nsx' ∈ obs xs S` show ?thesis by(simp add:Let_def)
qed
qed
qed simp
lemma obsE [consumes 2]:
assumes "ns' ∈ obs ns S" and "∀n ∈ set (tl ns). return_node n"
obtains nsx n nsx' n' where "ns = nsx@n#nsx'" and "ns' = n'#nsx'"
and "n' ∈ obs_intra n S"
and "∀nx ∈ set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
and "∀xs x xs'. nsx = xs@x#xs' ∧ obs_intra x S ≠ {}
--> (∃x'' ∈ set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
proof(atomize_elim)
from `ns' ∈ obs ns S` `∀n ∈ set (tl ns). return_node n`
show "∃nsx n nsx' n'. ns = nsx @ n # nsx' ∧ ns' = n' # nsx' ∧
n' ∈ obs_intra n S ∧ (∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S) ∧
(∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S))"
proof(induct ns)
case Nil thus ?case by simp
next
case (Cons nx ns'')
note IH = `[|ns' ∈ obs ns'' S; ∀a∈set (tl ns''). return_node a|]
==> ∃nsx n nsx' n'. ns'' = nsx @ n # nsx' ∧ ns' = n' # nsx' ∧
n' ∈ obs_intra n S ∧
(∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S) ∧
(∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S))`
from `∀a∈set (tl (nx # ns'')). return_node a` have "∀n ∈ set ns''. return_node n"
by simp
show ?case
proof(cases ns'')
case Nil
with `ns' ∈ obs (nx#ns'') S` obtain x where "ns' = [x]" and "x ∈ obs_intra nx S"
by(auto simp:Let_def split:split_if_asm)
with Nil show ?thesis by fastforce
next
case Cons
with `∀n ∈ set ns''. return_node n` have "∀a∈set (tl ns''). return_node a"
by simp
show ?thesis
proof(cases "∃n' ∈ set ns''. ∃nx'. call_of_return_node n' nx' ∧ nx' ∉ S")
case True
with `ns' ∈ obs (nx#ns'') S` have "ns' ∈ obs ns'' S" by simp
from IH[OF this `∀a∈set (tl ns''). return_node a`]
obtain nsx n nsx' n' where split:"ns'' = nsx @ n # nsx'"
"ns' = n' # nsx'" "n' ∈ obs_intra n S"
"∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
and imp:"∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
by blast
from True `ns'' = nsx @ n # nsx'`
`∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S`
have "(∃nx'. call_of_return_node n nx' ∧ nx' ∉ S) ∨
(∃n'∈set nsx. ∃nx'. call_of_return_node n' nx' ∧ nx' ∉ S)" by fastforce
thus ?thesis
proof
assume "∃nx'. call_of_return_node n nx' ∧ nx' ∉ S"
with split show ?thesis by clarsimp
next
assume "∃n'∈set nsx. ∃nx'. call_of_return_node n' nx' ∧ nx' ∉ S"
with imp have "∀xs x xs'. nx#nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
apply clarsimp apply(case_tac xs) apply auto
by(erule_tac x="list" in allE,auto)+
with split Cons show ?thesis by auto
qed
next
case False
hence "∀n'∈set ns''. ∀nx'. call_of_return_node n' nx' --> nx' ∈ S" by simp
show ?thesis
proof(cases "obs_intra nx S = {}")
case True
with `ns' ∈ obs (nx#ns'') S` have "ns' ∈ obs ns'' S" by simp
from IH[OF this `∀a∈set (tl ns''). return_node a`]
obtain nsx n nsx' n' where split:"ns'' = nsx @ n # nsx'"
"ns' = n' # nsx'" "n' ∈ obs_intra n S"
"∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
and imp:"∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
by blast
from True imp Cons
have "∀xs x xs'. nx#nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} -->
(∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
by clarsimp(case_tac xs,clarsimp+,erule_tac x="list" in allE,auto)
with split Cons show ?thesis by auto
next
case False
with `∀n'∈set ns''. ∀nx'. call_of_return_node n' nx' --> nx' ∈ S`
`ns' ∈ obs (nx # ns'') S`
obtain nx'' where "ns' = nx''#ns''" and "nx'' ∈ obs_intra nx S"
by(fastforce simp:Let_def split:split_if_asm)
{ fix n' assume "n'∈set ns''"
with `∀n ∈ set ns''. return_node n` have "return_node n'" by simp
hence "∃!n''. call_of_return_node n' n''"
by(rule return_node_call_of_return_node)
from `n'∈set ns''`
`∀n'∈set ns''. ∀nx'. call_of_return_node n' nx' --> nx' ∈ S`
have "∀nx'. call_of_return_node n' nx' --> nx' ∈ S" by simp
with `∃!n''. call_of_return_node n' n''`
have "∃n''. call_of_return_node n' n'' ∧ n'' ∈ S" by fastforce }
with `ns' = nx''#ns''` `nx'' ∈ obs_intra nx S` show ?thesis by fastforce
qed
qed
qed
qed
qed
lemma obs_split_det:
assumes "xs@x#xs' = ys@y#ys'"
and "obs_intra x S ≠ {}"
and "∀x' ∈ set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S"
and "∀zs z zs'. xs = zs@z#zs' ∧ obs_intra z S ≠ {}
--> (∃z'' ∈ set (zs'@[x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S)"
and "obs_intra y S ≠ {}"
and "∀y' ∈ set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S"
and "∀zs z zs'. ys = zs@z#zs' ∧ obs_intra z S ≠ {}
--> (∃z'' ∈ set (zs'@[y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)"
shows "xs = ys ∧ x = y ∧ xs' = ys'"
using assms
proof(induct xs arbitrary:ys)
case Nil
note impy = `∀zs z zs'. ys = zs@z#zs' ∧ obs_intra z S ≠ {}
--> (∃z'' ∈ set (zs'@[y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)`
show ?case
proof(cases "ys = []")
case True
with Nil `[]@x#xs' = ys@y#ys'` show ?thesis by simp
next
case False
with `[] @ x # xs' = ys @ y # ys'`
obtain zs where "x#zs = ys" and "xs' = zs@y#ys'" by(auto simp:Cons_eq_append_conv)
from `x#zs = ys` `obs_intra x S ≠ {}` impy
have "∃z'' ∈ set (zs@[y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S"
by blast
with `xs' = zs@y#ys'` `∀x' ∈ set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S`
have False by fastforce
thus ?thesis by simp
qed
next
case (Cons w ws)
note IH = `!!ys. [|ws @ x # xs' = ys @ y # ys'; obs_intra x S ≠ {};
∀x'∈set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S;
∀zs z zs'. ws = zs @ z # zs' ∧ obs_intra z S ≠ {} -->
(∃z''∈set (zs' @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S);
obs_intra y S ≠ {}; ∀y'∈set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S;
∀zs z zs'. ys = zs @ z # zs' ∧ obs_intra z S ≠ {} -->
(∃z''∈set (zs' @ [y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)|]
==> ws = ys ∧ x = y ∧ xs' = ys'`
note impw = `∀zs z zs'. w # ws = zs @ z # zs' ∧ obs_intra z S ≠ {} -->
(∃z''∈set (zs' @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S)`
note impy = `∀zs z zs'. ys = zs @ z # zs' ∧ obs_intra z S ≠ {} -->
(∃z''∈set (zs' @ [y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)`
show ?case
proof(cases ys)
case Nil
with `(w#ws) @ x # xs' = ys @ y # ys'` have "y = w" and "ys' = ws @ x # xs'"
by simp_all
from `y = w` `obs_intra y S ≠ {}` impw
have "∃z''∈set (ws @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S" by blast
with `ys' = ws @ x # xs'`
`∀y'∈set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S`
have False by fastforce
thus ?thesis by simp
next
case (Cons w' ws')
with `(w # ws) @ x # xs' = ys @ y # ys'` have "w = w'"
and "ws @ x # xs' = ws' @ y # ys'" by simp_all
from impw have imp1:"∀zs z zs'. ws = zs @ z # zs' ∧ obs_intra z S ≠ {} -->
(∃z''∈set (zs' @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S)"
by clarsimp(erule_tac x="w#zs" in allE,clarsimp)
from Cons impy have imp2:"∀zs z zs'. ws' = zs @ z # zs' ∧ obs_intra z S ≠ {} -->
(∃z''∈set (zs' @ [y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)"
by clarsimp(erule_tac x="w'#zs" in allE,clarsimp)
from IH[OF `ws @ x # xs' = ws' @ y # ys'` `obs_intra x S ≠ {}`
`∀x'∈set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S` imp1
`obs_intra y S ≠ {}` `∀y'∈set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S`
imp2]
have "ws = ws' ∧ x = y ∧ xs' = ys'" .
with `w = w'` Cons show ?thesis by simp
qed
qed
lemma in_obs_valid:
assumes "ns' ∈ obs ns S" and "∀n ∈ set ns. valid_node n"
shows "∀n ∈ set ns'. valid_node n"
using `ns' ∈ obs ns S` `∀n ∈ set ns. valid_node n`
by(induct ns)(auto intro:in_obs_intra_valid simp:Let_def split:split_if_asm)
end
end