Theory CFGExit

theory CFGExit imports CFG begin

subsection ‹Adds an exit node to the abstract CFG›

locale CFGExit = CFG sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main
  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" +
  fixes Exit::"'node"  ("'('_Exit'_')")
  assumes Exit_source [dest]: "valid_edge a; sourcenode a = (_Exit_)  False"
  and get_proc_Exit:"get_proc (_Exit_) = Main"
  and Exit_no_return_target:
    "valid_edge a; kind a = Q↩⇘pf; targetnode 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


subsubsection ‹Definition of method_exit›

definition method_exit :: "'node  bool"
  where "method_exit n  n = (_Exit_)  
  (a Q p f. n = sourcenode a  valid_edge a  kind a = Q↩⇘pf)"


lemma method_exit_cases:
  "method_exit n; n = (_Exit_)  P;
    a Q f p. n = sourcenode a; valid_edge a; kind a = Q↩⇘pf  P  P"
by(fastforce simp:method_exit_def)


lemma method_exit_inner_path:
  assumes "method_exit n" and "n -asι* n'" shows "as = []"
  using method_exit n
proof(rule method_exit_cases)
  assume "n = (_Exit_)"
  show ?thesis
  proof(cases as)
    case (Cons a' as')
    with n -asι* n' have "n = sourcenode a'" and "valid_edge a'"
      by(auto elim:path_split_Cons simp:intra_path_def)
    with n = (_Exit_) have "sourcenode a' = (_Exit_)" by simp
    with valid_edge a' have False by(rule Exit_source)
    thus ?thesis by simp
  qed simp
next
  fix a Q f p
  assume "n = sourcenode a" and "valid_edge a" and "kind a = Q↩⇘pf"
  show ?thesis
  proof(cases as)
    case (Cons a' as')
    with n -asι* n' have "n = sourcenode a'" and "valid_edge a'" 
      and "intra_kind (kind a')"
      by(auto elim:path_split_Cons simp:intra_path_def)
    from valid_edge a kind a = Q↩⇘pf valid_edge a' n = sourcenode a 
      n = sourcenode a' intra_kind (kind a')
    have False by(fastforce dest:return_edges_only simp:intra_kind_def)
    thus ?thesis by simp
  qed simp
qed


subsubsection ‹Definition of inner_node›

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


subsubsection ‹Lemmas on paths with (_Exit_)›

lemma path_Exit_source:
  "n -as→* n'; n = (_Exit_)  n' = (_Exit_)  as = []"
proof(induct rule:path.induct)
  case (Cons_path n'' as n' a n)
  from n = (_Exit_) sourcenode a = n valid_edge a have False 
    by -(rule Exit_source,simp_all)
  thus ?case by simp
qed simp

lemma [dest]:"(_Exit_) -as→* n'  n' = (_Exit_)  as = []"
  by(fastforce elim!:path_Exit_source)

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



lemma vpa_no_slpa:
  "valid_path_aux cs as; n -as→* n'; valid_call_list cs n; cs  [];
    xs ys. as = xs@ys  (¬ same_level_path_aux cs xs  upd_cs cs xs  [])
   a Q r fs. valid_edge a  kind a = Q:r↪⇘get_proc n'fs"
proof(induct arbitrary:n rule:vpa_induct)
  case (vpa_empty cs)
  from valid_call_list cs n cs  [] obtain Q r fs where "valid_edge (hd cs)"
    and "kind (hd cs) = Q:r↪⇘get_proc nfs"
    apply(unfold valid_call_list_def)
    apply(drule hd_Cons_tl[THEN sym])
    apply(erule_tac x="[]" in allE) 
    apply(erule_tac x="hd cs" in allE)
    by auto
  from n -[]→* n' have "n = n'" by fastforce
  with valid_edge (hd cs) kind (hd cs) = Q:r↪⇘get_proc nfs show ?case by blast
next
  case (vpa_intra cs a as)
  note IH = n. n -as→* n'; valid_call_list cs n; cs  [];
    xs ys. as = xs@ys  ¬ same_level_path_aux cs xs  upd_cs cs xs  []
     a' Q' r' fs'. valid_edge a'  kind a' = Q':r'↪⇘get_proc n'fs'
  note all = xs ys. a#as = xs@ys 
     ¬ same_level_path_aux cs xs  upd_cs cs xs  []
  from n -a#as→* n' have "sourcenode a = n" and "valid_edge a" 
    and "targetnode a -as→* n'"
    by(auto intro:path_split_Cons)
  from valid_call_list cs n cs  [] obtain Q r fs where "valid_edge (hd cs)"
    and "kind (hd cs) = Q:r↪⇘get_proc nfs"
    apply(unfold valid_call_list_def)
    apply(drule hd_Cons_tl[THEN sym])
    apply(erule_tac x="[]" in allE) 
    apply(erule_tac x="hd cs" in allE)
    by auto
  from valid_edge a intra_kind (kind a)
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with kind (hd cs) = Q:r↪⇘get_proc nfs sourcenode a = n
  have "kind (hd cs) = Q:r↪⇘get_proc (targetnode a)fs" by simp
  from valid_call_list cs n sourcenode a = n
    get_proc (sourcenode a) = get_proc (targetnode a)
  have "valid_call_list cs (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cs'" in allE)
    apply(erule_tac x="c" in allE)
    by(auto split:list.split)
  from all intra_kind (kind a)
  have "xs ys. as = xs@ys  ¬ same_level_path_aux cs xs  upd_cs cs xs  []"
    apply clarsimp apply(erule_tac x="a#xs" in allE)
    by(auto simp:intra_kind_def)
  from IH[OF targetnode a -as→* n' valid_call_list cs (targetnode a)
    cs  [] this] show ?case .
