Theory Postdomination

section ‹Postdomination›

theory Postdomination imports CFGExit begin

text ‹For static interprocedural slicing, we only consider standard control 
  dependence, hence we only need standard postdomination.›

locale Postdomination = CFGExit sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") +
  assumes Entry_path:"valid_node n ⟹ ∃as. (_Entry_) -as→⇩√* n"
  and Exit_path:"valid_node n ⟹ ∃as. n -as→⇩√* (_Exit_)"
  and method_exit_unique:
    "⟦method_exit n; method_exit n'; get_proc n = get_proc n'⟧ ⟹ n = n'"

begin

lemma get_return_edges_unique:
  assumes "valid_edge a" and "a' ∈ get_return_edges a" and "a'' ∈ get_return_edges a"
  shows "a' = a''"
proof -
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› 
  obtain Q r p fs where "kind a = Q:r↪⇘p⇙fs"
    by(fastforce dest!:only_call_get_return_edges)
  with ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
    by(fastforce dest!:call_return_edges)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
    by(rule get_return_edges_valid)
  from this ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p" 
    by(rule get_proc_return)
  from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› have "method_exit (sourcenode a')"
    by(fastforce simp:method_exit_def)
  from ‹valid_edge a› ‹a'' ∈ get_return_edges a› ‹kind a = Q:r↪⇘p⇙fs›
  obtain Q'' f'' where "kind a'' = Q''↩⇘p⇙f''" by(fastforce dest!:call_return_edges)
  from ‹valid_edge a› ‹a'' ∈ get_return_edges a› have "valid_edge a''" 
    by(rule get_return_edges_valid)
  from this ‹kind a'' = Q''↩⇘p⇙f''› have "get_proc (sourcenode a'') = p" 
    by(rule get_proc_return)
  from ‹valid_edge a''› ‹kind a'' = Q''↩⇘p⇙f''› have "method_exit (sourcenode a'')"
    by(fastforce simp:method_exit_def)
  with ‹method_exit (sourcenode a')› ‹get_proc (sourcenode a') = p›
    ‹get_proc (sourcenode a'') = p› have "sourcenode a' = sourcenode a''"
    by(fastforce elim!:method_exit_unique)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a›
  obtain ax' where "valid_edge ax'" and "sourcenode ax' = sourcenode a"
    and "targetnode ax' = targetnode a'" and "intra_kind(kind ax')"
    by -(drule call_return_node_edge,auto simp:intra_kind_def)
  from ‹valid_edge a› ‹a'' ∈ get_return_edges a›
  obtain ax'' where "valid_edge ax''" and "sourcenode ax'' = sourcenode a"
    and "targetnode ax'' = targetnode a''" and "intra_kind(kind ax'')"
    by -(drule call_return_node_edge,auto simp:intra_kind_def)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge ax'› 
    ‹sourcenode ax' = sourcenode a› ‹intra_kind(kind ax')›
    ‹valid_edge ax''› ‹sourcenode ax'' = sourcenode a› ‹intra_kind(kind ax'')›
  have "ax' = ax''" by -(drule call_only_one_intra_edge,auto)
  with ‹targetnode ax' = targetnode a'› ‹targetnode ax'' = targetnode a''›
  have "targetnode a' = targetnode a''" by simp
  with ‹valid_edge a'› ‹valid_edge a''› ‹sourcenode a' = sourcenode a''›
  show ?thesis by(rule edge_det)
qed


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


lemma postdominate_implies_inner_path: 
  assumes "n' postdominates n" 
  obtains as where "n -as→⇩ι* n'" and "n' ∉ set (sourcenodes as)"
