Theory WeakSimulation

section ‹The weak simulation›

theory WeakSimulation imports Slice begin

context SDG begin

lemma call_node_notin_slice_return_node_neither:
  assumes "call_of_return_node n n'" and "n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
  shows "n ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof -
  from ‹call_of_return_node n n'› obtain a a' where "return_node n"
    and "valid_edge a" and "n' = sourcenode a"
    and "valid_edge a'" and "a' ∈ get_return_edges a" 
    and "n = targetnode a'" by(fastforce simp:call_of_return_node_def)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q p r fs 
    where "kind a = Q:r↪⇘p⇙fs" by(fastforce dest!:only_call_get_return_edges)
  with ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
    by(fastforce dest!:call_return_edges)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
  have "CFG_node (sourcenode a) s-p→⇘sum⇙ CFG_node (targetnode a')"
    by(fastforce intro:sum_SDG_call_summary_edge)
  show ?thesis
  proof
    assume "n ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹n = targetnode a'› have "CFG_node (targetnode a') ∈ HRB_slice S"
      by(simp add:SDG_to_CFG_set_def)
    hence "CFG_node (sourcenode a) ∈ HRB_slice S"
    proof(induct "CFG_node (targetnode a')" rule:HRB_slice_cases)
      case (phase1 nx)
      with ‹CFG_node (sourcenode a) s-p→⇘sum⇙ CFG_node (targetnode a')›
      show ?case by(fastforce intro:combine_SDG_slices.combSlice_refl sum_slice1 
                              simp:HRB_slice_def)
    next
      case (phase2 nx n' n'' p')
      from ‹CFG_node (targetnode a') ∈ sum_SDG_slice2 n'› 
        ‹CFG_node (sourcenode a) s-p→⇘sum⇙ CFG_node (targetnode a')› ‹valid_edge a›
      have "CFG_node (sourcenode a) ∈ sum_SDG_slice2 n'"
        by(fastforce intro:sum_slice2)
      with ‹n' ∈ sum_SDG_slice1 nx› ‹n'' s-p'→⇘ret⇙ CFG_node (parent_node n')› ‹nx ∈ S›
      show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
                              simp:HRB_slice_def)
    qed
    with ‹n' ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹n' = sourcenode a› show False 
      by(simp add:SDG_to_CFG_set_def HRB_slice_def)
  qed
qed


lemma edge_obs_intra_slice_eq:
assumes "valid_edge a" and "intra_kind (kind a)" and "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
  shows "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = 
         obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
proof -
  from assms have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
                   obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
    by(rule edge_obs_intra_subset)
  from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
  { fix x assume "x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
    and "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
    have "∃as. targetnode a -as→⇩ι* x"
    proof(cases "method_exit x")
      case True
      from ‹valid_edge a› have "valid_node (targetnode a)" by simp
      then obtain asx where "targetnode a -asx→⇩√* (_Exit_)" 
        by(fastforce dest:Exit_path)
      then obtain as pex where "targetnode a -as→⇩ι* pex" and "method_exit pex"
        by -(erule valid_Exit_path_intra_path)
      hence "get_proc pex = get_proc (targetnode a)"
        by -(rule intra_path_get_procs[THEN sym])
      also from ‹valid_edge a› ‹intra_kind (kind a)› 
      have "… = get_proc (sourcenode a)"
        by -(rule get_proc_intra[THEN sym])
      also from ‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› True
      have "… = get_proc x"
        by(fastforce elim:obs_intraE intro:intra_path_get_procs)
      finally have "pex = x" using ‹method_exit pex› True
        by -(rule method_exit_unique)
      with ‹targetnode a -as→⇩ι* pex› show ?thesis by fastforce
    next
      case False
      with ‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
      have "x postdominates (sourcenode a)" by(rule obs_intra_postdominate)
      with ‹valid_edge a› ‹intra_kind (kind a)› ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
        ‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
      have "x postdominates (targetnode a)"
        by(fastforce elim:postdominate_inner_path_targetnode path_edge obs_intraE 
                    simp:intra_path_def sourcenodes_def)
      thus ?thesis by(fastforce elim:postdominate_implies_inner_path)
    qed
    then obtain as where "targetnode a -as→⇩ι* x" by blast
    from ‹x ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
    have "x ∈ ⌊HRB_slice S⌋⇘CFG⇙" by -(erule obs_intraE)
    have "∃x' ∈ ⌊HRB_slice S⌋⇘CFG⇙. ∃as'. targetnode a -as'→⇩ι* x' ∧ 
      (∀a' ∈ set (sourcenodes as'). a' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
    proof(cases "∃a' ∈ set (sourcenodes as). a' ∈ ⌊HRB_slice S⌋⇘CFG⇙")
      case True
      then obtain zs z zs' where "sourcenodes as = zs@z#zs'"
        and "z ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "∀z' ∈ set zs. z' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
        by(erule split_list_first_propE)
      then obtain ys y ys'
        where "sourcenodes ys = zs" and "as = ys@y#ys'"
        and "sourcenode y = z"
        by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
      from ‹targetnode a -as→⇩ι* x› ‹as = ys@y#ys'›
      have "targetnode a -ys@y#ys'→* x" and "∀y' ∈ set ys. intra_kind (kind y')"
        by(simp_all add:intra_path_def)
      from ‹targetnode a -ys@y#ys'→* x› have "targetnode a -ys→* sourcenode y"
        by(rule path_split)
      with ‹∀y' ∈ set ys. intra_kind (kind y')› ‹sourcenode y = z›
        ‹∀z' ∈ set zs. z' ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹z ∈ ⌊HRB_slice S⌋⇘CFG⇙›
        ‹sourcenodes ys = zs›
      show ?thesis by(fastforce simp:intra_path_def)
    next
      case False
      with ‹targetnode a -as→⇩ι* x› ‹x ∈ ⌊HRB_slice S⌋⇘CFG⇙›
      show ?thesis by fastforce
    qed
    hence "∃y. y ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
      by(fastforce intro:obs_intra_elem)
    with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}› 
    have False by simp }
  with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆
        obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹valid_node (sourcenode a)›
  show ?thesis by(cases "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}") 
                 (auto dest!:obs_intra_singleton_disj)
qed


lemma intra_edge_obs_slice:
  assumes "ms ≠ []" and "ms'' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a" 
  and "intra_kind (kind a)" 
  and disj:"(∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ 
                               m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
  and "hd ms = sourcenode a" and "ms' = targetnode a#tl ms" 
  and "∀n ∈ set (tl ms'). return_node n"
  shows "ms'' ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙"
proof -
  from ‹ms'' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙› ‹∀n ∈ set (tl ms'). return_node n›
  obtain msx m msx' mx m' where "ms' = msx@m#msx'" and "ms'' = mx#msx'"
    and "mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
    and "∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    and imp:"∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
    ⟶ (∃x'' ∈ set (xs'@[m]). ∃mx. call_of_return_node x'' mx ∧ 
                                   mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
    by(erule obsE)
  show ?thesis
  proof(cases msx)
    case Nil
    with ‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
      disj ‹ms' = msx@m#msx'› ‹hd ms = sourcenode a› ‹ms' = targetnode a#tl ms›
    have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by(cases ms) auto
    from ‹ms' = msx@m#msx'› ‹ms' = targetnode a#tl ms› Nil 
    have "m = targetnode a" by simp
    with ‹valid_edge a› ‹intra_kind (kind a)› ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
      ‹mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
    have "mx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
      by(fastforce dest:edge_obs_intra_subset)
    from ‹ms' = msx@m#msx'› Nil ‹ms' = targetnode a # tl ms› 
      ‹hd ms = sourcenode a› ‹ms ≠ []›
    have "ms = []@sourcenode a#msx'" by(cases ms) auto
    with ‹ms'' = mx#msx'› ‹mx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›  
      ‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙› Nil
    show ?thesis by(fastforce intro!:obsI)
  next
    case (Cons x xs)
    with ‹ms' = msx@m#msx'› ‹ms' = targetnode a # tl ms›
    have "msx = targetnode a#xs" by simp
    from Cons ‹ms' = msx@m#msx'› ‹ms' = targetnode a # tl ms› ‹hd ms = sourcenode a›
    have "ms = (sourcenode a#xs)@m#msx'" by(cases ms) auto
    from disj ‹ms = (sourcenode a#xs)@m#msx'› 
      ‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    have disj2:"(∃m ∈ set (xs@[m]). ∃m'. call_of_return_node m m' ∧ 
                            m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
      by fastforce
    hence "∀zs z zs'. sourcenode a#xs = zs@z#zs' ∧ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
      ⟶ (∃z'' ∈ set (zs'@[m]). ∃mx. call_of_return_node z'' mx ∧ 
                                   mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
    proof(cases "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙")
      case True
      with ‹hd ms = sourcenode a› have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
      with ‹valid_edge a› ‹intra_kind (kind a)›
      have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = 
        obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
        by(rule edge_obs_intra_slice_eq)
      with imp ‹msx = targetnode a#xs› show ?thesis
        by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
    next
      case False
      with ‹hd ms = sourcenode a› ‹valid_edge a› 
      have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
        by(fastforce intro!:n_in_obs_intra)
      from False disj2 
      have "∃m ∈ set (xs@[m]). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
        by simp
      with imp ‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}›
        ‹msx = targetnode a#xs› show ?thesis
        by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
    qed
    with ‹ms' = msx@m#msx'› ‹ms' = targetnode a # tl ms› ‹hd ms = sourcenode a›
      ‹ms'' = mx#msx'› ‹mx ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› 
      ‹∀nx ∈ set msx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
      ‹ms = (sourcenode a#xs)@m#msx'›
    show ?thesis by(simp del:obs.simps)(rule obsI,auto)
  qed
qed



subsection ‹Silent moves›

inductive silent_move :: 
  "'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒ 
  (('var ⇀ 'val) × 'ret) list ⇒ 'edge ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
("_,_ ⊢ '(_,_') -_→⇩τ '(_,_')" [51,50,0,0,50,0,0] 51) 

where silent_move_intra:
  "⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
    (∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
    hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
    length s' = length s; length ms = length s;
    hd ms = sourcenode a; ms' = (targetnode a)#tl ms⟧  
  ⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"

  | silent_move_call:
  "⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘p⇙fs; 
    valid_edge a'; a' ∈ get_return_edges a;
    (∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
    hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙; ∀m ∈ set (tl ms). return_node m;
    length ms = length s; length s' = Suc(length s); 
    hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms⟧  
  ⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"

  | silent_move_return:
  "⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q↩⇘p⇙f'; 
    ∃m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙;
    ∀m ∈ set (tl ms). return_node m; length ms = length s; length s = Suc(length s');
    s' ≠ []; hd ms = sourcenode a; hd(tl ms) = targetnode a; ms' = tl ms⟧  
  ⟹ S,f ⊢ (ms,s) -a→⇩τ (ms',s')"


lemma silent_move_valid_nodes:
  "⟦S,f ⊢ (ms,s) -a→⇩τ (ms',s'); ∀m ∈ set ms'. valid_node m⟧
  ⟹ ∀m ∈ set ms. valid_node m"
by(induct rule:silent_move.induct)(case_tac ms,auto)+


lemma silent_move_return_node:
  "S,f ⊢ (ms,s) -a→⇩τ (ms',s') ⟹ ∀m ∈ set (tl ms'). return_node m"
proof(induct rule:silent_move.induct)
  case (silent_move_intra f a s s' ms n⇩c ms')
  thus ?case by simp
next
  case (silent_move_call f a s s' Q r p fs a' ms n⇩c ms')
  from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
  have "return_node (targetnode a')" by(fastforce simp:return_node_def)
  with ‹∀m∈set (tl ms). return_node m› ‹ms' = targetnode a # targetnode a' # tl ms›
  show ?case by simp
next
  case (silent_move_return f a s s' Q p f' ms n⇩c ms')
  thus ?case by(cases "tl ms") auto
qed


lemma silent_move_equal_length:
  assumes "S,f ⊢ (ms,s) -a→⇩τ (ms',s')" 
  shows "length ms = length s" and "length ms' = length s'"
proof -
  from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
  have "length ms = length s ∧ length ms' = length s'"
  proof(induct rule:silent_move.induct)
    case (silent_move_intra f a s s' ms n⇩c ms')
    from ‹pred (f a) s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
    from ‹length ms = length s› ‹ms' = targetnode a # tl ms›
      ‹length s' = length s› show ?case by simp
  next
    case (silent_move_call f a s s' Q r p fs a' ms n⇩c ms')
    from ‹pred (f a) s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
    from ‹length ms = length s› ‹length s' = Suc (length s)› 
      ‹ms' = targetnode a # targetnode a' # tl ms› show ?case by simp
  next
    case (silent_move_return f a s s' Q p f' ms n⇩c ms')
    from ‹length ms = length s› ‹length s = Suc (length s')› ‹ms' = tl ms› ‹s' ≠ []›
    show ?case by simp
  qed
  thus "length ms = length s" and "length ms' = length s'" by simp_all
qed


lemma silent_move_obs_slice:
  "⟦S,kind ⊢ (ms,s) -a→⇩τ (ms',s'); msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙; 
    ∀n ∈ set (tl ms'). return_node n⟧
  ⟹ msx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct S f≡"kind" ms s a ms' s' rule:silent_move.induct)
  case (silent_move_intra a s s' ms n⇩c ms')
  from ‹pred (kind a) s› ‹length ms = length s› have "ms ≠ []"
    by(cases s) auto
  with silent_move_intra show ?case by -(rule intra_edge_obs_slice)
next
  case (silent_move_call a s s' Q r p fs a' ms S ms')
  note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ 
    m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
  from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
  have "return_node (targetnode a')" by(fastforce simp:return_node_def)
  with ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹valid_edge a'›
  have "call_of_return_node (targetnode a') (sourcenode a)"
    by(simp add:call_of_return_node_def) blast
  from ‹pred (kind a) s› ‹length ms = length s›
  have "ms ≠ []" by(cases s) auto
  from disj
  show ?case
  proof
    assume "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹hd ms = sourcenode a› have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
    with ‹call_of_return_node (targetnode a') (sourcenode a)›
      ‹ms' = targetnode a # targetnode a' # tl ms›
    have "∃n' ∈ set (tl ms'). ∃nx. call_of_return_node n' nx ∧ nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
      by fastforce
    with ‹msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙› ‹ms' = targetnode a # targetnode a' # tl ms›
    have "msx ∈ obs (targetnode a' # tl ms) ⌊HRB_slice S⌋⇘CFG⇙" by simp
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    obtain a'' where "valid_edge a''" and [simp]:"sourcenode a'' = sourcenode a"
      and [simp]:"targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
      by -(drule call_return_node_edge,auto simp:intra_kind_def)
    from ‹∀m∈set (tl ms'). return_node m› ‹ms' = targetnode a # targetnode a' # tl ms›
    have "∀m∈set (tl ms). return_node m" by simp
    with ‹ms ≠ []› ‹msx ∈ obs (targetnode a'#tl ms) ⌊HRB_slice S⌋⇘CFG⇙›
      ‹valid_edge a''› ‹intra_kind(kind a'')› disj
      ‹hd ms = sourcenode a›
    show ?case by -(rule intra_edge_obs_slice,fastforce+)
  next
    assume "∃m∈set (tl ms).
      ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹ms ≠ []› ‹msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙›
      ‹ms' = targetnode a # targetnode a' # tl ms›
    show ?thesis by(cases ms) auto
  qed
next
  case (silent_move_return a s s' Q p f' ms S ms')
  from ‹length ms = length s› ‹length s = Suc (length s')› ‹s' ≠ []›
  have "ms ≠ []" and "tl ms ≠ []" by(auto simp:length_Suc_conv)
  from ‹∃m∈set (tl ms).
    ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
    ‹tl ms ≠ []› ‹hd (tl ms) = targetnode a›
  have "(∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
    (∃m∈set (tl (tl ms)). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
    by(cases "tl ms") auto
  hence "obs ms ⌊HRB_slice S⌋⇘CFG⇙ = obs (tl ms) ⌊HRB_slice S⌋⇘CFG⇙"
  proof
    assume "∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    from ‹tl ms ≠ []› have "hd (tl ms) ∈ set (tl ms)" by simp
    with ‹hd (tl ms) = targetnode a› have "targetnode a ∈ set (tl ms)" by simp
    with ‹ms ≠ []› 
      ‹∃m'. call_of_return_node (targetnode a) m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
    have "∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ 
      m' ∉ ⌊HRB_slice S⌋⇘CFG⇙" by(cases ms) auto
    with ‹ms ≠ []› show ?thesis by(cases ms) auto
  next
    assume "∃m∈set (tl (tl ms)). ∃m'. call_of_return_node m m' ∧ 
      m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹ms ≠ []› ‹tl ms ≠ []› show ?thesis
      by(cases ms,auto simp:Let_def)(case_tac list,auto)+
  qed
  with ‹ms' = tl ms› ‹msx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙› show ?case by simp
qed



lemma silent_move_empty_obs_slice:
  assumes "S,f ⊢ (ms,s) -a→⇩τ (ms',s')" and "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}"
  shows "obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(rule ccontr)
  assume "obs ms ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
  then obtain xs where "xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
  from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
  have "∀m ∈ set (tl ms). return_node m"
    by(fastforce elim!:silent_move.cases simp:call_of_return_node_def)
  with ‹xs ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙›
  obtain msx m msx' m' where assms:"ms = msx@m#msx'" "xs = m'#msx'"
    "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙" 
    "∀mx ∈ set msx'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    "∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
    ⟶ (∃x'' ∈ set (xs'@[m]). ∃mx. call_of_return_node x'' mx ∧ 
                              mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
    by(erule obsE)
  from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')› ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› assms
  show False
  proof(induct rule:silent_move.induct)
    case (silent_move_intra f a s s' ms S ms')
    note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ 
      m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
    note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ 
      (∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
    note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    show False
    proof(cases msx)
      case Nil
      with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have [simp]:"m = sourcenode a"
        and "tl ms = msx'" by simp_all
      from Nil ‹ms' = targetnode a # tl ms› ‹ms = msx @ m # msx'›
      have "ms' = msx @ targetnode a # msx'" by simp
      from msx' disj ‹tl ms = msx'› ‹hd ms = sourcenode a›
      have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
      with ‹valid_edge a› ‹intra_kind (kind a)›
      have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ =
        obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by(rule edge_obs_intra_slice_eq)
      with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
      have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by simp
      from msx Nil have "∀xs x xs'. msx = xs@x#xs' ∧  
        obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ 
        (∃x''∈set (xs' @ [targetnode a]). ∃mx. call_of_return_node x'' mx ∧ 
        mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" by simp
      with ‹m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙› msx' 
        ‹ms' = msx @ targetnode a # msx'›
      have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
      with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
    next
      case (Cons y ys)
      with ‹ms = msx @ m # msx'› ‹ms' = targetnode a # tl ms› ‹hd ms = sourcenode a›
      have "ms' = targetnode a # ys @ m # msx'" and "y = sourcenode a" 
        and "tl ms = ys @ m # msx'" by simp_all
      { fix x assume "x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
        have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
        proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
          case True
          from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
          from this True 
          have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
            by(rule n_in_obs_intra)
          thus ?thesis by simp
        next
          case False
          from ‹valid_edge a› ‹intra_kind (kind a)› False
          have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = 
            obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
            by(rule edge_obs_intra_slice_eq)
          with ‹x ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙› show ?thesis
            by fastforce
        qed }
      with msx Cons ‹y = sourcenode a› 
      have "∀xs x xs'. targetnode a # ys = xs@x#xs' ∧ 
        obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ (∃x''∈set (xs' @ [m]). 
        ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
        apply clarsimp apply(case_tac xs) apply auto
        apply(erule_tac x="[]" in allE) apply clarsimp
        apply(erule_tac x="sourcenode a # list" in allE) apply auto
        done
      with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx' 
        ‹ms' = targetnode a # ys @ m # msx'›
      have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
      with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
    qed
  next
    case (silent_move_call f a s s' Q r p fs a' ms S ms')
    note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ 
      m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
    note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ 
      (∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
    note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain a'' where "valid_edge a''"
      and "sourcenode a'' = sourcenode a" and "targetnode a'' = targetnode a'"
      and "intra_kind (kind a'')" 
      by(fastforce dest:call_return_node_edge simp:intra_kind_def)
    from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
    have "call_of_return_node (targetnode a') (sourcenode a)"
      by(fastforce simp:call_of_return_node_def return_node_def)
    show False
    proof(cases msx)
      case Nil
      with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have [simp]:"m = sourcenode a"
        and "tl ms = msx'" by simp_all
      from Nil ‹ms' = targetnode a # targetnode a' # tl ms› ‹ms = msx @ m # msx'›
      have "ms' = targetnode a # targetnode a' # msx'" by simp
      from msx' disj ‹tl ms = msx'› ‹hd ms = sourcenode a›
      have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
      from ‹valid_edge a''› ‹intra_kind (kind a'')› ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
        ‹sourcenode a'' = sourcenode a› ‹targetnode a'' = targetnode a'›
      have "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ = 
         obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
        by(fastforce dest:edge_obs_intra_slice_eq)
      with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› 
      have "m' ∈ obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙" by simp
      from this msx' have "m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
        by(fastforce intro:obsI)
      from ‹call_of_return_node (targetnode a') (sourcenode a)›
        ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
      have "∃m' ∈ set (targetnode a'#msx').
        ∃mx. call_of_return_node m' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
        by fastforce
      with ‹m'#msx' ∈ obs (targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙›
      have "m'#msx' ∈ obs (targetnode a#targetnode a'#msx') ⌊HRB_slice S⌋⇘CFG⇙"
        by simp
      with ‹ms' = targetnode a # targetnode a' # msx'› ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}›
      show False by simp
    next
      case (Cons y ys)
      with ‹ms = msx @ m # msx'› ‹ms' = targetnode a # targetnode a' # tl ms› 
        ‹hd ms = sourcenode a›
      have "ms' = targetnode a # targetnode a' # ys @ m # msx'" 
        and "y = sourcenode a" and "tl ms = ys @ m # msx'" by simp_all
      show False
      proof(cases "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ 
          (∃x''∈set (targetnode a' # ys @ [m]).
          ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
        case True
        hence imp:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶
          (∃x''∈set (targetnode a' # ys @ [m]).
          ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)" .
        show False
        proof(cases "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ 
            (∃x''∈set (ys @ [m]). ∃mx. call_of_return_node x'' mx ∧ 
            mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)")
          case True
          with imp msx Cons ‹y = sourcenode a› 
          have "∀xs x xs'. targetnode a # targetnode a' # ys = xs@x#xs' ∧ 
            obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ (∃x''∈set (xs' @ [m]). 
            ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
            apply clarsimp apply(case_tac xs) apply fastforce
            apply(case_tac list) apply fastforce apply clarsimp
            apply(erule_tac x="sourcenode a # lista" in allE) apply auto
            done
          with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx' 
            ‹ms' = targetnode a # targetnode a' # ys @ m # msx'›
          have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by -(rule obsI,auto)
          with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
        next
          case False
          hence "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
            and all:"∀x''∈set (ys @ [m]). ∀mx. call_of_return_node x'' mx ⟶ 
            mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
            by fastforce+
          have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
          proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
            case True
            from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
            from this True 
            have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
              by(rule n_in_obs_intra)
            thus ?thesis by simp
          next
            case False
            with ‹sourcenode a'' = sourcenode a›
            have "sourcenode a'' ∉ ⌊HRB_slice S⌋⇘CFG⇙" by simp
            with ‹valid_edge a''› ‹intra_kind (kind a'')›
            have "obs_intra (targetnode a'') ⌊HRB_slice S⌋⇘CFG⇙ = 
              obs_intra (sourcenode a'') ⌊HRB_slice S⌋⇘CFG⇙"
              by(rule edge_obs_intra_slice_eq)
            with ‹obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}› 
              ‹sourcenode a'' = sourcenode a› ‹targetnode a'' = targetnode a'›
            show ?thesis by fastforce 
          qed
          with msx Cons ‹y = sourcenode a› all
          show False by simp blast
        qed
      next
        case False
        hence "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}"
          and all:"∀x''∈set (targetnode a' # ys @ [m]). 
          ∀mx. call_of_return_node x'' mx ⟶ mx ∈ ⌊HRB_slice S⌋⇘CFG⇙"
          by fastforce+
        with Cons ‹y = sourcenode a› msx 
        have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}" by auto blast
        from ‹call_of_return_node (targetnode a') (sourcenode a)› all
        have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
        from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
        from this ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙› 
        have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
          by(rule n_in_obs_intra)
        with ‹obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
      qed
    qed
  next
    case (silent_move_return f a s s' Q p f' ms S ms')
    note msx = ‹∀xs x xs'. msx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶ 
      (∃x''∈set (xs' @ [m]). ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
    note msx' = ‹∀mx∈set msx'. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    show False
    proof(cases msx)
      case Nil
      with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› have  "tl ms = msx'" by simp
      with ‹∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
        msx'
      show False by fastforce
    next
      case (Cons y ys)
      with ‹ms = msx @ m # msx'› ‹hd ms = sourcenode a› ‹ms' = tl ms›
      have "ms' = ys @ m # msx'" and "y = sourcenode a" by simp_all
      from msx Cons have "∀xs x xs'. ys = xs@x#xs' ∧ 
        obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {} ⟶  (∃x''∈set (xs' @ [m]). 
        ∃mx. call_of_return_node x'' mx ∧ mx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
        by auto (erule_tac x="y # xs" in allE,auto)
      with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› msx' ‹ms' = ys @ m # msx'›
      have "m'#msx' ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" by(rule obsI)
      with ‹obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
    qed
  qed
qed



inductive silent_moves :: 
  "'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒ 
  (('var ⇀ 'val) × 'ret) list ⇒ 'edge list ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
("_,_ ⊢ '(_,_') =_⇒⇩τ '(_,_')" [51,50,0,0,50,0,0] 51)

  where silent_moves_Nil: "length ms = length s ⟹ S,f ⊢ (ms,s) =[]⇒⇩τ (ms,s)"

  | silent_moves_Cons:
  "⟦S,f ⊢ (ms,s) -a→⇩τ (ms',s'); S,f ⊢ (ms',s') =as⇒⇩τ (ms'',s'')⟧ 
  ⟹ S,f ⊢ (ms,s) =a#as⇒⇩τ (ms'',s'')"


lemma silent_moves_equal_length:
  assumes "S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')" 
  shows "length ms = length s" and "length ms' = length s'"
proof -
  from ‹S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')› 
  have "length ms = length s ∧ length ms' = length s'"
  proof(induct rule:silent_moves.induct)
    case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
    from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
    have "length ms = length s" and "length ms' = length s'" 
      by(rule silent_move_equal_length)+
    with ‹length ms' = length s' ∧ length ms'' = length s''›
    show ?case by simp
  qed simp
  thus "length ms = length s" "length ms' = length s'" by simp_all
qed


lemma silent_moves_Append:
  "⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s''); S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')⟧
  ⟹ S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')"
by(induct rule:silent_moves.induct)(auto intro:silent_moves.intros)


lemma silent_moves_split:
  assumes "S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')"
  obtains ms'' s'' where "S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s'')"
  and "S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')"
proof(atomize_elim)
  from ‹S,f ⊢ (ms,s) =as@as'⇒⇩τ (ms',s')›
  show "∃ms'' s''. S,f ⊢ (ms,s) =as⇒⇩τ (ms'',s'') ∧ S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')"
  proof(induct as arbitrary:ms s)
    case Nil
    from ‹S,f ⊢ (ms,s) =[] @ as'⇒⇩τ (ms',s')› have "length ms = length s"
      by(fastforce intro:silent_moves_equal_length)
    hence "S,f ⊢ (ms,s) =[]⇒⇩τ (ms,s)" by(rule silent_moves_Nil)
    with ‹S,f ⊢ (ms,s) =[] @ as'⇒⇩τ (ms',s')› show ?case by fastforce
  next
    case (Cons ax asx)
    note IH = ‹⋀ms s. S,f ⊢ (ms,s) =asx @ as'⇒⇩τ (ms',s') ⟹
      ∃ms'' s''. S,f ⊢ (ms,s) =asx⇒⇩τ (ms'',s'') ∧ S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')›
    from ‹S,f ⊢ (ms,s) =(ax # asx) @ as'⇒⇩τ (ms',s')›
    obtain msx sx where "S,f ⊢ (ms,s) -ax→⇩τ (msx,sx)"
      and "S,f ⊢ (msx,sx) =asx @ as'⇒⇩τ (ms',s')"
      by(auto elim:silent_moves.cases)
    from IH[OF this(2)] obtain ms'' s'' where "S,f ⊢ (msx,sx) =asx⇒⇩τ (ms'',s'')"
      and "S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')" by blast
    from ‹S,f ⊢ (ms,s) -ax→⇩τ (msx,sx)› ‹S,f ⊢ (msx,sx) =asx⇒⇩τ (ms'',s'')›
    have "S,f ⊢ (ms,s) =ax#asx⇒⇩τ (ms'',s'')" by(rule silent_moves_Cons)
    with ‹S,f ⊢ (ms'',s'') =as'⇒⇩τ (ms',s')› show ?case by blast
  qed
qed


lemma valid_nodes_silent_moves:
  "⟦S,f⊢ (ms,s) =as'⇒⇩τ (ms',s'); ∀m ∈ set ms. valid_node m⟧
  ⟹ ∀m ∈ set ms'. valid_node m"
proof(induct rule:silent_moves.induct)
  case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
  note IH = ‹∀m∈set ms'. valid_node m ⟹ ∀m∈set ms''. valid_node m›
  from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')› ‹∀m∈set ms. valid_node m›
  have "∀m∈set ms'. valid_node m"
    apply - apply(erule silent_move.cases) apply auto
    by(cases ms,auto dest:get_return_edges_valid)+
  from IH[OF this] show ?case .
qed simp


lemma return_nodes_silent_moves:
  "⟦S,f ⊢ (ms,s) =as'⇒⇩τ (ms',s'); ∀m ∈ set (tl ms). return_node m⟧
  ⟹ ∀m ∈ set (tl ms'). return_node m"
by(induct rule:silent_moves.induct,auto dest:silent_move_return_node)


lemma silent_moves_intra_path:
  "⟦S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s'); ∀a ∈ set as. intra_kind(kind a)⟧
  ⟹ ms = ms' ∧ get_proc m = get_proc m'"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m
  rule:silent_moves.induct)
  case (silent_moves_Cons S f sx a msx' sx' as s'')
  thus ?case
  proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
    case (silent_move_intra f a s s' n⇩c msx')
    note IH = ‹⋀m. ⟦msx' = m # ms; ∀a∈set as. intra_kind (kind a)⟧
      ⟹ ms = ms' ∧ get_proc m = get_proc m'›
    from ‹msx' = targetnode a # tl (m # ms)›
    have "msx' = targetnode a # ms" by simp
    from ‹∀a∈set (a # as). intra_kind (kind a)› have "∀a∈set as. intra_kind (kind a)"
      by simp
    from IH[OF ‹msx' = targetnode a # ms› this]
    have "ms = ms'" and "get_proc (targetnode a) = get_proc m'" by simp_all
    moreover
    from ‹valid_edge a› ‹intra_kind (kind a)›
    have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
    moreover
    from ‹hd (m # ms) = sourcenode a› have "m = sourcenode a" by simp
    ultimately show ?case using ‹ms = ms'› by simp
  qed (auto simp:intra_kind_def)
qed simp


lemma silent_moves_nodestack_notempty: 
  "⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); ms ≠ []⟧ ⟹ ms' ≠ []"
apply(induct S f ms s as ms' s' rule:silent_moves.induct) apply auto
apply(erule silent_move.cases) apply auto
apply(case_tac "tl msa") by auto


lemma silent_moves_obs_slice:
  "⟦S,kind ⊢ (ms,s) =as⇒⇩τ (ms',s'); mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙; 
  ∀n ∈ set (tl ms'). return_node n⟧
  ⟹ mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀n ∈ set (tl ms). return_node n)"
proof(induct S f≡"kind" ms s as ms' s' rule:silent_moves.induct)
  case silent_moves_Nil thus ?case by simp
next
  case (silent_moves_Cons S ms s a ms' s' as ms'' s'')
  note IH = ‹⟦mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙; ∀m∈set (tl ms''). return_node m⟧
    ⟹ mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙ ∧ (∀m∈set (tl ms'). return_node m)›
  from IH[OF ‹mx ∈ obs ms'' ⌊HRB_slice S⌋⇘CFG⇙› ‹∀m∈set (tl ms''). return_node m›]
  have "mx ∈ obs ms' ⌊HRB_slice S⌋⇘CFG⇙" and "∀m∈set (tl ms'). return_node m"
    by simp_all
  with ‹S,kind ⊢ (ms,s) -a→⇩τ (ms',s')›
  have "mx ∈ obs ms ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce intro:silent_move_obs_slice)
  moreover
  from ‹S,kind ⊢ (ms,s) -a→⇩τ (ms',s')› have "∀m∈set (tl ms). return_node m"
    by(fastforce elim:silent_move.cases)
  ultimately show ?case by simp
qed


lemma silent_moves_empty_obs_slice:
  "⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}⟧
  ⟹ obs ms ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(induct rule:silent_moves.induct)
  case silent_moves_Nil thus ?case by simp
next
  case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
  note IH = ‹obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {} ⟹ obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}›
  from IH[OF ‹obs ms'' ⌊HRB_slice S⌋⇘CFG⇙ = {}›]
  have "obs ms' ⌊HRB_slice S⌋⇘CFG⇙ = {}" by simp
  with ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
  show ?case by -(rule silent_move_empty_obs_slice,fastforce)
qed


lemma silent_moves_preds_transfers:
  assumes "S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')"
  shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
  from ‹S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')›
  have "preds (map f as) s ∧ transfers (map f as) s = s'"
  proof(induct rule:silent_moves.induct)
    case silent_moves_Nil thus ?case by simp
  next
    case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
    from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')›
    have "pred (f a) s" and "transfer (f a) s = s'" by(auto elim:silent_move.cases)
    with ‹preds (map f as) s' ∧ transfers (map f as) s' = s''›
    show ?case by fastforce
  qed
  thus "preds (map f as) s" and "transfers (map f as) s = s'" by simp_all
qed



lemma silent_moves_intra_path_obs:
  assumes "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙" and "length s = length (m#msx')"
  and "∀m ∈ set msx'. return_node m"
  obtains as' where "S,slice_kind S ⊢ (m#msx',s) =as'⇒⇩τ (m'#msx',s)"
proof(atomize_elim)
  from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
  obtain as where "m -as→⇩ι* m'" and "m' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    by -(erule obs_intraE)
  from ‹m -as→⇩ι* m'› obtain x where "distance m m' x" and "x ≤ length as"
    by(erule every_path_distance)
  from ‹distance m m' x› ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙›
    ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
  show "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
  proof(induct x arbitrary:m s rule:nat.induct)
    fix m fix s::"(('var ⇀ 'val) × 'ret) list"
    assume "distance m m' 0" and "length s = length (m#msx')"
    then obtain as' where "m -as'→⇩ι* m'" and "length as' = 0"
      by(auto elim:distance.cases)
    hence "m -[]→⇩ι* m'" by(cases as) auto
    hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
    with ‹length s = length (m#msx')›[THEN sym]
    have "S,slice_kind S ⊢ (m#msx',s) =[]⇒⇩τ (m#msx',s)" 
      by -(rule silent_moves_Nil)
    thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by simp blast
  next
    fix x m fix s::"(('var ⇀ 'val) × 'ret) list"
    assume "distance m m' (Suc x)" and "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
      and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
      and IH:"⋀m s. ⟦distance m m' x; m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙;
                     length s = length (m#msx'); ∀m ∈ set msx'. return_node m⟧
      ⟹ ∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
    from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› have "valid_node m"
      by(rule in_obs_intra_valid)
    with ‹distance m m' (Suc x)› have "m ≠ m'"
      by(fastforce elim:distance.cases dest:empty_path simp:intra_path_def)
    have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    proof
      assume isin:"m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
        by(fastforce intro!:n_in_obs_intra)
      with ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› ‹m ≠ m'› show False by simp
    qed
    from ‹distance m m' (Suc x)› obtain a where "valid_edge a" and "m = sourcenode a"
      and "intra_kind(kind a)" and "distance (targetnode a) m' x"
      and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                               distance (targetnode a') m' x ∧
                                               valid_edge a' ∧ intra_kind (kind a') ∧ 
                                               targetnode a' = mx)"
      by -(erule distance_successor_distance,simp+)
    from ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› 
    have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
      by(rule obs_intra_singleton_element)
    with ‹valid_edge a› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹intra_kind(kind a)›
    have disj:"obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {} ∨ 
               obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m'}"
      by -(drule_tac S="⌊HRB_slice S⌋⇘CFG⇙" in edge_obs_intra_subset,auto)
    from ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› 
      ‹m = sourcenode a›
    have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
      by(cases s)
    (auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
    from ‹distance (targetnode a) m' x› obtain asx where "targetnode a -asx→⇩ι* m'" 
      and "length asx = x" and "∀as'. targetnode a -as'→⇩ι* m' ⟶ x ≤ length as'"
      by(auto elim:distance.cases)
    from ‹targetnode a -asx→⇩ι* m'› ‹m' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    obtain mx where "mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" 
      by(erule path_ex_obs_intra)
    with disj have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
    from IH[OF ‹distance (targetnode a) m' x› this length 
      ‹∀m ∈ set msx'. return_node m›]
    obtain asx' where moves:"S,slice_kind S ⊢ 
      (targetnode a#msx',transfer (slice_kind S a) s) =asx'⇒⇩τ 
      (m'#msx',transfer (slice_kind S a) s)" by blast
    have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
    proof(cases "kind a")
      fix f assume "kind a = ⇑f"
      with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› have "slice_kind S a = ⇑id"
        by(fastforce intro:slice_kind_Upd)
      with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
    next
      fix Q assume "kind a = (Q)⇩√"
      with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
        ‹m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙› ‹distance (targetnode a) m' x›
        ‹distance m m' (Suc x)› target
      have "slice_kind S a = (λs. True)⇩√"
        by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
      with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
    next
      fix Q r p fs assume "kind a = Q:r↪⇘p⇙fs"
      with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    next
      fix Q p f assume "kind a = Q↩⇘p⇙f"
      with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    qed
    hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
      by simp_all
    with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹valid_edge a›
      ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
    have "S,slice_kind S ⊢ (sourcenode a#msx',s) -a→⇩τ 
                             (targetnode a#msx',transfer (slice_kind S a) s)"
      by(fastforce intro:silent_move_intra)
    with moves ‹transfer (slice_kind S a) s = s› ‹m = sourcenode a›
    have "S,slice_kind S ⊢ (m#msx',s) =a#asx'⇒⇩τ (m'#msx',s)"
      by(fastforce intro:silent_moves_Cons)
    thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by blast
  qed
qed


lemma silent_moves_intra_path_no_obs:
  assumes "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}" and "method_exit m'"
  and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')"
  and "∀m ∈ set msx'. return_node m"
  obtains as where "S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
proof(atomize_elim)
  from ‹method_exit m'› ‹get_proc m = get_proc m'› ‹valid_node m›
  obtain as where "m -as→⇩ι* m'" by(erule intra_path_to_matching_method_exit)
  then obtain x where "distance m m' x" and "x ≤ length as"
    by(erule every_path_distance)
  from ‹distance m m' x› ‹m -as→⇩ι* m'› ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}›
    ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
  show "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
  proof(induct x arbitrary:m as s rule:nat.induct)
    fix m fix s::"(('var ⇀ 'val) × 'ret) list"
    assume "distance m m' 0" and "length s = length (m#msx')"
    then obtain as' where "m -as'→⇩ι* m'" and "length as' = 0"
      by(auto elim:distance.cases)
    hence "m -[]→⇩ι* m'" by(cases as) auto
    hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
    with ‹length s = length (m#msx')›[THEN sym]
    have "S,slice_kind S ⊢ (m#msx',s) =[]⇒⇩τ (m#msx',s)" 
      by(fastforce intro:silent_moves_Nil)
    thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by simp blast
  next
    fix x m as fix s::"(('var ⇀ 'val) × 'ret) list"
    assume "distance m m' (Suc x)" and "m -as→⇩ι* m'"
      and "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}"
      and "length s = length (m#msx')" and "∀m ∈ set msx'. return_node m"
      and IH:"⋀m as s. ⟦distance m m' x; m -as→⇩ι* m'; 
      obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}; length s = length (m#msx'); 
      ∀m ∈ set msx'. return_node m⟧
      ⟹ ∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)"
    from ‹m -as→⇩ι* m'› have "valid_node m" 
      by(fastforce intro:path_valid_node simp:intra_path_def)
    from ‹m -as→⇩ι* m'› have "get_proc m = get_proc m'" by(rule intra_path_get_procs)
    have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    proof
      assume "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
        by(fastforce intro!:n_in_obs_intra)
      with ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}› show False by simp
    qed
    from ‹distance m m' (Suc x)› obtain a where "valid_edge a" and "m = sourcenode a"
      and "intra_kind(kind a)" and "distance (targetnode a) m' x"
      and target:"targetnode a = (SOME mx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                               distance (targetnode a') m' x ∧
                                               valid_edge a' ∧ intra_kind (kind a') ∧ 
                                               targetnode a' = mx)"
      by -(erule distance_successor_distance,simp+)
    from ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› 
      ‹m = sourcenode a›
    have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
      by(cases s)
    (auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
    from ‹distance (targetnode a) m' x› obtain asx where "targetnode a -asx→⇩ι* m'" 
      and "length asx = x" and "∀as'. targetnode a -as'→⇩ι* m' ⟶ x ≤ length as'"
      by(auto elim:distance.cases)
    from ‹valid_edge a› ‹intra_kind(kind a)› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› 
      ‹m = sourcenode a› ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}›
    have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}"
      by(fastforce dest:edge_obs_intra_subset)
    from IH[OF ‹distance (targetnode a) m' x› ‹targetnode a -asx→⇩ι* m'› this
      length ‹∀m ∈ set msx'. return_node m›] obtain as' 
      where moves:"S,slice_kind S ⊢ 
      (targetnode a#msx',transfer (slice_kind S a) s) =as'⇒⇩τ 
      (m'#msx',transfer (slice_kind S a) s)" by blast
    have "pred (slice_kind S a) s ∧ transfer (slice_kind S a) s = s"
    proof(cases "kind a")
      fix f assume "kind a = ⇑f"
      with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› have "slice_kind S a = ⇑id"
        by(fastforce intro:slice_kind_Upd)
      with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
    next
      fix Q assume "kind a = (Q)⇩√"
      with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
        ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {}› ‹distance (targetnode a) m' x›
        ‹distance m m' (Suc x)› ‹method_exit m'› ‹get_proc m = get_proc m'› target
      have "slice_kind S a = (λs. True)⇩√"
        by(fastforce intro:slice_kind_Pred_empty_obs_nearer_SOME)
     with ‹length s = length (m#msx')› show ?thesis by(cases s) auto
    next
      fix Q r p fs assume "kind a = Q:r↪⇘p⇙fs"
      with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    next
      fix Q p f assume "kind a = Q↩⇘p⇙f"
      with ‹intra_kind(kind a)› have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    qed
    hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
      by simp_all
    with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹valid_edge a›
      ‹intra_kind(kind a)› ‹length s = length (m#msx')› ‹∀m ∈ set msx'. return_node m›
    have "S,slice_kind S ⊢ (sourcenode a#msx',s) -a→⇩τ 
                             (targetnode a#msx',transfer (slice_kind S a) s)"
      by(fastforce intro:silent_move_intra)
    with moves ‹transfer (slice_kind S a) s = s› ‹m = sourcenode a›
    have "S,slice_kind S ⊢ (m#msx',s) =a#as'⇒⇩τ (m'#msx',s)"
      by(fastforce intro:silent_moves_Cons)
    thus "∃as. S,slice_kind S ⊢ (m#msx',s) =as⇒⇩τ (m'#msx',s)" by blast
  qed
qed


lemma silent_moves_vpa_path:
  assumes "S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" 
  and "ms = targetnodes rs" and "valid_return_list rs m"
  and "length rs = length cs"
  shows "m -as→* m'" and "valid_path_aux cs as"
proof -
  from assms have "m -as→* m' ∧ valid_path_aux cs as"
  proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m cs ms rs
      rule:silent_moves.induct)
    case (silent_moves_Nil msx sx n⇩c f)
    from ‹valid_node m'› have "m' -[]→* m'"
      by (rule empty_path)
    thus ?case by fastforce
  next
    case (silent_moves_Cons S f sx a msx' sx' as s'')
    thus ?case
    proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
      case (silent_move_intra f a sx sx' n⇩c msx')
      note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
        ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); 
        ms = targetnodes rs; valid_return_list rs m;
        length rs = length cs⟧
        ⟹ m -as→* m' ∧ valid_path_aux cs as›
      from ‹msx' = targetnode a # tl (m # ms)›
      have "msx' = targetnode a # ms" by simp
      from ‹valid_edge a› ‹intra_kind (kind a)›
      have "get_proc (sourcenode a) = get_proc (targetnode a)"
        by(rule get_proc_intra)
      with ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
      have "valid_return_list rs (targetnode a)"
        apply(clarsimp simp:valid_return_list_def)
        apply(erule_tac x="cs'" in allE) apply clarsimp
        by(case_tac cs') auto
      from ‹valid_edge a› have "valid_node (targetnode a)" by simp
      from IH[OF ‹msx' = targetnode a # ms› this 
        ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
        ‹ms = targetnodes rs› ‹valid_return_list rs (targetnode a)›
        ‹length rs = length cs›]
      have "targetnode a -as→* m'" and "valid_path_aux cs as" by simp_all
      from ‹valid_edge a› ‹targetnode a -as→* m'› 
        ‹hd (m # ms) = sourcenode a›
      have "m -a#as→* m'" by(fastforce intro:Cons_path)
      moreover
      from ‹intra_kind (kind a)› ‹valid_path_aux cs as›
      have "valid_path_aux cs (a # as)" by(fastforce simp:intra_kind_def)
      ultimately show ?case by simp
    next
      case (silent_move_call f a sx sx' Q r p fs a' n⇩c msx')
      note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
        ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); 
        ms = targetnodes rs; valid_return_list rs m;
        length rs = length cs⟧
        ⟹ m -as→* m' ∧ valid_path_aux cs as›
      from ‹valid_edge a› have "valid_node (targetnode a)" by simp
      from ‹length rs = length cs› 
      have "length (a'#rs) = length (a#cs)" by simp
      from ‹msx' = targetnode a # targetnode a' # tl (m # ms)›
      have "msx' = targetnode a # targetnode a' # ms" by simp
      from ‹ms = targetnodes rs› have "targetnode a' # ms = targetnodes (a' # rs)"
        by(simp add:targetnodes_def)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
        by(rule get_proc_call)
      from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
        by(rule get_return_edges_valid)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
      obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
      from ‹valid_edge a› ‹a' ∈ get_return_edges a›
      have "get_proc (sourcenode a) = get_proc (targetnode a')"
        by(rule get_proc_get_return_edge)
      with ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a›
        ‹get_proc (targetnode a) = p› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
      have "valid_return_list (a' # rs) (targetnode a)"
        apply(clarsimp simp:valid_return_list_def)
        apply(case_tac cs') apply auto
        apply(erule_tac x="list" in allE) apply clarsimp
        by(case_tac list)(auto simp:targetnodes_def)
      from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
        ‹a' ∈ get_return_edges a›
      have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
        by auto(case_tac i,auto)
      from IH[OF ‹msx' = targetnode a # targetnode a' # ms› ‹valid_node (targetnode a)› this 
        ‹targetnode a' # ms = targetnodes (a' # rs)› 
        ‹valid_return_list (a' # rs) (targetnode a)› ‹length (a'#rs) = length (a#cs)›]
      have "targetnode a -as→* m'" and "valid_path_aux (a # cs) as" by simp_all
      from ‹valid_edge a› ‹targetnode a -as→* m'› 
        ‹hd (m # ms) = sourcenode a›
      have "m -a#as→* m'" by(fastforce intro:Cons_path)
      moreover
      from ‹valid_path_aux (a # cs) as› ‹kind a = Q:r↪⇘p⇙fs›
      have "valid_path_aux cs (a # as)" by simp
      ultimately show ?case by simp
    next
      case (silent_move_return f a sx sx' Q p f' n⇩c msx')
      note IH = ‹⋀m cs ms rs. ⟦msx' = m # ms; valid_node m;
        ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); 
        ms = targetnodes rs; valid_return_list rs m;
        length rs = length cs⟧
        ⟹ m -as→* m' ∧ valid_path_aux cs as›
      from ‹valid_edge a› have "valid_node (targetnode a)" by simp
      from ‹length (m # ms) = length sx› ‹length sx = Suc (length sx')› 
        ‹sx' ≠ []›
      obtain x xs where "ms = x#xs" by(cases ms) auto
      with ‹ms = targetnodes rs› obtain r' rs' where "rs = r'#rs'" 
        and "x = targetnode r'" and "xs = targetnodes rs'" 
        by(auto simp:targetnodes_def)
      with ‹length rs = length cs› obtain c' cs' where "cs = c'#cs'"
        and "length rs' = length cs'"
        by(cases cs) auto
      from ‹ms = x#xs› ‹length (m # ms) = length sx› 
        ‹length sx = Suc (length sx')›
      have "length sx' = Suc (length xs)" by simp
      from ‹ms = x#xs› ‹msx' = tl (m # ms)› ‹hd (tl (m # ms)) = targetnode a›
        ‹length (m # ms) = length sx› ‹length sx = Suc (length sx')› ‹sx' ≠ []›
      have "msx' = targetnode a#xs" by simp
      from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
        ‹rs = r'#rs'› ‹cs = c'#cs'›
      have "r' ∈ get_return_edges c'" by fastforce
      from ‹ms = x#xs› ‹hd (tl (m # ms)) = targetnode a›
      have "x = targetnode a" by simp
      with ‹valid_return_list rs m› ‹rs = r'#rs'› ‹x = targetnode r'›
      have "valid_return_list rs' (targetnode a)"
        apply(clarsimp simp:valid_return_list_def)
        apply(erule_tac x="r'#cs'" in allE) apply clarsimp
        by(case_tac cs')(auto simp:targetnodes_def)
      from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
        ‹rs = r'#rs'› ‹cs = c'#cs'›
      have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
        and "r' ∈ get_return_edges c'" by auto
      from IH[OF ‹msx' = targetnode a#xs› ‹valid_node (targetnode a)› 
        ‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)› ‹xs = targetnodes rs'›
        ‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'›]
      have "targetnode a -as→* m'" and "valid_path_aux cs' as" by simp_all
      from ‹valid_edge a› ‹targetnode a -as→* m'› 
        ‹hd (m # ms) = sourcenode a›
      have "m -a#as→* m'" by(fastforce intro:Cons_path)
      moreover
      from ‹ms = x#xs› ‹hd (tl (m # ms)) = targetnode a›
      have "x = targetnode a" by simp
      from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
      have "method_exit (sourcenode a)" by(fastforce simp:method_exit_def)
      from ‹valid_return_list rs m› ‹hd (m # ms) = sourcenode a› 
        ‹rs = r'#rs'›
      have "get_proc (sourcenode a) = get_proc (sourcenode r') ∧
        method_exit (sourcenode r') ∧ valid_edge r'"
        apply(clarsimp simp:valid_return_list_def method_exit_def)
        apply(erule_tac x="[]" in allE) 
        by(auto dest:get_proc_return)
      hence "get_proc (sourcenode a) = get_proc (sourcenode r')"
        and "method_exit (sourcenode r')" and "valid_edge r'" by simp_all
      with ‹method_exit (sourcenode a)› have "sourcenode r' = sourcenode a"
        by(fastforce intro:method_exit_unique)
      with ‹valid_edge a› ‹valid_edge r'› ‹x = targetnode r'› ‹x = targetnode a›
      have "r' = a" by(fastforce intro:edge_det)
      with ‹r' ∈ get_return_edges c'› ‹valid_path_aux cs' as› ‹cs = c'#cs'› 
        ‹kind a = Q↩⇘p⇙f'›
      have "valid_path_aux cs (a # as)" by simp
      ultimately show ?case by simp
    qed
  qed
  thus "m -as→* m'" and "valid_path_aux cs as" by simp_all
qed



subsection ‹Observable moves›


inductive observable_move ::
  "'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒ 
   (('var ⇀ 'val) × 'ret) list ⇒ 'edge ⇒ 'node list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
("_,_ ⊢ '(_,_') -_→ '(_,_')" [51,50,0,0,50,0,0] 51) 
 
  where observable_move_intra:
  "⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a); 
    ∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
    hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length s' = length s; length ms = length s;
    hd ms = sourcenode a; ms' = (targetnode a)#tl ms⟧  
  ⟹ S,f ⊢ (ms,s) -a→ (ms',s')"

  | observable_move_call:
  "⟦pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘p⇙fs; 
    valid_edge a'; a' ∈ get_return_edges a;
    ∀m ∈ set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
    hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙; length ms = length s; length s' = Suc(length s); 
    hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms⟧  
  ⟹ S,f ⊢ (ms,s) -a→ (ms',s')"

  | observable_move_return:
  "⟦pred (f a) s; transfer (f a) s = s'; valid_edge