# Theory Postdomination

```section ‹Postdomination›

theory Postdomination imports CFGExit begin

subsection ‹Standard Postdomination›

locale Postdomination = CFGExit sourcenode targetnode kind valid_edge Entry Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Exit :: "'node" ("'('_Exit'_')") +
assumes Entry_path:"valid_node n ⟹ ∃as. (_Entry_) -as→* n"
and Exit_path:"valid_node n ⟹ ∃as. n -as→* (_Exit_)"

begin

definition postdominate :: "'node ⇒ 'node ⇒ bool" ("_ postdominates _" [51,0])
where postdominate_def:"n' postdominates n ≡
(valid_node n ∧ valid_node n' ∧
((∀as. n -as→* (_Exit_) ⟶ n' ∈ set (sourcenodes as))))"

lemma postdominate_implies_path:
assumes "n' postdominates n" obtains as where "n -as→* n'"
proof(atomize_elim)
from ‹n' postdominates n› have "valid_node n"
and all:"∀as. n -as→* (_Exit_) ⟶ n' ∈ set(sourcenodes as)"
by(auto simp:postdominate_def)
from ‹valid_node n› obtain as where "n -as→* (_Exit_)" by(auto dest:Exit_path)
with all have "n' ∈ set(sourcenodes as)" by simp
then obtain ns ns' where "sourcenodes as = ns@n'#ns'" by(auto dest:split_list)
then obtain as' a as'' where "sourcenodes as' = ns"
and "sourcenode a = n'" and "as = as'@a#as''"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹n -as→* (_Exit_)› ‹as = as'@a#as''› have "n -as'→* sourcenode a"
by(fastforce dest:path_split)
with ‹sourcenode a = n'› show "∃as. n -as→* n'" by blast
qed

lemma postdominate_refl:
assumes valid:"valid_node n" and notExit:"n ≠ (_Exit_)"
shows "n postdominates n"
using valid
proof(induct rule:valid_node_cases)
case Entry
{ fix as assume path:"(_Entry_) -as→* (_Exit_)"
hence notempty:"as ≠ []"
apply - apply(erule path.cases)
by (drule sym,simp,drule Exit_noteq_Entry,auto)
with path have "hd (sourcenodes as) = (_Entry_)"
by(fastforce intro:path_sourcenode)
with notempty have "(_Entry_) ∈ set (sourcenodes as)"
by(fastforce intro:hd_in_set simp:sourcenodes_def) }
with Entry show ?thesis by(simp add:postdominate_def)
next
case Exit
with notExit have False by simp
thus ?thesis by simp
next
case inner
show ?thesis
proof(cases "∃as. n -as→* (_Exit_)")
case True
{ fix as' assume path':"n -as'→* (_Exit_)"
with inner have notempty:"as' ≠ []"
by(cases as',auto elim!:path.cases simp:inner_node_def)
with path' inner have hd:"hd (sourcenodes as') = n"
by -(rule path_sourcenode)
from notempty have "sourcenodes as' ≠ []" by(simp add:sourcenodes_def)
with hd[THEN sym] have "n ∈ set (sourcenodes as')" by simp }
hence "∀as. n -as→* (_Exit_) ⟶ n ∈ set (sourcenodes as)" by simp
with True inner show ?thesis by(simp add:postdominate_def inner_is_valid)
next
case False
with inner show ?thesis by(simp add:postdominate_def inner_is_valid)
qed
qed

lemma postdominate_trans:
assumes pd1:"n'' postdominates n" and pd2:"n' postdominates n''"
shows "n' postdominates n"
proof -
from pd1 pd2 have valid:"valid_node n" and valid':"valid_node n'"
{ fix as assume path:"n -as→* (_Exit_)"
with pd1 have "n'' ∈ set (sourcenodes as)" by(simp add:postdominate_def)
then obtain ns' ns'' where "sourcenodes as = ns'@n''#ns''"
by(auto dest:split_list)
then obtain as' as'' a
where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
and source:"sourcenode a = n''"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from as path have "n -as'@a#as''→* (_Exit_)" by simp
with source have path':"n'' -a#as''→* (_Exit_)"
by(fastforce dest:path_split_second)
with pd2 have "n' ∈ set(sourcenodes (a#as''))"
by(auto simp:postdominate_def)
with as have "n' ∈ set(sourcenodes as)" by(auto simp:sourcenodes_def) }
with valid valid' show ?thesis by(simp add:postdominate_def)
qed

lemma postdominate_antisym:
assumes pd1:"n' postdominates n" and pd2:"n postdominates n'"
shows "n = n'"
proof -
from pd1 have valid:"valid_node n" and valid':"valid_node n'"
by(auto simp:postdominate_def)
from valid obtain as where path1:"n -as→* (_Exit_)" by(fastforce dest:Exit_path)
from valid' obtain as' where path2:"n' -as'→* (_Exit_)" by(fastforce dest:Exit_path)
from pd1 path1 have "∃nx ∈ set(sourcenodes as). nx = n'"
then obtain ns ns' where sources:"sourcenodes as = ns@n'#ns'"
and all:"∀nx ∈ set ns'. nx ≠ n'"
by(fastforce elim!: rightmost_element_property)
from sources obtain asx a asx' where ns':"ns' = sourcenodes asx'"
and as:"as = asx@a#asx'" and source:"sourcenode a = n'"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from path1 as have "n -asx@a#asx'→* (_Exit_)" by simp
with source have "n' -a#asx'→* (_Exit_)" by(fastforce dest:path_split_second)
with pd2 have "n ∈ set(sourcenodes (a#asx'))" by(simp add:postdominate_def)
with source have "n = n' ∨ n ∈ set(sourcenodes asx')" by(simp add:sourcenodes_def)
thus ?thesis
proof
assume "n = n'" thus ?thesis .
next
assume "n ∈ set(sourcenodes asx')"
then obtain nsx' nsx'' where "sourcenodes asx' = nsx'@n#nsx''"
by(auto dest:split_list)
then obtain asi asi' a' where asx':"asx' = asi@a'#asi'"
and source':"sourcenode a' = n"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
with path1 as have "n -(asx@a#asi)@a'#asi'→* (_Exit_)" by simp
with source' have "n -a'#asi'→* (_Exit_)" by(fastforce dest:path_split_second)
with pd1 have "n' ∈ set(sourcenodes (a'#asi'))" by(auto simp:postdominate_def)
with source' have "n' = n ∨ n' ∈ set(sourcenodes asi')"
thus ?thesis
proof
assume "n' = n" thus ?thesis by(rule sym)
next
assume "n' ∈ set(sourcenodes asi')"
with asx' ns' have "n' ∈ set ns'" by(simp add:sourcenodes_def)
with all have False by blast
thus ?thesis by simp
qed
qed
qed

lemma postdominate_path_branch:
assumes "n -as→* n''" and "n' postdominates n''" and "¬ n' postdominates n"
obtains a as' as'' where "as = as'@a#as''" and "valid_edge a"
and "¬ n' postdominates (sourcenode a)" and "n' postdominates (targetnode a)"
proof(atomize_elim)
from assms
show "∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' postdominates (sourcenode a) ∧ n' postdominates (targetnode a)"
proof(induct rule:path.induct)
case (Cons_path n'' as nx a n)
note IH = ‹⟦n' postdominates nx; ¬ n' postdominates n''⟧
⟹ ∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' postdominates sourcenode a ∧ n' postdominates targetnode a›
show ?case
proof(cases "n' postdominates n''")
case True
with ‹¬ n' postdominates n› ‹sourcenode a = n› ‹targetnode a = n''›
‹valid_edge a›
show ?thesis by blast
next
case False
from IH[OF ‹n' postdominates nx› this] show ?thesis
by clarsimp(rule_tac x="a#as'" in exI,clarsimp)
qed
qed simp
qed

lemma Exit_no_postdominator:
"(_Exit_) postdominates n ⟹ False"
by(fastforce dest:Exit_path simp:postdominate_def)

lemma postdominate_path_targetnode:
assumes "n' postdominates n" and "n -as→* n''" and "n' ∉ set(sourcenodes as)"
shows "n' postdominates n''"
proof -
from ‹n' postdominates n› have "valid_node n" and "valid_node n'"
and all:"∀as''. n -as''→* (_Exit_) ⟶ n' ∈ set(sourcenodes as'')"
from ‹n -as→* n''› have "valid_node n''" by(fastforce dest:path_valid_node)
have "∀as''. n'' -as''→* (_Exit_) ⟶ n' ∈ set(sourcenodes as'')"
proof(rule ccontr)
assume "¬ (∀as''. n'' -as''→* (_Exit_) ⟶ n' ∈ set (sourcenodes as''))"
then obtain as'' where "n'' -as''→* (_Exit_)"
and "n' ∉ set (sourcenodes as'')" by blast
from ‹n -as→* n''› ‹n'' -as''→* (_Exit_)› have "n -as@as''→* (_Exit_)"
by(rule path_Append)
with ‹n' ∉ set(sourcenodes as)› ‹n' ∉ set (sourcenodes as'')›
have "n' ∉ set (sourcenodes (as@as''))"
with ‹n -as@as''→* (_Exit_)› ‹n' postdominates n› show False
qed
with ‹valid_node n'› ‹valid_node n''› show ?thesis by(simp add:postdominate_def)
qed

lemma not_postdominate_source_not_postdominate_target:
assumes "¬ n postdominates (sourcenode a)" and "valid_node n" and "valid_edge a"
obtains ax where "sourcenode a = sourcenode ax" and "valid_edge ax"
and "¬ n postdominates targetnode ax"
proof(atomize_elim)
show "∃ax. sourcenode a = sourcenode ax ∧ valid_edge ax ∧
¬ n postdominates targetnode ax"
proof -
from assms obtain asx
where "sourcenode a -asx→* (_Exit_)"
and "n ∉ set(sourcenodes asx)" by(auto simp:postdominate_def)
from ‹sourcenode a -asx→* (_Exit_)› ‹valid_edge a›
obtain ax asx' where [simp]:"asx = ax#asx'"
apply - apply(erule path.cases)
apply(drule_tac s="(_Exit_)" in sym)
apply simp
apply(drule Exit_source)
by simp_all
with ‹sourcenode a -asx→* (_Exit_)› have "sourcenode a -[]@ax#asx'→* (_Exit_)"
by simp
hence "valid_edge ax" and "sourcenode a = sourcenode ax"
and "targetnode ax -asx'→* (_Exit_)"
by(fastforce dest:path_split)+
with ‹n ∉ set(sourcenodes asx)› have "¬ n postdominates targetnode ax"
by(fastforce simp:postdominate_def sourcenodes_def)
with ‹sourcenode a = sourcenode ax› ‹valid_edge ax› show ?thesis by blast
qed
qed

lemma inner_node_Entry_edge:
assumes "inner_node n"
obtains a where "valid_edge a" and "inner_node (targetnode a)"
and "sourcenode a = (_Entry_)"
proof(atomize_elim)
from ‹inner_node n› have "valid_node n" by(rule inner_is_valid)
then obtain as where "(_Entry_) -as→* n" by(fastforce dest:Entry_path)
show "∃a. valid_edge a ∧ inner_node (targetnode a) ∧ sourcenode a = (_Entry_)"
proof(cases "as = []")
case True
with ‹inner_node n› ‹(_Entry_) -as→* n› have False
by(fastforce simp:inner_node_def)
thus ?thesis by simp
next
case False
with ‹(_Entry_) -as→* n› obtain a' as' where "as = a'#as'"
and "(_Entry_) = sourcenode a'" and "valid_edge a'"
and "targetnode a' -as'→* n"
by -(erule path_split_Cons)
from ‹valid_edge a'› have "valid_node (targetnode a')" by simp
thus ?thesis
proof(cases "targetnode a'" rule:valid_node_cases)
case Entry
from ‹valid_edge a'› this have False by(rule Entry_target)
thus ?thesis by simp
next
case Exit
with ‹targetnode a' -as'→* n› ‹inner_node n›
have False by simp (drule path_Exit_source,auto simp:inner_node_def)
thus ?thesis by simp
next
case inner
with ‹valid_edge a'› ‹(_Entry_) = sourcenode a'› show ?thesis by simp blast
qed
qed
qed

lemma inner_node_Exit_edge:
assumes "inner_node n"
obtains a where "valid_edge a" and "inner_node (sourcenode a)"
and "targetnode a = (_Exit_)"
proof(atomize_elim)
from ‹inner_node n› have "valid_node n" by(rule inner_is_valid)
then obtain as where "n -as→* (_Exit_)" by(fastforce dest:Exit_path)
show "∃a. valid_edge a ∧ inner_node (sourcenode a) ∧ targetnode a = (_Exit_)"
proof(cases "as = []")
case True
with ‹inner_node n› ‹n -as→* (_Exit_)› have False by fastforce
thus ?thesis by simp
next
case False
with ‹n -as→* (_Exit_)› obtain a' as' where "as = as'@[a']"
and "n -as'→* sourcenode a'" and "valid_edge a'"
and "(_Exit_) = targetnode a'" by -(erule path_split_snoc)
from ‹valid_edge a'› have "valid_node (sourcenode a')" by simp
thus ?thesis
proof(cases "sourcenode a'" rule:valid_node_cases)
case Entry
with ‹n -as'→* sourcenode a'› ‹inner_node n›
have False by simp (drule path_Entry_target,auto simp:inner_node_def)
thus ?thesis by simp
next
case Exit
from ‹valid_edge a'› this have False by(rule Exit_source)
thus ?thesis by simp
next
case inner
with ‹valid_edge a'› ‹(_Exit_) = targetnode a'› show ?thesis by simp blast
qed
qed
qed

end

subsection ‹Strong Postdomination›

locale StrongPostdomination =
Postdomination sourcenode targetnode kind valid_edge Entry Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Exit :: "'node" ("'('_Exit'_')") +
assumes successor_set_finite: "valid_node n ⟹
finite {n'. ∃a'. valid_edge a' ∧ sourcenode a' = n ∧ targetnode a' = n'}"

begin

definition  strong_postdominate :: "'node ⇒ 'node ⇒ bool"
("_ strongly-postdominates _" [51,0])
where strong_postdominate_def:"n' strongly-postdominates n ≡
(n' postdominates n ∧
(∃k ≥ 1. ∀as nx. n -as→* nx ∧
length as ≥ k ⟶ n' ∈ set(sourcenodes as)))"

lemma strong_postdominate_prop_smaller_path:
assumes all:"∀as nx. n -as→* nx ∧ length as ≥ k ⟶ n' ∈ set(sourcenodes as)"
and "n -as→* n''" and "length as ≥ k"
obtains as' as'' where "n -as'→* n'" and "length as' < k" and "n' -as''→* n''"
and "as = as'@as''"
proof(atomize_elim)
show "∃as' as''. n -as'→* n' ∧ length as' < k ∧ n' -as''→* n'' ∧ as = as'@as''"
proof(rule ccontr)
assume "¬ (∃as' as''. n -as'→* n' ∧ length as' < k ∧ n' -as''→* n'' ∧
as = as'@as'')"
hence all':"∀as' as''. n -as'→* n' ∧ n' -as''→* n'' ∧ as = as'@as''
⟶ length as' ≥ k" by fastforce
from all ‹n -as→* n''› ‹length as ≥ k› have "∃nx ∈ set(sourcenodes as). nx = n'"
by fastforce
then obtain ns ns' where "sourcenodes as = ns@n'#ns'"
and "∀nx ∈ set ns. nx ≠ n'"
by(fastforce elim!:split_list_first_propE)
then obtain asx a asx' where [simp]:"ns = sourcenodes asx"
and [simp]:"as = asx@a#asx'" and "sourcenode a = n'"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹n -as→* n''› have "n -asx@a#asx'→* n''" by simp
with ‹sourcenode a = n'› have "n -asx→* n'" and "valid_edge a"
and "targetnode a -asx'→* n''" by(fastforce dest:path_split)+
with ‹sourcenode a = n'› have "n' -a#asx'→* n''" by(fastforce intro:Cons_path)
with ‹n -asx→* n'› all' have "length asx ≥ k" by simp
with ‹n -asx→* n'› all have "n' ∈ set(sourcenodes asx)" by fastforce
with ‹∀nx ∈ set ns. nx ≠ n'› show False by fastforce
qed
qed

lemma strong_postdominate_refl:
assumes "valid_node n" and "n ≠ (_Exit_)"
shows "n strongly-postdominates n"
proof -
from assms have "n postdominates n" by(rule postdominate_refl)
{ fix as nx assume "n -as→* nx" and "length as ≥ 1"
then obtain a' as' where [simp]:"as = a'#as'" by(cases as) auto
with ‹n -as→* nx› have "n -[]@a'#as'→* nx" by simp
hence "n = sourcenode a'" by(fastforce dest:path_split)
hence "n ∈ set(sourcenodes as)" by(simp add:sourcenodes_def) }
hence "∀as nx. n -as→* nx ∧ length as ≥ 1 ⟶ n ∈ set(sourcenodes as)"
by auto
hence "∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k ⟶ n ∈ set(sourcenodes as)"
by blast
with ‹n postdominates n› show ?thesis by(simp add:strong_postdominate_def)
qed

lemma strong_postdominate_trans:
assumes "n'' strongly-postdominates n" and "n' strongly-postdominates n''"
shows "n' strongly-postdominates n"
proof -
from ‹n'' strongly-postdominates n› have "n'' postdominates n"
and paths1:"∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n'' ∈ set(sourcenodes as)"
by(auto simp only:strong_postdominate_def)
from paths1 obtain k1
where all1:"∀as nx. n -as→* nx ∧ length as ≥ k1 ⟶ n'' ∈ set(sourcenodes as)"
and "k1 ≥ 1" by blast
from ‹n' strongly-postdominates n''› have "n' postdominates n''"
and paths2:"∃k ≥ 1. ∀as nx. n'' -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)"
by(auto simp only:strong_postdominate_def)
from paths2 obtain k2
where all2:"∀as nx. n'' -as→* nx ∧ length as ≥ k2 ⟶ n' ∈ set(sourcenodes as)"
and "k2 ≥ 1" by blast
from ‹n'' postdominates n› ‹n' postdominates n''›
have "n' postdominates n" by(rule postdominate_trans)
{ fix as nx assume "n -as→* nx" and "length as ≥ k1 + k2"
hence "length as ≥ k1" by fastforce
with ‹n -as→* nx› all1 obtain asx asx' where "n -asx→* n''"
and "length asx < k1" and "n'' -asx'→* nx"
and [simp]:"as = asx@asx'" by -(erule strong_postdominate_prop_smaller_path)
with ‹length as ≥ k1 + k2› have "length asx' ≥ k2" by fastforce
with ‹n'' -asx'→* nx› all2 have "n' ∈ set(sourcenodes asx')" by fastforce
hence "n' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def) }
with ‹k1 ≥ 1› ‹k2 ≥ 1› have "∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)"
by(rule_tac x="k1 + k2" in exI,auto)
with ‹n' postdominates n› show ?thesis by(simp add:strong_postdominate_def)
qed

lemma strong_postdominate_antisym:
"⟦n' strongly-postdominates n; n strongly-postdominates n'⟧ ⟹ n = n'"
by(fastforce intro:postdominate_antisym simp:strong_postdominate_def)

lemma strong_postdominate_path_branch:
assumes "n -as→* n''" and "n' strongly-postdominates n''"
and "¬ n' strongly-postdominates n"
obtains a as' as'' where "as = as'@a#as''" and "valid_edge a"
and "¬ n' strongly-postdominates (sourcenode a)"
and "n' strongly-postdominates (targetnode a)"
proof(atomize_elim)
from assms
show "∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' strongly-postdominates (sourcenode a) ∧
n' strongly-postdominates (targetnode a)"
proof(induct rule:path.induct)
case (Cons_path n'' as nx a n)
note IH = ‹⟦n' strongly-postdominates nx; ¬ n' strongly-postdominates n''⟧
⟹ ∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' strongly-postdominates sourcenode a ∧
n' strongly-postdominates targetnode a›
show ?case
proof(cases "n' strongly-postdominates n''")
case True
with ‹¬ n' strongly-postdominates n› ‹sourcenode a = n› ‹targetnode a = n''›
‹valid_edge a›
show ?thesis by blast
next
case False
from IH[OF ‹n' strongly-postdominates nx› this] show ?thesis
by clarsimp(rule_tac x="a#as'" in exI,clarsimp)
qed
qed simp
qed

lemma Exit_no_strong_postdominator:
"⟦(_Exit_) strongly-postdominates n; n -as→* (_Exit_)⟧ ⟹ False"
by(fastforce intro:Exit_no_postdominator path_valid_node simp:strong_postdominate_def)

lemma strong_postdominate_path_targetnode:
assumes "n' strongly-postdominates n" and "n -as→* n''"
and "n' ∉ set(sourcenodes as)"
shows "n' strongly-postdominates n''"
proof -
from ‹n' strongly-postdominates n› have "n' postdominates n"
and "∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)"
by(auto simp only:strong_postdominate_def)
then obtain k where "k ≥ 1"
and paths:"∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)" by auto
from ‹n' postdominates n› ‹n -as→* n''› ‹n' ∉ set(sourcenodes as)›
have "n' postdominates n''"
by(rule postdominate_path_targetnode)
{ fix as' nx assume "n'' -as'→* nx" and "length as' ≥ k"
with ‹n -as→* n''› have "n -as@as'→* nx" and "length (as@as') ≥ k"
by(auto intro:path_Append)
with paths have "n' ∈ set(sourcenodes (as@as'))" by fastforce
with ‹n' ∉ set(sourcenodes as)› have "n' ∈ set(sourcenodes as')"
by(fastforce simp:sourcenodes_def) }
with ‹k ≥ 1› have "∃k ≥ 1. ∀as' nx. n'' -as'→* nx ∧ length as' ≥ k
⟶ n' ∈ set(sourcenodes as')" by auto
with ‹n' postdominates n''› show ?thesis by(simp add:strong_postdominate_def)
qed

lemma not_strong_postdominate_successor_set:
assumes "¬ n strongly-postdominates (sourcenode a)" and "valid_node n"
and "valid_edge a"
and all:"∀nx ∈ N. ∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
targetnode a' = nx ∧ n strongly-postdominates nx"
obtains a' where "valid_edge a'" and "sourcenode a' =  sourcenode a"
and "targetnode a' ∉ N"
proof(atomize_elim)
show "∃a'. valid_edge a' ∧ sourcenode a' =  sourcenode a ∧ targetnode a' ∉ N"
proof(cases "n postdominates (sourcenode a)")
case False
with ‹valid_edge a› ‹valid_node n›
obtain a' where [simp]:"sourcenode a = sourcenode a'"
and "valid_edge a'" and "¬ n postdominates targetnode a'"
by -(erule not_postdominate_source_not_postdominate_target)
with all have "targetnode a' ∉ N" by(auto simp:strong_postdominate_def)
with ‹valid_edge a'› show ?thesis by simp blast
next
case True
let ?M = "{n'. ∃a'. valid_edge a' ∧ sourcenode a' =  sourcenode a ∧
targetnode a' = n'}"
let ?M' = "{n'. ∃a'. valid_edge a' ∧ sourcenode a' =  sourcenode a ∧
targetnode a' = n' ∧ n strongly-postdominates n'}"
let ?N' = "(λn'. SOME i. i ≥ 1 ∧
(∀as nx. n' -as→* nx ∧ length as ≥ i
⟶ n ∈ set(sourcenodes as))) ` N"
obtain k where [simp]:"k = Max ?N'" by simp
have eq:"{x ∈ ?M. (λn'. n strongly-postdominates n') x} = ?M'" by auto
from ‹valid_edge a› have "finite ?M" by(simp add:successor_set_finite)
hence "finite {x ∈ ?M. (λn'. n strongly-postdominates n') x}" by fastforce
with eq have "finite ?M'" by simp
from all have "N ⊆ ?M'" by auto
with ‹finite ?M'› have "finite N" by(auto intro:finite_subset)
hence "finite ?N'" by fastforce
show ?thesis
proof(rule ccontr)
assume "¬ (∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
targetnode a' ∉ N)"
hence allImp:"∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a
⟶ targetnode a' ∈ N" by blast
from True ‹¬ n strongly-postdominates (sourcenode a)›
have allPaths:"∀k ≥ 1. ∃as nx. sourcenode a -as→* nx ∧ length as ≥ k
∧ n ∉ set(sourcenodes as)" by(auto simp:strong_postdominate_def)
then obtain as nx where "sourcenode a -as→* nx"
and "length as ≥ k + 1" and "n ∉ set(sourcenodes as)"
by (erule_tac x="k + 1" in allE) auto
then obtain ax as' where [simp]:"as = ax#as'" and "valid_edge ax"
and "sourcenode ax = sourcenode a" and "targetnode ax -as'→* nx"
by -(erule path.cases,auto)
with allImp have "targetnode ax ∈ N" by fastforce
with all have "n strongly-postdominates (targetnode ax)"
by auto
then obtain k' where k':"k' = (SOME i. i ≥ 1 ∧
(∀as nx. targetnode ax -as→* nx ∧ length as ≥ i
⟶ n ∈ set(sourcenodes as)))" by simp
with ‹n strongly-postdominates (targetnode ax)›
have "k' ≥ 1 ∧ (∀as nx. targetnode ax -as→* nx ∧ length as ≥ k'
⟶ n ∈ set(sourcenodes as))"
by(auto elim!:someI_ex simp:strong_postdominate_def)
hence "k' ≥ 1"
and spdAll:"∀as nx. targetnode ax -as→* nx ∧ length as ≥ k'
⟶ n ∈ set(sourcenodes as)"
by simp_all
from ‹targetnode ax ∈ N› k' have "k' ∈ ?N'" by blast
with ‹targetnode ax ∈ N› have "?N' ≠ {}" by auto
with ‹k' ∈ ?N'› have "k' ≤ Max ?N'" using ‹finite ?N'› by(fastforce intro:Max_ge)
hence "k' ≤ k" by simp
with ‹targetnode ax -as'→* nx› ‹length as ≥ k + 1› spdAll
have "n ∈ set(sourcenodes as')"
by fastforce
with ‹n ∉ set(sourcenodes as)› show False by(simp add:sourcenodes_def)
qed
qed
qed

lemma not_strong_postdominate_predecessor_successor:
assumes "¬ n strongly-postdominates (sourcenode a)"
and "valid_node n" and "valid_edge a"
obtains a' where "valid_edge a'" and "sourcenode a' = sourcenode a"
and "¬ n strongly-postdominates (targetnode a')"
proof(atomize_elim)
show "∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
¬ n strongly-postdominates (targetnode a')"
proof(rule ccontr)
assume "¬ (∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
¬ n strongly-postdominates targetnode a')"
hence all:"∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a ⟶
n strongly-postdominates (targetnode a')" by auto
let ?N = "{n'. ∃a'. sourcenode a' =  sourcenode a ∧ valid_edge a' ∧
targetnode a' = n'}"
from all have "∀nx ∈ ?N. ∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
targetnode a' = nx ∧ n strongly-postdominates nx"
by auto
with assms obtain a' where "valid_edge a'"
and "sourcenode a' =  sourcenode a" and "targetnode a' ∉ ?N"
by(erule not_strong_postdominate_successor_set)
thus False by auto
qed
qed

end

end
```