Theory Postdomination

Up to index of Isabelle/HOL/Jinja/Slicing

theory Postdomination
imports CFGExit
header {* \isaheader{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'"
by(simp_all add:postdominate_def)
{ 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'"
by(simp add:postdominate_def)
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')"
by(simp add:sourcenodes_def)
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'')"
by(simp_all add:postdominate_def)
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''))"
by(simp add:sourcenodes_def)
with `n -as@as''->* (_Exit_)` `n' postdominates n` show False
by(simp add:postdominate_def)
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)
apply simp_all
by fastforce
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
moreover
from this `targetnode ax ∈ N` have "?N' ≠ {}" by auto
ultimately 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