next
  case (vpa_Call cs a as Q r p fs)
  note IH = n. n -as→* n'; valid_call_list (a#cs) n; a#cs  [];
    xs ys. as = xs@ys  ¬ same_level_path_aux (a#cs) xs  upd_cs (a#cs) xs  []
     a' Q' r' fs'. valid_edge a'  kind a' = Q':r'↪⇘get_proc n'fs'
  note all = xs ys.
    a#as = xs@ys  ¬ same_level_path_aux cs xs  upd_cs cs xs  []
  from n -a#as→* n' have "sourcenode a = n" and "valid_edge a" 
    and "targetnode a -as→* n'"
    by(auto intro:path_split_Cons)
  from valid_edge a kind a = Q:r↪⇘pfs have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  with kind a = Q:r↪⇘pfs have "kind a = Q:r↪⇘get_proc (targetnode a)fs" by simp
  with valid_call_list cs n valid_edge a sourcenode a = n
  have "valid_call_list (a#cs) (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(case_tac cs') apply auto
    apply(erule_tac x="list" in allE)
    apply(erule_tac x="c" in allE)
    by(auto split:list.split simp:sourcenodes_def)
  from all kind a = Q:r↪⇘pfs
  have "xs ys. as = xs@ys 
     ¬ same_level_path_aux (a#cs) xs  upd_cs (a#cs) xs  []"
    apply clarsimp apply(erule_tac x="a#xs" in allE)
    by auto
  from IH[OF targetnode a -as→* n' valid_call_list (a#cs) (targetnode a)
    _ this] show ?case by simp
next
  case (vpa_ReturnEmpty cs a as Q p fx)
  from cs  [] cs = [] have False by simp
  thus ?case by simp
next
  case (vpa_ReturnCons cs a as Q p f c' cs')
  note IH = n. n -as→* n'; valid_call_list cs' n; cs'  [];
    xs ys. as = xs@ys  ¬ same_level_path_aux cs' xs  upd_cs cs' xs  []
     a' Q' r' fs'. valid_edge a'  kind a' = Q':r'↪⇘get_proc n'fs'
  note all = xs ys. a#as = xs@ys 
     ¬ same_level_path_aux cs xs  upd_cs cs xs  []
  from n -a#as→* n' have "sourcenode a = n" and "valid_edge a" 
    and "targetnode a -as→* n'"
    by(auto intro:path_split_Cons)
  from valid_call_list cs n cs = c'#cs' have "valid_edge c'"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="[]" in allE)
    by auto
  show ?case
  proof(cases "cs' = []")
    case True
    with all cs = c'#cs' kind a = Q↩⇘pf a  get_return_edges c' have False
      by(erule_tac x="[a]" in allE,fastforce)
    thus ?thesis by simp
  next
    case False
    with valid_call_list cs n cs = c'#cs'
    have "valid_call_list cs' (sourcenode c')"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c'#cs'" in allE)
      apply(auto simp:sourcenodes_def)
       apply(case_tac cs') apply auto
      apply(case_tac list) apply(auto simp:sourcenodes_def)
      done
    from valid_edge c' a  get_return_edges c'
    have "get_proc (sourcenode c') = get_proc (targetnode a)"
      by(rule get_proc_get_return_edge)
    with valid_call_list cs' (sourcenode c')
    have "valid_call_list cs' (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
    apply(erule_tac x="cs'" in allE)
    apply(erule_tac x="c" in allE)
    by(auto split:list.split)
    from all kind a = Q↩⇘pf cs = c'#cs' a  get_return_edges c'
    have "xs ys. as = xs@ys  ¬ same_level_path_aux cs' xs  upd_cs cs' xs  []"
      apply clarsimp apply(erule_tac x="a#xs" in allE)
      by auto  
    from IH[OF targetnode a -as→* n' valid_call_list cs' (targetnode a)
      False this] show ?thesis .
  qed
qed


lemma valid_Exit_path_cases:
  assumes "n -as* (_Exit_)" and "as  []"
  shows "(a' as'. as = a'#as'  intra_kind(kind a')) 
         (a' as' Q p f. as = a'#as'  kind a' = Q↩⇘pf) 
         (as' as'' n'. as = as'@as''  as'  []  n -as'sl* n')"
proof -
  from as  [] obtain a' as' where "as = a'#as'" by(cases as) auto
  thus ?thesis
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra with as = a'#as' show ?thesis by simp
  next
    case Return with as = a'#as' show ?thesis by simp
  next
    case (Call Q r p f)
    from n -as* (_Exit_) have "n -as→* (_Exit_)" and "valid_path_aux [] as"
      by(simp_all add:vp_def valid_path_def)
    from n -as→* (_Exit_) as = a'#as'
    have "sourcenode a' = n" and "valid_edge a'" and "targetnode a' -as'→* (_Exit_)"
      by(auto intro:path_split_Cons)
    from valid_path_aux [] as as = a'#as' Call
    have "valid_path_aux [a'] as'" by simp
    from valid_edge a' Call
    have "valid_call_list [a'] (targetnode a')"
      apply(clarsimp simp:valid_call_list_def)
      apply(case_tac cs') 
      by(auto intro:get_proc_call[THEN sym])
    show ?thesis
    proof(cases "xs ys. as' = xs@ys  
        (¬ same_level_path_aux [a'] xs  upd_cs [a'] xs  [])")
      case True
      with valid_path_aux [a'] as' targetnode a' -as'→* (_Exit_)
        valid_call_list [a'] (targetnode a')
      obtain ax Qx rx fsx where "valid_edge ax" and "kind ax = Qx:rx↪⇘get_proc (_Exit_)fsx"
        by(fastforce dest!:vpa_no_slpa)
      hence False by(fastforce intro:Main_no_call_target simp:get_proc_Exit)
      thus ?thesis by simp
    next
      case False
      then obtain xs ys where "as' = xs@ys" and "same_level_path_aux [a'] xs"
        and "upd_cs [a'] xs = []" by auto
      with Call have "same_level_path (a'#xs)" by(simp add:same_level_path_def)
      from upd_cs [a'] xs = [] have "xs  []" by auto
      with targetnode a' -as'→* (_Exit_) as' = xs@ys
      have "targetnode a' -xs→* last(targetnodes xs)"
        apply(cases xs rule:rev_cases)
        by(auto intro:path_Append path_split path_edge simp:targetnodes_def)
      with sourcenode a' = n valid_edge a' same_level_path (a'#xs)
      have "n -a'#xssl* last(targetnodes xs)"
        by(fastforce intro:Cons_path simp:slp_def)
      with as = a'#as' as' = xs@ys Call 
      have "as' as'' n'. as = as'@as''  as'  []  n -as'sl* n'"
        by(rule_tac x="a'#xs" in exI) auto
      thus ?thesis by simp
    qed
  qed
qed


lemma valid_Exit_path_descending_path:
  assumes "n -as* (_Exit_)"
  obtains as' where "n -as'* (_Exit_)" 
  and "set(sourcenodes as')  set(sourcenodes as)"
  and "a'  set as'. intra_kind(kind a')  (Q f p. kind a' = Q↩⇘pf)"
proof(atomize_elim)
  from n -as* (_Exit_)
  show "as'. n -as'* (_Exit_)  set(sourcenodes as')  set(sourcenodes as)
              (a'  set as'. intra_kind(kind a')  (Q f p. kind a' = Q↩⇘pf))"
  proof(induct as arbitrary:n rule:length_induct)
    fix as n
    assume IH:"as''. length as'' < length as 
      (n'. n' -as''* (_Exit_) 
       (as'. n' -as'* (_Exit_)  set (sourcenodes as')  set (sourcenodes as'') 
              (a'set as'. intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf))))"
      and "n -as* (_Exit_)"
    show "as'. n -as'* (_Exit_)  set(sourcenodes as')  set(sourcenodes as)
              (a'  set as'. intra_kind(kind a')  (Q f p. kind a' = Q↩⇘pf))"
    proof(cases "as = []")
      case True
      with n -as* (_Exit_) show ?thesis by(fastforce simp:sourcenodes_def vp_def)
    next
      case False
      with n -as* (_Exit_)
      have "((a' as'. as = a'#as'  intra_kind(kind a')) 
         (a' as' Q p f. as = a'#as'  kind a' = Q↩⇘pf)) 
         (as' as'' n'. as = as'@as''  as'  []  n -as'sl* n')"
        by(auto dest!:valid_Exit_path_cases)
      thus ?thesis apply -
      proof(erule disjE)+
        assume "a' as'. as = a'#as'  intra_kind(kind a')"
        then obtain a' as' where "as = a'#as'" and "intra_kind(kind a')" by blast
        from n -as* (_Exit_) as = a'#as'
        have "sourcenode a' = n" and "valid_edge a'" 
          and "targetnode a' -as'* (_Exit_)"
          by(auto intro:vp_split_Cons)
        from valid_edge a' intra_kind(kind a')
        have "sourcenode a' -[a']sl* targetnode a'"
          by(fastforce intro:path_edge intras_same_level_path simp:slp_def)
        from IH targetnode a' -as'* (_Exit_) as = a'#as'
        obtain xs where "targetnode a' -xs* (_Exit_)" 
          and "set (sourcenodes xs)  set (sourcenodes as')"
          and "a'set xs. intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf)"
          apply(erule_tac x="as'" in allE) by auto
        from sourcenode a' -[a']sl* targetnode a' targetnode a' -xs* (_Exit_)
        have "sourcenode a' -[a']@xs* (_Exit_)" by(rule slp_vp_Append)
        with sourcenode a' = n have "n -a'#xs* (_Exit_)" by simp
        moreover
        from set (sourcenodes xs)  set (sourcenodes as') as = a'#as'
        have "set (sourcenodes (a'#xs))  set (sourcenodes as)"
          by(auto simp:sourcenodes_def)
        moreover
        from a'set xs. intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf) 
          intra_kind(kind a')
        have "a'set (a'#xs). intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf)"
          by fastforce
        ultimately show ?thesis by blast
      next
        assume "a' as' Q p f. as = a'#as'  kind a' = Q↩⇘pf"
        then obtain a' as' Q p f where "as = a'#as'" and "kind a' = Q↩⇘pf" by blast
        from n -as* (_Exit_) as = a'#as'
        have "sourcenode a' = n" and "valid_edge a'" 
          and "targetnode a' -as'* (_Exit_)"
          by(auto intro:vp_split_Cons)
        from IH targetnode a' -as'* (_Exit_) as = a'#as'
        obtain xs where "targetnode a' -xs* (_Exit_)" 
          and "set (sourcenodes xs)  set (sourcenodes as')"
          and "a'set xs. intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf)"
          apply(erule_tac x="as'" in allE) by auto
        from sourcenode a' = n valid_edge a' kind a' = Q↩⇘pf
          targetnode a' -xs* (_Exit_)
        have "n -a'#xs* (_Exit_)"
          by(fastforce intro:Cons_path simp:vp_def valid_path_def)
        moreover
        from set (sourcenodes xs)  set (sourcenodes as') as = a'#as'
        have "set (sourcenodes (a'#xs))  set (sourcenodes as)"
          by(auto simp:sourcenodes_def)
        moreover
        from a'set xs. intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf) 
          kind a' = Q↩⇘pf
        have "a'set (a'#xs). intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf)"
          by fastforce
        ultimately show ?thesis by blast
      next
        assume "as' as'' n'. as = as'@as''  as'  []  n -as'sl* n'"
        then obtain as' as'' n' where "as = as'@as''" and "as'  []"
          and "n -as'sl* n'" by blast
        from n -as* (_Exit_) as = as'@as'' as'  []
        have "last(targetnodes as') -as''* (_Exit_)"
          by(cases as' rule:rev_cases,auto intro:vp_split simp:targetnodes_def)
        from n -as'sl* n' as'  [] have "last(targetnodes as') = n'"
          by(fastforce intro:path_targetnode simp:slp_def)
        from as = as'@as'' as'  [] have "length as'' < length as" by simp
        with IH last(targetnodes as') -as''* (_Exit_)
          last(targetnodes as') = n'
        obtain xs where "n' -xs* (_Exit_)" 
          and "set (sourcenodes xs)  set (sourcenodes as'')"
          and "a'set xs. intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf)"
          apply(erule_tac x="as''" in allE) by auto
        from n -as'sl* n' obtain ys where "n -ysι* n'"
          and "set(sourcenodes ys)  set(sourcenodes as')"
          by(erule same_level_path_inner_path)
        from n -ysι* n' n' -xs* (_Exit_) have "n -ys@xs* (_Exit_)"
          by(fastforce intro:slp_vp_Append intra_path_slp)
        moreover
        from set (sourcenodes xs)  set (sourcenodes as'')
          set(sourcenodes ys)  set(sourcenodes as') as = as'@as''
        have "set (sourcenodes (ys@xs))  set(sourcenodes as)"
          by(auto simp:sourcenodes_def)
        moreover
        from a'set xs. intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf)
          n -ysι* n'
        have "a'set (ys@xs). intra_kind (kind a')  (Q f p. kind a' = Q↩⇘pf)"
          by(fastforce simp:intra_path_def)
        ultimately show ?thesis by blast
      qed
    qed
  qed
qed


lemma valid_Exit_path_intra_path:
  assumes "n -as* (_Exit_)" 
  obtains as' pex where "n -as'ι* pex" and "method_exit pex" 
  and "set(sourcenodes as')  set(sourcenodes as)"
proof(atomize_elim)
  from n -as* (_Exit_)
  obtain as' where "n -as'* (_Exit_)" 
    and "set(sourcenodes as')  set(sourcenodes as)"
    and all:"a'  set as'. intra_kind(kind a')  (Q f p. kind a' = Q↩⇘pf)"
    by(erule valid_Exit_path_descending_path)
  show "as' pex. n -as'ι* pex  method_exit pex  
                  set(sourcenodes as')  set(sourcenodes as)"
  proof(cases "a'  set as'. Q f p. kind a' = Q↩⇘pf")
    case True
    then obtain asx ax asx' where [simp]:"as' = asx@ax#asx'" 
      and "Q f p. kind ax = Q↩⇘pf" and "a'  set asx. ¬ (Q f p. kind a' = Q↩⇘pf)"
      by(erule split_list_first_propE)
    with all 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 elim:path_split simp:vp_def)
    from n -asx→* sourcenode ax a'  set asx. intra_kind(kind a')
    have "n -asxι* sourcenode ax" by(simp add:intra_path_def)
    moreover
    from valid_edge ax Q f p. kind ax = Q↩⇘pf
    have "method_exit (sourcenode ax)" by(fastforce simp:method_exit_def)
    moreover
    from set(sourcenodes as')  set(sourcenodes as)
    have "set(sourcenodes asx)  set(sourcenodes as)" by(simp add:sourcenodes_def)
    ultimately show ?thesis by blast
  next
    case False
    with all n -as'* (_Exit_) have "n -as'ι* (_Exit_)" 
      by(fastforce simp:vp_def intra_path_def)
    moreover have "method_exit (_Exit_)" by(simp add:method_exit_def)
    ultimately show ?thesis using set(sourcenodes as')  set(sourcenodes as)
      by blast
  qed
qed



end 

end