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'"
    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