# Theory Observable

```section ‹Observable Sets of Nodes›

theory Observable imports "../Basic/CFG" begin

context CFG begin

inductive_set obs :: "'node ⇒ 'node set ⇒ 'node set"
for n::"'node" and S::"'node set"
where obs_elem:
"⟦n -as→* n'; ∀nx ∈ set(sourcenodes as). nx ∉ S; n' ∈ S⟧ ⟹ n' ∈ obs n S"

lemma obsE:
assumes "n' ∈ obs n S"
obtains as where "n -as→* n'" and "∀nx ∈ set(sourcenodes as). nx ∉ S"
and "n' ∈ S"
proof(atomize_elim)
from ‹n' ∈ obs n S›
have "∃as. n -as→* n' ∧ (∀nx ∈ set(sourcenodes as). nx ∉ S) ∧ n' ∈ S"
by(auto elim:obs.cases)
thus "∃as. n -as→* n' ∧ (∀nx∈set (sourcenodes as). nx ∉ S) ∧ n' ∈ S" by blast
qed

lemma n_in_obs:
assumes "valid_node n" and "n ∈ S" shows "obs n S = {n}"
proof -
from ‹valid_node n› have "n -[]→* n" by(rule empty_path)
with ‹n ∈ S› have "n ∈ obs n S" by(fastforce elim:obs_elem simp:sourcenodes_def)
{ fix n' assume "n' ∈ obs n S"
have "n' = n"
proof(rule ccontr)
assume "n' ≠ n"
from ‹n' ∈ obs n S› obtain as where "n -as→* n'"
and "∀nx ∈ set(sourcenodes as). nx ∉ S"
and "n' ∈ S" by(erule obsE)
from ‹n -as→* n'› ‹∀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 n S› show ?thesis by fastforce
qed

lemma in_obs_valid:
assumes "n' ∈ obs n S" shows "valid_node n" and "valid_node n'"
using ‹n' ∈ obs n S›
by(auto elim:obsE intro:path_valid_node)

lemma edge_obs_subset:
assumes"valid_edge a" and "sourcenode a ∉ S"
shows "obs (targetnode a) S ⊆ obs (sourcenode a) S"
proof
fix n assume "n ∈ obs (targetnode a) S"
then obtain as where "targetnode a -as→* n"
and all:"∀nx ∈ set(sourcenodes as). nx ∉ S" and "n ∈ S" by(erule obsE)
from ‹valid_edge a› ‹targetnode a -as→* n›
have "sourcenode a -a#as→* n" by(fastforce intro:Cons_path)
moreover
from all ‹sourcenode a ∉ S› have "∀nx ∈ set(sourcenodes (a#as)). nx ∉ S"
ultimately show "n ∈ obs (sourcenode a) S" using ‹n ∈ S›
by(rule obs_elem)
qed

lemma path_obs_subset:
"⟦n -as→* n'; ∀n' ∈ set(sourcenodes as). n' ∉ S⟧
⟹ obs n' S ⊆ obs n S"
proof(induct rule:path.induct)
case (Cons_path n'' as n' a n)
note IH = ‹∀n'∈set (sourcenodes as). n' ∉ S ⟹ obs n' S ⊆ obs n'' S›
from ‹∀n'∈set (sourcenodes (a#as)). n' ∉ S›
have all:"∀n'∈set (sourcenodes as). n' ∉ S" and "sourcenode a ∉ S"
from IH[OF all] have "obs n' S ⊆ obs n'' S" .
from ‹valid_edge a› ‹targetnode a = n''› ‹sourcenode a = n› ‹sourcenode a ∉ S›
have "obs n'' S ⊆ obs n S" by(fastforce dest:edge_obs_subset)
with ‹obs n' S ⊆ obs n'' S› show ?case by fastforce
qed simp

lemma path_ex_obs:
assumes "n -as→* n'" and "n' ∈ S"
obtains m where "m ∈ obs n S"
proof(atomize_elim)
show "∃m. m ∈ obs n S"
proof(cases "∀nx ∈ set(sourcenodes as). nx ∉ S")
case True
with ‹n -as→* n'› ‹n' ∈ S› have "n' ∈ obs n S" by -(rule obs_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)
with ‹nx ∈ S› ‹∀n' ∈ set ns. n' ∉ S› ‹ns = sourcenodes as'› have "nx ∈ obs n S"
by(fastforce intro:obs_elem)
thus ?thesis by fastforce
qed
qed

end

end

```