Theory Slicing.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'"
    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)
      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