proof(atomize_elim)
  from ‹n' postdominates n› have "valid_node n"
    and all:"∀as pex. (n -as→⇩ι* pex ∧ method_exit pex) ⟶ n' ∈ set (sourcenodes as)"
    by(auto simp:postdominate_def)
  from ‹valid_node n› obtain asx where "n -asx→⇩√* (_Exit_)" by(auto dest:Exit_path)
  then obtain as where "n -as→⇩√* (_Exit_)"
    and "∀a ∈ set as. intra_kind(kind a) ∨ (∃Q f p. kind a = Q↩⇘p⇙f)"
    by -(erule valid_Exit_path_descending_path)
  show "∃as. n -as→⇩ι* n' ∧ n' ∉ set (sourcenodes as)"
  proof(cases "∃a ∈ set as. ∃Q f p. kind a = Q↩⇘p⇙f")
    case True
    then obtain asx ax asx' where [simp]:"as = asx@ax#asx'" 
      and "∃Q f p. kind ax = Q↩⇘p⇙f" and "∀a ∈ set asx. ∀Q f p. kind a ≠ Q↩⇘p⇙f"
      by -(erule split_list_first_propE,simp)
    with ‹∀a ∈ set as. intra_kind(kind a) ∨ (∃Q f p. kind a = Q↩⇘p⇙f)›
    have "∀a ∈ set asx. intra_kind(kind a)" by auto
    from ‹n -as→⇩√* (_Exit_)› have "n -asx→⇩√* sourcenode ax"
      and "valid_edge ax" by(auto dest:vp_split)
    from ‹n -asx→⇩√* sourcenode ax› ‹∀a ∈ set asx. intra_kind(kind a)›
    have "n -asx→⇩ι* sourcenode ax" by(simp add:vp_def intra_path_def)
    from ‹valid_edge ax› ‹∃Q f p. kind ax = Q↩⇘p⇙f› 
    have "method_exit (sourcenode ax)" by(fastforce simp:method_exit_def)
    with ‹n -asx→⇩ι* sourcenode ax› all have "n' ∈ set (sourcenodes asx)" by fastforce
    then obtain xs ys where "sourcenodes asx = xs@n'#ys" and "n' ∉ set xs"
      by(fastforce dest:split_list_first)
    then obtain as' a as'' where "xs = sourcenodes as'"
      and [simp]:"asx = as'@a#as''" and "sourcenode a = n'"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from ‹n -asx→⇩ι* sourcenode ax› have "n -as'→⇩ι* sourcenode a"
      by(fastforce dest:path_split simp:intra_path_def)
    with ‹sourcenode a = n'› ‹n' ∉ set xs› ‹xs = sourcenodes as'›
    show ?thesis by fastforce
  next
    case False
    with ‹∀a ∈ set as. intra_kind(kind a) ∨ (∃Q f p. kind a = Q↩⇘p⇙f)›
    have "∀a ∈ set as. intra_kind(kind a)" by fastforce
    with ‹n -as→⇩√* (_Exit_)› all have "n' ∈ set (sourcenodes as)"
      by(auto simp:vp_def intra_path_def simp:method_exit_def)
    then obtain xs ys where "sourcenodes as = xs@n'#ys" and "n' ∉ set xs"
      by(fastforce dest:split_list_first)
    then obtain as' a as'' where "xs = sourcenodes as'"
      and [simp]:"as = as'@a#as''" and "sourcenode a = n'"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from ‹n -as→⇩√* (_Exit_)› ‹∀a ∈ set as. intra_kind(kind a)› ‹as = as'@a#as''›
    have "n -as'→⇩ι* sourcenode a"
      by(fastforce dest:path_split simp:vp_def intra_path_def)
    with ‹sourcenode a = n'› ‹n' ∉ set xs› ‹xs = sourcenodes as'›
    show ?thesis by fastforce
  qed
qed


lemma postdominate_variant:
  assumes "n' postdominates n" 
  shows "∀as. n -as→⇩√* (_Exit_) ⟶ n' ∈ set (sourcenodes as)"
