# Theory SCDObservable

```section ‹Observable sets w.r.t.\ standard control dependence›

theory SCDObservable imports Observable HRBSlice begin

context SDG begin

lemma matched_bracket_assms_variant:
assumes "n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V'→⇘in⇙ n⇩2" and "matched n⇩2 ns' n⇩3"
and "n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4"
and "call_of_return_node (parent_node n⇩4) (parent_node n⇩1)"
obtains a a' where "valid_edge a" and "a' ∈ get_return_edges a"
and "sourcenode a = parent_node n⇩1" and "targetnode a = parent_node n⇩2"
and "sourcenode a' = parent_node n⇩3" and "targetnode a' = parent_node n⇩4"
proof(atomize_elim)
from ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V'→⇘in⇙ n⇩2› obtain a Q r fs where "valid_edge a"
and "kind a = Q:r↪⇘p⇙fs" and "parent_node n⇩1 = sourcenode a"
and "parent_node n⇩2 = targetnode a"
by(fastforce elim:SDG_edge.cases)
from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› obtain a' Q' f'
where "valid_edge a'" and "kind a' = Q'↩⇘p⇙f'"
and "parent_node n⇩3 = sourcenode a'" and "parent_node n⇩4 = targetnode a'"
by(fastforce elim:SDG_edge.cases)
from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
obtain ax where "valid_edge ax" and "∃Q r fs. kind ax = Q:r↪⇘p⇙fs"
and "a' ∈ get_return_edges ax"
by -(drule return_needs_call,fastforce+)
from ‹valid_edge a› ‹valid_edge ax› ‹kind a = Q:r↪⇘p⇙fs› ‹∃Q r fs. kind ax = Q:r↪⇘p⇙fs›
have "targetnode a = targetnode ax" by(fastforce dest:same_proc_call_unique_target)
from ‹valid_edge a'› ‹a' ∈ get_return_edges ax› ‹valid_edge ax›
have "call_of_return_node (targetnode a') (sourcenode ax)"
by(fastforce simp:return_node_def call_of_return_node_def)
with ‹call_of_return_node (parent_node n⇩4) (parent_node n⇩1)›
‹parent_node n⇩4 = targetnode a'›
have "sourcenode ax = parent_node n⇩1" by fastforce
with ‹valid_edge ax› ‹a' ∈ get_return_edges ax› ‹targetnode a = targetnode ax›
‹parent_node n⇩2 = targetnode a› ‹parent_node n⇩3 = sourcenode a'›
‹parent_node n⇩4 = targetnode a'›
show "∃a a'. valid_edge a ∧ a' ∈ get_return_edges a ∧
sourcenode a = parent_node n⇩1 ∧ targetnode a = parent_node n⇩2 ∧
sourcenode a' = parent_node n⇩3 ∧ targetnode a' = parent_node n⇩4"
by fastforce
qed

subsection ‹Observable set of standard control dependence is at most a singleton›

definition SDG_to_CFG_set :: "'node SDG_node set ⇒ 'node set" ("⌊_⌋⇘CFG⇙")
where "⌊S⌋⇘CFG⇙ ≡ {m. CFG_node m ∈ S}"

lemma [intro]:"∀n ∈ S. valid_SDG_node n ⟹ ∀n ∈ ⌊S⌋⇘CFG⇙. valid_node n"
by(fastforce simp:SDG_to_CFG_set_def)

lemma Exit_HRB_Slice:
assumes "n ∈ ⌊HRB_slice {CFG_node (_Exit_)}⌋⇘CFG⇙" shows "n = (_Exit_)"
proof -
from ‹n ∈ ⌊HRB_slice {CFG_node (_Exit_)}⌋⇘CFG⇙›
have "CFG_node n ∈ HRB_slice {CFG_node (_Exit_)}"
thus ?thesis
proof(induct "CFG_node n" rule:HRB_slice_cases)
case (phase1 nx)
from ‹nx ∈ {CFG_node (_Exit_)}› have "nx = CFG_node (_Exit_)" by simp
with ‹CFG_node n ∈ sum_SDG_slice1 nx›
have "CFG_node n = CFG_node (_Exit_) ∨
(∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
by(induct rule:sum_SDG_slice1.induct) auto
then show ?thesis by(fastforce dest:Exit_no_sum_SDG_edge_target)
next
case (phase2 nx n' n'' p)
from ‹nx ∈ {CFG_node (_Exit_)}› have "nx = CFG_node (_Exit_)" by simp
with ‹n' ∈ sum_SDG_slice1 nx›
have "n' = CFG_node (_Exit_) ∨
(∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
by(induct rule:sum_SDG_slice1.induct) auto
hence "n' = CFG_node (_Exit_)" by(fastforce dest:Exit_no_sum_SDG_edge_target)
with ‹CFG_node n ∈ sum_SDG_slice2 n'›
have "CFG_node n = CFG_node (_Exit_) ∨
(∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
by(induct rule:sum_SDG_slice2.induct) auto
then show ?thesis by(fastforce dest:Exit_no_sum_SDG_edge_target)
qed
qed

lemma Exit_in_obs_intra_slice_node:
assumes "(_Exit_) ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙"
shows "CFG_node (_Exit_) ∈ S"
proof -
let ?S' = "⌊HRB_slice S⌋⇘CFG⇙"
from ‹(_Exit_) ∈ obs_intra n' ?S'› obtain as where "n' -as→⇩ι* (_Exit_)"
and "∀nx ∈ set(sourcenodes as). nx ∉ ?S'" and "(_Exit_) ∈ ?S'"
by(erule obs_intraE)
from ‹(_Exit_) ∈ ?S'›
have "CFG_node (_Exit_) ∈ HRB_slice S" by(simp add:SDG_to_CFG_set_def)
thus ?thesis
proof(induct "CFG_node (_Exit_)" rule:HRB_slice_cases)
case (phase1 nx)
thus ?case
by(induct "CFG_node (_Exit_)" rule:sum_SDG_slice1.induct,
auto dest:Exit_no_sum_SDG_edge_source)
next
case (phase2 nx n' n'' p)
from ‹CFG_node (_Exit_) ∈ sum_SDG_slice2 n'› ‹n' ∈ sum_SDG_slice1 nx› ‹nx ∈ S›
show ?case
apply(induct n≡"CFG_node (_Exit_)" rule:sum_SDG_slice2.induct)
apply(auto dest:Exit_no_sum_SDG_edge_source)
apply(hypsubst_thin)
apply(induct n≡"CFG_node (_Exit_)" rule:sum_SDG_slice1.induct)
apply(auto dest:Exit_no_sum_SDG_edge_source)
done
qed
qed

lemma obs_intra_postdominate:
assumes "n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙" and "¬ method_exit n"
shows "n postdominates n'"
proof(rule ccontr)
assume "¬ n postdominates n'"
from ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› have "valid_node n"
by(fastforce dest:in_obs_intra_valid)
with ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› ‹¬ method_exit n› have "n postdominates n"
by(fastforce intro:postdominate_refl)
from ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› obtain as where "n' -as→⇩ι* n"
and all_notinS:"∀n' ∈ set(sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "n ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(erule obs_intraE)
from ‹n postdominates n› ‹¬ n postdominates n'› ‹n' -as→⇩ι* n›
obtain as' a as'' where [simp]:"as = as'@a#as''"
and "valid_edge a" and "¬ n postdominates (sourcenode a)"
and "n postdominates (targetnode a)"  and "intra_kind (kind a)"
by(fastforce elim!:postdominate_path_branch simp:intra_path_def)
from ‹n' -as→⇩ι* n› have "sourcenode a -a#as''→⇩ι* n"
by(fastforce elim:path_split intro:Cons_path simp:intra_path_def)
with ‹¬ n postdominates (sourcenode a)› ‹valid_edge a› ‹valid_node n›
obtain asx pex where "sourcenode a -asx→⇩ι* pex" and "method_exit pex"
and "n ∉ set(sourcenodes asx)" by(fastforce simp:postdominate_def)
have "asx ≠ []"
proof
assume "asx = []"
with ‹sourcenode a -asx→⇩ι* pex› have "sourcenode a = pex"
by(fastforce simp:intra_path_def)
from ‹method_exit pex› show False
proof(rule method_exit_cases)
assume "pex = (_Exit_)"
with ‹sourcenode a = pex› have "sourcenode a = (_Exit_)" by simp
with ‹valid_edge a› show False by(rule Exit_source)
next
fix a' Q f p
assume "pex = sourcenode a'" and "valid_edge a'" and "kind a' = Q↩⇘p⇙f"
from ‹valid_edge a'› ‹kind a' = Q↩⇘p⇙f› ‹valid_edge a› ‹intra_kind (kind a)›
‹sourcenode a = pex› ‹pex = sourcenode a'›
show False by(fastforce dest:return_edges_only simp:intra_kind_def)
qed
qed
then obtain ax asx' where [simp]:"asx = ax#asx'" by(cases asx) auto
with ‹sourcenode a -asx→⇩ι* pex› have "sourcenode a -ax#asx'→* pex"
hence "valid_edge ax" and [simp]:"sourcenode a = sourcenode ax"
and "targetnode ax -asx'→* pex" by(auto elim:path_split_Cons)
with ‹sourcenode a -asx→⇩ι* pex› have "targetnode ax -asx'→⇩ι* pex"
with ‹valid_edge ax› ‹n ∉ set(sourcenodes asx)› ‹method_exit pex›
have "¬ n postdominates targetnode ax"
by(fastforce simp:postdominate_def sourcenodes_def)
from ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› all_notinS
have "n ∉ set (sourcenodes (a#as''))"
by(fastforce elim:obs_intra.cases simp:sourcenodes_def)
from ‹sourcenode a -asx→⇩ι* pex› have "intra_kind (kind ax)"
with ‹sourcenode a -a#as''→⇩ι* n› ‹n postdominates (targetnode a)›
‹¬ n postdominates targetnode ax› ‹valid_edge ax›
‹n ∉ set (sourcenodes (a#as''))› ‹intra_kind (kind a)›
have "(sourcenode a) controls n"
by(fastforce simp:control_dependence_def)
hence "CFG_node (sourcenode a) s⟶⇘cd⇙ CFG_node n"
by(fastforce intro:sum_SDG_cdep_edge)
with ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(auto elim!:obs_intraE combine_SDG_slices.cases
intro:combine_SDG_slices.intros sum_SDG_slice1.intros
sum_SDG_slice2.intros simp:HRB_slice_def SDG_to_CFG_set_def)
with all_notinS show False by(simp add:sourcenodes_def)
qed

lemma obs_intra_singleton_disj:
assumes "valid_node n"
shows "(∃m. obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}) ∨
obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(rule ccontr)
assume "¬ ((∃m. obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}) ∨
obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {})"
hence "∃nx nx'. nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ∧
nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ∧ nx ≠ nx'" by auto
then obtain nx nx' where "nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
and "nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙" and "nx ≠ nx'" by auto
from ‹nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› obtain as where "n -as→⇩ι* nx"
and all:"∀n' ∈ set(sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(erule obs_intraE)
from ‹n -as→⇩ι* nx› have "n -as→* nx" and "∀a ∈ set as. intra_kind (kind a)"
hence "valid_node nx" by(fastforce dest:path_valid_node)
with ‹nx ∈ ⌊HRB_slice S⌋⇘CFG⇙› have "obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}"
by -(rule n_in_obs_intra)
with ‹n -as→* nx› ‹nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙›
‹nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ nx'› have "as ≠ []"
by(fastforce elim:path.cases simp:intra_path_def)
with ‹n -as→* nx› ‹nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙›
‹nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ nx'›
‹obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}› ‹∀a ∈ set as. intra_kind (kind a)› all
have "∃a as' as''. n -as'→⇩ι* sourcenode a ∧ targetnode a -as''→⇩ι* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧ intra_kind (kind a) ∧
obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx} ∧
(¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}))"
proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note IH = ‹⋀nx'. ⟦n' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙;
nx' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙; n' ≠ nx';
obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'};
∀a∈set as. intra_kind (kind a);
∀n'∈set (sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙; as ≠ []⟧
⟹ ∃a as' as''. n'' -as'→⇩ι* sourcenode a ∧ targetnode a -as''→⇩ι* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ intra_kind (kind a) ∧
obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {n'} ∧
(¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}))›
note more_than_one = ‹n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙›
‹nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› ‹n' ≠ nx'›
from ‹∀a∈set (a#as). intra_kind (kind a)›
have "∀a∈set as. intra_kind (kind a)" and "intra_kind (kind a)" by simp_all
from ‹∀n'∈set (sourcenodes (a#as)). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
have all:"∀n'∈set (sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
show ?case
proof(cases "as = []")
case True
with ‹n'' -as→* n'› have [simp]:"n'' = n'" by(fastforce elim:path.cases)
from more_than_one ‹sourcenode a = n›
have "¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {})"
by auto
with ‹targetnode a = n''› ‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}›
‹sourcenode a = n› True ‹valid_edge a› ‹intra_kind (kind a)›
show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="[]" in exI)
by(auto intro:empty_path simp:intra_path_def)
next
case False
from ‹n'' -as→* n'› ‹∀a∈set (a # as). intra_kind (kind a)›
have "n'' -as→⇩ι* n'" by(simp add:intra_path_def)
with all
have subset:"obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ ⊆ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙"
by -(rule path_obs_intra_subset)
thus ?thesis
proof(cases "obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙")
case True
with ‹n'' -as→⇩ι* n'› ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''›
‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}› ‹intra_kind (kind a)› more_than_one
show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="as" in exI)
by(fastforce intro:empty_path simp:intra_path_def)
next
case False
with subset
have "obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ ⊂ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙" by simp
with ‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}›
obtain ni where "n' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙"
and "ni ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙" and "n' ≠ ni" by auto
from IH[OF this ‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}›
‹∀a∈set as. intra_kind (kind a)› all ‹as ≠ []›] obtain a' as' as''
where "n'' -as'→⇩ι* sourcenode a'"
and hyps:"targetnode a' -as''→⇩ι* n'" "valid_edge a'" "as = as'@a'#as''"
"intra_kind (kind a')" "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ = {n'}"
"¬ (∃m. obs_intra (sourcenode a') ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a') ⌊HRB_slice S⌋⇘CFG⇙ = {})"
by blast
from ‹n'' -as'→⇩ι* sourcenode a'› ‹valid_edge a› ‹sourcenode a = n›
‹targetnode a = n''› ‹intra_kind (kind a)› ‹intra_kind (kind a')›
have "n -a#as'→⇩ι* sourcenode a'"
by(fastforce intro:path.Cons_path simp:intra_path_def)
with hyps show ?thesis
apply(rule_tac x="a'" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="as''" in exI)
by fastforce
qed
qed
qed simp
then obtain a as' as'' where "valid_edge a" and "intra_kind (kind a)"
and "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}"
and more_than_one:"¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {})"
by blast
have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof(rule ccontr)
assume "¬ sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
hence "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by simp
with ‹valid_edge a›
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
with more_than_one show False by simp
qed
with ‹valid_edge a› ‹intra_kind (kind a)›
have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
by(rule edge_obs_intra_subset)
with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}›
have "nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by simp
with more_than_one obtain m
where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" and "nx ≠ m" by auto
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› have "valid_node m"
by(fastforce dest:in_obs_intra_valid)
from ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}› have "valid_node nx"
by(fastforce dest:in_obs_intra_valid)
show False
proof(cases "m postdominates (sourcenode a)")
case True
with ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m postdominates nx"
by(fastforce intro:postdominate_inner_path_targetnode elim:obs_intraE)
with ‹nx ≠ m› have "¬ nx postdominates m" by(fastforce dest:postdominate_antisym)
with ‹valid_node nx› ‹valid_node m› obtain asx pex where "m -asx→⇩ι* pex"
and "method_exit pex" and "nx ∉ set(sourcenodes asx)"
by(fastforce simp:postdominate_def)
have "¬ nx postdominates (sourcenode a)"
proof
assume "nx postdominates sourcenode a"
from ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
obtain asx' where "sourcenode a -asx'→⇩ι* m" and "nx ∉ set(sourcenodes asx')"
by(fastforce elim:obs_intraE)
with ‹m -asx→⇩ι* pex› have "sourcenode a -asx'@asx→⇩ι* pex"
by(fastforce intro:path_Append simp:intra_path_def)
with ‹nx ∉ set(sourcenodes asx)› ‹nx ∉ set(sourcenodes asx')›
‹nx postdominates sourcenode a› ‹method_exit pex› show False
by(fastforce simp:sourcenodes_def postdominate_def)
qed
show False
proof(cases "method_exit nx")
case True
from ‹m postdominates nx› obtain xs where "nx -xs→⇩ι* m"
by -(erule postdominate_implies_inner_path)
with True have "nx = m"
by(fastforce dest!:method_exit_inner_path simp:intra_path_def)
with ‹nx ≠ m› show False by simp
next
case False
with ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "nx postdominates sourcenode a" by(rule obs_intra_postdominate)
with ‹¬ nx postdominates (sourcenode a)› show False by simp
qed
next
case False
show False
proof(cases "method_exit m")
case True
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
obtain xs where "sourcenode a -xs→⇩ι* m" and "nx ∉ set(sourcenodes xs)"
by(fastforce elim:obs_intraE)
obtain x' xs' where [simp]:"xs = x'#xs'"
proof(cases xs)
case Nil
with ‹sourcenode a -xs→⇩ι* m› have [simp]:"sourcenode a = m"
by(fastforce simp:intra_path_def)
with ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(metis obs_intraE)
with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
by(rule n_in_obs_intra)
with ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ m› have False
by fastforce
thus ?thesis by simp
qed blast
from ‹sourcenode a -xs→⇩ι* m› have "sourcenode a = sourcenode x'"
and "valid_edge x'" and "targetnode x' -xs'→⇩ι* m"
and "intra_kind (kind x')"
by(auto elim:path_split_Cons simp:intra_path_def)
from ‹targetnode x' -xs'→⇩ι* m› ‹nx ∉ set(sourcenodes xs)› ‹valid_edge x'›
‹valid_node m› True
have "¬ nx postdominates (targetnode x')"
by(fastforce simp:postdominate_def sourcenodes_def)
show False
proof(cases "method_exit nx")
case True
from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "get_proc m = get_proc nx"
by(fastforce elim:obs_intraE dest:intra_path_get_procs)
with ‹method_exit m› ‹method_exit nx› have "m = nx"
by(rule method_exit_unique)
with ‹nx ≠ m› show False by simp
next
case False
with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}›
have "nx postdominates (targetnode a)"
by(fastforce intro:obs_intra_postdominate)
from ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}›
obtain ys where "targetnode a -ys→⇩ι* nx"
and "∀nx' ∈ set(sourcenodes ys). nx' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
and "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce elim:obs_intraE)
hence "nx ∉ set(sourcenodes ys)"by fastforce
have "sourcenode a ≠ nx"
proof
assume "sourcenode a = nx"
from ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙" by -(erule obs_intraE)
with ‹valid_node nx›
have "obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}" by -(erule n_in_obs_intra)
with ‹sourcenode a = nx› ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹nx ≠ m› show False by fastforce
qed
with ‹nx ∉ set(sourcenodes ys)› have "nx ∉ set(sourcenodes (a#ys))"
by(fastforce simp:sourcenodes_def)
from ‹valid_edge a› ‹targetnode a -ys→⇩ι* nx› ‹intra_kind (kind a)›
have "sourcenode a -a#ys→⇩ι* nx"
by(fastforce intro:Cons_path simp:intra_path_def)
from ‹sourcenode a -a#ys→⇩ι* nx› ‹nx ∉ set(sourcenodes (a#ys))›
‹intra_kind (kind a)› ‹nx postdominates (targetnode a)›
‹valid_edge x'› ‹intra_kind (kind x')› ‹¬ nx postdominates (targetnode x')›
‹sourcenode a = sourcenode x'›
have "(sourcenode a) controls nx"
by(fastforce simp:control_dependence_def)
hence "CFG_node (sourcenode a) ⟶⇘cd⇙ CFG_node nx"
by(fastforce intro:SDG_cdep_edge)
with ‹nx ∈ ⌊HRB_slice S⌋⇘CFG⇙› have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
by(fastforce elim!:combine_SDG_slices.cases
dest:SDG_edge_sum_SDG_edge cdep_slice1 cdep_slice2
intro:combine_SDG_slices.intros
simp:HRB_slice_def SDG_to_CFG_set_def)
with ‹valid_edge a›
have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
by(fastforce intro!:n_in_obs_intra)
with ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ m›
show False by simp
qed
next
case False
with ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
have "m postdominates (sourcenode a)" by(rule obs_intra_postdominate)
with ‹¬ m postdominates (sourcenode a)› show False by simp
qed
qed
qed

lemma obs_intra_finite:"valid_node n ⟹ finite (obs_intra n ⌊HRB_slice S⌋⇘CFG⇙)"
by(fastforce dest:obs_intra_singleton_disj[of _ S])

lemma obs_intra_singleton:"valid_node n ⟹ card (obs_intra n ⌊HRB_slice S⌋⇘CFG⇙) ≤ 1"
by(fastforce dest:obs_intra_singleton_disj[of _ S])

lemma obs_intra_singleton_element:
"m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ⟹ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
apply -
apply(frule in_obs_intra_valid)
apply(drule obs_intra_singleton_disj) apply auto
done

lemma obs_intra_the_element:
"m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ⟹ (THE m. m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙) = m"
by(fastforce dest:obs_intra_singleton_element)

lemma obs_singleton_element:
assumes "ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙" and "∀n ∈ set (tl ns). return_node n"
shows "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {ms}"
proof -
from ‹ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙› ‹∀n ∈ set (tl ns). return_node n›
obtain nsx n nsx' n' where "ns = nsx@n#nsx'" and "ms = n'#nsx'"
and split:"n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
"∀nx ∈ set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
"∀xs x xs'. nsx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
⟶ (∃x'' ∈ set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧
nx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
from ‹n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙›
have "obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {n'}"
by(fastforce intro!:obs_intra_singleton_element)
{ fix xs assume "xs ≠ ms" and "xs ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙"
from ‹xs ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙› ‹∀n ∈ set (tl ns). return_node n›
obtain zs z zs' z' where "ns = zs@z#zs'" and "xs = z'#zs'"
and "z' ∈ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙"
and "∀z' ∈ set zs'. ∃nx'. call_of_return_node z' nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
and "∀xs x xs'. zs = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
⟶ (∃x'' ∈ set (xs'@[z]). ∃nx. call_of_return_node x'' nx ∧
nx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
by(erule obsE)
with ‹ns = nsx@n#nsx'› split
have "nsx = zs ∧ n = z ∧ nsx' = zs'"
by -(rule obs_split_det[of _ _ _ _ _ _ "⌊HRB_slice S⌋⇘CFG⇙"],fastforce+)
with ‹obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {n'}› ‹z' ∈ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙›
have "z' = n'" by simp
with ‹xs ≠ ms› ‹ms = n'#nsx'› ‹xs = z'#zs'› ‹nsx = zs ∧ n = z ∧ nsx' = zs'›
have False by simp }
with ‹ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙› show ?thesis by fastforce
qed

lemma obs_finite:"∀n ∈ set (tl ns). return_node n
⟹ finite (obs ns ⌊HRB_slice S⌋⇘CFG⇙)"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])

lemma obs_singleton:"∀n ∈ set (tl ns). return_node n
⟹ card (obs ns ⌊HRB_slice S⌋⇘CFG⇙) ≤ 1"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])

lemma obs_the_element:
"⟦ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙; ∀n ∈ set (tl ns). return_node n⟧
⟹ (THE ms. ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙) = ms"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])

end

end
```