Session HRB-Slicing

Theory AuxLemmas

section ‹Auxiliary lemmas›

theory AuxLemmas imports Main begin

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

Theory BasicDefs

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.

  Static Slicing analyses a CFG prior to execution. Whereas dynamic
  slicing can provide better results for certain inputs (i.e.\ trace and
  initial state), static slicing is more conservative but provides
  results independent of inputs. 

  Correctness for static slicing is defined using a weak
  simulation between nodes and states when traversing the original and
  the sliced graph. The weak simulation property demands that if a
  (node,state) tuples $(n_1,s_1)$ simulates $(n_2,s_2)$
  and making an observable move in the original graph leads from 
  $(n_1,s_1)$ to $(n_1',s_1')$, this tuple simulates a 
  tuple $(n_2,s_2)$ which is the result of making an
  observable move in the sliced graph beginning in $(n_2',s_2')$.  
›

section ‹Basic Definitions›

fun fun_upds :: "('a  'b)  'a list  'b list  ('a  'b)"
where "fun_upds f [] ys = f"
  | "fun_upds f xs [] = f"
  | "fun_upds f (x#xs) (y#ys) = (fun_upds f xs ys)(x := y)"

notation fun_upds ("_'(_ /[:=]/ _')")

lemma fun_upds_nth:
  "i < length xs; length xs = length ys; distinct xs
   f(xs [:=] ys)(xs!i) = (ys!i)"
proof(induct xs arbitrary:ys i)
  case Nil thus ?case by simp