proof -
  from ‹n' postdominates n›
  have all:"∀as pex. (n -as→⇩ι* pex ∧ method_exit pex) ⟶ n' ∈ set (sourcenodes as)"
    by(simp add:postdominate_def)
  { fix as assume "n -as→⇩√* (_Exit_)"
    then obtain as' pex where "n -as'→⇩ι* pex" and "method_exit pex"
      and "set(sourcenodes as') ⊆ set(sourcenodes as)"
      by(erule valid_Exit_path_intra_path)
    from ‹n -as'→⇩ι* pex› ‹method_exit pex› ‹n' postdominates n›
    have "n' ∈ set (sourcenodes as')" by(fastforce simp:postdominate_def)
    with ‹set(sourcenodes as') ⊆ set(sourcenodes as)›
    have "n' ∈ set (sourcenodes as)" by fastforce }
  thus ?thesis by simp
qed


lemma postdominate_refl:
  assumes "valid_node n" and "¬ method_exit n" shows "n postdominates n"
using ‹valid_node n›
proof(induct rule:valid_node_cases)
  case Entry
  { fix as pex assume "(_Entry_) -as→⇩ι* pex" and "method_exit pex"
    from ‹method_exit pex› have "(_Entry_) ∈ set (sourcenodes as)"
    proof(rule method_exit_cases)
      assume "pex = (_Exit_)"
      with ‹(_Entry_) -as→⇩ι* pex› have "as ≠ []" 
        apply(clarsimp simp:intra_path_def) apply(erule path.cases)
        by (drule sym,simp,drule Exit_noteq_Entry,auto)
      with ‹(_Entry_) -as→⇩ι* pex› have "hd (sourcenodes as) = (_Entry_)" 
        by(fastforce intro:path_sourcenode simp:intra_path_def)
      with ‹as ≠ []›show ?thesis by(fastforce intro:hd_in_set simp:sourcenodes_def)
    next
      fix a Q p f assume "pex = sourcenode a" and "valid_edge a" and "kind a = Q↩⇘p⇙f"
      from ‹(_Entry_) -as→⇩ι* pex› have "get_proc (_Entry_) = get_proc pex"
        by(rule intra_path_get_procs)
      hence "get_proc pex = Main" by(simp add:get_proc_Entry)
      from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
        by(rule get_proc_return)
      with ‹pex = sourcenode a› ‹get_proc pex = Main› have "p = Main" by simp
      with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have False
        by simp (rule Main_no_return_source)
      thus ?thesis by simp
    qed }
  with Entry show ?thesis 
    by(fastforce intro:empty_path simp:postdominate_def intra_path_def)
next
  case Exit
  with ‹¬ method_exit n› have False by(simp add:method_exit_def)
  thus ?thesis by simp
next
  case inner
  show ?thesis
  proof(cases "∃as. n -as→⇩√* (_Exit_)")
    case True
    { fix as pex assume "n -as→⇩ι* pex" and "method_exit pex"
      with ‹¬ method_exit n› have "as ≠ []" 
        by(fastforce elim:path.cases simp:intra_path_def)
      with ‹n -as→⇩ι* pex› inner have "hd (sourcenodes as) = n"
        by(fastforce intro:path_sourcenode simp:intra_path_def)
      from ‹as ≠ []› have "sourcenodes as ≠ []" by(simp add:sourcenodes_def)
      with ‹hd (sourcenodes as) = n›[THEN sym] 
      have "n ∈ set (sourcenodes as)" by simp }
    hence "∀as pex. (n -as→⇩ι* pex ∧ method_exit pex) ⟶ n ∈ set (sourcenodes as)"
      by fastforce
    with True inner show ?thesis 
      by(fastforce intro:empty_path 
                   simp:postdominate_def inner_is_valid intra_path_def)
  next
    case False
    with inner show ?thesis by(fastforce dest:inner_is_valid Exit_path)
  qed
qed



lemma postdominate_trans:
  assumes "n'' postdominates n" and "n' postdominates n''"
  shows "n' postdominates n"
proof -
  from ‹n'' postdominates n› ‹n' postdominates n''›
  have "valid_node n" and "valid_node n'" by(simp_all add:postdominate_def)
  { fix as pex assume "n -as→⇩ι* pex" and "method_exit pex"
    with ‹n'' postdominates n› have "n'' ∈ set (sourcenodes as)"
      by(fastforce simp:postdominate_def)
    then obtain ns' ns'' where "sourcenodes as = ns'@n''#ns''"
      by(auto dest:split_list)
    then obtain as' as'' a where "sourcenodes as'' = ns''" and [simp]:"as=as'@a#as''"
      and [simp]:"sourcenode a = n''"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from ‹n -as→⇩ι* pex› have "n -as'@a#as''→⇩ι* pex" by simp
    hence "n'' -a#as''→⇩ι* pex"
      by(fastforce dest:path_split_second simp:intra_path_def)
    with ‹n' postdominates n''› ‹method_exit pex›
    have "n' ∈ set(sourcenodes (a#as''))" by(fastforce simp:postdominate_def)
    hence "n' ∈ set (sourcenodes as)" by(fastforce simp:sourcenodes_def) }
  with ‹valid_node n› ‹valid_node n'›
  show ?thesis by(fastforce simp:postdominate_def)
qed


lemma postdominate_antisym:
  assumes "n' postdominates n" and "n postdominates n'"
  shows "n = n'"
proof -
  from ‹n' postdominates n› have "valid_node n" and "valid_node n'" 
    by(auto simp:postdominate_def)
  from ‹valid_node n› obtain asx where "n -asx→⇩√* (_Exit_)" by(auto dest:Exit_path)
  then obtain as' pex where "n -as'→⇩ι* pex" and "method_exit pex"
    by -(erule valid_Exit_path_intra_path)
  with ‹n' postdominates n› have "∃nx ∈ set(sourcenodes as'). nx = n'"
    by(fastforce simp:postdominate_def)
  then obtain ns ns' where "sourcenodes as' = ns@n'#ns'"
    and "∀nx ∈ set ns'. nx ≠ n'"
    by(fastforce elim!:split_list_last_propE)
  from ‹sourcenodes as' = ns@n'#ns'› obtain asx a asx' 
    where [simp]:"ns' = sourcenodes asx'" "as' = asx@a#asx'" "sourcenode a = n'"
    by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
  from ‹n -as'→⇩ι* pex› have "n' -a#asx'→⇩ι* pex"
    by(fastforce dest:path_split_second simp:intra_path_def)
  with ‹n postdominates n'› ‹method_exit pex› have "n ∈ set(sourcenodes (a#asx'))" 
    by(fastforce simp:postdominate_def)
  hence "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 [simp]:"asx' = asi@a'#asi'" "sourcenode a' = n"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    with ‹n -as'→⇩ι* pex› have "n -(asx@a#asi)@a'#asi'→⇩ι* pex" by simp
    hence "n -(asx@a#asi)@a'#asi'→* pex"
      and "∀a ∈ set ((asx@a#asi)@a'#asi'). intra_kind (kind a)"
      by(simp_all add:intra_path_def)
    from ‹n -(asx@a#asi)@a'#asi'→* pex›
    have "n -a'#asi'→* pex" by(fastforce dest:path_split_second)
    with ‹∀a ∈ set ((asx@a#asi)@a'#asi'). intra_kind (kind a)›
    have "n -a'#asi'→⇩ι* pex" by(simp add:intra_path_def)
    with ‹n' postdominates n› ‹method_exit pex› 
    have "n' ∈ set(sourcenodes (a'#asi'))" by(fastforce simp:postdominate_def)
    hence "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 ‹∀nx ∈ set ns'. nx ≠ n'› have False by(fastforce simp:sourcenodes_def)
      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:
  assumes "(_Exit_) postdominates n" shows False
proof -
  from ‹(_Exit_) postdominates n› have "valid_node n" by(simp add:postdominate_def)
  from ‹valid_node n› obtain asx where "n -asx→⇩√* (_Exit_)" by(auto dest:Exit_path)
  then obtain as' pex where "n -as'→⇩ι* pex" and "method_exit pex"
    by -(erule valid_Exit_path_intra_path)
  with ‹(_Exit_) postdominates n› have "(_Exit_) ∈ set (sourcenodes as')"
    by(fastforce simp:postdominate_def)
  with ‹n -as'→⇩ι* pex› show False by(fastforce simp:intra_path_def)
qed


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


lemma not_postdominate_source_not_postdominate_target:
  assumes "¬ n postdominates (sourcenode a)" 
  and "valid_node n" and "valid_edge a" and "intra_kind (kind 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 pex 
      where "sourcenode a -asx→⇩ι* pex" and "method_exit pex"
      and "n ∉ set(sourcenodes asx)" by(fastforce simp:postdominate_def)
    show ?thesis
    proof(cases asx)
      case Nil
      with ‹sourcenode a -asx→⇩ι* pex› have "pex = sourcenode a"
        by(fastforce simp:intra_path_def)
      with ‹method_exit pex› have "method_exit (sourcenode a)" by simp
      thus ?thesis
      proof(rule method_exit_cases)
        assume "sourcenode a = (_Exit_)"
        with ‹valid_edge a› have False by(rule Exit_source)
        thus ?thesis by simp
      next
        fix a' Q f p assume "sourcenode a = sourcenode a'"
          and "valid_edge a'" and "kind a' = Q↩⇘p⇙f"
        hence False using ‹intra_kind (kind a)› ‹valid_edge a›
          by(fastforce dest:return_edges_only simp:intra_kind_def)
        thus ?thesis by simp
      qed
    next
      case (Cons ax asx')
      with ‹sourcenode a -asx→⇩ι* pex›
      have "sourcenode a -[]@ax#asx'→* pex" 
        and "∀a ∈ set (ax#asx'). intra_kind (kind a)" by(simp_all add:intra_path_def)
      from ‹sourcenode a -[]@ax#asx'→* pex›
      have "sourcenode a = sourcenode ax" and "valid_edge ax"
        and "targetnode ax -asx'→* pex"  by(fastforce dest:path_split)+
      with ‹∀a ∈ set (ax#asx'). intra_kind (kind a)›
      have "targetnode ax -asx'→⇩ι* pex" by(simp add:intra_path_def)
      with ‹n ∉ set(sourcenodes asx)› Cons ‹method_exit pex›
      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
qed


lemma inner_node_Exit_edge:
  assumes "inner_node n" 
  obtains a where "valid_edge a" and "intra_kind (kind 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 ∧ intra_kind (kind a) ∧ inner_node (sourcenode a) ∧ 
    targetnode a = (_Exit_)"
  proof(cases "as = []")
    case True
    with ‹inner_node n› ‹n -as→⇩√* (_Exit_)› have False by(fastforce simp:vp_def)
    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 vp_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'› have "n -as'→* (_Entry_)" by(simp add:vp_def)
      with ‹inner_node n›
      have False by -(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
      have "intra_kind (kind a')"
      proof(cases "kind a'" rule:edge_kind_cases)
        case Intra thus ?thesis by simp
      next
        case (Call Q r p fs)
        with ‹valid_edge a'› have "get_proc(targetnode a') = p" by(rule get_proc_call)
        with ‹(_Exit_) = targetnode a'› get_proc_Exit have "p = Main" by simp
        with ‹kind a' = Q:r↪⇘p⇙fs› have "kind a' = Q:r↪⇘Main⇙fs" by simp
        with ‹valid_edge a'› have False by(rule Main_no_call_target)
        thus ?thesis by simp
      next
        case (Return Q p f)
        from ‹valid_edge a'› ‹kind a' = Q↩⇘p⇙f› ‹(_Exit_) = targetnode a'›[THEN sym]
        have False by(rule Exit_no_return_target)
        thus ?thesis by simp
      qed
      with ‹valid_edge a'› ‹(_Exit_) = targetnode a'› ‹inner_node (sourcenode a')› 
      show ?thesis by simp blast
    qed
  qed
qed


lemma inner_node_Entry_edge:
  assumes "inner_node n" 
  obtains a where "valid_edge a" and "intra_kind (kind 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 ∧ intra_kind (kind 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 vp_def)
    thus ?thesis by simp
  next
    case False
    with ‹(_Entry_) -as→⇩√* n› obtain a' as' where "as = a'#as'" 
      and "targetnode a' -as'→⇩√* n" and "valid_edge a'" 
      and "(_Entry_) = sourcenode a'" by -(erule vp_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› have "(_Exit_) -as'→* n" by(simp add:vp_def)
      with ‹inner_node n›
      have False by -(drule path_Exit_source,auto simp:inner_node_def)
      thus ?thesis by simp
    next
      case inner
      have "intra_kind (kind a')"
      proof(cases "kind a'" rule:edge_kind_cases)
        case Intra thus ?thesis by simp
      next
        case (Call Q r p fs)
        from ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs› 
          ‹(_Entry_) = sourcenode a'›[THEN sym]
        have False by(rule Entry_no_call_source)
        thus ?thesis by simp
      next
        case (Return Q p f)
        with ‹valid_edge a'› have "get_proc(sourcenode a') = p" 
          by(rule get_proc_return)
        with ‹(_Entry_) = sourcenode a'› get_proc_Entry have "p = Main" by simp
        with ‹kind a' = Q↩⇘p⇙f› have "kind a' = Q↩⇘Main⇙f" by simp
        with ‹valid_edge a'› have False by(rule Main_no_return_source)
        thus ?thesis by simp
      qed
      with ‹valid_edge a'› ‹(_Entry_) = sourcenode a'› ‹inner_node (targetnode a')› 
      show ?thesis by simp blast
    qed
  qed
qed


lemma intra_path_to_matching_method_exit:
  assumes "method_exit n'" and "get_proc n = get_proc n'" and "valid_node n"
  obtains as where "n -as→⇩ι* n'"
proof(atomize_elim)
  from ‹valid_node n› obtain as' where "n -as'→⇩√* (_Exit_)"
    by(fastforce dest:Exit_path)
  then obtain as mex where "n -as→⇩ι* mex" and "method_exit mex"
    by(fastforce elim:valid_Exit_path_intra_path)
  from ‹n -as→⇩ι* mex› have "get_proc n = get_proc mex" 
    by(rule intra_path_get_procs)
  with ‹method_exit n'› ‹get_proc n = get_proc n'› ‹method_exit mex›
  have "mex = n'" by(fastforce intro:method_exit_unique)
  with ‹n -as→⇩ι* mex› show "∃as. n -as→⇩ι* n'" by fastforce
qed


end

end