section ‹Auxiliary lemmas›

theory AuxLemmas imports Main begin

abbreviation "arbitrary == undefined"

text ‹Lemmas about left- and rightmost elements in lists›

lemma leftmost_element_property:
  assumes "∃x ∈ set xs. P x"
  obtains zs x' ys where "xs = zs@x'#ys" and "P x'" and "∀z ∈ set zs. ¬ P z"
proof(atomize_elim)
  from ‹∃x ∈ set xs. P x› 
  show "∃zs x' ys. xs = zs @ x' # ys ∧ P x' ∧ (∀z∈set zs. ¬ P z)"
  proof(induct xs)
    case Nil thus ?case by simp
  next
    case (Cons x' xs')
    note IH = ‹∃a∈set xs'. P a
      ⟹ ∃zs x' ys. xs' = zs@x'#ys ∧ P x' ∧ (∀z∈set zs. ¬ P z)›
    show ?case
    proof (cases "P x'")
      case True
      then have "(∃ys. x' # xs' = [] @ x' # ys) ∧ P x' ∧ (∀x∈set []. ¬ P x)" by simp
      then show ?thesis by blast
    next
      case False
      with ‹∃y∈set (x'#xs'). P y› have "∃y∈set xs'. P y" by simp
      from IH[OF this] obtain y ys zs where "xs' = zs@y#ys"
        and "P y" and "∀z∈set zs. ¬ P z" by blast
      from ‹∀z∈set zs. ¬ P z› False have "∀z∈set (x'#zs). ¬ P z" by simp
      with ‹xs' = zs@y#ys› ‹P y› show ?thesis by (metis Cons_eq_append_conv)
    qed
  qed
qed



lemma rightmost_element_property:
  assumes "∃x ∈ set xs. P x"
  obtains ys x' zs where "xs = ys@x'#zs" and "P x'" and "∀z ∈ set zs. ¬ P z"
proof(atomize_elim)
  from ‹∃x ∈ set xs. P x›
  show "∃ys x' zs. xs = ys @ x' # zs ∧ P x' ∧ (∀z∈set zs. ¬ P z)"
  proof(induct xs)
    case Nil thus ?case by simp
  next
    case (Cons x' xs')
    note IH = ‹∃a∈set xs'. P a
      ⟹ ∃ys x' zs. xs' = ys @ x' # zs ∧ P x' ∧ (∀z∈set zs. ¬ P z)›
    show ?case
    proof(cases "∃y∈set xs'. P y")
      case True
      from IH[OF this] obtain y ys zs where "xs' = ys @ y # zs"
        and "P y" and "∀z∈set zs. ¬ P z" by blast
      thus ?thesis by (metis Cons_eq_append_conv)
    next
      case False
      with ‹∃y∈set (x'#xs'). P y› have "P x'" by simp
      with False show ?thesis by (metis eq_Nil_appendI)
    qed
  qed
qed


text ‹Lemma concerning maps and ‹@››

lemma map_append_append_maps:
  assumes map:"map f xs = ys@zs"
  obtains xs' xs'' where "map f xs' = ys" and "map f xs'' = zs" and "xs=xs'@xs''"
by (metis append_eq_conv_conj append_take_drop_id assms drop_map take_map that)


text ‹Lemma concerning splitting of @{term list}s›

lemma  path_split_general:
assumes all:"∀zs. xs ≠ ys@zs"
obtains j zs where "xs = (take j ys)@zs" and "j < length ys"
  and "∀k > j. ∀zs'. xs ≠ (take k ys)@zs'"