next
  case (Cons x' xs')
  note IH = ys i. i < length xs'; length xs' = length ys; distinct xs'
     f(xs' [:=] ys) (xs'!i) = ys!i
  from ‹distinct (x'#xs') have "distinct xs'" and "x'  set xs'" by simp_all
  from ‹length (x'#xs') = length ys obtain y' ys' where [simp]:"ys = y'#ys'"
    and "length xs' = length ys'"
    by(cases ys) auto
  show ?case
  proof(cases i)
    case 0 thus ?thesis by simp
  next
    case (Suc j)
    with i < length (x'#xs') have "j < length xs'" by simp
    from IH[OF this ‹length xs' = length ys' ‹distinct xs']
    have "f(xs' [:=] ys') (xs'!j) = ys'!j" .
    with x'  set xs' j < length xs'
    have "f((x'#xs') [:=] ys) ((x'#xs')!(Suc j)) = ys!(Suc j)" by fastforce
    with Suc show ?thesis by simp
  qed
qed


lemma fun_upds_eq:
  assumes "V  set xs" and "length xs = length ys" and "distinct xs"
  shows "f(xs [:=] ys) V = f'(xs [:=] ys) V"
proof -
  from V  set xs obtain i where "i < length xs" and "xs!i = V"
    by(fastforce simp:in_set_conv_nth)
  with ‹length xs = length ys ‹distinct xs
  have "f(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
  moreover
  from i < length xs xs!i = V ‹length xs = length ys ‹distinct xs
  have "f'(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
  ultimately show ?thesis using xs!i = V by simp
qed


lemma fun_upds_notin:"x  set xs  f(xs [:=] ys) x = f x"
by(induct xs arbitrary:ys,auto,case_tac ys,auto)


subsection distinct_fst›
 
definition distinct_fst :: "('a × 'b) list  bool" where
  "distinct_fst    distinct  map fst"

lemma distinct_fst_Nil [simp]:
  "distinct_fst []" 
  by(simp add:distinct_fst_def)

lemma distinct_fst_Cons [simp]:
  "distinct_fst ((k,x)#kxs) = (distinct_fst kxs  (y. (k,y)  set kxs))"
by(auto simp:distinct_fst_def image_def)


lemma distinct_fst_isin_same_fst:
  "(x,y)  set xs; (x,y')  set xs; distinct_fst xs
   y = y'"
by(induct xs,auto simp:distinct_fst_def image_def)


subsection‹Edge kinds›

text ‹Every procedure has a unique name, e.g. in object oriented languages
  pname› refers to class + procedure.›

text ‹A state is a call stack of tuples, which consists of:
  \begin{enumerate}
  \item data information, i.e.\ a mapping from the local variables in the call 
  frame to their values, and
  \item control flow information, e.g.\ which node called the current procedure.
  \end{enumerate}

  Update and predicate edges check and manipulate only the data information
  of the top call stack element. Call and return edges however may use the data and
  control flow information present in the top stack element to state if this edge is
  traversable. The call edge additionally has a list of functions to determine what
  values the parameters have in a certain call frame and control flow information for
  the return. The return edge is concerned with passing the values 
  of the return parameter values to the underlying stack frame. See the funtions 
  transfer› and pred› in locale CFG›.›

datatype (dead 'var, dead 'val, dead 'ret, dead 'pname) edge_kind =
    UpdateEdge "('var  'val)  ('var  'val)"                  ("_")
  | PredicateEdge "('var  'val)  bool"                         ("'(_')")
  | CallEdge "('var  'val) × 'ret  bool" "'ret" "'pname"  
             "(('var  'val)  'val) list"                       ("_:_↪⇘__" 70)
  | ReturnEdge "('var  'val) × 'ret  bool" "'pname" 
               "('var  'val)  ('var  'val)  ('var  'val)" ("_↩⇘__" 70)


definition intra_kind :: "('var,'val,'ret,'pname) edge_kind  bool"
where "intra_kind et  (f. et = f)  (Q. et = (Q))"


lemma edge_kind_cases [case_names Intra Call Return]:
  "intra_kind et  P; Q r p fs. et = Q:rpfs  P;
    Q p f. et = Qpf  P  P"
by(cases et,auto simp:intra_kind_def)


end

Theory CFG

section ‹CFG›

theory CFG imports BasicDefs begin

subsection ‹The abstract CFG›

subsubsection ‹Locale fixes and assumptions›

locale CFG =
  fixes sourcenode :: "'edge  'node"
  fixes targetnode :: "'edge  'node"
  fixes kind :: "'edge  ('var,'val,'ret,'pname) edge_kind"
  fixes valid_edge :: "'edge  bool"
  fixes Entry::"'node" ("'('_Entry'_')")
  fixes get_proc::"'node  'pname"
  fixes get_return_edges::"'edge  'edge set"
  fixes procs::"('pname × 'var list × 'var list) list"
  fixes Main::"'pname"
  assumes Entry_target [dest]: "valid_edge a; targetnode a = (_Entry_)  False"
  and get_proc_Entry:"get_proc (_Entry_) = Main"
  and Entry_no_call_source:
    "valid_edge a; kind a = Q:rpfs; sourcenode a = (_Entry_)  False"
  and edge_det: 
    "valid_edge a; valid_edge a'; sourcenode a = sourcenode a'; 
      targetnode a = targetnode a'  a = a'" 
  and Main_no_call_target:"valid_edge a; kind a = Q:rMainf  False" 
  and Main_no_return_source:"valid_edge a; kind a = Q'Mainf'  False" 
  and callee_in_procs: 
    "valid_edge a; kind a = Q:rpfs  ins outs. (p,ins,outs)  set procs" 
  and get_proc_intra:"valid_edge a; intra_kind(kind a)
     get_proc (sourcenode a) = get_proc (targetnode a)" 
  and get_proc_call:
    "valid_edge a; kind a = Q:rpfs  get_proc (targetnode a) = p"
  and get_proc_return:
    "valid_edge a; kind a = Q'pf'  get_proc (sourcenode a) = p"
  and call_edges_only:"valid_edge a; kind a = Q:rpfs 
     a'. valid_edge a'  targetnode a' = targetnode a  
            (Qx rx fsx. kind a' = Qx:rxpfsx)"
  and return_edges_only:"valid_edge a; kind a = Q'pf' 
     a'. valid_edge a'  sourcenode a' = sourcenode a  
            (Qx fx. kind a' = Qxpfx)" 
  and get_return_edge_call:
    "valid_edge a; kind a = Q:rpfs  get_return_edges a  {}" 
  and get_return_edges_valid:
    "valid_edge a; a'  get_return_edges a  valid_edge a'" 
  and only_call_get_return_edges:
    "valid_edge a; a'  get_return_edges a  Q r p fs. kind a = Q:rpfs" 
  and call_return_edges:
    "valid_edge a; kind a = Q:rpfs; a'  get_return_edges a 
     Q' f'. kind a' = Q'pf'" 
  and return_needs_call: "valid_edge a; kind a = Q'pf'
     ∃!a'. valid_edge a'  (Q r fs. kind a' = Q:rpfs)  a  get_return_edges a'"
  and intra_proc_additional_edge: 
    "valid_edge a; a'  get_return_edges a
     a''. valid_edge a''  sourcenode a'' = targetnode a  
              targetnode a'' = sourcenode a'  kind a'' = (λcf. False)"
  and call_return_node_edge: 
  "valid_edge a; a'  get_return_edges a
     a''. valid_edge a''  sourcenode a'' = sourcenode a  
             targetnode a'' = targetnode a'  kind a'' = (λcf. False)"
  and call_only_one_intra_edge:
    "valid_edge a; kind a = Q:rpfs 
     ∃!a'. valid_edge a'  sourcenode a' = sourcenode a  intra_kind(kind a')"
 and return_only_one_intra_edge:
    "valid_edge a; kind a = Q'pf' 
     ∃!a'. valid_edge a'  targetnode a' = targetnode a  intra_kind(kind a')"
  and same_proc_call_unique_target:
    "valid_edge a; valid_edge a'; kind a = Q1:r1pfs1;  kind a' = Q2:r2pfs2
     targetnode a = targetnode a'"
  and unique_callers:"distinct_fst procs" 
  and distinct_formal_ins:"(p,ins,outs)  set procs  distinct ins"
  and distinct_formal_outs:"(p,ins,outs)  set procs  distinct outs"

begin


lemma get_proc_get_return_edge:
  assumes "valid_edge a" and "a'  get_return_edges a"
  shows "get_proc (sourcenode a) = get_proc (targetnode a')"
proof -
  from assms obtain ax where "valid_edge ax" and "sourcenode a = sourcenode ax"
    and "targetnode a' = targetnode ax" and "intra_kind(kind ax)"
    by(auto dest:call_return_node_edge simp:intra_kind_def)
  thus ?thesis by(fastforce intro:get_proc_intra)
qed


lemma call_intra_edge_False:
  assumes "valid_edge a" and "kind a = Q:rpfs" and "valid_edge a'" 
  and "sourcenode a = sourcenode a'" and "intra_kind(kind a')"
  shows "kind a' = (λcf. False)"
proof -
  from valid_edge a kind a = Q:rpfs obtain ax where "ax  get_return_edges a"
    by(fastforce dest:get_return_edge_call)
  with valid_edge a obtain a'' where "valid_edge a''" 
    and "sourcenode a'' = sourcenode a" and "kind a'' = (λcf. False)"
    by(fastforce dest:call_return_node_edge)
  from kind a'' = (λcf. False) have "intra_kind(kind a'')" 
    by(simp add:intra_kind_def)
  with assms valid_edge a'' sourcenode a'' = sourcenode a 
    kind a'' = (λcf. False)
  show ?thesis by(fastforce dest:call_only_one_intra_edge)
qed


lemma formal_in_THE: 
  "valid_edge a; kind a = Q:rpfs; (p,ins,outs)  set procs
   (THE ins. outs. (p,ins,outs)  set procs) = ins"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)

lemma formal_out_THE: 
  "valid_edge a; kind a = Qpf; (p,ins,outs)  set procs
   (THE outs. ins. (p,ins,outs)  set procs) = outs"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)


subsubsection ‹Transfer and predicate functions›

fun params :: "(('var  'val)  'val) list  ('var  'val)  'val option list"
where "params [] cf = []"
  | "params (f#fs) cf = (f cf)#params fs cf"


lemma params_nth: 
  "i < length fs  (params fs cf)!i = (fs!i) cf"
by(induct fs arbitrary:i,auto,case_tac i,auto)


lemma [simp]:"length (params fs cf) = length fs"
  by(induct fs) auto


fun transfer :: "('var,'val,'ret,'pname) edge_kind  (('var  'val) × 'ret) list  
  (('var  'val) × 'ret) list"
where "transfer (f) (cf#cfs)    = (f (fst cf),snd cf)#cfs"
  | "transfer (Q) (cf#cfs)      = (cf#cfs)"
  | "transfer (Q:rpfs) (cf#cfs) = 
       (let ins = THE ins. outs. (p,ins,outs)  set procs in
                            (Map.empty(ins [:=] params fs (fst cf)),r)#cf#cfs)"
  | "transfer (Qpf )(cf#cfs)    = (case cfs of []  []
                                 | cf'#cfs'  (f (fst cf) (fst cf'),snd cf')#cfs')"
  | "transfer et [] = []"

fun transfers :: "('var,'val,'ret,'pname) edge_kind list  (('var  'val) × 'ret) list 
                  (('var  'val) × 'ret) list"
where "transfers [] s   = s"
  | "transfers (et#ets) s = transfers ets (transfer et s)"


fun pred :: "('var,'val,'ret,'pname) edge_kind  (('var  'val) × 'ret) list  bool"
where "pred (f) (cf#cfs) = True"
  | "pred (Q) (cf#cfs)   = Q (fst cf)"
  | "pred (Q:rpfs) (cf#cfs) = Q (fst cf,r)"
  | "pred (Qpf) (cf#cfs) = (Q cf  cfs  [])"
  | "pred et [] = False"

fun preds :: "('var,'val,'ret,'pname) edge_kind list  (('var  'val) × 'ret) list  bool"
where "preds [] s   = True"
  | "preds (et#ets) s = (pred et s  preds ets (transfer et 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


abbreviation state_val :: "(('var  'val) × 'ret) list  'var  'val"
  where "state_val s V  (fst (hd s)) V"


subsubsection valid_node›

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›

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_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(atomize_elim)
  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'
  show "a' as'. as = a'#as'  n = sourcenode a'  valid_edge a'  
                 targetnode a' -as'→* n'"
    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(atomize_elim)
  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'
  show "as' a'. as = as'@[a']  n -as'→* sourcenode a'  valid_edge a'  
                 n' = targetnode a'"
    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(atomize_elim)
  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)
  thus "a n. sourcenode a = (_Entry_)  targetnode a = n  n -tl as→* n'  
              valid_edge a  a = hd as"
  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  ('var,'val,'ret,'pname) 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


subsubsection ‹Intraprocedural paths›

definition intra_path :: "'node  'edge list  'node  bool" 
  ("_ -_ι* _" [51,0,0] 80)
where "n -asι* n'  n -as→* n'  (a  set as. intra_kind(kind a))"

lemma intra_path_get_procs:
  assumes "n -asι* n'" shows "get_proc n = get_proc n'"
proof -
  from n -asι* n' have "n -as→* n'" and "a  set as. intra_kind(kind a)"
    by(simp_all add:intra_path_def)
  thus ?thesis
  proof(induct as arbitrary:n)
    case Nil thus ?case by fastforce
  next
    case (Cons a' as')
    note IH = n. n -as'→* n'; aset as'. intra_kind (kind a)
       get_proc n = get_proc n'
    from aset (a'#as'). intra_kind (kind a)
    have "intra_kind(kind a')" and "aset as'. intra_kind (kind a)" by simp_all
    from n -a'#as'→* n' have "sourcenode a' = n" and "valid_edge a'"
      and "targetnode a' -as'→* n'" by(auto elim:path.cases)
    from IH[OF targetnode a' -as'→* n' aset as'. intra_kind (kind a)]
    have "get_proc (targetnode a') = get_proc n'" .
    from valid_edge a' ‹intra_kind(kind a') 
    have "get_proc (sourcenode a') = get_proc (targetnode a')"
      by(rule get_proc_intra)
    with sourcenode a' = n get_proc (targetnode a') = get_proc n'
    show ?case by simp
  qed
qed


lemma intra_path_Append:
  "n -asι* n''; n'' -as'ι* n'  n -as@as'ι* n'"
by(fastforce intro:path_Append simp:intra_path_def)


lemma get_proc_get_return_edges: 
  assumes "valid_edge a" and "a'  get_return_edges a"
  shows "get_proc(targetnode a) = get_proc(sourcenode a')"
proof -
  from valid_edge a a'  get_return_edges a
  obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
    and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)"
    by(fastforce dest:intra_proc_additional_edge)
  from valid_edge a'' kind a'' = (λcf. False)
  have "get_proc(sourcenode a'') = get_proc(targetnode a'')"
    by(fastforce intro:get_proc_intra simp:intra_kind_def)
  with sourcenode a'' = targetnode a targetnode a'' = sourcenode a'
  show ?thesis by simp
qed


subsubsection ‹Valid paths›

declare conj_cong[fundef_cong]

fun valid_path_aux :: "'edge list  'edge list  bool"
  where "valid_path_aux cs []  True"
  | "valid_path_aux cs (a#as)  
       (case (kind a) of Q:rpfs  valid_path_aux (a#cs) as
                       | Qpf  case cs of []  valid_path_aux [] as
                                     | c'#cs'  a  get_return_edges c' 
                                                 valid_path_aux cs' as
                       |    _  valid_path_aux cs as)"


lemma vpa_induct [consumes 1,case_names vpa_empty vpa_intra vpa_Call vpa_ReturnEmpty
  vpa_ReturnCons]:
  assumes major: "valid_path_aux xs ys"
  and rules: "cs. P cs []"
    "cs a as. intra_kind(kind a); valid_path_aux cs as; P cs as  P cs (a#as)"
    "cs a as Q r p fs. kind a = Q:rpfs; valid_path_aux (a#cs) as; P (a#cs) as 
       P cs (a#as)"
    "cs a as Q p f. kind a = Qpf; cs = []; valid_path_aux [] as; P [] as 
       P cs (a#as)"
    "cs a as Q p f c' cs' . kind a = Qpf; cs = c'#cs'; valid_path_aux cs' as;
                              a  get_return_edges c'; P cs' as
      P cs (a#as)"
  shows "P xs ys"
using major
apply(induct ys arbitrary: xs)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)


lemma valid_path_aux_intra_path:
  "a  set as. intra_kind(kind a)  valid_path_aux cs as"
by(induct as,auto simp:intra_kind_def)


lemma valid_path_aux_callstack_prefix:
  "valid_path_aux (cs@cs') as  valid_path_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpa_induct)
  case vpa_empty thus ?case by simp
next
  case (vpa_intra a as)
  hence "valid_path_aux cs as" by simp
  with ‹intra_kind (kind a) show ?case by(cases "kind a",auto simp:intra_kind_def)
next
  case (vpa_Call a as Q r p fs cs'' cs')
  note IH = xs ys. a#cs''@cs' = xs@ys  valid_path_aux xs as
  have "a#cs''@cs' = (a#cs'')@cs'" by simp
  from IH[OF this] have "valid_path_aux (a#cs'') as" .
  with kind a = Q:rpfs show ?case by simp
next
  case (vpa_ReturnEmpty a as Q p f cs'' cs')
  hence "valid_path_aux cs'' as" by simp
  with kind a = Qpf cs''@cs' = [] show ?case by simp
next
  case (vpa_ReturnCons a as Q p f c' cs' csx csx')
  note IH = xs ys. cs' = xs@ys  valid_path_aux xs as
  from csx@csx' = c'#cs' 
  have "csx = []  csx' = c'#cs'  (zs. csx = c'#zs  zs@csx' = cs')"
    by(simp add:append_eq_Cons_conv)
  thus ?case
  proof
    assume "csx = []  csx' = c'#cs'"
    hence "csx = []" and "csx' = c'#cs'" by simp_all
    from csx' = c'#cs' have "cs' = []@tl csx'" by simp
    from IH[OF this] have "valid_path_aux [] as" .
    with csx = [] kind a = Qpf show ?thesis by simp
  next
    assume "zs. csx = c'#zs  zs@csx' = cs'"
    then obtain zs where "csx = c'#zs" and "cs' = zs@csx'" by auto
    from IH[OF cs' = zs@csx'] have "valid_path_aux zs as" .
    with csx = c'#zs kind a = Qpf a  get_return_edges c' 
    show ?thesis by simp
  qed
qed


fun upd_cs :: "'edge list  'edge list  'edge list"
  where "upd_cs cs [] = cs"
  | "upd_cs cs (a#as) =
       (case (kind a) of Q:rpfs  upd_cs (a#cs) as
                       | Qpf  case cs of []  upd_cs cs as
                                      | c'#cs'  upd_cs cs' as
                       |    _  upd_cs cs as)"


lemma upd_cs_empty [dest]:
  "upd_cs cs [] = []  cs = []"
by(cases cs) auto


lemma upd_cs_intra_path:
  "a  set as. intra_kind(kind a)  upd_cs cs as = cs"
by(induct as,auto simp:intra_kind_def)


lemma upd_cs_Append:
  "upd_cs cs as = cs'; upd_cs cs' as' = cs''  upd_cs cs (as@as') = cs''"
by(induct as arbitrary:cs,auto split:edge_kind.split list.split)


lemma upd_cs_empty_split:
  assumes "upd_cs cs as = []" and "cs  []" and "as  []"
  obtains xs ys where "as = xs@ys" and "xs  []" and "upd_cs cs xs = []"
  and "xs' ys'. xs = xs'@ys'  ys'  []  upd_cs cs xs'  []"
  and "upd_cs [] ys = []"
proof(atomize_elim)
  from ‹upd_cs cs as = [] cs  [] as  []
  show "xs ys. as = xs@ys  xs  []  upd_cs cs xs = []  
             (xs' ys'. xs = xs'@ys'  ys'  []  upd_cs cs xs'  [])  
             upd_cs [] ys = []"
  proof(induct as arbitrary:cs)
    case Nil thus ?case by simp
  next
    case (Cons a' as')
    note IH = cs. upd_cs cs as' = []; cs  []; as'  []
       xs ys. as' = xs@ys  xs  []  upd_cs cs xs = [] 
                 (xs' ys'. xs = xs'@ys'  ys'  []  upd_cs cs xs'  [])  
                 upd_cs [] ys = []
    show ?case
    proof(cases "kind a'" rule:edge_kind_cases)
      case Intra
      with ‹upd_cs cs (a'#as') = [] have "upd_cs cs as' = []"
        by(fastforce simp:intra_kind_def)
      with cs  [] have "as'  []" by fastforce
      from IH[OF ‹upd_cs cs as' = [] cs  [] this] obtain xs ys where "as' = xs@ys"
        and "xs  []" and "upd_cs cs xs = []" and "upd_cs [] ys = []"
        and "xs' ys'. xs = xs'@ys'  ys'  []  upd_cs cs xs'  []" by blast
      from ‹upd_cs cs xs = [] Intra have "upd_cs cs (a'#xs) = []"
        by(fastforce simp:intra_kind_def)
      from xs' ys'. xs = xs'@ys'  ys'  []  upd_cs cs xs'  [] xs  [] Intra
      have "xs' ys'. a'#xs = xs'@ys'  ys'  []  upd_cs cs xs'  []"
        apply auto
        apply(case_tac xs') apply(auto simp:intra_kind_def)
        by(erule_tac x="[]" in allE,fastforce)+
      with as' = xs@ys ‹upd_cs cs (a'#xs) = [] ‹upd_cs [] ys = []
      show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
    next
      case (Call Q p f)
      with ‹upd_cs cs (a'#as') = [] have "upd_cs (a'#cs) as' = []" by simp
      with cs  [] have "as'  []" by fastforce
      from IH[OF ‹upd_cs (a'#cs) as' = [] _ this] obtain xs ys where "as' = xs@ys"
        and "xs  []" and "upd_cs (a'#cs) xs = []" and "upd_cs [] ys = []"
        and "xs' ys'. xs = xs'@ys'  ys'  []  upd_cs (a'#cs) xs'  []" by blast
      from ‹upd_cs (a'#cs) xs = [] Call have "upd_cs cs (a'#xs) = []" by simp
      from xs' ys'. xs = xs'@ys'  ys'  []  upd_cs (a'#cs) xs'  [] 
        xs  [] cs  [] Call
      have "xs' ys'. a'#xs = xs'@ys'  ys'  []  upd_cs cs xs'  []"
        by auto(case_tac xs',auto)
      with as' = xs@ys ‹upd_cs cs (a'#xs) = [] ‹upd_cs [] ys = []
      show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
    next
      case (Return Q p f)
      with ‹upd_cs cs (a'#as') = [] cs  [] obtain c' cs' where "cs = c'#cs'"
        and "upd_cs cs' as' = []" by(cases cs) auto
      show ?thesis
      proof(cases "cs' = []")
        case True
        with cs = c'#cs' ‹upd_cs cs' as' = [] Return show ?thesis
          apply(rule_tac x="[a']" in exI) apply clarsimp
          by(case_tac xs') auto
      next
        case False
        with ‹upd_cs cs' as' = [] have "as'  []" by fastforce
        from IH[OF ‹upd_cs cs' as' = [] False this] obtain xs ys where "as' = xs@ys"
          and "xs  []" and "upd_cs cs' xs = []" and "upd_cs [] ys = []"
          and "xs' ys'. xs = xs'@ys'  ys'  []  upd_cs cs' xs'  []" by blast
        from ‹upd_cs cs' xs = [] cs = c'#cs' Return have "upd_cs cs (a'#xs) = []"
          by simp
        from xs' ys'. xs = xs'@ys'  ys'  []  upd_cs cs' xs'  []
          xs  [] cs = c'#cs' Return
        have "xs' ys'. a'#xs = xs'@ys'  ys'  []  upd_cs cs xs'  []"
          by auto(case_tac xs',auto)
        with as' = xs@ys ‹upd_cs cs (a'#xs) = [] ‹upd_cs [] ys = []
        show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
      qed
    qed
  qed
qed


lemma upd_cs_snoc_Return_Cons:
  assumes "kind a = Qpf"
  shows "upd_cs cs as = c'#cs'  upd_cs cs (as@[a]) = cs'"
proof(induct as arbitrary:cs)
  case Nil
  with kind a = Qpf have "upd_cs cs [a] = cs'" by simp
 thus ?case by simp
next
  case (Cons a' as')
  note IH = cs. upd_cs cs as' = c'#cs'  upd_cs cs (as'@[a]) = cs'
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    with ‹upd_cs cs (a'#as') = c'#cs'
    have "upd_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def)
    from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
    with Intra show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Call
    with ‹upd_cs cs (a'#as') = c'#cs'
    have "upd_cs (a'#cs) as' = c'#cs'" by simp
    from IH[OF this] have "upd_cs (a'#cs) (as'@[a]) = cs'" .
    with Call show ?thesis by simp
  next
    case Return
    show ?thesis
    proof(cases cs)
      case Nil
      with ‹upd_cs cs (a'#as') = c'#cs' Return
      have "upd_cs cs as' = c'#cs'" by simp
      from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
      with Nil Return show ?thesis by simp
    next
      case (Cons cx csx)
      with ‹upd_cs cs (a'#as') = c'#cs' Return
      have "upd_cs csx as' = c'#cs'" by simp
      from IH[OF this] have "upd_cs csx (as'@[a]) = cs'" .
      with Cons Return show ?thesis by simp
    qed
  qed
qed


lemma upd_cs_snoc_Call:
  assumes "kind a = Q:rpfs"
  shows "upd_cs cs (as@[a]) = a#(upd_cs cs as)"
proof(induct as arbitrary:cs)
  case Nil
  with kind a = Q:rpfs show ?case by simp
next
  case (Cons a' as')
  note IH = cs. upd_cs cs (as'@[a]) = a#upd_cs cs as'
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra 
    with IH[of cs] show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Call
    with IH[of "a'#cs"] show ?thesis by simp
  next
    case Return
    show ?thesis
    proof(cases cs)
      case Nil
      with IH[of "[]"] Return show ?thesis by simp
    next
      case (Cons cx csx)
      with IH[of csx] Return show ?thesis by simp
    qed
  qed
qed





lemma valid_path_aux_split:
  assumes "valid_path_aux cs (as@as')"
  shows "valid_path_aux cs as" and "valid_path_aux (upd_cs cs as) as'"
  using ‹valid_path_aux cs (as@as')
proof(induct cs "as@as'" arbitrary:as as' rule:vpa_induct)
  case (vpa_intra cs a as as'')
  note IH1 = xs ys. as = xs@ys  valid_path_aux cs xs
  note IH2 = xs ys. as = xs@ys  valid_path_aux (upd_cs cs xs) ys
  { case 1
    from vpa_intra
    have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      thus ?thesis by simp
    next
      assume "xs. a#xs = as''  as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH1[OF as = xs@as'] have "valid_path_aux cs xs" .
      with a#xs = as'' ‹intra_kind (kind a)
      show ?thesis by(fastforce simp:intra_kind_def)
    qed
  next
    case 2
    from vpa_intra
    have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux (upd_cs cs []) (tl as')" by simp
      with as'' = []  a#as = as' ‹intra_kind (kind a)
      show ?thesis by(fastforce simp:intra_kind_def)
    next
      assume "xs. a#xs = as''  as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF as = xs@as'] have "valid_path_aux (upd_cs cs xs) as'" .
      from a#xs = as'' ‹intra_kind (kind a) 
      have "upd_cs cs xs = upd_cs cs as''" by(fastforce simp:intra_kind_def)
      with ‹valid_path_aux (upd_cs cs xs) as'
      show ?thesis by simp
    qed
  }
next
  case (vpa_Call cs a as Q r p fs as'')
  note IH1 = xs ys. as = xs@ys  valid_path_aux (a#cs) xs
  note IH2 = xs ys. as = xs@ys    valid_path_aux (upd_cs (a#cs) xs) ys
  { case 1
    from vpa_Call
    have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      thus ?thesis by simp
    next
      assume "xs. a#xs = as''  as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH1[OF as = xs@as'] have "valid_path_aux (a#cs) xs" .
      with a#xs = as''[THEN sym] kind a = Q:rpfs
      show ?thesis by simp
    qed
  next
    case 2
    from vpa_Call
    have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux (upd_cs (a#cs) []) (tl as')" .
      with as'' = []  a#as = as' kind a = Q:rpfs
      show ?thesis by clarsimp
    next
      assume "xs. a#xs = as''  as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF as = xs@as'] have "valid_path_aux (upd_cs (a # cs) xs) as'" .
      with a#xs = as''[THEN sym]  kind a = Q:rpfs
      show ?thesis by simp
    qed
  }
next
  case (vpa_ReturnEmpty cs a as Q p f as'')
  note IH1 = xs ys. as = xs@ys  valid_path_aux [] xs
  note IH2 = xs ys. as = xs@ys  valid_path_aux (upd_cs [] xs) ys
  { case 1
    from vpa_ReturnEmpty
    have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      thus ?thesis by simp
    next
      assume "xs. a#xs = as''  as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH1[OF as = xs@as'] have "valid_path_aux [] xs" .
      with a#xs = as''[THEN sym] kind a = Qpf cs = []
      show ?thesis by simp
    qed
  next
    case 2
    from vpa_ReturnEmpty
    have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux [] (tl as')" by simp
      with as'' = []  a#as = as' kind a = Qpf cs = []
      show ?thesis by fastforce
    next
      assume "xs. a#xs = as''  as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF as = xs@as'] have "valid_path_aux (upd_cs [] xs) as'" .
      from a#xs = as''[THEN sym] kind a = Qpf cs = []
      have "upd_cs [] xs = upd_cs cs as''" by simp
      with ‹valid_path_aux (upd_cs [] xs) as' show ?thesis by simp
    qed
  }
next
  case (vpa_ReturnCons cs a as Q p f c' cs' as'')
  note IH1 = xs ys. as = xs@ys  valid_path_aux cs' xs
  note IH2 = xs ys. as = xs@ys  valid_path_aux (upd_cs cs' xs) ys
  { case 1
    from vpa_ReturnCons
    have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      thus ?thesis by simp
    next
       assume "xs. a#xs = as''  as = xs@as'"
       then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
       from IH1[OF as = xs@as'] have "valid_path_aux cs' xs" .
       with a#xs = as''[THEN sym] kind a = Qpf cs = c'#cs'
         a  get_return_edges c'
       show ?thesis by simp
     qed
   next
     case 2
     from vpa_ReturnCons
     have "as'' = []  a#as = as'  (xs. a#xs = as''  as = xs@as')"
      by(simp add:Cons_eq_append_conv)
    thus ?case
    proof
      assume "as'' = []  a#as = as'"
      hence "as = []@tl as'" by(cases as') auto
      from IH2[OF this] have "valid_path_aux (upd_cs cs' []) (tl as')" .
       with as'' = []  a#as = as' kind a = Qpf cs = c'#cs'
         a  get_return_edges c'
       show ?thesis by fastforce
    next
      assume "xs. a#xs = as''  as = xs@as'"
      then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
      from IH2[OF as = xs@as'] have "valid_path_aux (upd_cs cs' xs) as'" .
      from a#xs = as''[THEN sym] kind a = Qpf cs = c'#cs'
      have "upd_cs cs' xs = upd_cs cs as''" by simp
      with ‹valid_path_aux (upd_cs cs' xs) as' show ?thesis by simp
    qed
  }
qed simp_all


lemma valid_path_aux_Append:
  "valid_path_aux cs as; valid_path_aux (upd_cs cs as) as'
   valid_path_aux cs (as@as')"
by(induct rule:vpa_induct,auto simp:intra_kind_def)


lemma vpa_snoc_Call:
  assumes "kind a = Q:rpfs"
  shows "valid_path_aux cs as  valid_path_aux cs (as@[a])"
proof(induct rule:vpa_induct)
  case (vpa_empty cs)
  from kind a = Q:rpfs have "valid_path_aux cs [a]" by simp
  thus ?case by simp
next
  case (vpa_intra cs a' as')
  from ‹valid_path_aux cs (as'@[a]) ‹intra_kind (kind a')
  have "valid_path_aux cs (a'#(as'@[a]))"
    by(fastforce simp:intra_kind_def)
  thus ?case by simp
next
  case (vpa_Call cs a' as' Q' r' p' fs')
  from ‹valid_path_aux (a'#cs) (as'@[a]) kind a' = Q':r'p'fs'
  have "valid_path_aux cs (a'#(as'@[a]))" by simp
  thus ?case by simp
next
  case (vpa_ReturnEmpty cs a' as' Q' p' f')
  from ‹valid_path_aux [] (as'@[a]) kind a' = Q'p'f' cs = []
  have "valid_path_aux cs (a'#(as'@[a]))" by simp
  thus ?case by simp
next
  case (vpa_ReturnCons cs a' as' Q' p' f' c' cs')
  from ‹valid_path_aux cs' (as'@[a]) kind a' = Q'p'f' cs = c'#cs'
    a'  get_return_edges c'
  have "valid_path_aux cs (a'#(as'@[a]))" by simp
  thus ?case by simp
qed



definition valid_path :: "'edge list  bool"
  where "valid_path as  valid_path_aux [] as"


lemma valid_path_aux_valid_path:
  "valid_path_aux cs as  valid_path as"
by(fastforce intro:valid_path_aux_callstack_prefix simp:valid_path_def)

lemma valid_path_split:
  assumes "valid_path (as@as')" shows "valid_path as" and "valid_path as'"
  using ‹valid_path (as@as')
  apply(auto simp:valid_path_def)
   apply(erule valid_path_aux_split)
  apply(drule valid_path_aux_split(2))
  by(fastforce intro:valid_path_aux_callstack_prefix)



definition valid_path' :: "'node  'edge list  'node  bool"
  ("_ -_* _" [51,0,0] 80)
where vp_def:"n -as* n'  n -as→* n'  valid_path as"


lemma intra_path_vp:
  assumes "n -asι* n'" shows "n -as* n'"
proof -
  from n -asι* n' have "n -as→* n'" and "a  set as. intra_kind(kind a)"
    by(simp_all add:intra_path_def)
  from a  set as. intra_kind(kind a) have "valid_path_aux [] as"
    by(rule valid_path_aux_intra_path)
  thus ?thesis using n -as→* n' by(simp add:vp_def valid_path_def)
qed


lemma vp_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(atomize_elim)
  from n -as* n' as  [] obtain a' as' where "as = a'#as'"
    and "n = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
    by(fastforce elim:path_split_Cons simp:vp_def)
  from n -as* n' have "valid_path as" by(simp add:vp_def)
  from as = a'#as' have "as = [a']@as'" by simp
  with ‹valid_path as have "valid_path ([a']@as')" by simp
  hence "valid_path as'" by(rule valid_path_split)
  with targetnode a' -as'→* n' have "targetnode a' -as'* n'" by(simp add:vp_def)
  with as = a'#as' n = sourcenode a' valid_edge a'
  show "a' as'. as = a'#as'  n = sourcenode a'  valid_edge a'  
                 targetnode a' -as'* n'" by blast
qed

lemma vp_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(atomize_elim)
  from n -as* n' as  [] obtain a' as' where "as = as'@[a']"
    and "n -as'→* sourcenode a'" and "valid_edge a'" and "n' = targetnode a'"
    by(clarsimp simp:vp_def)(erule path_split_snoc,auto)
  from n -as* n' as = as'@[a'] have "valid_path (as'@[a'])" by(simp add:vp_def)
  hence "valid_path as'" by(rule valid_path_split)
  with n -as'→* sourcenode a' have "n -as'* sourcenode a'" by(simp add:vp_def)
  with as = as'@[a'] valid_edge a' n' = targetnode a'
  show "as' a'. as = as'@[a']  n -as'* sourcenode a'  valid_edge a'  
                 n' = targetnode a'"
  by blast
qed

lemma vp_split:
  assumes "n -as@a#as'* n'"
  shows "n -as* sourcenode a" and "valid_edge a" and "targetnode a -as'* n'"
proof -
  from n -as@a#as'* n' have "n -as→* sourcenode a" and "valid_edge a" 
    and "targetnode a -as'→* n'"
    by(auto intro:path_split simp:vp_def)
  from n -as@a#as'* n' have "valid_path (as@a#as')" by(simp add:vp_def)
  hence "valid_path as" and "valid_path (a#as')" by(auto intro:valid_path_split)
  from ‹valid_path (a#as') have "valid_path ([a]@as')" by simp
  hence "valid_path as'"  by(rule valid_path_split)
  with n -as→* sourcenode a ‹valid_path as valid_edge a targetnode a -as'→* n'
  show "n -as* sourcenode a" "valid_edge a" "targetnode a -as'* n'"
    by(auto simp:vp_def)
qed

lemma vp_split_second:
  assumes "n -as@a#as'* n'" shows "sourcenode a -a#as'* n'"
proof -
  from n -as@a#as'* n' have "sourcenode a -a#as'→* n'"
    by(fastforce elim:path_split_second simp:vp_def)
  from n -as@a#as'* n' have "valid_path (as@a#as')" by(simp add:vp_def)
  hence "valid_path (a#as')" by(rule valid_path_split)
  with sourcenode a -a#as'→* n' show ?thesis by(simp add:vp_def)
qed




function valid_path_rev_aux :: "'edge list  'edge list  bool"
  where "valid_path_rev_aux cs []  True"
  | "valid_path_rev_aux cs (as@[a])  
       (case (kind a) of Qpf  valid_path_rev_aux (a#cs) as
                       | Q:rpfs  case cs of []  valid_path_rev_aux [] as
                                     | c'#cs'  c'  get_return_edges a 
                                                 valid_path_rev_aux cs' as
                       |    _  valid_path_rev_aux cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order



lemma vpra_induct [consumes 1,case_names vpra_empty vpra_intra vpra_Return 
  vpra_CallEmpty vpra_CallCons]:
  assumes major: "valid_path_rev_aux xs ys"
  and rules: "cs. P cs []"
    "cs a as. intra_kind(kind a); valid_path_rev_aux cs as; P cs as 
       P cs (as@[a])"
    "cs a as Q p f. kind a = Qpf; valid_path_rev_aux (a#cs) as; P (a#cs) as 
       P cs (as@[a])"
    "cs a as Q r p fs. kind a = Q:rpfs; cs = []; valid_path_rev_aux [] as; 
         P [] as  P cs (as@[a])"
    "cs a as Q r p fs c' cs'. kind a = Q:rpfs; cs = c'#cs'; 
         valid_path_rev_aux cs' as; c'  get_return_edges a; P cs' as
      P cs (as@[a])"
  shows "P xs ys"
using major
apply(induct ys arbitrary:xs rule:rev_induct)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)


lemma vpra_callstack_prefix:
  "valid_path_rev_aux (cs@cs') as  valid_path_rev_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpra_induct)
  case vpra_empty thus ?case by simp
next
  case (vpra_intra a as)
  hence "valid_path_rev_aux cs as" by simp
  with ‹intra_kind (kind a) show ?case by(fastforce simp:intra_kind_def)
next
  case (vpra_Return a as Q p f)
  note IH = ds ds'. a#cs@cs' = ds@ds'  valid_path_rev_aux ds as
  have "a#cs@cs' = (a#cs)@cs'" by simp
  from IH[OF this] have "valid_path_rev_aux (a#cs) as" .
  with kind a = Qpf show ?case by simp
next
  case (vpra_CallEmpty a as Q r p fs)
  hence "valid_path_rev_aux cs as" by simp
  with kind a = Q:rpfs cs@cs' = [] show ?case by simp
next
  case (vpra_CallCons a as Q r p fs c' csx)
  note IH = cs cs'. csx = cs@cs'  valid_path_rev_aux cs as
  from cs@cs' = c'#csx
  have "(cs = []  cs' = c'#csx)  (zs. cs = c'#zs  zs@cs' = csx)"
    by(simp add:append_eq_Cons_conv)
  thus ?case
  proof
    assume "cs = []  cs' = c'#csx"
    hence "cs = []" and "cs' = c'#csx" by simp_all
    from cs' = c'#csx have "csx = []@tl cs'" by simp
    from IH[OF this] have "valid_path_rev_aux [] as" .
    with cs = [] kind a = Q:rpfs show ?thesis by simp
  next
    assume "zs. cs = c'#zs  zs@cs' = csx"
    then obtain zs where "cs = c'#zs" and "csx = zs@cs'" by auto
    from IH[OF csx = zs@cs'] have "valid_path_rev_aux zs as" .
    with cs = c'#zs kind a = Q:rpfs c'  get_return_edges a show ?thesis by simp
  qed
qed



function upd_rev_cs :: "'edge list  'edge list  'edge list"
  where "upd_rev_cs cs [] = cs"
  | "upd_rev_cs cs (as@[a]) =
       (case (kind a) of Qpf  upd_rev_cs (a#cs) as
                       | Q:rpfs  case cs of []  upd_rev_cs cs as
                                      | c'#cs'  upd_rev_cs cs' as
                       |    _  upd_rev_cs cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order


lemma upd_rev_cs_empty [dest]:
  "upd_rev_cs cs [] = []  cs = []"
by(cases cs) auto


lemma valid_path_rev_aux_split:
  assumes "valid_path_rev_aux cs (as@as')"
  shows "valid_path_rev_aux cs as'" and "valid_path_rev_aux (upd_rev_cs cs as') as"
  using ‹valid_path_rev_aux cs (as@as')
proof(induct cs "as@as'" arbitrary:as as' rule:vpra_induct)
  case (vpra_intra cs a as as'')
  note IH1 = xs ys. as = xs@ys  valid_path_rev_aux cs ys
  note IH2 = xs ys. as = xs@ys  valid_path_rev_aux (upd_rev_cs cs ys) xs
  { case 1
    from vpra_intra
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      thus ?thesis by simp
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF as = as''@xs] have "valid_path_rev_aux cs xs" .
      with xs@[a] = as' ‹intra_kind (kind a)
      show ?thesis by(fastforce simp:intra_kind_def)
    qed
  next
    case 2
    from vpra_intra
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs cs []) (butlast as'')" .
      with as' = []  as@[a] = as'' ‹intra_kind (kind a)
      show ?thesis by(fastforce simp:intra_kind_def)
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF as = as''@xs] have "valid_path_rev_aux (upd_rev_cs cs xs) as''" .
      from xs@[a] = as' ‹intra_kind (kind a) 
      have "upd_rev_cs cs xs = upd_rev_cs cs as'" by(fastforce simp:intra_kind_def)
      with ‹valid_path_rev_aux (upd_rev_cs cs xs) as''
      show ?thesis by simp
    qed
  }
next
  case (vpra_Return cs a as Q p f as'')
  note IH1 = xs ys. as = xs@ys  valid_path_rev_aux (a#cs) ys
  note IH2 = xs ys. as = xs@ys  valid_path_rev_aux (upd_rev_cs (a#cs) ys) xs
  { case 1
    from vpra_Return
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      thus ?thesis by simp
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF as = as''@xs] have "valid_path_rev_aux (a#cs) xs" .
      with xs@[a] = as' kind a = Qpf
      show ?thesis by fastforce
    qed
  next
    case 2
    from vpra_Return
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] 
      have "valid_path_rev_aux (upd_rev_cs (a#cs) []) (butlast as'')" .
      with as' = []  as@[a] = as'' kind a = Qpf
      show ?thesis by fastforce
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF as = as''@xs] 
      have "valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''" .
      from xs@[a] = as' kind a = Qpf
      have "upd_rev_cs (a#cs) xs = upd_rev_cs cs as'" by fastforce
      with ‹valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''
      show ?thesis by simp
    qed
  }
next
  case (vpra_CallEmpty cs a as Q r p fs as'')
  note IH1 = xs ys. as = xs@ys  valid_path_rev_aux [] ys
  note IH2 = xs ys. as = xs@ys  valid_path_rev_aux (upd_rev_cs [] ys) xs
  { case 1
    from vpra_CallEmpty
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      thus ?thesis by simp
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF as = as''@xs] have "valid_path_rev_aux [] xs" .
      with xs@[a] = as' kind a = Q:rpfs cs = []
      show ?thesis by fastforce
    qed
  next
    case 2
    from vpra_CallEmpty
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] 
      have "valid_path_rev_aux (upd_rev_cs [] []) (butlast as'')" .
      with as' = []  as@[a] = as'' kind a = Q:rpfs cs = []
      show ?thesis by fastforce
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF as = as''@xs] 
      have "valid_path_rev_aux (upd_rev_cs [] xs) as''" .
      with xs@[a] = as' kind a = Q:rpfs cs = [] 
      show ?thesis by fastforce
    qed
  }
next
  case (vpra_CallCons cs a as Q r p fs c' cs' as'')
  note IH1 = xs ys. as = xs@ys  valid_path_rev_aux cs' ys
  note IH2 = xs ys. as = xs@ys  valid_path_rev_aux (upd_rev_cs cs' ys) xs
  { case 1
    from vpra_CallCons
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      thus ?thesis by simp
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH1[OF as = as''@xs] have "valid_path_rev_aux cs' xs" .
      with xs@[a] = as' kind a = Q:rpfs cs = c' # cs' c'  get_return_edges a
      show ?thesis by fastforce
    qed
  next
    case 2
    from vpra_CallCons
    have "as' = []  as@[a] = as''  (xs. as = as''@xs  xs@[a] = as')"
      by(cases as' rule:rev_cases) auto
    thus ?case
    proof
      assume "as' = []  as@[a] = as''"
      hence "as = butlast as''@[]" by(cases as) auto
      from IH2[OF this] 
      have "valid_path_rev_aux (upd_rev_cs cs' []) (butlast as'')" .
      with as' = []  as@[a] = as'' kind a = Q:rpfs cs = c' # cs'
        c'  get_return_edges a show ?thesis by fastforce
    next
      assume "xs. as = as''@xs  xs@[a] = as'"
      then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
      from IH2[OF as = as''@xs] 
      have "valid_path_rev_aux (upd_rev_cs cs' xs) as''" .
      with xs@[a] = as' kind a = Q:rpfs cs = c' # cs'
        c'  get_return_edges a
      show ?thesis by fastforce
    qed
  }
qed simp_all


lemma valid_path_rev_aux_Append:
  "valid_path_rev_aux cs as'; valid_path_rev_aux (upd_rev_cs cs as') as
   valid_path_rev_aux cs (as@as')"
by(induct rule:vpra_induct,
   auto simp:intra_kind_def simp del:append_assoc simp:append_assoc[THEN sym])


lemma vpra_Cons_intra:
  assumes "intra_kind(kind a)"
  shows "valid_path_rev_aux cs as  valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
  case (vpra_empty cs)
  have "valid_path_rev_aux cs []" by simp
  with ‹intra_kind(kind a) have "valid_path_rev_aux cs ([]@[a])"
    by(simp only:valid_path_rev_aux.simps intra_kind_def,fastforce)
  thus ?case by simp
qed(simp only:append_Cons[THEN sym] valid_path_rev_aux.simps intra_kind_def,fastforce)+


lemma vpra_Cons_Return:
  assumes "kind a = Qpf"
  shows "valid_path_rev_aux cs as  valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
  case (vpra_empty cs)
  from kind a = Qpf have "valid_path_rev_aux cs ([]@[a])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
next
  case (vpra_intra cs a' as')
  from ‹valid_path_rev_aux cs (a#as') ‹intra_kind (kind a')
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,fastforce simp:intra_kind_def)
  thus ?case by simp
next
  case (vpra_Return cs a' as' Q' p' f')
  from ‹valid_path_rev_aux (a'#cs) (a#as') kind a' = Q'p'f'
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
next
  case (vpra_CallEmpty cs a' as' Q' r' p' fs')
  from ‹valid_path_rev_aux [] (a#as') kind a' = Q':r'p'fs' cs = []
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
next
  case (vpra_CallCons cs a' as' Q' r' p' fs' c' cs')
  from ‹valid_path_rev_aux cs' (a#as') kind a' = Q':r'p'fs' cs = c'#cs'
    c'  get_return_edges a'
  have "valid_path_rev_aux cs ((a#as')@[a'])"
    by(simp only:valid_path_rev_aux.simps,clarsimp)
  thus ?case by simp
qed


(*<*)
lemmas append_Cons_rev = append_Cons[THEN sym]
declare append_Cons [simp del] append_Cons_rev [simp]
(*>*)

lemma upd_rev_cs_Cons_intra:
  assumes "intra_kind(kind a)" shows "upd_rev_cs cs (a#as) = upd_rev_cs cs as"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  from ‹intra_kind (kind a)
  have "upd_rev_cs cs ([]@[a]) = upd_rev_cs cs []"
    by(simp only:upd_rev_cs.simps,auto simp:intra_kind_def)
  thus ?case by simp
next
  case (snoc a' as')
  note IH = cs. upd_rev_cs cs (a#as') = upd_rev_cs cs as'
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    from IH have "upd_rev_cs cs (a#as') = upd_rev_cs cs as'" .
    with Intra have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
      by(fastforce simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Return
    from IH have "upd_rev_cs (a'#cs) (a#as') = upd_rev_cs (a'#cs) as'" .
    with Return have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
      by(auto simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      from IH have "upd_rev_cs [] (a#as') = upd_rev_cs [] as'" .
      with Call Nil have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    next
      case (Cons c' cs')
      from IH have "upd_rev_cs cs' (a#as') = upd_rev_cs cs' as'" .
      with Call Cons have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    qed
  qed
qed



lemma upd_rev_cs_Cons_Return:
  assumes "kind a = Qpf" shows "upd_rev_cs cs (a#as) = a#(upd_rev_cs cs as)"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  with kind a = Qpf have "upd_rev_cs cs ([]@[a]) = a#(upd_rev_cs cs [])"
    by(simp only:upd_rev_cs.simps) clarsimp
  thus ?case by simp
next
  case (snoc a' as')
  note IH = cs. upd_rev_cs cs (a#as') = a#upd_rev_cs cs as'
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    from IH have "upd_rev_cs cs (a#as') = a#(upd_rev_cs cs as')" .
    with Intra have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
      by(fastforce simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Return
    from IH have "upd_rev_cs (a'#cs) (a#as') = a#(upd_rev_cs (a'#cs) as')" .
    with Return have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
      by(auto simp:intra_kind_def)
    thus ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      from IH have "upd_rev_cs [] (a#as') = a#(upd_rev_cs [] as')" .
      with Call Nil have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    next
      case (Cons c' cs')
      from IH have "upd_rev_cs cs' (a#as') = a#(upd_rev_cs cs' as')" .
      with Call Cons 
      have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
        by(auto simp:intra_kind_def)
      thus ?thesis by simp
    qed
  qed
qed


lemma upd_rev_cs_Cons_Call_Cons:
  assumes "kind a = Q:rpfs"
  shows "upd_rev_cs cs as = c'#cs'  upd_rev_cs cs (a#as) = cs'"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  with kind a = Q:rpfs have "upd_rev_cs cs ([]@[a]) = cs'"
    by(simp only:upd_rev_cs.simps) clarsimp
 thus ?case by simp
next
  case (snoc a' as')
  note IH = cs. upd_rev_cs cs as' = c'#cs'  upd_rev_cs cs (a#as') = cs'
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    with ‹upd_rev_cs cs (as'@[a']) = c'#cs'
    have "upd_rev_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def)
    from IH[OF this] have "upd_rev_cs cs (a#as') = cs'" .
    with Intra show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Return
    with ‹upd_rev_cs cs (as'@[a']) = c'#cs'
    have "upd_rev_cs (a'#cs) as' = c'#cs'" by simp
    from IH[OF this] have "upd_rev_cs (a'#cs) (a#as') = cs'" .
    with Return show ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      with ‹upd_rev_cs cs (as'@[a']) = c'#cs' Call
      have "upd_rev_cs cs as' = c'#cs'" by simp
      from IH[OF this] have "upd_rev_cs cs (a#as') = cs'" .
      with Nil Call show ?thesis by simp
    next
      case (Cons cx csx)
      with ‹upd_rev_cs cs (as'@[a']) = c'#cs' Call
      have "upd_rev_cs csx as' = c'#cs'" by simp
      from IH[OF this] have "upd_rev_cs csx (a#as') = cs'" .
      with Cons Call show ?thesis by simp
    qed
  qed
qed


lemma upd_rev_cs_Cons_Call_Cons_Empty:
  assumes "kind a = Q:rpfs"
  shows "upd_rev_cs cs as = []  upd_rev_cs cs (a#as) = []"
proof(induct as arbitrary:cs rule:rev_induct)
  case Nil
  with kind a = Q:rpfs have "upd_rev_cs cs ([]@[a]) = []"
    by(simp only:upd_rev_cs.simps) clarsimp
 thus ?case by simp
next
  case (snoc a' as')
  note IH = cs. upd_rev_cs cs as' = []  upd_rev_cs cs (a#as') = []
  show ?case
  proof(cases "kind a'" rule:edge_kind_cases)
    case Intra
    with ‹upd_rev_cs cs (as'@[a']) = []
    have "upd_rev_cs cs as' = []" by(fastforce simp:intra_kind_def)
    from IH[OF this] have "upd_rev_cs cs (a#as') = []" .
    with Intra show ?thesis by(fastforce simp:intra_kind_def)
  next
    case Return
    with ‹upd_rev_cs cs (as'@[a']) = []
    have "upd_rev_cs (a'#cs) as' = []" by simp
    from IH[OF this] have "upd_rev_cs (a'#cs) (a#as') = []" .
    with Return show ?thesis by simp
  next
    case Call
    show ?thesis
    proof(cases cs)
      case Nil
      with ‹upd_rev_cs cs (as'@[a']) = [] Call
      have "upd_rev_cs cs as' = []" by simp
      from IH[OF this] have "upd_rev_cs cs (a#as') = []" .
      with Nil Call show ?thesis by simp
    next
      case (Cons cx csx)
      with ‹upd_rev_cs cs (as'@[a']) = [] Call
      have "upd_rev_cs csx as' = []" by simp
      from IH[OF this] have "upd_rev_cs csx (a#as') = []" .
      with Cons Call show ?thesis by simp
    qed
  qed
qed

(*<*)declare append_Cons [simp] append_Cons_rev [simp del](*>*)


definition valid_call_list :: "'edge list  'node  bool"
  where "valid_call_list cs n 
  cs' c cs''. cs = cs'@c#cs''  (valid_edge c  (Q r p fs. (kind c = Q:rpfs)  
                    p = get_proc (case cs' of []  n | _  last (sourcenodes cs'))))"

definition valid_return_list :: "'edge list  'node  bool"
  where "valid_return_list cs n 
  cs' c cs''. cs = cs'@c#cs''  (valid_edge c  (Q p f. (kind c = Qpf)  
                    p = get_proc (case cs' of []  n | _  last (targetnodes cs'))))"


lemma valid_call_list_valid_edges: 
  assumes "valid_call_list cs n" shows "c  set cs. valid_edge c"
proof -
  from ‹valid_call_list cs n 
  have "cs' c cs''. cs = cs'@c#cs''  valid_edge c"
    by(simp add:valid_call_list_def)
  thus ?thesis
  proof(induct cs)
    case Nil thus ?case by simp
  next
    case (Cons cx csx)
    note IH = cs' c cs''. csx = cs'@c#cs''  valid_edge c 
                            aset csx. valid_edge a
    from cs' c cs''. cx#csx = cs'@c#cs''  valid_edge c
    have "valid_edge cx" by blast
    from cs' c cs''. cx#csx = cs'@c#cs''  valid_edge c
    have "cs' c cs''. csx = cs'@c#cs''  valid_edge c"
      by auto(erule_tac x="cx#cs'" in allE,auto)
    from IH[OF this] valid_edge cx show ?case by simp
  qed
qed


lemma valid_return_list_valid_edges: 
  assumes "valid_return_list rs n" shows "r  set rs. valid_edge r"
proof -
  from ‹valid_return_list rs n 
  have "rs' r rs''. rs = rs'@r#rs''  valid_edge r"
    by(simp add:valid_return_list_def)
  thus ?thesis
  proof(induct rs)
    case Nil thus ?case by simp
  next
    case (Cons rx rsx)
    note IH = rs' r rs''. rsx = rs'@r#rs''  valid_edge r 
                            aset rsx. valid_edge a
    from rs' r rs''. rx#rsx = rs'@r#rs''  valid_edge r
    have "valid_edge rx" by blast
    from rs' r rs''. rx#rsx = rs'@r#rs''  valid_edge r
    have "rs' r rs''. rsx = rs'@r#rs''  valid_edge r"
      by auto(erule_tac x="rx#rs'" in allE,auto)
    from IH[OF this] valid_edge rx show ?case by simp
  qed
qed


lemma vpra_empty_valid_call_list_rev:
  "valid_call_list cs n  valid_path_rev_aux [] (rev cs)"
proof(induct cs arbitrary:n)
  case Nil thus ?case by simp
next
  case (Cons c' cs')
  note IH = n. valid_call_list cs' n  valid_path_rev_aux [] (rev cs')
  from ‹valid_call_list (c'#cs') n 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 clarsimp
    by(case_tac cs',auto simp:sourcenodes_def)
  from IH[OF this] have "valid_path_rev_aux [] (rev cs')" .
  moreover
  from ‹valid_call_list (c'#cs') n obtain Q r p fs where "kind c' = Q:rpfs"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE) fastforce
  ultimately show ?case by simp
qed


lemma vpa_upd_cs_cases:
  "valid_path_aux cs as; valid_call_list cs n; n -as→* n'
   case (upd_cs cs as) of []  (c  set cs. a  set as. a  get_return_edges c)
                      | cx#csx  valid_call_list (cx#csx) n'"
proof(induct arbitrary:n rule:vpa_induct)
  case (vpa_empty cs)
  from n -[]→* n' have "n = n'" by fastforce
  with ‹valid_call_list cs n show ?case by(cases cs) auto
next
  case (vpa_intra cs a' as')
  note IH = n. valid_call_list cs n; n -as'→* n'
     case (upd_cs cs as') of []  cset cs. aset as'. a  get_return_edges c
                         | cx#csx  valid_call_list (cx # csx) n'
  from ‹intra_kind (kind a') have "upd_cs cs (a'#as') = upd_cs cs as'"
    by(fastforce simp:intra_kind_def)
  from n -a'#as'→* n' have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  from valid_edge a' ‹intra_kind (kind a')
  have "get_proc (sourcenode a') = get_proc (targetnode a')" by(rule get_proc_intra)
  with ‹valid_call_list cs n have "valid_call_list cs (targetnode a')"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cs'" in allE) apply clarsimp
    by(case_tac cs') auto
  from IH[OF this targetnode a' -as'→* n'] ‹upd_cs cs (a'#as') = upd_cs cs as'
  show ?case by(cases "upd_cs cs as'") auto
next
  case (vpa_Call cs a' as' Q r p fs)
  note IH = n. valid_call_list (a'#cs) n; n -as'→* n'
     case (upd_cs (a'#cs) as') 
             of []  cset (a'#cs). aset as'. a  get_return_edges c
          | cx#csx  valid_call_list (cx # csx) n'
  from kind a' = Q:rpfs have "upd_cs (a'#cs) as' = upd_cs cs (a'#as')"
    by simp
  from n -a'#as'→* n' have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  from valid_edge a' kind a' = Q:rpfs
  have "get_proc (targetnode a') = p" by(rule get_proc_call)
  with valid_edge a' kind a' = Q:rpfs ‹valid_call_list cs 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 clarsimp
    by(case_tac list,auto simp:sourcenodes_def)
  from IH[OF this targetnode a' -as'→* n'] 
    ‹upd_cs (a'#cs) as' = upd_cs cs (a'#as')
  have "case upd_cs cs (a'#as') 
         of []  cset (a' # cs). aset as'. a  get_return_edges c
    | cx # csx  valid_call_list (cx # csx) n'" by simp
  thus ?case by(cases "upd_cs cs (a'#as')") simp+
next
  case (vpa_ReturnEmpty cs a' as' Q p f)
  note IH = n. valid_call_list [] n; n -as'→* n'
     case (upd_cs [] as') 
             of []  cset []. aset as'. a  get_return_edges c
          | cx#csx  valid_call_list (cx # csx) n'
  from kind a' = Qpf cs = [] have "upd_cs [] as' = upd_cs cs (a'#as')"
    by simp
  from n -a'#as'→* n' have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  have "valid_call_list [] (targetnode a')" by(simp add:valid_call_list_def)
  from IH[OF this targetnode a' -as'→* n']
    ‹upd_cs [] as' = upd_cs cs (a'#as')
  have "case (upd_cs cs (a'#as')) 
         of []  cset []. aset as'. a  get_return_edges c
    | cx#csx  valid_call_list (cx#csx) n'" by simp
  with cs = [] show ?case by(cases "upd_cs cs (a'#as')") simp+
next
  case (vpa_ReturnCons cs a' as' Q p f c' cs')
  note IH = n. valid_call_list cs' n; n -as'→* n'
     case (upd_cs cs' as') 
             of []  cset cs'. aset as'. a  get_return_edges c
          | cx#csx  valid_call_list (cx # csx) n'
  from kind a' = Qpf cs = c'#cs' a'  get_return_edges c' 
  have "upd_cs cs' as' = upd_cs cs (a'#as')" by simp
  from n -a'#as'→* n' have [simp]:"n = sourcenode a'" and "valid_edge a'"
    and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
  from ‹valid_call_list cs n cs = c'#cs' have "valid_edge c'"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE,auto)
  with a'  get_return_edges c' obtain ax where "valid_edge ax"
    and sources:"sourcenode ax = sourcenode c'" 
    and targets:"targetnode ax = targetnode a'" and "kind ax = (λcf. False)"
    by(fastforce dest:call_return_node_edge)
  from valid_edge ax sources[THEN sym] targets[THEN sym] kind ax = (λcf. False)
  have "get_proc (sourcenode c') = get_proc (targetnode a')"
    by(fastforce intro:get_proc_intra simp:intra_kind_def)
  with ‹valid_call_list cs n cs = c'#cs'
  have "valid_call_list cs' (targetnode a')"
    apply(clarsimp simp:valid_call_list_def)
    apply(hypsubst_thin)
    apply(erule_tac x="c'#cs'" in allE)
    by(case_tac cs',auto simp:sourcenodes_def)
  from IH[OF this targetnode a' -as'→* n'] 
    ‹upd_cs cs' as' = upd_cs cs (a'#as')
  have "case (upd_cs cs (a'#as')) 
         of []  cset cs'. aset as'. a  get_return_edges c
    | cx#csx  valid_call_list (cx#csx) n'" by simp
  with cs = c' # cs' a'  get_return_edges c' show ?case
    by(cases "upd_cs cs (a'#as')") simp+
qed


lemma vpa_valid_call_list_valid_return_list_vpra:
  "valid_path_aux cs cs'; valid_call_list cs n; valid_return_list cs' n'
   valid_path_rev_aux cs' (rev cs)"
proof(induct arbitrary:n n' rule:vpa_induct)
  case (vpa_empty cs)
  from ‹valid_call_list cs n show ?case by(rule vpra_empty_valid_call_list_rev)
next
  case (vpa_intra cs a as)
  from ‹intra_kind (kind a) ‹valid_return_list (a#as) n'
  have False apply(clarsimp simp:valid_return_list_def)
    by(erule_tac x="[]" in allE,clarsimp simp:intra_kind_def)
  thus ?case by simp
next
  case (vpa_Call cs a as Q r p fs)
  from kind a = Q:rpfs ‹valid_return_list (a#as) n'
  have False apply(clarsimp simp:valid_return_list_def)
    by(erule_tac x="[]" in allE,clarsimp)
  thus ?case by simp
next
  case (vpa_ReturnEmpty cs a as Q p f)
  from cs = [] show ?case by simp
next
  case (vpa_ReturnCons cs a as Q p f c' cs')
  note IH = n n'. valid_call_list cs' n; valid_return_list as n'
     valid_path_rev_aux as (rev cs')
  from ‹valid_return_list (a#as) n' have "valid_return_list as (targetnode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="a#cs'" in allE)
    by(case_tac cs',auto simp:targetnodes_def)
  from ‹valid_call_list cs n cs = c'#cs'
  have "valid_call_list cs' (sourcenode c')"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="c'#cs'" in allE)
    by(case_tac cs',auto simp:sourcenodes_def)
  from ‹valid_call_list cs n cs = c'#cs' have "valid_edge c'"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE,auto)
  with a  get_return_edges c' obtain Q' r' p' f' where "kind c' = Q':r'p'f'"
    apply(cases "kind c'" rule:edge_kind_cases)
    by(auto dest:only_call_get_return_edges simp:intra_kind_def)
  from IH[OF ‹valid_call_list cs' (sourcenode c')
    ‹valid_return_list as (targetnode a)]
  have "valid_path_rev_aux as (rev cs')" .
  with kind a = Qpf cs = c'#cs' a  get_return_edges c' kind c' = Q':r'p'f'
  show ?case by simp
qed
 


lemma vpa_to_vpra:
  "valid_path_aux cs as; valid_path_aux (upd_cs cs as) cs'; 
    n -as→* n'; valid_call_list cs n; valid_return_list cs' n'' 
   valid_path_rev_aux cs' as  valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)"
proof(induct arbitrary:n rule:vpa_induct)
  case vpa_empty thus ?case
    by(fastforce intro:vpa_valid_call_list_valid_return_list_vpra)
next
  case (vpa_intra cs a as)
  note IH = n. valid_path_aux (upd_cs cs as) cs'; n -as→* n';
    valid_call_list cs n; valid_return_list cs' n''
     valid_path_rev_aux cs' as 
       valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)
  from n -a#as→* n' have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from valid_edge a ‹intra_kind (kind a)
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with ‹valid_call_list cs n n = sourcenode a
  have "valid_call_list cs (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cs'" in allE) apply clarsimp
    by(case_tac cs') auto
  from ‹valid_path_aux (upd_cs cs (a#as)) cs' ‹intra_kind (kind a)
  have "valid_path_aux (upd_cs cs as) cs'"
    by(fastforce simp:intra_kind_def)
  from IH[OF this targetnode a -as→* n' ‹valid_call_list cs (targetnode a)
    ‹valid_return_list cs' n'']
  have "valid_path_rev_aux cs' as" 
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)" by simp_all
  from  ‹intra_kind (kind a) ‹valid_path_rev_aux cs' as
  have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_intra)
  from ‹intra_kind (kind a) have "upd_rev_cs cs' (a#as) = upd_rev_cs cs' as"
    by(simp add:upd_rev_cs_Cons_intra)
  with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)
  have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
  with ‹valid_path_rev_aux cs' (a#as) show ?case by simp
next
  case (vpa_Call cs a as Q r p fs)
  note IH = n. valid_path_aux (upd_cs (a#cs) as) cs'; n -as→* n';
    valid_call_list (a#cs) n; valid_return_list cs' n''
     valid_path_rev_aux cs' as 
       valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))
  from n -a#as→* n' have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from valid_edge a kind a = Q:rpfs have "p = get_proc (targetnode a)"
    by(rule get_proc_call[THEN sym])
  from ‹valid_call_list cs n n = sourcenode a
  have "valid_call_list cs (sourcenode a)" by simp
  with kind a = Q:rpfs valid_edge a p = get_proc (targetnode a)
  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 clarsimp
    by(case_tac list,auto simp:sourcenodes_def)
  from kind a = Q:rpfs have "upd_cs cs (a#as) = upd_cs (a#cs) as"
    by simp
  with ‹valid_path_aux (upd_cs cs (a#as)) cs'
  have "valid_path_aux (upd_cs (a#cs) as) cs'" by simp
  from IH[OF this targetnode a -as→* n' ‹valid_call_list (a#cs) (targetnode a)
    ‹valid_return_list cs' n'']
  have "valid_path_rev_aux cs' as"
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))" by simp_all
  show ?case
  proof(cases "upd_rev_cs cs' as")
    case Nil
    with kind a = Q:rpfs
    have "upd_rev_cs cs' (a#as) = []" by(rule upd_rev_cs_Cons_Call_Cons_Empty)
    with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs)) kind a = Q:rpfs Nil
    have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
    from Nil kind a = Q:rpfs have "valid_path_rev_aux (upd_rev_cs cs' as) ([]@[a])"
      by(simp only:valid_path_rev_aux.simps) clarsimp
    with ‹valid_path_rev_aux cs' as have "valid_path_rev_aux cs' ([a]@as)"
      by(fastforce intro:valid_path_rev_aux_Append)
    with ‹valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)
    show ?thesis by simp
  next
    case (Cons cx csx)
    with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs)) kind a = Q:rpfs
    have match:"cx  get_return_edges a" "valid_path_rev_aux csx (rev cs)" by auto
    from kind a = Q:rpfs Cons have "upd_rev_cs cs' (a#as) = csx"
      by(rule upd_rev_cs_Cons_Call_Cons)
    with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev(a#cs)) kind a = Q:rpfs match
    have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
    from Cons kind a = Q:rpfs match
    have "valid_path_rev_aux (upd_rev_cs cs' as) ([]@[a])"
      by(simp only:valid_path_rev_aux.simps) clarsimp
    with ‹valid_path_rev_aux cs' as have "valid_path_rev_aux cs' ([a]@as)"
      by(fastforce intro:valid_path_rev_aux_Append)
    with ‹valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)
    show ?thesis by simp
  qed
next
  case (vpa_ReturnEmpty cs a as Q p f)
  note IH = n. valid_path_aux (upd_cs [] as) cs'; n -as→* n';
    valid_call_list [] n; valid_return_list cs' n''
     valid_path_rev_aux cs' as 
       valid_path_rev_aux (upd_rev_cs cs' as) (rev [])
  from n -a#as→* n' have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from cs = [] kind a = Qpf have "upd_cs cs (a#as) = upd_cs [] as"
    by simp
  with ‹valid_path_aux (upd_cs cs (a#as)) cs'
  have "valid_path_aux (upd_cs [] as) cs'" by simp
  from IH[OF this targetnode a -as→* n' _ ‹valid_return_list cs' n'']
  have "valid_path_rev_aux cs' as" 
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev [])" 
    by(auto simp:valid_call_list_def)
  from kind a = Qpf ‹valid_path_rev_aux cs' as
  have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_Return)
  moreover
  from cs = [] have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)"
    by simp
  ultimately show ?case by simp
next
  case (vpa_ReturnCons cs a as Q p f cx csx)
  note IH = n. valid_path_aux (upd_cs csx as) cs'; n -as→* n';
    valid_call_list csx n; valid_return_list cs' n''
     valid_path_rev_aux cs' as 
       valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)
  note match = cs = cx#csx a  get_return_edges cx
  from n -a#as→* n' have "n = sourcenode a" and "valid_edge a"
    and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
  from cs = cx#csx ‹valid_call_list cs n have "valid_edge cx"
    apply(clarsimp simp:valid_call_list_def)
    by(erule_tac x="[]" in allE) clarsimp
  with match have "get_proc (sourcenode cx) = get_proc (targetnode a)"
    by(fastforce intro:get_proc_get_return_edge)
  with ‹valid_call_list cs n cs = cx#csx
  have "valid_call_list csx (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cx#cs'" in allE) apply clarsimp
    by(case_tac cs',auto simp:sourcenodes_def)
  from kind a = Qpf match have "upd_cs cs (a#as) = upd_cs csx as" by simp
  with ‹valid_path_aux (upd_cs cs (a#as)) cs'
  have "valid_path_aux (upd_cs csx as) cs'" by simp
  from IH[OF this targetnode a -as→* n' ‹valid_call_list csx (targetnode a)
    ‹valid_return_list cs' n'']
  have "valid_path_rev_aux cs' as" 
    and "valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)" by simp_all
  from kind a = Qpf ‹valid_path_rev_aux cs' as
  have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_Return)
  from match valid_edge cx obtain Q' r' p' f' where "kind cx = Q':r'p'f'"
    by(fastforce dest!:only_call_get_return_edges)
  from kind a = Qpf have "upd_rev_cs cs' (a#as) = a#(upd_rev_cs cs' as)"
    by(rule upd_rev_cs_Cons_Return)
  with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev csx) kind a = Qpf 
    kind cx = Q':r'p'f' match
  have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)"
    by simp
  with ‹valid_path_rev_aux cs' (a#as) show ?case by simp
qed


lemma vp_to_vpra:
  "n -as* n'  valid_path_rev_aux [] as"
by(fastforce elim:vpa_to_vpra[THEN conjunct1] 
            simp:vp_def valid_path_def valid_call_list_def valid_return_list_def)




subsubsection ‹Same level paths›


fun same_level_path_aux :: "'edge list  'edge list  bool"
  where "same_level_path_aux cs []  True"
  | "same_level_path_aux cs (a#as)  
       (case (kind a) of Q:rpfs  same_level_path_aux (a#cs) as
                       | Qpf  case cs of []  False
                                     | c'#cs'  a  get_return_edges c' 
                                             same_level_path_aux cs' as
                       |    _  same_level_path_aux cs as)"


lemma slpa_induct [consumes 1,case_names slpa_empty slpa_intra slpa_Call 
  slpa_Return]:
  assumes major: "same_level_path_aux xs ys"
  and rules: "cs. P cs []"
    "cs a as. intra_kind(kind a); same_level_path_aux cs as; P cs as 
       P cs (a#as)"
    "cs a as Q r p fs. kind a = Q:rpfs; same_level_path_aux (a#cs) as; P (a#cs) as 
       P cs (a#as)"
    "cs a as Q p f c' cs'. kind a = Qpf; cs = c'#cs'; same_level_path_aux cs' as;
                             a  get_return_edges c'; P cs' as
      P cs (a#as)"
  shows "P xs ys"
using major
apply(induct ys arbitrary: xs)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)


lemma slpa_cases [consumes 4,case_names intra_path return_intra_path]:
  assumes "same_level_path_aux cs as" and "upd_cs cs as = []"
  and "c  set cs. valid_edge c" and "a  set as. valid_edge a"
  obtains "a  set as. intra_kind(kind a)"
  | asx a asx' Q p f c' cs' where "as = asx@a#asx'" and "same_level_path_aux cs asx"
    and "kind a = Qpf" and "upd_cs cs asx = c'#cs'" and "upd_cs cs (asx@[a]) = []" 
    and "a  get_return_edges c'" and "valid_edge c'"
    and "a  set asx'. intra_kind(kind a)"
proof(atomize_elim)
  from assms
  show "(aset as. intra_kind (kind a)) 
    (asx a asx' Q p f c' cs'. as = asx@a#asx'  same_level_path_aux cs asx 
       kind a = Qpf  upd_cs cs asx = c'#cs'  upd_cs cs (asx@[a]) = []  
       a  get_return_edges c'  valid_edge c'  (aset asx'. intra_kind (kind a)))"
  proof(induct rule:slpa_induct)
    case (slpa_empty cs)
    have "aset []. intra_kind (kind a)" by simp
    thus ?case by simp
  next
    case (slpa_intra cs a as)
    note IH = upd_cs cs as = []; cset cs. valid_edge c; a'set as. valid_edge a' 
       (aset as. intra_kind (kind a)) 
      (asx a asx' Q p f c' cs'. as = asx@a#asx'  same_level_path_aux cs asx 
        kind a = Qpf   upd_cs cs asx = c' # cs'  upd_cs cs (asx@[a]) = []  
        a  get_return_edges c'  valid_edge c'  (aset asx'. intra_kind (kind a)))
    from a'set (a#as). valid_edge a' have "a'set as. valid_edge a'" by simp
    from ‹intra_kind (kind a) ‹upd_cs cs (a#as) = []
    have "upd_cs cs as = []" by(fastforce simp:intra_kind_def)
    from IH[OF this cset cs. valid_edge c a'set as. valid_edge a'] show ?case
    proof
      assume "aset as. intra_kind (kind a)"
      with ‹intra_kind (kind a) have "a'set (a#as). intra_kind (kind a')"
        by simp
      thus ?case by simp
    next
      assume "asx a asx' Q p f c' cs'. as = asx@a#asx'  same_level_path_aux cs asx 
                kind a = Qpf  upd_cs cs asx = c'#cs'  upd_cs cs (asx@[a]) = []  
                a  get_return_edges c'  valid_edge c'  
                (aset asx'. intra_kind (kind a))"
      then obtain asx a' Q p f asx' c' cs' where "as = asx@a'#asx'" 
        and "same_level_path_aux cs asx" and "upd_cs cs (asx@[a']) = []"
        and "upd_cs cs asx = c'#cs'" and assms:"a'  get_return_edges c'"
        "kind a' = Qpf" "valid_edge c'" "aset asx'. intra_kind (kind a)"
        by blast
      from as = asx@a'#asx' have "a#as = (a#asx)@a'#asx'" by simp
      moreover
      from ‹intra_kind (kind a) ‹same_level_path_aux cs asx
      have "same_level_path_aux cs (a#asx)" by(fastforce simp:intra_kind_def)
      moreover
      from ‹upd_cs cs asx = c'#cs' ‹intra_kind (kind a)
      have "upd_cs cs (a#asx) = c'#cs'" by(fastforce simp:intra_kind_def)
      moreover
      from ‹upd_cs cs (asx@[a']) = [] ‹intra_kind (kind a)
      have "upd_cs cs ((a#asx)@[a']) = []" by(fastforce simp:intra_kind_def)
      ultimately show ?case using assms by blast
    qed
  next
    case (slpa_Call cs a as Q r p fs)
    note IH = upd_cs (a#cs) as = []; cset (a#cs). valid_edge c;
      a'set as. valid_edge a'  
      (a'set as. intra_kind (kind a')) 
      (asx a' asx' Q' p' f' c' cs'. as = asx@a'#asx'  
        same_level_path_aux (a#cs) asx  kind a' = Q'p'f'  
        upd_cs (a#cs) asx = c'#cs'  upd_cs (a#cs) (asx@[a']) = []  
        a'  get_return_edges c'  valid_edge c'  
        (a'set asx'. intra_kind (kind a')))
    from a'set (a#as). valid_edge a' have "valid_edge a" 
      and "a'set as. valid_edge a'" by simp_all
    from cset cs. valid_edge c valid_edge a have "cset (a#cs). valid_edge c"
      by simp
    from ‹upd_cs cs (a#as) = [] kind a = Q:rpfs
    have "upd_cs (a#cs) as = []" by simp
    from IH[OF this cset (a#cs). valid_edge c a'set as. valid_edge a']
    show ?case
    proof
      assume "a'set as. intra_kind (kind a')"
      with kind a = Q:rpfs have "upd_cs cs (a#as) = a#cs"
        by(fastforce intro:upd_cs_intra_path)
      with ‹upd_cs cs (a#as) = [] have False by simp
      thus ?case by simp
    next
      assume "asx a' asx' Q p f c' cs'. as = asx@a'#asx'  
                same_level_path_aux (a#cs) asx  kind a' = Qpf  
                upd_cs (a#cs) asx = c'#cs'  upd_cs (a#cs) (asx@[a']) = []  
                a'  get_return_edges c'  valid_edge c'  
                (aset asx'. intra_kind (kind a))"
      then obtain asx a' Q' p' f' asx' c' cs' where "as = asx@a'#asx'" 
        and "same_level_path_aux (a#cs) asx" and "upd_cs (a#cs) (asx@[a']) = []"
        and "upd_cs (a#cs) asx = c'#cs'" and assms:"a'  get_return_edges c'"
        "kind a' = Q'p'f'" "valid_edge c'" "aset asx'. intra_kind (kind a)"
        by blast
      from as = asx@a'#asx' have "a#as = (a#asx)@a'#asx'" by simp
      moreover
      from kind a = Q:rpfs ‹same_level_path_aux (a#cs) asx
      have "same_level_path_aux cs (a#asx)" by simp
      moreover
      from kind a = Q:rpfs ‹upd_cs (a#cs) asx = c'#cs'
      have "upd_cs cs (a#asx) = c'#cs'" by simp
      moreover
      from kind a = Q:rpfs ‹upd_cs (a#cs) (asx@[a']) = []
      have "upd_cs cs ((a#asx)@[a']) = []" by simp
      ultimately show ?case using assms by blast
    qed
  next
    case (slpa_Return cs a as Q p f c' cs')
    note IH = upd_cs cs' as = []; cset cs'. valid_edge c; 
      a'set as. valid_edge a'  
      (a'set as. intra_kind (kind a')) 
      (asx a' asx' Q' p' f' c'' cs''. as = asx@a'#asx'  
        same_level_path_aux cs' asx  kind a' = Q'p'f'  upd_cs cs' asx = c''#cs'' 
        upd_cs cs' (asx@[a']) = []  a'  get_return_edges c''  valid_edge c''  
        (a'set asx'. intra_kind (kind a')))
    from a'set (a#as). valid_edge a' have "valid_edge a" 
      and "a'set as. valid_edge a'" by simp_all
    from cset cs. valid_edge c cs = c' # cs'
    have "valid_edge c'" and "cset cs'. valid_edge c" by simp_all
    from ‹upd_cs cs (a#as) = [] kind a = Qpf cs = c'#cs' 
      a  get_return_edges c' have "upd_cs cs' as = []" by simp
    from IH[OF this cset cs'. valid_edge c a'set as. valid_edge a'] show ?case
    proof
      assume "a'set as. intra_kind (kind a')"
      hence "upd_cs cs' as = cs'" by(rule upd_cs_intra_path)
      with ‹upd_cs cs' as = [] have "cs' = []" by simp
      with cs = c'#cs' a  get_return_edges c' kind a = Qpf
      have "upd_cs cs [a] = []" by simp
      moreover
      from cs = c'#cs' have "upd_cs cs []  []" by simp
      moreover
      have "same_level_path_aux cs []" by simp
      ultimately show ?case 
        using kind a = Qpf a'set as. intra_kind (kind a') cs = c'#cs'
          a  get_return_edges c' valid_edge c'
        by fastforce
    next
      assume "asx a' asx' Q' p' f' c'' cs''. as = asx@a'#asx' 
        same_level_path_aux cs' asx  kind a' = Q'p'f'  upd_cs cs' asx = c''#cs'' 
        upd_cs cs' (asx@[a']) = []  a'  get_return_edges c''  valid_edge c'' 
        (a'set asx'. intra_kind (kind a'))"
      then obtain asx a' asx' Q' p' f' c'' cs'' where "as = asx@a'#asx'"
        and "same_level_path_aux cs' asx" and "upd_cs cs' asx = c''#cs''" 
        and "upd_cs cs' (asx@[a']) = []" and assms:"a'  get_return_edges c''" 
        "kind a' = Q'p'f'" "valid_edge c''" "a'set asx'. intra_kind (kind a')"
        by blast
      from as = asx@a'#asx' have "a#as = (a#asx)@a'#asx'" by simp
      moreover
      from ‹same_level_path_aux cs' asx cs = c'#cs' a  get_return_edges c'
        kind a = Qpf
      have "same_level_path_aux cs (a#asx)" by simp
      moreover
      from ‹upd_cs cs' asx = c''#cs'' kind a = Qpf cs = c'#cs'
      have "upd_cs cs (a#asx) = c''#cs''" by simp
      moreover
      from ‹upd_cs cs' (asx@[a']) = [] cs = c'#cs' a  get_return_edges c'
        kind a = Qpf
      have "upd_cs cs ((a#asx)@[a']) = []" by simp
      ultimately show ?case using assms by blast
    qed
  qed
qed


lemma same_level_path_aux_valid_path_aux: 
  "same_level_path_aux cs as  valid_path_aux cs as"
by(induct rule:slpa_induct,auto split:edge_kind.split simp:intra_kind_def)


lemma same_level_path_aux_Append:
  "same_level_path_aux cs as; same_level_path_aux (upd_cs cs as) as'
   same_level_path_aux cs (as@as')"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma same_level_path_aux_callstack_Append:
  "same_level_path_aux cs as  same_level_path_aux (cs@cs') as"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma same_level_path_upd_cs_callstack_Append:
  "same_level_path_aux cs as; upd_cs cs as = cs' 
   upd_cs (cs@cs'') as = (cs'@cs'')"
by(induct rule:slpa_induct,auto split:edge_kind.split simp:intra_kind_def)


lemma slpa_split:
  assumes "same_level_path_aux cs as" and "as = xs@ys" and "upd_cs cs xs = []"
  shows "same_level_path_aux cs xs" and "same_level_path_aux [] ys"
using assms
proof(induct arbitrary:xs ys rule:slpa_induct)
  case (slpa_empty cs) case 1
  from [] = xs@ys show ?case by simp
next
  case (slpa_empty cs) case 2
  from [] = xs@ys show ?case by simp
next
  case (slpa_intra cs a as)
  note IH1 = xs ys. as = xs@ys; upd_cs cs xs = []  same_level_path_aux cs xs
  note IH2 = xs ys. as = xs@ys; upd_cs cs xs = []  same_level_path_aux [] ys
  { case 1
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with a#as = xs@ys have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = [] Cons ‹intra_kind (kind a)
      have "upd_cs cs xs' = []" by(fastforce simp:intra_kind_def)
      from IH1[OF as = xs'@ys this] have "same_level_path_aux cs xs'" .
      with a = x' ‹intra_kind (kind a) Cons
      show ?thesis by(fastforce simp:intra_kind_def)
    qed
  next
    case 2
    show ?case
    proof(cases xs)
      case Nil
      with ‹upd_cs cs xs = [] have "cs = []" by fastforce
      with Nil a#as = xs@ys ‹same_level_path_aux cs as ‹intra_kind (kind a)
      show ?thesis by(cases ys,auto simp:intra_kind_def)
    next
      case (Cons x' xs')
      with a#as = xs@ys have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = [] Cons ‹intra_kind (kind a)
      have "upd_cs cs xs' = []" by(fastforce simp:intra_kind_def)
      from IH2[OF as = xs'@ys this] show ?thesis .
    qed
  }
next
  case (slpa_Call cs a as Q r p fs)
  note IH1 = xs ys. as = xs@ys; upd_cs (a#cs) xs = [] 
     same_level_path_aux (a#cs) xs
  note IH2 = xs ys. as = xs@ys; upd_cs (a#cs) xs = [] 
     same_level_path_aux [] ys
  { case 1
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with a#as = xs@ys have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = [] Cons kind a = Q:rpfs
      have "upd_cs (a#cs) xs' = []" by simp
      from IH1[OF as = xs'@ys this] have "same_level_path_aux (a#cs) xs'" .
      with a = x' kind a = Q:rpfs Cons show ?thesis by simp
    qed
  next
    case 2
    show ?case
    proof(cases xs)
      case Nil
      with ‹upd_cs cs xs = [] have "cs = []" by fastforce
      with Nil a#as = xs@ys ‹same_level_path_aux (a#cs) as kind a = Q:rpfs
      show ?thesis by(cases ys) auto
    next
      case (Cons x' xs')
      with a#as = xs@ys have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = [] Cons kind a = Q:rpfs
      have "upd_cs (a#cs) xs' = []" by simp
      from IH2[OF as = xs'@ys this] show ?thesis .
    qed
  }
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH1 = xs ys. as = xs@ys; upd_cs cs' xs = []  same_level_path_aux cs' xs
  note IH2 = xs ys. as = xs@ys; upd_cs cs' xs = []  same_level_path_aux [] ys
  { case 1
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
    next
      case (Cons x' xs')
      with a#as = xs@ys have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = [] Cons kind a = Qpf cs = c'#cs'
      have "upd_cs cs' xs' = []" by simp
      from IH1[OF as = xs'@ys this] have "same_level_path_aux cs' xs'" .
      with a = x' kind a = Qpf cs = c'#cs' a  get_return_edges c' Cons 
      show ?thesis by simp
    qed
  next
    case 2
    show ?case
    proof(cases xs)
      case Nil
      with ‹upd_cs cs xs = [] have "cs = []" by fastforce 
      with cs = c'#cs' have False by simp
      thus ?thesis by simp
    next
      case (Cons x' xs')
      with a#as = xs@ys have "a = x'" and "as = xs'@ys" by simp_all
      with ‹upd_cs cs xs = [] Cons kind a = Qpf cs = c'#cs'
      have "upd_cs cs' xs' = []" by simp
      from IH2[OF as = xs'@ys this] show ?thesis .
    qed
  }
qed


lemma slpa_number_Calls_eq_number_Returns:
  "same_level_path_aux cs as; upd_cs cs as = []; 
    a  set as. valid_edge a; c  set cs. valid_edge c
   length [aas@cs. Q r p fs. kind a = Q:rpfs] = 
     length [aas. Q p f. kind a = Qpf]"
apply(induct rule:slpa_induct)
by(auto split:list.split edge_kind.split intro:only_call_get_return_edges 
         simp:intra_kind_def)


lemma slpa_get_proc:
  "same_level_path_aux cs as; upd_cs cs as = []; n -as→* n'; 
    c  set cs. valid_edge c
   (if cs = [] then get_proc n else get_proc(last(sourcenodes cs))) = get_proc n'"
proof(induct arbitrary:n rule:slpa_induct)
  case slpa_empty thus ?case by fastforce
next
  case (slpa_intra cs a as)
  note IH = n. upd_cs cs as = []; n -as→* n'; aset cs. valid_edge a
     (if cs = [] then get_proc n else get_proc (last (sourcenodes cs))) = 
        get_proc n'
  from ‹intra_kind (kind a) ‹upd_cs cs (a#as) = []
  have "upd_cs cs as = []" by(cases "kind a",auto simp:intra_kind_def)
  from n -a#as→* n' have "n -[]@a#as→* n'" by simp
  hence "valid_edge a" and "n = sourcenode a" and "targetnode a -as→* n'"
    by(fastforce dest:path_split)+
  from valid_edge a ‹intra_kind (kind a) n = sourcenode a
  have "get_proc n = get_proc (targetnode a)"
    by(fastforce intro:get_proc_intra)
  from IH[OF ‹upd_cs cs as = [] targetnode a -as→* n' aset cs. valid_edge a]
  have "(if cs = [] then get_proc (targetnode a) 
         else get_proc (last (sourcenodes cs))) = get_proc n'" .
  with get_proc n = get_proc (targetnode a) show ?case by auto
next
  case (slpa_Call cs a as Q r p fs)
  note IH = n. upd_cs (a#cs) as = []; n -as→* n'; aset (a#cs). valid_edge a
     (if a#cs = [] then get_proc n else get_proc (last (sourcenodes (a#cs)))) = 
        get_proc n'
  from kind a = Q:rpfs ‹upd_cs cs (a#as) = []
  have "upd_cs (a#cs) as = []" by simp
  from n -a#as→* n' have "n -[]@a#as→* n'" by simp
  hence "valid_edge a" and "n = sourcenode a" and "targetnode a -as→* n'"
    by(fastforce dest:path_split)+
  from valid_edge a aset cs. valid_edge a have "aset (a#cs). valid_edge a"
    by simp
  from IH[OF ‹upd_cs (a#cs) as = [] targetnode a -as→* n' this]
  have "get_proc (last (sourcenodes (a#cs))) = get_proc n'" by simp
  with n = sourcenode a show ?case by(cases cs,auto simp:sourcenodes_def)
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = n. upd_cs cs' as = []; n -as→* n'; aset cs'. valid_edge a
     (if cs' = [] then get_proc n else get_proc (last (sourcenodes cs'))) = 
       get_proc n'
  from aset cs. valid_edge a cs = c'#cs'
  have "valid_edge c'" and "aset cs'. valid_edge a" by simp_all
  from kind a = Qpf ‹upd_cs cs (a#as) = [] cs = c'#cs'
  have "upd_cs cs' as = []" by simp
  from n -a#as→* n' have "n -[]@a#as→* n'" by simp
  hence "n = sourcenode a" and "targetnode a -as→* n'"
    by(fastforce dest:path_split)+
  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)
  from IH[OF ‹upd_cs cs' as = [] targetnode a -as→* n' aset cs'. valid_edge a]
  have "(if cs' = [] then get_proc (targetnode a) 
         else get_proc (last (sourcenodes cs'))) = get_proc n'" .
  with cs = c'#cs' get_proc (sourcenode c') = get_proc (targetnode a)
  show ?case by(auto simp:sourcenodes_def)
qed


lemma slpa_get_return_edges:
  "same_level_path_aux cs as; cs  []; upd_cs cs as = [];
  xs ys. as = xs@ys  ys  []  upd_cs cs xs  []
   last as  get_return_edges (last cs)"
proof(induct rule:slpa_induct)
  case (slpa_empty cs)
  from cs  [] ‹upd_cs cs [] = [] have False by fastforce
  thus ?case by simp
next
  case (slpa_intra cs a as)
  note IH = cs  []; upd_cs cs as = []; 
              xs ys. as = xs@ys  ys  []  upd_cs cs xs  []
     last as  get_return_edges (last cs)
  show ?case
  proof(cases "as = []")
    case True
    with ‹intra_kind (kind a) ‹upd_cs cs (a#as) = [] have "cs = []"
      by(fastforce simp:intra_kind_def)
    with cs  [] have False by simp
    thus ?thesis by simp
  next
    case False
    from ‹intra_kind (kind a) ‹upd_cs cs (a#as) = [] have "upd_cs cs as = []"
      by(fastforce simp:intra_kind_def)
    from xs ys. a#as = xs@ys  ys  []  upd_cs cs xs  [] ‹intra_kind (kind a)
    have "xs ys. as = xs@ys  ys  []  upd_cs cs xs  []"
      apply(clarsimp,erule_tac x="a#xs" in allE)
      by(auto simp:intra_kind_def)
    from IH[OF cs  [] ‹upd_cs cs as = [] this] 
    have "last as  get_return_edges (last cs)" .
    with False show ?thesis by simp
  qed
next
  case (slpa_Call cs a as Q r p fs)
  note IH = a#cs  []; upd_cs (a#cs) as = [];
    xs ys. as = xs@ys  ys  []  upd_cs (a#cs) xs  []
     last as  get_return_edges (last (a#cs))
  show ?case
  proof(cases "as = []")
    case True
    with kind a = Q:rpfs ‹upd_cs cs (a#as) = [] have "a#cs = []" by simp
    thus ?thesis by simp
  next
    case False
    from kind a = Q:rpfs ‹upd_cs cs (a#as) = [] have "upd_cs (a#cs) as = []"
      by simp
    from xs ys. a#as = xs@ys  ys  []  upd_cs cs xs  [] kind a = Q:rpfs
    have "xs ys. as = xs@ys  ys  []  upd_cs (a#cs) xs  []"
      by(clarsimp,erule_tac x="a#xs" in allE,simp)
    from IH[OF _ ‹upd_cs (a#cs) as = [] this] 
    have "last as  get_return_edges (last (a#cs))" by simp
    with False cs  [] show ?thesis by(simp add:targetnodes_def)
  qed
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = cs'  []; upd_cs cs' as = []; 
    xs ys. as = xs@ys  ys  []  upd_cs cs' xs  []
     last as  get_return_edges (last cs')
  show ?case
  proof(cases "as = []")
    case True
    with kind a = Qpf cs = c'#cs' ‹upd_cs cs (a#as) = []
    have "cs' = []" by simp
    with cs = c'#cs' a  get_return_edges c' True
    show ?thesis by simp
  next
    case False
    from kind a = Qpf cs = c'#cs' ‹upd_cs cs (a#as) = []
    have "upd_cs cs' as = []" by simp
    show ?thesis
    proof(cases "cs' = []")
      case True
      with cs = c'#cs' kind a = Qpf have "upd_cs cs [a] = []" by simp
      with xs ys. a#as = xs@ys  ys  []  upd_cs cs xs  [] False have False
        apply(erule_tac x="[a]" in allE) by fastforce
      thus ?thesis by simp
    next
      case False
      from xs ys. a#as = xs@ys  ys  []  upd_cs cs xs  []
        kind a = Qpf cs = c'#cs'
      have "xs ys. as = xs@ys  ys  []  upd_cs cs' xs  []"
        by(clarsimp,erule_tac x="a#xs" in allE,simp)
      from IH[OF False ‹upd_cs cs' as = [] this]
      have "last as  get_return_edges (last cs')" .
      with as  [] False cs = c'#cs' show ?thesis by(simp add:targetnodes_def)
    qed
  qed
qed


lemma slpa_callstack_length:
  assumes "same_level_path_aux cs as" and "length cs = length cfsx"
  obtains cfx cfsx' where "transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs"
  and "transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs'"
  and "length cfsx' = length (upd_cs cs as)"
proof(atomize_elim)
  from assms show "cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs 
    transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' 
    length cfsx' = length (upd_cs cs as)"
  proof(induct arbitrary:cfsx cf rule:slpa_induct)
    case (slpa_empty cs) thus ?case by(simp add:kinds_def)
  next
    case (slpa_intra cs a as)
    note IH = cfsx cf. length cs = length cfsx 
      cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs 
                  transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' 
                  length cfsx' = length (upd_cs cs as)
    from ‹intra_kind (kind a) 
    have "length (upd_cs cs (a#as)) = length (upd_cs cs as)"
      by(fastforce simp:intra_kind_def)
    show ?case
    proof(cases cfsx)
      case Nil
      with ‹length cs = length cfsx have "length cs = length []" by simp
      from Nil ‹intra_kind (kind a) 
      obtain cfx where transfer:"transfer (kind a) (cfsx@cf#cfs) = []@cfx#cfs"
        "transfer (kind a) (cfsx@cf#cfs') = []@cfx#cfs'"
        by(cases "kind a",auto simp:kinds_def intra_kind_def)
      from IH[OF ‹length cs = length []] obtain cfsx' cfx' 
        where "transfers (kinds as) ([]@cfx#cfs) = cfsx'@cfx'#cfs"
        and "transfers (kinds as) ([]@cfx#cfs') = cfsx'@cfx'#cfs'"
        and "length cfsx' = length (upd_cs cs as)" by blast
      with ‹length (upd_cs cs (a#as)) = length (upd_cs cs as) transfer
      show ?thesis by(fastforce simp:kinds_def)
    next
      case (Cons x xs)
      with ‹intra_kind (kind a) obtain cfx' 
        where transfer:"transfer (kind a) (cfsx@cf#cfs) = (cfx'#xs)@cf#cfs"
        "transfer (kind a) (cfsx@cf#cfs') = (cfx'#xs)@cf#cfs'"
        by(cases "kind a",auto simp:kinds_def intra_kind_def)
      from ‹length cs = length cfsx Cons have "length cs = length (cfx'#xs)"
        by simp
      from IH[OF this] obtain cfs'' cf''
        where "transfers (kinds as) ((cfx'#xs)@cf#cfs) = cfs''@cf''#cfs"
        and "transfers (kinds as) ((cfx'#xs)@cf#cfs') = cfs''@cf''#cfs'"
        and "length cfs'' = length (upd_cs cs as)" by blast
      with ‹length (upd_cs cs (a#as)) = length (upd_cs cs as) transfer
      show ?thesis by(fastforce simp:kinds_def)
    qed
  next
    case (slpa_Call cs a as Q r p fs)
    note IH = cfsx cf. length (a#cs) = length cfsx 
      cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs 
                  transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' 
                  length cfsx' = length (upd_cs (a#cs) as)
    from kind a = Q:rpfs
    obtain cfx where transfer:"transfer (kind a) (cfsx@cf#cfs) = (cfx#cfsx)@cf#cfs"
      "transfer (kind a) (cfsx@cf#cfs') = (cfx#cfsx)@cf#cfs'"
      by(cases cfsx) auto
    from ‹length cs = length cfsx have "length (a#cs) = length (cfx#cfsx)"
      by simp
    from IH[OF this] obtain cfsx' cfx' 
      where "transfers (kinds as) ((cfx#cfsx)@cf#cfs) = cfsx'@cfx'#cfs"
      and "transfers (kinds as) ((cfx#cfsx)@cf#cfs') = cfsx'@cfx'#cfs'"
      and "length cfsx' = length (upd_cs (a#cs) as)" by blast
    with kind a = Q:rpfs transfer show ?case by(fastforce simp:kinds_def)
  next
     case (slpa_Return cs a as Q p f c' cs')
     note IH = cfsx cf. length cs' = length cfsx 
       cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs 
                   transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' 
                   length cfsx' = length (upd_cs cs' as)
     from kind a = Qpf cs = c'#cs'
     have "length (upd_cs cs (a#as)) = length (upd_cs cs' as)" by simp
     show ?case
     proof(cases cs')
       case Nil
       with cs = c'#cs' ‹length cs = length cfsx obtain cfx
         where [simp]:"cfsx = [cfx]" by(cases cfsx) auto
       with kind a = Qpf obtain cf' 
         where transfer:"transfer (kind a) (cfsx@cf#cfs) = []@cf'#cfs"
         "transfer (kind a) (cfsx@cf#cfs') = []@cf'#cfs'"
         by fastforce
       from Nil have "length cs' = length []" by simp
       from IH[OF this] obtain cfsx' cfx' 
         where "transfers (kinds as) ([]@cf'#cfs) = cfsx'@cfx'#cfs"
         and "transfers (kinds as) ([]@cf'#cfs') = cfsx'@cfx'#cfs'"
         and "length cfsx' = length (upd_cs cs' as)" by blast
       with ‹length (upd_cs cs (a#as)) = length (upd_cs cs' as) transfer
       show ?thesis by(fastforce simp:kinds_def)
    next
      case (Cons cx csx)
      with cs = c'#cs' ‹length cs = length cfsx obtain x x' xs
        where [simp]:"cfsx = x#x'#xs" and "length xs = length csx"
        by(cases cfsx,auto,case_tac list,fastforce+)
      with kind a = Qpf obtain cf' 
        where transfer:"transfer (kind a) ((x#x'#xs)@cf#cfs) = (cf'#xs)@cf#cfs"
        "transfer (kind a) ((x#x'#xs)@cf#cfs') = (cf'#xs)@cf#cfs'"
        by fastforce
      from cs = c'#cs' ‹length cs = length cfsx have "length cs' = length (cf'#xs)"
        by simp
      from IH[OF this] obtain cfsx' cfx 
        where "transfers (kinds as) ((cf'#xs)@cf#cfs) = cfsx'@cfx#cfs"
        and "transfers (kinds as) ((cf'#xs)@cf#cfs') = cfsx'@cfx#cfs'"
        and "length cfsx' = length (upd_cs cs' as)" by blast
      with ‹length (upd_cs cs (a#as)) = length (upd_cs cs' as) transfer
      show ?thesis by(fastforce simp:kinds_def)
    qed
  qed
qed


lemma slpa_snoc_intra:
  "same_level_path_aux cs as; intra_kind (kind a) 
   same_level_path_aux cs (as@[a])"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma slpa_snoc_Call:
  "same_level_path_aux cs as; kind a = Q:rpfs
   same_level_path_aux cs (as@[a])"
by(induct rule:slpa_induct,auto simp:intra_kind_def)


lemma vpa_Main_slpa:
  "valid_path_aux cs as; m -as→* m'; as  []; 
    valid_call_list cs m; get_proc m' = Main;
    get_proc (case cs of []  m | _  sourcenode (last cs)) = Main
   same_level_path_aux cs as  upd_cs cs as = []"
proof(induct arbitrary:m rule:vpa_induct)
  case (vpa_empty cs) thus ?case by simp
next
  case (vpa_intra cs a as)
  note IH = m. m -as→* m'; as  []; valid_call_list cs m; get_proc m' = Main;
    get_proc (case cs of []  m | a # list  sourcenode (last cs)) = Main
     same_level_path_aux cs as  upd_cs cs as = []
  from m -a # as→* m' have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from valid_edge a ‹intra_kind (kind a) 
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  show ?case
  proof(cases "as = []")
    case True
    with targetnode a -as→* m' have "targetnode a = m'" by fastforce
    with get_proc (sourcenode a) = get_proc (targetnode a) 
      sourcenode a = m get_proc m' = Main
    have "get_proc m = Main" by simp
    have "cs = []"
    proof(cases cs)
      case Cons
      with ‹valid_call_list cs m
      obtain c Q r p fs where "valid_edge c" and "kind c = Q:rget_proc mfs"
        by(auto simp:valid_call_list_def,erule_tac x="[]" in allE,
           auto simp:sourcenodes_def)
      with get_proc m = Main have "kind c = Q:rMainfs" by simp
      with valid_edge c have False by(rule Main_no_call_target)
      thus ?thesis by simp
    qed simp
    with True ‹intra_kind (kind a) show ?thesis by(fastforce simp:intra_kind_def)
  next
    case False
    from ‹valid_call_list cs m sourcenode a = m
      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 get_proc (case cs of []  m | _  sourcenode (last cs)) = Main
      sourcenode a = m get_proc (sourcenode a) = get_proc (targetnode a)
    have "get_proc (case cs of []  targetnode a | _  sourcenode (last cs)) = Main"
      by(cases cs) auto
    from IH[OF targetnode a -as→* m' False ‹valid_call_list cs (targetnode a)
      get_proc m' = Main this]
    have "same_level_path_aux cs as  upd_cs cs as = []" .
    with ‹intra_kind (kind a) show ?thesis by(fastforce simp:intra_kind_def)
  qed
next
  case (vpa_Call cs a as Q r p fs)
  note IH = m. m -as→* m'; as  []; valid_call_list (a # cs) m; 
    get_proc m' = Main; 
    get_proc (case a # cs of []  m | _  sourcenode (last (a # cs))) = Main
     same_level_path_aux (a # cs) as  upd_cs (a # cs) as = []
  from m -a # as→* m' have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from valid_edge a kind a = Q:rpfs have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  show ?case
  proof(cases "as = []")
    case True
    with targetnode a -as→* m' have "targetnode a = m'" by fastforce
    with get_proc (targetnode a) = p get_proc m' = Main kind a = Q:rpfs
    have "kind a = Q:rMainfs" by simp
    with valid_edge a have False by(rule Main_no_call_target)
    thus ?thesis by simp
  next
    case False
    from get_proc (targetnode a) = p ‹valid_call_list cs m valid_edge a
      kind a = Q:rpfs sourcenode a = m
    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)
      by(case_tac list)(auto simp:sourcenodes_def)
    from get_proc (case cs of []  m | _  sourcenode (last cs)) = Main
      sourcenode a = m
    have "get_proc (case a # cs of []  targetnode a 
      | _  sourcenode (last (a # cs))) = Main"
      by(cases cs) auto
    from IH[OF targetnode a -as→* m' False ‹valid_call_list (a#cs) (targetnode a)
      get_proc m' = Main this]
    have "same_level_path_aux (a # cs) as  upd_cs (a # cs) as = []" .
    with kind a = Q:rpfs show ?thesis by simp
  qed
next
  case (vpa_ReturnEmpty cs a as Q p f)
  note IH = m. m -as→* m'; as  []; valid_call_list [] m; get_proc m' = Main;
    get_proc (case [] of []  m | a # list  sourcenode (last [])) = Main
     same_level_path_aux [] as  upd_cs [] as = []
  from m -a # as→* m' have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from valid_edge a kind a = Qpf have "get_proc (sourcenode a) = p" 
    by(rule get_proc_return)
  from get_proc (case cs of []  m | a # list  sourcenode (last cs)) = Main
    cs = []
  have "get_proc m = Main" by simp
  with sourcenode a = m get_proc (sourcenode a) = p have "p = Main" by simp
  with kind a = Qpf have "kind a = QMainf" by simp
  with valid_edge a have False by(rule Main_no_return_source)
  thus ?case by simp
next
  case (vpa_ReturnCons cs a as Q p f c' cs')
  note IH = m. m -as→* m'; as  []; valid_call_list cs' m; get_proc m' = Main;
    get_proc (case cs' of []  m | a # list  sourcenode (last cs')) = Main
     same_level_path_aux cs' as  upd_cs cs' as = []
  from m -a # as→* m' have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
  from valid_edge a kind a = Qpf have "get_proc (sourcenode a) = p" 
    by(rule get_proc_return)
  from ‹valid_call_list cs m cs = c' # cs'
  have "valid_edge c'" 
    by(auto simp:valid_call_list_def,erule_tac x="[]" in allE,auto)
  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)
  show ?case
  proof(cases "as = []")
    case True
    with targetnode a -as→* m' have "targetnode a = m'" by fastforce
    with get_proc m' = Main have "get_proc (targetnode a) = Main" by simp
    from get_proc (sourcenode c') = get_proc (targetnode a)
      get_proc (targetnode a) = Main
    have "get_proc (sourcenode c') = Main" by simp
    have "cs' = []"
    proof(cases cs')
      case (Cons cx csx)
      with cs = c' # cs' ‹valid_call_list cs m
      obtain Qx rx fsx where "valid_edge cx" 
        and "kind cx = Qx:rxget_proc (sourcenode c')fsx"
        by(auto simp:valid_call_list_def,erule_tac x="[c']" in allE,
           auto simp:sourcenodes_def)
      with get_proc (sourcenode c') = Main have "kind cx = Qx:rxMainfsx" by simp
      with valid_edge cx have False by(rule Main_no_call_target)
      thus ?thesis by simp
    qed simp
    with True cs = c' # cs' a  get_return_edges c' kind a = Qpf
    show ?thesis by simp
  next
    case False
    from ‹valid_call_list cs m cs = c' # cs'
      get_proc (sourcenode c') = get_proc (targetnode a)
    have "valid_call_list cs' (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c' # cs'" in allE)
      by(case_tac cs')(auto simp:sourcenodes_def)
    from get_proc (case cs of []  m | a # list  sourcenode (last cs)) = Main
      cs = c' # cs' get_proc (sourcenode c') = get_proc (targetnode a)
    have "get_proc (case cs' of []  targetnode a 
      | _  sourcenode (last cs')) = Main"
      by(cases cs') auto
    from IH[OF targetnode a -as→* m' False ‹valid_call_list cs' (targetnode a)
      get_proc m' = Main this]
    have "same_level_path_aux cs' as  upd_cs cs' as = []" .
    with kind a = Qpf cs = c' # cs' a  get_return_edges c'
    show ?thesis by simp
  qed
qed



definition same_level_path :: "'edge list  bool"
  where "same_level_path as  same_level_path_aux [] as  upd_cs [] as = []"


lemma same_level_path_valid_path:
  "same_level_path as  valid_path as"
by(fastforce intro:same_level_path_aux_valid_path_aux
             simp:same_level_path_def valid_path_def)


lemma same_level_path_Append:
  "same_level_path as; same_level_path as'  same_level_path (as@as')"
by(fastforce elim:same_level_path_aux_Append upd_cs_Append simp:same_level_path_def)


lemma same_level_path_number_Calls_eq_number_Returns:
  "same_level_path as; a  set as. valid_edge a  
  length [