Theory Observable

```section ‹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"
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)"
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"
from ‹∀a ∈ set (a#as). intra_kind (kind a)›
have "intra_kind (kind a)" and "∀a ∈ set as. intra_kind (kind a)"
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
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:if_split_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 (hypsubst_thin,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:if_split_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:if_split_asm)

end

end

```