Theory Postdomination

header {* \isaheader{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->⇣\<surd>* n"
  and Exit_path:"valid_node n ==> ∃as. n -as->⇣\<surd>* (_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\<hookrightarrow>⇘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'\<hookleftarrow>⇘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'\<hookleftarrow>⇘p⇙f'` have "get_proc (sourcenode a') = p" 
    by(rule get_proc_return)
  from `valid_edge a'` `kind a' = Q'\<hookleftarrow>⇘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\<hookrightarrow>⇘p⇙fs`
  obtain Q'' f'' where "kind a'' = Q''\<hookleftarrow>⇘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''\<hookleftarrow>⇘p⇙f''` have "get_proc (sourcenode a'') = p" 
    by(rule get_proc_return)
  from `valid_edge a''` `kind a'' = Q''\<hookleftarrow>⇘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\<hookrightarrow>⇘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->⇣\<surd>* (_Exit_)" by(auto dest:Exit_path)
  then obtain as where "n -as->⇣\<surd>* (_Exit_)"
    and "∀a ∈ set as. intra_kind(kind a) ∨ (∃Q f p. kind a = Q\<hookleftarrow>⇘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\<hookleftarrow>⇘p⇙f")
    case True
    then obtain asx ax asx' where [simp]:"as = asx@ax#asx'" 
      and "∃Q f p. kind ax = Q\<hookleftarrow>⇘p⇙f" and "∀a ∈ set asx. ∀Q f p. kind a ≠ Q\<hookleftarrow>⇘p⇙f"
      by -(erule split_list_first_propE,simp)
    with `∀a ∈ set as. intra_kind(kind a) ∨ (∃Q f p. kind a = Q\<hookleftarrow>⇘p⇙f)`
    have "∀a ∈ set asx. intra_kind(kind a)" by auto
    from `n -as->⇣\<surd>* (_Exit_)` have "n -asx->⇣\<surd>* sourcenode ax"
      and "valid_edge ax" by(auto dest:vp_split)
    from `n -asx->⇣\<surd>* 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\<hookleftarrow>⇘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\<hookleftarrow>⇘p⇙f)`
    have "∀a ∈ set as. intra_kind(kind a)" by fastforce
    with `n -as->⇣\<surd>* (_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->⇣\<surd>* (_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->⇣\<surd>* (_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->⇣\<surd>* (_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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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->⇣\<surd>* (_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->⇣\<surd>* (_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->⇣\<surd>* (_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\<hookleftarrow>⇘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->⇣\<surd>* (_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->⇣\<surd>* (_Exit_)` have False by(fastforce simp:vp_def)
    thus ?thesis by simp
  next
    case False
    with `n -as->⇣\<surd>* (_Exit_)` obtain a' as' where "as = as'@[a']" 
      and "n -as'->⇣\<surd>* 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'->⇣\<surd>* 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\<hookrightarrow>⇘p⇙fs` have "kind a' = Q:r\<hookrightarrow>⇘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\<hookleftarrow>⇘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->⇣\<surd>* 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->⇣\<surd>* n` have False
      by(fastforce simp:inner_node_def vp_def)
    thus ?thesis by simp
  next
    case False
    with `(_Entry_) -as->⇣\<surd>* n` obtain a' as' where "as = a'#as'" 
      and "targetnode a' -as'->⇣\<surd>* 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'->⇣\<surd>* 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\<hookrightarrow>⇘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\<hookleftarrow>⇘p⇙f` have "kind a' = Q\<hookleftarrow>⇘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'->⇣\<surd>* (_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