proof(atomize_elim)
  from ‹∀zs. xs ≠ ys@zs›
  show "∃j zs. xs = take j ys @ zs ∧ j < length ys ∧ 
               (∀k>j. ∀zs'. xs ≠ take k ys @ zs')"
  proof(induct ys arbitrary:xs)
    case Nil thus ?case by auto
  next
    case (Cons y' ys')
    note IH = ‹⋀xs. ∀zs. xs ≠ ys' @ zs ⟹
      ∃j zs. xs = take j ys' @ zs ∧ j < length ys' ∧ 
      (∀k. j < k ⟶ (∀zs'. xs ≠ take k ys' @ zs'))›
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with ‹∀zs. xs ≠ (y' # ys') @ zs› have "x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)"
        by simp
      show ?thesis
      proof(cases "x' = y'")
        case True
        with ‹x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)› have "∀zs. xs' ≠ ys' @ zs" by simp
        from IH[OF this] have "∃j zs. xs' = take j ys' @ zs ∧ j < length ys' ∧
          (∀k. j < k ⟶ (∀zs'. xs' ≠ take k ys' @ zs'))" .
        then obtain j zs where "xs' = take j ys' @ zs"
          and "j < length ys'"
          and all_sub:"∀k. j < k ⟶ (∀zs'. xs' ≠ take k ys' @ zs')"
          by blast
        from ‹xs' = take j ys' @ zs› True
          have "(x'#xs') = take (Suc j) (y' # ys') @ zs"
          by simp
        from all_sub True have all_imp:"∀k. j < k ⟶ 
          (∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs')"
          by auto
        { fix l assume "(Suc j) < l"
          then obtain k where [simp]:"l = Suc k" by(cases l) auto
          with ‹(Suc j) < l› have "j < k" by simp
          with all_imp 
          have "∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs'"
            by simp
          hence "∀zs'. (x'#xs') ≠ take l (y' # ys') @ zs'"
            by simp }
        with ‹(x'#xs') = take (Suc j) (y' # ys') @ zs› ‹j < length ys'› Cons
        show ?thesis by (metis Suc_length_conv less_Suc_eq_0_disj)
      next
        case False
        with Cons have "∀i zs'. i > 0 ⟶ xs ≠ take i (y' # ys') @ zs'"
          by auto(case_tac i,auto)
        moreover
        have "∃zs. xs = take 0 (y' # ys') @ zs" by simp
        ultimately show ?thesis by(rule_tac x="0" in exI,auto)
      qed
    qed
  qed
qed

end

chapter ‹The Framework›

theory BasicDefs imports AuxLemmas begin

text ‹
  As slicing is a program analysis that can be completely based on the
  information given in the CFG, we want to provide a framework which
  allows us to formalize and prove properties of slicing regardless of
  the actual programming language. So the starting point for the formalization 
  is the definition of an abstract CFG, i.e.\ without considering features 
  specific for certain languages. By doing so we ensure that our framework 
  is as generic as possible since all proofs hold for every language whose 
  CFG conforms to this abstract CFG.  This abstract CFG can be used as a 
  basis for static intraprocedural slicing as well as for dynamic slicing, 
  if in the dynamic case all method calls are inlined (i.e., abstract CFG 
  paths conform to traces).
›

section ‹Basic Definitions›

subsection‹Edge kinds›

datatype 'state edge_kind = Update "'state ⇒ 'state"           ("⇑_")
                          | Predicate "'state ⇒ bool"      ("'(_')⇩√")


subsection ‹Transfer and predicate functions›

fun transfer :: "'state edge_kind ⇒ 'state ⇒ 'state"
where "transfer (⇑f) s = f s"
  | "transfer (P)⇩√ s   = s"

fun transfers :: "'state edge_kind list ⇒ 'state ⇒ 'state"
where "transfers [] s   = s"
  | "transfers (e#es) s = transfers es (transfer e s)"

fun pred :: "'state edge_kind ⇒ 'state ⇒ bool"
where "pred (⇑f) s = True"
  | "pred (P)⇩√ s   = (P s)"

fun preds :: "'state edge_kind list ⇒ 'state ⇒ bool"
where "preds [] s   = True"
  | "preds (e#es) s = (pred e s ∧ preds es (transfer e s))"



lemma transfers_split:
  "(transfers (ets@ets') s) = (transfers ets' (transfers ets s))"
by(induct ets arbitrary:s) auto

lemma preds_split:
  "(preds (ets@ets') s) = (preds ets s ∧ preds ets' (transfers ets s))"
by(induct ets arbitrary:s) auto


lemma transfers_id_no_influence:
  "transfers [et ← ets. et ≠ ⇑id] s = transfers ets s"
by(induct ets arbitrary:s,auto)

lemma preds_True_no_influence:
  "preds [et ← ets. et ≠ (λs. True)⇩√] s = preds ets s"
by(induct ets arbitrary:s,auto)

end

section ‹CFG›

theory CFG imports BasicDefs begin

subsection ‹The abstract CFG›

locale CFG =
  fixes sourcenode :: "'edge ⇒ 'node"
  fixes targetnode :: "'edge ⇒ 'node"
  fixes kind :: "'edge ⇒ 'state edge_kind"
  fixes valid_edge :: "'edge ⇒ bool"
  fixes Entry::"'node" ("'('_Entry'_')")
  assumes Entry_target [dest]: "⟦valid_edge a; targetnode a = (_Entry_)⟧ ⟹ False"
  and edge_det: 
  "⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a'; 
    targetnode a = targetnode a'⟧ ⟹ a = a'"

begin

definition valid_node :: "'node ⇒ bool"
  where "valid_node n ≡ 
  (∃a. valid_edge a ∧ (n = sourcenode a ∨ n = targetnode a))"

lemma [simp]: "valid_edge a ⟹ valid_node (sourcenode a)"
  by(fastforce simp:valid_node_def)

lemma [simp]: "valid_edge a ⟹ valid_node (targetnode a)"
  by(fastforce simp:valid_node_def)


subsection ‹CFG paths and lemmas›

inductive path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
  ("_ -_→* _" [51,0,0] 80)
where 
  empty_path:"valid_node n ⟹ n -[]→* n"

  | Cons_path:
  "⟦n'' -as→* n'; valid_edge a; sourcenode a = n; targetnode a = n''⟧
    ⟹ n -a#as→* n'"


lemma path_valid_node:
  assumes "n -as→* n'" shows "valid_node n" and "valid_node n'"
  using ‹n -as→* n'›
  by(induct rule:path.induct,auto)

lemma empty_path_nodes [dest]:"n -[]→* n' ⟹ n = n'"
  by(fastforce elim:path.cases)

lemma path_valid_edges:"n -as→* n' ⟹ ∀a ∈ set as. valid_edge a"
by(induct rule:path.induct) auto


lemma path_edge:"valid_edge a ⟹ sourcenode a -[a]→* targetnode a"
  by(fastforce intro:Cons_path empty_path)


lemma path_Entry_target [dest]:
  assumes "n -as→* (_Entry_)"
  shows "n = (_Entry_)" and "as = []"
using ‹n -as→* (_Entry_)›
proof(induct n as n'≡"(_Entry_)" rule:path.induct)
  case (Cons_path n'' as a n)
  from ‹targetnode a = n''› ‹valid_edge a› ‹n'' = (_Entry_)› have False
    by -(rule Entry_target,simp_all)
  { case 1
    with ‹False› show ?case ..
  next
    case 2
    with ‹False› show ?case ..
  }
qed simp_all



lemma path_Append:"⟦n -as→* n''; n'' -as'→* n'⟧ 
  ⟹ n -as@as'→* n'"
by(induct rule:path.induct,auto intro:Cons_path)


lemma path_split:
  assumes "n -as@a#as'→* n'"
  shows "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'"
  using ‹n -as@a#as'→* n'›
proof(induct as arbitrary:n)
  case Nil case 1
  thus ?case by(fastforce elim:path.cases intro:empty_path)
next
  case Nil case 2
  thus ?case by(fastforce elim:path.cases intro:path_edge)
next
  case Nil case 3
  thus ?case by(fastforce elim:path.cases)
next
  case (Cons ax asx) 
  note IH1 = ‹⋀n. n -asx@a#as'→* n' ⟹ n -asx→* sourcenode a›
  note IH2 = ‹⋀n. n -asx@a#as'→* n' ⟹ valid_edge a›
  note IH3 = ‹⋀n. n -asx@a#as'→* n' ⟹ targetnode a -as'→* n'›
  { case 1 
    hence "sourcenode ax = n" and "targetnode ax -asx@a#as'→* n'" and "valid_edge ax"
      by(auto elim:path.cases)
    from IH1[OF ‹ targetnode ax -asx@a#as'→* n'›] 
    have "targetnode ax -asx→* sourcenode a" .
    with ‹sourcenode ax = n› ‹valid_edge ax› show ?case by(fastforce intro:Cons_path)
  next
    case 2 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH2[OF this] show ?case .
  next
    case 3 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
    from IH3[OF this] show ?case .
  }
qed


lemma path_split_Cons:
  assumes "n -as→* n'" and "as ≠ []"
  obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
  and "valid_edge a'" and "targetnode a' -as'→* n'"
proof -
  from ‹as ≠ []› obtain a' as' where "as = a'#as'" by(cases as) auto
  with ‹n -as→* n'› have "n -[]@a'#as'→* n'" by simp
  hence "n -[]→* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(rule path_split)+
  from ‹n -[]→* sourcenode a'› have "n = sourcenode a'" by fast
  with ‹as = a'#as'› ‹valid_edge a'› ‹targetnode a' -as'→* n'› that show ?thesis 
    by fastforce
qed


lemma path_split_snoc:
  assumes "n -as→* n'" and "as ≠ []"
  obtains a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'"
  and "valid_edge a'" and "n' = targetnode a'"
proof -
  from ‹as ≠ []› obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
  with ‹n -as→* n'› have "n -as'@a'#[]→* n'" by simp
  hence "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]→* n'"
    by(rule path_split)+
  from ‹targetnode a' -[]→* n'› have "n' = targetnode a'" by fast
  with ‹as = as'@[a']› ‹valid_edge a'› ‹n -as'→* sourcenode a'› that show ?thesis 
    by fastforce
qed


lemma path_split_second:
  assumes "n -as@a#as'→* n'" shows "sourcenode a -a#as'→* n'"
proof -
  from ‹n -as@a#as'→* n'› have "valid_edge a" and "targetnode a -as'→* n'"
    by(auto intro:path_split)
  thus ?thesis by(fastforce intro:Cons_path)
qed


lemma path_Entry_Cons:
  assumes "(_Entry_) -as→* n'" and "n' ≠ (_Entry_)"
  obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n"
  and "n -tl as→* n'" and "valid_edge a" and "a = hd as"
proof -
  from ‹(_Entry_) -as→* n'› ‹n' ≠ (_Entry_)› have "as ≠ []"
    by(cases as,auto elim:path.cases)
  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)
  with that show ?thesis by fastforce
qed


lemma path_det:
  "⟦n -as→* n'; n -as→* n''⟧ ⟹ n' = n''"
proof(induct as arbitrary:n)
  case Nil thus ?case by(auto elim:path.cases)
next
  case (Cons a' as')
  note IH = ‹⋀n. ⟦n -as'→* n'; n -as'→* n''⟧ ⟹ n' = n''›
  from ‹n -a'#as'→* n'› have "targetnode a' -as'→* n'" 
    by(fastforce elim:path_split_Cons)
  from ‹n -a'#as'→* n''› have "targetnode a' -as'→* n''" 
    by(fastforce elim:path_split_Cons)
  from IH[OF ‹targetnode a' -as'→* n'› this] show ?thesis .
qed


definition
  sourcenodes :: "'edge list ⇒ 'node list"
  where "sourcenodes xs ≡ map sourcenode xs"

definition
  kinds :: "'edge list ⇒ 'state edge_kind list"
  where "kinds xs ≡ map kind xs"

definition
  targetnodes :: "'edge list ⇒ 'node list"
  where "targetnodes xs ≡ map targetnode xs"


lemma path_sourcenode:
  "⟦n -as→* n'; as ≠ []⟧ ⟹ hd (sourcenodes as) = n"
by(fastforce elim:path_split_Cons simp:sourcenodes_def)



lemma path_targetnode:
  "⟦n -as→* n'; as ≠ []⟧ ⟹ last (targetnodes as) = n'"
by(fastforce elim:path_split_snoc simp:targetnodes_def)



lemma sourcenodes_is_n_Cons_butlast_targetnodes:
  "⟦n -as→* n'; as ≠ []⟧ ⟹ 
  sourcenodes as = n#(butlast (targetnodes as))"
proof(induct as arbitrary:n)
  case Nil thus ?case by simp
next
  case (Cons a' as')
  note IH = ‹⋀n. ⟦n -as'→* n'; as' ≠ []⟧
            ⟹ sourcenodes as' = n#(butlast (targetnodes as'))›
  from ‹n -a'#as'→* n'› have "n = sourcenode a'" and "targetnode a' -as'→* n'"
    by(auto elim:path_split_Cons)
  show ?case
  proof(cases "as' = []")
    case True
    with ‹targetnode a' -as'→* n'› have "targetnode a' = n'" by fast
    with True ‹n = sourcenode a'› show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF ‹targetnode a' -as'→* n'› this] 
    have "sourcenodes as' = targetnode a' # butlast (targetnodes as')" .
    with ‹n = sourcenode a'› False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed



lemma targetnodes_is_tl_sourcenodes_App_n':
  "⟦n -as→* n'; as ≠ []⟧ ⟹ 
    targetnodes as = (tl (sourcenodes as))@[n']"
proof(induct as arbitrary:n' rule:rev_induct)
  case Nil thus ?case by simp
next
  case (snoc a' as')
  note IH = ‹⋀n'. ⟦n -as'→* n'; as' ≠ []⟧
    ⟹ targetnodes as' = tl (sourcenodes as') @ [n']›
  from ‹n -as'@[a']→* n'› have "n -as'→* sourcenode a'" and "n' = targetnode a'"
    by(auto elim:path_split_snoc)
  show ?case
  proof(cases "as' = []")
    case True
    with ‹n -as'→* sourcenode a'› have "n = sourcenode a'" by fast
    with True ‹n' = targetnode a'› show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  next
    case False
    from IH[OF ‹n -as'→* sourcenode a'› this]
    have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']" .
    with ‹n' = targetnode a'› False show ?thesis
      by(simp add:sourcenodes_def targetnodes_def)
  qed
qed

lemma Entry_sourcenode_hd:
  assumes "n -as→* n'" and "(_Entry_) ∈ set (sourcenodes as)"
  shows "n = (_Entry_)" and "(_Entry_) ∉ set (sourcenodes (tl as))"
  using ‹n -as→* n'› ‹(_Entry_) ∈ set (sourcenodes as)›
proof(induct rule:path.induct)
  case (empty_path n) case 1
  thus ?case by(simp add:sourcenodes_def)
next
  case (empty_path n) case 2
  thus ?case by(simp add:sourcenodes_def)
next
  case (Cons_path n'' as n' a n)
  note IH1 = ‹(_Entry_) ∈ set(sourcenodes as) ⟹ n'' = (_Entry_)›
  note IH2 = ‹(_Entry_) ∈ set(sourcenodes as) ⟹ (_Entry_) ∉ set(sourcenodes(tl as))›
  have "(_Entry_) ∉ set (sourcenodes(tl(a#as)))"
  proof
    assume "(_Entry_) ∈ set (sourcenodes (tl (a#as)))"
    hence "(_Entry_) ∈ set (sourcenodes as)" by simp
    from IH1[OF this] have "n'' = (_Entry_)" by simp
    with ‹targetnode a = n''› ‹valid_edge a› show False by -(erule Entry_target,simp)
  qed
  hence "(_Entry_) ∉ set (sourcenodes(tl(a#as)))" by fastforce
  { case 1
    with ‹(_Entry_) ∉ set (sourcenodes(tl(a#as)))› ‹sourcenode a = n›
    show ?case by(simp add:sourcenodes_def)
  next
    case 2
    with ‹(_Entry_) ∉ set (sourcenodes(tl(a#as)))› ‹sourcenode a = n›
    show ?case by(simp add:sourcenodes_def)
  }
qed

end

end

theory CFGExit imports CFG begin

subsection ‹Adds an exit node to the abstract CFG›

locale CFGExit = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')") + 
  fixes Exit::"'node"  ("'('_Exit'_')")
  assumes Exit_source [dest]: "⟦valid_edge a; sourcenode a = (_Exit_)⟧ ⟹ False"
  and Entry_Exit_edge: "∃a. valid_edge a ∧ sourcenode a = (_Entry_) ∧
    targetnode a = (_Exit_) ∧ kind a = (λs. False)⇩√"
  
begin

lemma Entry_noteq_Exit [dest]:
  assumes eq:"(_Entry_) = (_Exit_)" shows "False"
proof -
  from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)" 
    and "valid_edge a" by blast
  with eq show False by simp(erule Exit_source)
qed

lemma Exit_noteq_Entry [dest]:"(_Exit_) = (_Entry_) ⟹ False"
  by(rule Entry_noteq_Exit[OF sym],simp)


lemma [simp]: "valid_node (_Entry_)"
proof -
  from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)" 
    and "valid_edge a" by blast
  thus ?thesis by(fastforce simp:valid_node_def)
qed

lemma [simp]: "valid_node (_Exit_)"
proof -
  from Entry_Exit_edge obtain a where "targetnode a = (_Exit_)"
    and "valid_edge a" by blast
  thus ?thesis by(fastforce simp:valid_node_def)
qed


definition inner_node :: "'node ⇒ bool"
  where inner_node_def: 
  "inner_node n ≡ valid_node n ∧ n ≠ (_Entry_) ∧ n ≠ (_Exit_)"


lemma inner_is_valid:
  "inner_node n ⟹ valid_node n"
by(simp add:inner_node_def valid_node_def)

lemma [dest]:
  "inner_node (_Entry_) ⟹ False"
by(simp add:inner_node_def)

lemma [dest]:
  "inner_node (_Exit_) ⟹ False" 
by(simp add:inner_node_def)

lemma [simp]:"⟦valid_edge a; targetnode a ≠ (_Exit_)⟧ 
  ⟹ inner_node (targetnode a)"
  by(simp add:inner_node_def,rule ccontr,simp,erule Entry_target)

lemma [simp]:"⟦valid_edge a; sourcenode a ≠ (_Entry_)⟧
  ⟹ inner_node (sourcenode a)"
  by(simp add:inner_node_def,rule ccontr,simp,erule Exit_source)

lemma valid_node_cases [consumes 1, case_names "Entry" "Exit" "inner"]:
  "⟦valid_node n; n = (_Entry_) ⟹ Q; n = (_Exit_) ⟹ Q;
    inner_node n ⟹ Q⟧ ⟹ Q"
apply(auto simp:valid_node_def)
 apply(case_tac "sourcenode a = (_Entry_)") apply auto
apply(case_tac "targetnode a = (_Exit_)") apply auto
done

lemma path_Exit_source [dest]:
  assumes "(_Exit_) -as→* n'" shows "n' = (_Exit_)" and "as = []"
  using ‹(_Exit_) -as→* n'›
proof(induct n≡"(_Exit_)" as n' rule:path.induct)
  case (Cons_path n'' as n' a)
  from ‹sourcenode a = (_Exit_)› ‹valid_edge a› have False 
    by -(rule Exit_source,simp_all)
  { case 1 with ‹False› show ?case ..
  next
    case 2 with ‹False› show ?case ..
  }
qed simp_all

lemma Exit_no_sourcenode[dest]:
  assumes isin:"(_Exit_) ∈ set (sourcenodes as)" and path:"n -as→* n'"
  shows False
proof -
  from isin obtain ns' ns'' where "sourcenodes as = ns'@(_Exit_)#ns''"
    by(auto dest:split_list simp:sourcenodes_def)
  then obtain as' as'' a where "as = as'@a#as''"
    and source:"sourcenode a = (_Exit_)"
    by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
  with path have "valid_edge a" by(fastforce dest:path_split)
  with source show ?thesis by -(erule Exit_source)
qed


end 

end

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