Theory Slice

section ‹Static backward slice›

theory Slice 
  imports Observable Distance DataDependence "../Basic/SemanticsCFG"  
begin

locale BackwardSlice = 
  CFG_wf sourcenode targetnode kind valid_edge Entry Def Use state_val
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" (‹'('_Entry'_')›) and Def :: "'node ⇒ 'var set"
  and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val" +
  fixes backward_slice :: "'node set ⇒ 'node set"
  assumes valid_nodes:"n ∈ backward_slice S ⟹ valid_node n"
  and refl:"⟦valid_node n; n ∈ S⟧ ⟹ n ∈ backward_slice S"
  and dd_closed:"⟦n' ∈ backward_slice S; n influences V in n'⟧ 
  ⟹ n ∈ backward_slice S"
  and obs_finite:"finite (obs n (backward_slice S))"
  and obs_singleton:"card (obs n (backward_slice S)) ≤ 1"

begin

lemma slice_n_in_obs:
  "n ∈ backward_slice S ⟹ obs n (backward_slice S) = {n}"
by(fastforce intro!:n_in_obs dest:valid_nodes)

lemma obs_singleton_disj: 
  "(∃m. obs n (backward_slice S) = {m}) ∨ obs n (backward_slice S) = {}"
proof -
  have "finite(obs n (backward_slice S))" by(rule obs_finite)
  show ?thesis
  proof(cases "card(obs n (backward_slice S)) = 0")
    case True
    with ‹finite(obs n (backward_slice S))› have "obs n (backward_slice S) = {}"
      by simp
    thus ?thesis by simp
  next
    case False
    have "card(obs n (backward_slice S)) ≤ 1" by(rule obs_singleton)
    with False have "card(obs n (backward_slice S)) = 1"
      by simp
    hence "∃m. obs n (backward_slice S) = {m}" by(fastforce dest:card_eq_SucD)
    thus ?thesis by simp
  qed
qed


lemma obs_singleton_element:
  assumes "m ∈ obs n (backward_slice S)" shows "obs n (backward_slice S) = {m}"
proof -
  have "(∃m. obs n (backward_slice S) = {m}) ∨ obs n (backward_slice S) = {}"
    by(rule obs_singleton_disj)
  with ‹m ∈ obs n (backward_slice S)› show ?thesis by fastforce
qed


lemma obs_the_element: 
  "m ∈ obs n (backward_slice S) ⟹ (THE m. m ∈ obs n (backward_slice S)) = m"
by(fastforce dest:obs_singleton_element)


subsection ‹Traversing the sliced graph›

text ‹‹slice_kind S a› conforms to @{term "kind a"} in the
  sliced graph›

definition slice_kind :: "'node set ⇒ 'edge ⇒ 'state edge_kind"
  where "slice_kind S a = (let S' = backward_slice S; n = sourcenode a in 
  (if sourcenode a ∈ S' then kind a
   else (case kind a of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ 
    (if obs (sourcenode a) S' = {} then 
      (let nx = (SOME n'. ∃a'. n = sourcenode a' ∧ valid_edge a' ∧ targetnode a' = n')
      in (if (targetnode a = nx) then (λs. True)⇩√ else (λs. False)⇩√))
     else (let m = THE m. m ∈ obs n S' in 
       (if (∃x. distance (targetnode a) m x ∧ distance n m (x + 1) ∧
            (targetnode a = (SOME nx'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                     distance (targetnode a') m x ∧
                                     valid_edge a' ∧ targetnode a' = nx'))) 
          then (λs. True)⇩√ else (λs. False)⇩√
       ))
     ))
  ))"


definition
  slice_kinds :: "'node set ⇒ 'edge list ⇒ 'state edge_kind list"
  where "slice_kinds S as ≡ map (slice_kind S) as"


lemma slice_kind_in_slice:
  "sourcenode a ∈ backward_slice S ⟹ slice_kind S a = kind a"
by(simp add:slice_kind_def)


lemma slice_kind_Upd:
  "⟦sourcenode a ∉ backward_slice S; kind a = ⇑f⟧ ⟹ slice_kind S a = ⇑id"
by(simp add:slice_kind_def)


lemma slice_kind_Pred_empty_obs_SOME:
  "⟦sourcenode a ∉ backward_slice S; kind a = (Q)⇩√; 
    obs (sourcenode a) (backward_slice S) = {}; 
    targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
                                  targetnode a' = n')⟧
  ⟹ slice_kind S a = (λs. True)⇩√"
by(simp add:slice_kind_def)


lemma slice_kind_Pred_empty_obs_not_SOME:
  "⟦sourcenode a ∉ backward_slice S; kind a = (Q)⇩√; 
    obs (sourcenode a) (backward_slice S) = {}; 
    targetnode a ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
                                  targetnode a' = n')⟧
  ⟹ slice_kind S a = (λs. False)⇩√"
by(simp add:slice_kind_def)


lemma slice_kind_Pred_obs_nearer_SOME:
  assumes "sourcenode a ∉ backward_slice S" and "kind a = (Q)⇩√" 
  and "m ∈ obs (sourcenode a) (backward_slice S)"
  and "distance (targetnode a) m x" "distance (sourcenode a) m (x + 1)"
  and "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
                                          distance (targetnode a') m x ∧
                                          valid_edge a' ∧ targetnode a' = n')"
  shows "slice_kind S a = (λs. True)⇩√"
proof -
  from ‹m ∈ obs (sourcenode a) (backward_slice S)›
  have "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
    by(rule obs_the_element[THEN sym])
  with assms show ?thesis
    by(fastforce simp:slice_kind_def Let_def)
qed


lemma slice_kind_Pred_obs_nearer_not_SOME:
  assumes "sourcenode a ∉ backward_slice S" and "kind a = (Q)⇩√" 
  and "m ∈ obs (sourcenode a) (backward_slice S)"
  and "distance (targetnode a) m x" "distance (sourcenode a) m (x + 1)"
  and "targetnode a ≠ (SOME nx'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                          distance (targetnode a') m x ∧
                                          valid_edge a' ∧ targetnode a' = nx')"
  shows "slice_kind S a = (λs. False)⇩√"
proof -
  from ‹m ∈ obs (sourcenode a) (backward_slice S)›
  have "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
    by(rule obs_the_element[THEN sym])
  with assms show ?thesis
    by(fastforce dest:distance_det simp:slice_kind_def Let_def)
qed


lemma slice_kind_Pred_obs_not_nearer:
  assumes "sourcenode a ∉ backward_slice S" and "kind a = (Q)⇩√" 
  and in_obs:"m ∈ obs (sourcenode a) (backward_slice S)"
  and dist:"distance (sourcenode a) m (x + 1)" 
           "¬ distance (targetnode a) m x"
  shows "slice_kind S a = (λs. False)⇩√"
proof -
  from in_obs have the:"m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
    by(rule obs_the_element[THEN sym])
  from dist have "¬ (∃x. distance (targetnode a) m x ∧ 
                            distance (sourcenode a) m (x + 1))"
    by(fastforce dest:distance_det)
  with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√› in_obs the show ?thesis
    by(fastforce simp:slice_kind_def Let_def)
qed


lemma kind_Predicate_notin_slice_slice_kind_Predicate:
  assumes "kind a = (Q)⇩√" and "sourcenode a ∉ backward_slice S"
  obtains Q' where "slice_kind S a = (Q')⇩√" and "Q' = (λs. False) ∨ Q' = (λs. True)"
proof(atomize_elim)
  show "∃Q'. slice_kind S a = (Q')⇩√ ∧ (Q' = (λs. False) ∨ Q' = (λs. True))"
  proof(cases "obs (sourcenode a) (backward_slice S) = {}")
    case True
    show ?thesis
    proof(cases "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                               valid_edge a' ∧ targetnode a' = n')")
      case True
      with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
        ‹obs (sourcenode a) (backward_slice S) = {}›
      have "slice_kind S a = (λs. True)⇩√" by(rule slice_kind_Pred_empty_obs_SOME)
      thus ?thesis by simp
    next
      case False
      with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
        ‹obs (sourcenode a) (backward_slice S) = {}›
      have "slice_kind S a = (λs. False)⇩√"
        by(rule slice_kind_Pred_empty_obs_not_SOME)
      thus ?thesis by simp
    qed
  next
    case False
    then obtain m where "m ∈ obs (sourcenode a) (backward_slice S)" by blast
    show ?thesis
    proof(cases "∃x. distance (targetnode a) m x ∧ 
        distance (sourcenode a) m (x + 1)")
      case True
      then obtain x where "distance (targetnode a) m x" 
        and "distance (sourcenode a) m (x + 1)" by blast
      show ?thesis
      proof(cases "targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
                                                 distance (targetnode a') m x ∧
                                                 valid_edge a' ∧ targetnode a' = n')")
        case True
        with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
          ‹m ∈ obs (sourcenode a) (backward_slice S)›
          ‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
        have "slice_kind S a = (λs. True)⇩√"
          by(rule slice_kind_Pred_obs_nearer_SOME)
        thus ?thesis by simp
      next
        case False
        with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√›
          ‹m ∈ obs (sourcenode a) (backward_slice S)›
          ‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
        have "slice_kind S a = (λs. False)⇩√"
          by(rule slice_kind_Pred_obs_nearer_not_SOME)
        thus ?thesis by simp
      qed
    next
      case False
      from ‹m ∈ obs (sourcenode a) (backward_slice S)›
      have "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
        by(rule obs_the_element[THEN sym])
      with ‹sourcenode a ∉ backward_slice S› ‹kind a = (Q)⇩√› False
        ‹m ∈ obs (sourcenode a) (backward_slice S)›
      have "slice_kind S a = (λs. False)⇩√"
        by(fastforce simp:slice_kind_def Let_def)
      thus ?thesis by simp
    qed
  qed
qed


lemma only_one_SOME_edge:
  assumes "valid_edge a"
  shows "∃!a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
               targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                              valid_edge a' ∧ targetnode a' = n')"
proof(rule ex_ex1I)
  show "∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
             targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                            valid_edge a' ∧ targetnode a' = n')"
  proof -
    have "(∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
                targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                               valid_edge a' ∧ targetnode a' = n')) =
      (∃n'. ∃a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧ targetnode a' = n')"
      apply(unfold some_eq_ex[of "λn'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                            valid_edge a' ∧ targetnode a' = n'"])
      by simp
    also have "…" using ‹valid_edge a› by blast
    finally show ?thesis .
  qed
next
  fix a' ax
  assume "sourcenode a = sourcenode a' ∧ valid_edge a' ∧
    targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                   valid_edge a' ∧ targetnode a' = n')"
    and "sourcenode a = sourcenode ax ∧ valid_edge ax ∧
    targetnode ax = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                              valid_edge a' ∧ targetnode a' = n')"
  thus "a' = ax" by(fastforce intro!:edge_det)
qed


lemma slice_kind_only_one_True_edge:
  assumes "sourcenode a = sourcenode a'" and "targetnode a ≠ targetnode a'" 
  and "valid_edge a" and "valid_edge a'" and "slice_kind S a = (λs. True)⇩√"
  shows "slice_kind S a' = (λs. False)⇩√"
proof -
  from assms obtain Q Q' where "kind a = (Q)⇩√"
    and "kind a' = (Q')⇩√" and det:"∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
    by(auto dest:deterministic)
  from ‹valid_edge a› have ex1:"∃!a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
               targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                              valid_edge a' ∧ targetnode a' = n')"
    by(rule only_one_SOME_edge)
  show ?thesis
  proof(cases "sourcenode a ∈ backward_slice S")
    case True
    with ‹slice_kind S a = (λs. True)⇩√› ‹kind a = (Q)⇩√› have "Q = (λs. True)"
      by(simp add:slice_kind_def Let_def)
    with det have "Q' = (λs. False)" by(simp add:fun_eq_iff)
    with True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'› show ?thesis
      by(simp add:slice_kind_def Let_def)
  next
    case False
    hence "sourcenode a ∉ backward_slice S" by simp
    thus ?thesis
    proof(cases "obs (sourcenode a) (backward_slice S) = {}")
      case True
      with ‹sourcenode a ∉ backward_slice S› ‹slice_kind S a = (λs. True)⇩√›
        ‹kind a = (Q)⇩√›
      have target:"targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                                 valid_edge a' ∧ targetnode a' = n')"
        by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
      have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                            valid_edge a' ∧ targetnode a' = n')"
      proof(rule ccontr)
        assume "¬ targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                                 valid_edge a' ∧ targetnode a' = n')"
        hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                              valid_edge a' ∧ targetnode a' = n')"
          by simp
        with ex1 target ‹sourcenode a = sourcenode a'› ‹valid_edge a›
          ‹valid_edge a'› have "a = a'" by blast
        with ‹targetnode a ≠ targetnode a'› show False by simp
      qed
      with ‹sourcenode a ∉ backward_slice S› True ‹kind a' = (Q')⇩√›
        ‹sourcenode a = sourcenode a'› show ?thesis 
        by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
    next
      case False
      hence "obs (sourcenode a) (backward_slice S) ≠ {}" .
      then obtain m where "m ∈ obs (sourcenode a) (backward_slice S)" by auto
      hence "m = (THE m. m ∈ obs (sourcenode a) (backward_slice S))"
        by(auto dest:obs_the_element)
      with ‹sourcenode a ∉ backward_slice S› 
        ‹obs (sourcenode a) (backward_slice S) ≠ {}› 
        ‹slice_kind S a = (λs. True)⇩√› ‹kind a = (Q)⇩√›
      obtain x x' where "distance (targetnode a) m x" 
        "distance (sourcenode a) m (x + 1)"
        and target:"targetnode a = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
                                                 distance (targetnode a') m x ∧
                                                 valid_edge a' ∧ targetnode a' = n')"
        by(auto simp:slice_kind_def Let_def fun_eq_iff split:if_split_asm)
      show ?thesis
      proof(cases "distance (targetnode a') m x")
        case False
        with ‹sourcenode a ∉ backward_slice S› ‹kind a' = (Q')⇩√›
          ‹m ∈ obs (sourcenode a) (backward_slice S)›
          ‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
          ‹sourcenode a = sourcenode a'› show ?thesis
          by(fastforce intro:slice_kind_Pred_obs_not_nearer)
      next
        case True
        from ‹valid_edge a› ‹distance (targetnode a) m x›
          ‹distance (sourcenode a) m (x + 1)›
        have ex1:"∃!a'. sourcenode a = sourcenode a' ∧ 
               distance (targetnode a') m x ∧ valid_edge a' ∧
               targetnode a' = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧
                                              distance (targetnode a') m x ∧
                                              valid_edge a' ∧ targetnode a' = nx)"
          by(fastforce intro!:only_one_SOME_dist_edge)
        have "targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                               distance (targetnode a') m x ∧
                                               valid_edge a' ∧ targetnode a' = n')"
        proof(rule ccontr)
          assume "¬ targetnode a' ≠ (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                                 distance (targetnode a') m x ∧
                                                 valid_edge a' ∧ targetnode a' = n')"
          hence "targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧
                                                distance (targetnode a') m x ∧
                                                valid_edge a' ∧ targetnode a' = n')"
            by simp
          with ex1 target ‹sourcenode a = sourcenode a'› 
            ‹valid_edge a› ‹valid_edge a'› 
            ‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
          have "a = a'" by auto
          with ‹targetnode a ≠ targetnode a'› show False by simp
        qed
        with ‹sourcenode a ∉ backward_slice S› 
          ‹kind a' = (Q')⇩√› ‹m ∈ obs (sourcenode a) (backward_slice S)›
          ‹distance (targetnode a) m x› ‹distance (sourcenode a) m (x + 1)›
          True ‹sourcenode a = sourcenode a'› show ?thesis
          by(fastforce intro:slice_kind_Pred_obs_nearer_not_SOME)
      qed
    qed
  qed
qed


lemma slice_deterministic:
  assumes "valid_edge a" and "valid_edge a'"
  and "sourcenode a = sourcenode a'" and "targetnode a ≠ targetnode a'"
  obtains Q Q' where "slice_kind S a = (Q)⇩√" and "slice_kind S a' = (Q')⇩√"
  and "∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
proof(atomize_elim)
  from assms obtain Q Q' 
    where "kind a = (Q)⇩√" and "kind a' = (Q')⇩√" 
    and det:"∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
    by(auto dest:deterministic)
  from ‹valid_edge a› have ex1:"∃!a'. sourcenode a = sourcenode a' ∧ valid_edge a' ∧
               targetnode a' = (SOME n'. ∃a'. sourcenode a = sourcenode a' ∧ 
                                              valid_edge a' ∧ targetnode a' = n')"
    by(rule only_one_SOME_edge)
  show "∃Q Q'. slice_kind S a = (Q)⇩√ ∧ slice_kind S a' = (Q')⇩√ ∧ 
                (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
  proof(cases "sourcenode a ∈ backward_slice S")
    case True
    with ‹kind a = (Q)⇩√› have "slice_kind S a = (Q)⇩√"
      by(simp add:slice_kind_def Let_def)
    from True ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'›
    have "slice_kind S a' = (Q')⇩√"
      by(simp add:slice_kind_def Let_def)
    with ‹slice_kind S a = (Q)⇩√› det show ?thesis by blast
  next
    case False
    with ‹kind a = (Q)⇩√› 
    have "slice_kind S a = (λs. True)⇩√ ∨ slice_kind S a = (λs. False)⇩√"
      by(simp add:slice_kind_def Let_def)
    thus ?thesis
    proof
      assume true:"slice_kind S a = (λs. True)⇩√"
      with ‹sourcenode a = sourcenode a'› ‹targetnode a ≠ targetnode a'›
        ‹valid_edge a› ‹valid_edge a'›
      have "slice_kind S a' = (λs. False)⇩√"
        by(rule slice_kind_only_one_True_edge)
      with true show ?thesis by simp
    next
      assume false:"slice_kind S a = (λs. False)⇩√"
      from False ‹kind a' = (Q')⇩√› ‹sourcenode a = sourcenode a'›
      have "slice_kind S a' = (λs. True)⇩√ ∨ slice_kind S a' = (λs. False)⇩√"
        by(simp add:slice_kind_def Let_def)
      with false show ?thesis by auto
    qed
  qed
qed




subsection ‹Observable and silent moves›

inductive silent_move :: 
  "'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge ⇒ 
  'node ⇒ 'state ⇒ bool" (‹_,_ ⊢ '(_,_') -_→⇩τ '(_,_')› [51,50,0,0,50,0,0] 51) 
 
  where silent_moveI:
  "⟦pred (f a) s; transfer (f a) s = s'; sourcenode a ∉ backward_slice S; 
    valid_edge a⟧  
  ⟹ S,f ⊢ (sourcenode a,s) -a→⇩τ (targetnode a,s')"


inductive silent_moves :: 
  "'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge list ⇒ 
  'node ⇒ 'state ⇒ bool" (‹_,_ ⊢ '(_,_') =_⇒⇩τ '(_,_')› [51,50,0,0,50,0,0] 51)

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

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


lemma silent_moves_obs_slice:
  "⟦S,f ⊢ (n,s) =as⇒⇩τ (n',s'); nx ∈ obs n' (backward_slice S)⟧
  ⟹ nx ∈ obs n (backward_slice S)"
proof(induct rule:silent_moves.induct)
  case silent_moves_Nil thus ?case by simp
next
  case (silent_moves_Cons S f n s a n' s' as n'' s'')
  from ‹nx ∈ obs n'' (backward_slice S)›
    ‹nx ∈ obs n'' (backward_slice S) ⟹ nx ∈ obs n' (backward_slice S)›
  have obs:"nx ∈ obs n' (backward_slice S)" by simp
  from ‹S,f ⊢ (n,s) -a→⇩τ (n',s')›
  have "n = sourcenode a" and "n' = targetnode a" and "valid_edge a" 
    and "n ∉ (backward_slice S)"
    by(auto elim:silent_move.cases)
  hence "obs n' (backward_slice S) ⊆ obs n (backward_slice S)"
    by simp(rule edge_obs_subset,simp+)
  with obs show ?case by blast
qed


lemma silent_moves_preds_transfers_path:
  "⟦S,f ⊢ (n,s) =as⇒⇩τ (n',s'); valid_node n⟧ 
  ⟹ preds (map f as) s ∧ transfers (map f as) s = s' ∧ n -as→* n'"
proof(induct rule:silent_moves.induct)
  case silent_moves_Nil thus ?case by(simp add:path.empty_path)
next
  case (silent_moves_Cons S f n s a n' s' as n'' s'')
  note IH = ‹valid_node n' ⟹
    preds (map f as) s' ∧ transfers (map f as) s' = s'' ∧ n' -as→* n''›
  from ‹S,f ⊢ (n,s) -a→⇩τ (n',s')› have "pred (f a) s" and "transfer (f a) s = s'"
    and "n = sourcenode a" and "n' = targetnode a" and "valid_edge a"
    by(auto elim:silent_move.cases)
  from ‹n' = targetnode a› ‹valid_edge a› have "valid_node n'" by simp
  from IH[OF this] have "preds (map f as) s'" and "transfers (map f as) s' = s''"
    and "n' -as→* n''" by simp_all
  from ‹n = sourcenode a› ‹n' = targetnode a› ‹valid_edge a› ‹n' -as→* n''›
  have "n -a#as→* n''" by(fastforce intro:Cons_path)
  with ‹pred (f a) s› ‹preds (map f as) s'› ‹transfer (f a) s = s'› 
    ‹transfers (map f as) s' = s''› show ?case by simp
qed


lemma obs_silent_moves:
  assumes "obs n (backward_slice S) = {n'}"
  obtains as where "S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)"
proof(atomize_elim)
  from ‹obs n (backward_slice S) = {n'}› 
  have "n' ∈ obs n (backward_slice S)" by simp
  then obtain as where "n -as→* n'" 
    and "∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)"
    and "n' ∈ (backward_slice S)" by(erule obsE)
  from ‹n -as→* n'› obtain x where "distance n n' x" and "x ≤ length as"
    by(erule every_path_distance)
  from ‹distance n n' x› ‹n' ∈ obs n (backward_slice S)› 
  show "∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)"
  proof(induct x arbitrary:n s rule:nat.induct)
    fix n s assume "distance n n' 0"
    then obtain as' where "n -as'→* n'" and "length as' = 0"
      by(auto elim:distance.cases)
    hence "n -[]→* n'" by(cases as) auto
    hence "n = n'" by(fastforce elim:path.cases)
    hence "S,slice_kind S ⊢ (n,s) =[]⇒⇩τ (n',s)" by(fastforce intro:silent_moves_Nil)
    thus "∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)" by blast
  next
    fix x n s 
    assume "distance n n' (Suc x)" and "n' ∈ obs n (backward_slice S)"
      and IH:"⋀n s. ⟦distance n n' x; n' ∈ obs n (backward_slice S)⟧ 
              ⟹ ∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)"
    from ‹n' ∈ obs n (backward_slice S)›
    have "valid_node n" by(rule in_obs_valid)
    with ‹distance n n' (Suc x)›
    have "n ≠ n'" by(fastforce elim:distance.cases dest:empty_path)
    have "n ∉ backward_slice S"
    proof
      assume isin:"n ∈ backward_slice S"
      with ‹valid_node n› have "obs n (backward_slice S) = {n}"
        by(fastforce intro!:n_in_obs)
      with ‹n' ∈ obs n (backward_slice S)› ‹n ≠ n'› show False by simp
    qed
    from ‹distance n n' (Suc x)› obtain a where "valid_edge a" 
      and "n = sourcenode a" and "distance (targetnode a) n' x"
      and target:"targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
                                     distance (targetnode a') n' x ∧
                                     valid_edge a' ∧ targetnode a' = nx)"
      by -(erule distance_successor_distance,simp+)
    from ‹n' ∈ obs n (backward_slice S)›
    have "obs n (backward_slice S) = {n'}"
      by(rule obs_singleton_element)
    with ‹valid_edge a› ‹n ∉ backward_slice S› ‹n = sourcenode a›
    have disj:"obs (targetnode a) (backward_slice S) = {} ∨ 
               obs (targetnode a) (backward_slice S) = {n'}"
      by -(drule_tac S="backward_slice S" in edge_obs_subset,auto)
    from ‹distance (targetnode a) n' x› obtain asx where "targetnode a -asx→* n'" 
      and "length asx = x" and "∀as'. targetnode a -as'→* n' ⟶ x ≤ length as'" 
      by(auto elim:distance.cases)
    from ‹targetnode a -asx→* n'› ‹n' ∈ (backward_slice S)›
    obtain m where "∃m. m ∈ obs (targetnode a) (backward_slice S)"
      by(fastforce elim:path_ex_obs)
    with disj have "n' ∈ obs (targetnode a) (backward_slice S)" by fastforce
    from IH[OF ‹distance (targetnode a) n' x› this,of "transfer (slice_kind S a) s"]
    obtain asx' where 
    moves:"S,slice_kind S ⊢ (targetnode a,transfer (slice_kind S a) s) =asx'⇒⇩τ 
                               (n',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")
      case (Update f)
      with ‹n ∉ backward_slice S› ‹n = sourcenode a› have "slice_kind S a = ⇑id" 
        by(fastforce intro:slice_kind_Upd)
      thus ?thesis by simp
    next
      case (Predicate Q)
      with ‹n ∉ backward_slice S› ‹n = sourcenode a›
        ‹n' ∈ obs n (backward_slice S)› ‹distance (targetnode a) n' x›
        ‹distance n n' (Suc x)› target
      have "slice_kind S a =  (λs. True)⇩√"
        by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
      thus ?thesis by simp
    qed
    hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
      by simp_all
    with ‹n ∉ backward_slice S› ‹n = sourcenode a› ‹valid_edge a›
    have "S,slice_kind S ⊢ (sourcenode a,s) -a→⇩τ 
                             (targetnode a,transfer (slice_kind S a) s)"
      by(fastforce intro:silent_moveI)
    with moves ‹transfer (slice_kind S a) s = s› ‹n = sourcenode a›
    have "S,slice_kind S ⊢ (n,s) =a#asx'⇒⇩τ (n',s)"
      by(fastforce intro:silent_moves_Cons)
    thus "∃as. S,slice_kind S ⊢ (n,s) =as⇒⇩τ (n',s)" by blast
  qed
qed


inductive observable_move ::
  "'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge ⇒ 
  'node ⇒ 'state ⇒ bool" (‹_,_ ⊢ '(_,_') -_→ '(_,_')› [51,50,0,0,50,0,0] 51) 
 
  where observable_moveI:
  "⟦pred (f a) s; transfer (f a) s = s'; sourcenode a ∈ backward_slice S; 
    valid_edge a⟧  
  ⟹ S,f ⊢ (sourcenode a,s) -a→ (targetnode a,s')"


inductive observable_moves :: 
  "'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge list ⇒ 
  'node ⇒ 'state ⇒ bool" (‹_,_ ⊢ '(_,_') =_⇒ '(_,_')› [51,50,0,0,50,0,0] 51) 

  where observable_moves_snoc:
  "⟦S,f ⊢ (n,s) =as⇒⇩τ (n',s'); S,f ⊢ (n',s') -a→ (n'',s'')⟧ 
  ⟹ S,f ⊢ (n,s) =as@[a]⇒ (n'',s'')"


lemma observable_move_notempty:
  "⟦S,f ⊢ (n,s) =as⇒ (n',s'); as = []⟧ ⟹ False"
by(induct rule:observable_moves.induct,simp)


lemma silent_move_observable_moves:
  "⟦S,f ⊢ (n'',s'') =as⇒ (n',s'); S,f ⊢ (n,s) -a→⇩τ (n'',s'')⟧
  ⟹ S,f ⊢ (n,s) =a#as⇒ (n',s')"
proof(induct rule:observable_moves.induct)
  case (observable_moves_snoc S f nx sx as n' s' a' n'' s'')
  from ‹S,f ⊢ (n,s) -a→⇩τ (nx,sx)› ‹S,f ⊢ (nx,sx) =as⇒⇩τ (n',s')›
  have "S,f ⊢ (n,s) =a#as⇒⇩τ (n',s')" by(rule silent_moves_Cons)
  with ‹S,f ⊢ (n',s') -a'→ (n'',s'')›
  have "S,f ⊢ (n,s) =(a#as)@[a']⇒ (n'',s'')"
    by -(rule observable_moves.observable_moves_snoc)
  thus ?case by simp
qed


lemma observable_moves_preds_transfers_path:
  "S,f ⊢ (n,s) =as⇒ (n',s')
  ⟹ preds (map f as) s ∧ transfers (map f as) s = s' ∧ n -as→* n'"
proof(induct rule:observable_moves.induct)
  case (observable_moves_snoc S f n s as n' s' a n'' s'')
  have "valid_node n"
  proof(cases as)
    case Nil
    with ‹S,f ⊢ (n,s) =as⇒⇩τ (n',s')› have "n = n'" and "s = s'"
      by(auto elim:silent_moves.cases)
    with ‹S,f ⊢ (n',s') -a→ (n'',s'')› show ?thesis
      by(fastforce elim:observable_move.cases)
  next
    case (Cons a' as')
    with ‹S,f ⊢ (n,s) =as⇒⇩τ (n',s')› show ?thesis
      by(fastforce elim:silent_moves.cases silent_move.cases)
  qed
  with ‹S,f ⊢ (n,s) =as⇒⇩τ (n',s')›
  have "preds (map f as) s" and "transfers (map f as) s = s'"
    and "n -as→* n'" by(auto dest:silent_moves_preds_transfers_path)
  from ‹S,f ⊢ (n',s') -a→ (n'',s'')› have "pred (f a) s'" 
    and "transfer (f a) s' = s''" and "n' = sourcenode a" and "n'' = targetnode a" 
    and "valid_edge a"
    by(auto elim:observable_move.cases)
  from ‹n' = sourcenode a› ‹n'' = targetnode a› ‹valid_edge a›
  have "n' -[a]→* n''" by(fastforce intro:path.intros)
  with ‹n -as→* n'› have "n -as@[a]→* n''" by(rule path_Append)
  with ‹preds (map f as) s› ‹pred (f a) s'› ‹transfer (f a) s' = s''›
    ‹transfers (map f as) s = s'›
  show ?case by(simp add:transfers_split preds_split)
qed




subsection ‹Relevant variables›

inductive_set relevant_vars :: "'node set ⇒ 'node ⇒ 'var set" (‹rv _›)
for S :: "'node set" and n :: "'node"

where rvI:
  "⟦n -as→* n'; n' ∈ backward_slice S; V ∈ Use n';
    ∀nx ∈ set(sourcenodes as). V ∉ Def nx⟧
  ⟹ V ∈ rv S n"


lemma rvE:
  assumes rv:"V ∈ rv S n"
  obtains as n' where "n -as→* n'" and "n' ∈ backward_slice S" and "V ∈ Use n'"
  and "∀nx ∈ set(sourcenodes as). V ∉ Def nx"
using rv
by(atomize_elim,auto elim!:relevant_vars.cases)



lemma eq_obs_in_rv:
  assumes obs_eq:"obs n (backward_slice S) = obs n' (backward_slice S)" 
  and "x ∈ rv S n" shows "x ∈ rv S n'"
proof -
  from ‹x ∈ rv S n› obtain as m 
    where "n -as→* m" and "m ∈ backward_slice S" and "x ∈ Use m"
    and "∀nx∈set (sourcenodes as). x ∉ Def nx"
    by(erule rvE)
  from ‹n -as→* m› have "valid_node m" by(fastforce dest:path_valid_node)
  from ‹n -as→* m› ‹m ∈ backward_slice S› 
  have "∃nx as' as''. nx ∈ obs n (backward_slice S) ∧ n -as'→* nx ∧ 
                                     nx -as''→* m ∧ as = as'@as''"
  proof(cases "∀nx ∈ set(sourcenodes as). nx ∉ backward_slice S")
    case True
    with ‹n -as→* m› ‹m ∈ backward_slice S› have "m ∈ obs n (backward_slice S)"
      by -(rule obs_elem)
    with ‹n -as→* m› ‹valid_node m› show ?thesis by(blast intro:empty_path)
  next
    case False
    hence "∃nx ∈ set(sourcenodes as). nx ∈ backward_slice S" by simp
    then obtain nx' ns ns' where "sourcenodes as = ns@nx'#ns'"
      and "nx' ∈ backward_slice S" 
      and "∀x ∈ set ns. x ∉ backward_slice S"
      by(fastforce elim!:split_list_first_propE)
    from ‹sourcenodes as = ns@nx'#ns'›
    obtain as' a' as'' where "ns = sourcenodes as'"
      and "as = as'@a'#as''" and "sourcenode a' = nx'"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from ‹n -as→* m› ‹as = as'@a'#as''› ‹sourcenode a' = nx'›
    have "n -as'→* nx'" and "valid_edge a'" and "targetnode a' -as''→* m"
      by(fastforce dest:path_split)+
    with ‹sourcenode a' = nx'› have "nx' -a'#as''→* m" by(fastforce intro:Cons_path)
    from ‹n -as'→* nx'› ‹nx' ∈ backward_slice S›
      ‹∀x ∈ set ns. x ∉ backward_slice S› ‹ns = sourcenodes as'› 
    have "nx' ∈ obs n (backward_slice S)" 
      by(fastforce intro:obs_elem)
    with ‹n -as'→* nx'› ‹nx' -a'#as''→* m› ‹as = as'@a'#as''› show ?thesis by blast
  qed
  then obtain nx as' as'' where "nx ∈ obs n (backward_slice S)"
    and "n -as'→* nx" and "nx -as''→* m" and "as = as'@as''"
    by blast
  from ‹nx ∈ obs n (backward_slice S)› obs_eq 
  have "nx ∈ obs n' (backward_slice S)" by auto
  then obtain asx where "n' -asx→* nx" 
    and "∀ni ∈ set(sourcenodes asx). ni ∉ backward_slice S" 
    and "nx ∈ backward_slice S"
    by(erule obsE)
  from ‹as = as'@as''› ‹∀nx∈set (sourcenodes as). x ∉ Def nx› 
  have "∀ni∈set (sourcenodes as''). x ∉ Def ni"
    by(auto simp:sourcenodes_def)
  from ‹∀ni ∈ set(sourcenodes asx). ni ∉ backward_slice S› ‹n' -asx→* nx›
  have "∀ni ∈ set(sourcenodes asx). x ∉ Def ni"
  proof(induct asx arbitrary:n')
    case Nil thus ?case by(simp add:sourcenodes_def)
  next
    case (Cons ax' asx')
    note IH = ‹⋀n'. ⟦∀ni∈set (sourcenodes asx'). ni ∉ backward_slice S; 
      n' -asx'→* nx⟧ 
        ⟹ ∀ni∈set (sourcenodes asx'). x ∉ Def ni›
    from ‹n' -ax'#asx'→* nx› have "n' -[]@ax'#asx'→* nx" by simp
    hence "targetnode ax' -asx'→* nx" and "n' = sourcenode ax'"
      by(fastforce dest:path_split)+
    from ‹∀ni∈set (sourcenodes (ax'#asx')). ni ∉ backward_slice S›
    have all:"∀ni∈set (sourcenodes asx'). ni ∉ backward_slice S" 
      and "sourcenode ax' ∉ backward_slice S"
      by(auto simp:sourcenodes_def)
    from IH[OF all ‹targetnode ax' -asx'→* nx›]
    have "∀ni∈set (sourcenodes asx'). x ∉ Def ni" .
    with ‹∀ni∈set (sourcenodes as''). x ∉ Def ni›
    have "∀ni∈set (sourcenodes (asx'@as'')). x ∉ Def ni"
      by(auto simp:sourcenodes_def)
    from ‹n' -ax'#asx'→* nx› ‹nx -as''→* m› have "n' -(ax'#asx')@as''→* m" 
      by-(rule path_Append)
    hence "n' -ax'#asx'@as''→* m" by simp
    have "x ∉ Def (sourcenode ax')"
    proof
      assume "x ∈ Def (sourcenode ax')"
      with ‹x ∈ Use m› ‹∀ni∈set (sourcenodes (asx'@as'')). x ∉ Def ni›
        ‹n' -ax'#asx'@as''→* m› ‹n' = sourcenode ax'› 
      have "n' influences x in m"
        by(auto simp:data_dependence_def)
      with ‹m ∈ backward_slice S› dd_closed have "n' ∈ backward_slice S" 
        by(auto simp:dd_closed)
      with ‹n' = sourcenode ax'› ‹sourcenode ax' ∉ backward_slice S›
      show False by simp
    qed
    with ‹∀ni∈set (sourcenodes (asx'@as'')). x ∉ Def ni›
    show ?case by(simp add:sourcenodes_def)
  qed
  with ‹∀ni∈set (sourcenodes as''). x ∉ Def ni› 
  have "∀ni∈set (sourcenodes (asx@as'')). x ∉ Def ni"
    by(auto simp:sourcenodes_def)
  from ‹n' -asx→* nx› ‹nx -as''→* m› have "n' -asx@as''→* m" by(rule path_Append)
  with ‹m ∈ backward_slice S› ‹x ∈ Use m› 
    ‹∀ni∈set (sourcenodes (asx@as'')). x ∉ Def ni› show "x ∈ rv S n'" by -(rule rvI)
qed


lemma closed_eq_obs_eq_rvs:
  fixes S :: "'node set"
  assumes "valid_node n" and "valid_node n'"
  and obs_eq:"obs n (backward_slice S) = obs n' (backward_slice S)"
  shows "rv S n = rv S n'"
proof
  show "rv S n ⊆ rv S n'"
  proof
    fix x assume "x ∈ rv S n"
    with ‹valid_node n› obs_eq show "x ∈ rv S n'" by -(rule eq_obs_in_rv)
  qed
next
  show "rv S n' ⊆ rv S n"
  proof
    fix x assume "x ∈ rv S n'"
    with ‹valid_node n'› obs_eq[THEN sym] show "x ∈ rv S n" by -(rule eq_obs_in_rv)
  qed
qed


lemma rv_edge_slice_kinds:
  assumes "valid_edge a" and "sourcenode a = n" and "targetnode a = n''"
  and "∀V∈rv S n. state_val s V = state_val s' V"
  and "preds (slice_kinds S (a#as)) s" and "preds (slice_kinds S (a#asx)) s'"
  shows "∀V∈rv S n''. state_val (transfer (slice_kind S a) s) V =
                       state_val (transfer (slice_kind S a) s') V"
proof
  fix V assume "V ∈ rv S n''"
  show "state_val (transfer (slice_kind S a) s) V =
    state_val (transfer (slice_kind S a) s') V"
  proof(cases "V ∈ Def n")
    case True
    show ?thesis
    proof(cases "sourcenode a ∈ backward_slice S")
      case True
      hence "slice_kind S a = kind a" by(rule slice_kind_in_slice)
      with ‹preds (slice_kinds S (a#as)) s› have "pred (kind a) s"
        by(simp add:slice_kinds_def)
      from ‹slice_kind S a = kind a› ‹preds (slice_kinds S (a#asx)) s'›
      have "pred (kind a) s'"
        by(simp add:slice_kinds_def)
      from ‹valid_edge a› ‹sourcenode a = n› have "n -[]→* n"
        by(fastforce intro:empty_path)
      with True ‹sourcenode a = n› have "∀V ∈ Use n. V ∈ rv S n"
        by(fastforce intro:rvI simp:sourcenodes_def)
      with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹sourcenode a = n›
      have "∀V ∈ Use (sourcenode a). state_val s V = state_val s' V" by blast
      from ‹valid_edge a› this ‹pred (kind a) s› ‹pred (kind a) s'›
      have "∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
        state_val (transfer (kind a) s') V"
        by(rule CFG_edge_transfer_uses_only_Use)
      with ‹V ∈ Def n› ‹sourcenode a = n› ‹slice_kind S a = kind a›
      show ?thesis by simp
    next
      case False
      from ‹V ∈ rv S n''› obtain xs nx where "n'' -xs→* nx"
        and "nx ∈ backward_slice S" and "V ∈ Use nx"
        and "∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'" by(erule rvE)
      from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› 
        ‹n'' -xs→* nx›
      have "n -a#xs→* nx" by -(rule path.Cons_path)
      with ‹V ∈ Def n› ‹V ∈ Use nx› ‹∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'›
      have "n influences V in nx" by(fastforce simp:data_dependence_def)
      with ‹nx ∈ backward_slice S› have "n ∈ backward_slice S"
        by(rule dd_closed)
      with ‹sourcenode a = n› False have False by simp
      thus ?thesis by simp
    qed
  next
    case False
    from ‹V ∈ rv S n''› obtain xs nx where "n'' -xs→* nx"
      and "nx ∈ backward_slice S" and "V ∈ Use nx"
      and "∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'" by(erule rvE)
    from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹n'' -xs→* nx›
    have "n -a#xs→* nx" by -(rule path.Cons_path)
    from False ‹∀nx' ∈ set(sourcenodes xs). V ∉ Def nx'› ‹sourcenode a = n›
    have "∀nx' ∈ set(sourcenodes (a#xs)). V ∉ Def nx'"
      by(simp add:sourcenodes_def)
    with ‹n -a#xs→* nx› ‹nx ∈ backward_slice S› ‹V ∈ Use nx›
    have "V ∈ rv S n" by(rule rvI)
    show ?thesis
    proof(cases "kind a")
      case (Predicate Q)
      show ?thesis
      proof(cases "sourcenode a ∈ backward_slice S")
        case True
        with Predicate have "slice_kind S a = (Q)⇩√"
          by(simp add:slice_kind_in_slice)
        with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
        show ?thesis by simp
      next
        case False
        with Predicate obtain Q' where "slice_kind S a = (Q')⇩√" 
          by -(erule kind_Predicate_notin_slice_slice_kind_Predicate)
        with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
        show ?thesis by simp
      qed
    next
      case (Update f)
      show ?thesis
      proof(cases "sourcenode a ∈ backward_slice S")
        case True
        hence "slice_kind S a = kind a" by(rule slice_kind_in_slice)
        from Update have "pred (kind a) s" by simp
        with ‹valid_edge a› ‹sourcenode a = n› ‹V ∉ Def n›
        have "state_val (transfer (kind a) s) V = state_val s V"
          by(fastforce intro:CFG_edge_no_Def_equal)
        from Update have "pred (kind a) s'" by simp
        with ‹valid_edge a› ‹sourcenode a = n› ‹V ∉ Def n›
        have "state_val (transfer (kind a) s') V = state_val s' V"
          by(fastforce intro:CFG_edge_no_Def_equal)
        with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
          ‹state_val (transfer (kind a) s) V = state_val s V›
          ‹slice_kind S a = kind a›
        show ?thesis by fastforce
      next
        case False
        with Update have "slice_kind S a = ⇑id" by -(rule slice_kind_Upd)
        with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹V ∈ rv S n›
        show ?thesis by fastforce
      qed
    qed
  qed
qed



lemma rv_branching_edges_slice_kinds_False:
  assumes "valid_edge a" and "valid_edge ax" 
  and "sourcenode a = n" and "sourcenode ax = n"
  and "targetnode a = n''" and "targetnode ax ≠ n''"
  and "preds (slice_kinds S (a#as)) s" and "preds (slice_kinds S (ax#asx)) s'"
  and "∀V∈rv S n. state_val s V = state_val s' V"
  shows False
proof -
  from ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = n› ‹sourcenode ax = n›
    ‹targetnode a = n''› ‹targetnode ax ≠ n''›
  obtain Q Q' where "kind a = (Q)⇩√" and "kind ax = (Q')⇩√"
    and "∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)"
    by(auto dest:deterministic)
  from ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = n› ‹sourcenode ax = n›
    ‹targetnode a = n''› ‹targetnode ax ≠ n''›
  obtain P P' where "slice_kind S a = (P)⇩√" 
    and "slice_kind S ax = (P')⇩√"
    and "∀s. (P s ⟶ ¬ P' s) ∧ (P' s ⟶ ¬ P s)"
    by -(erule slice_deterministic,auto)
  show ?thesis
  proof(cases "sourcenode a ∈ backward_slice S")
    case True
    hence "slice_kind S a = kind a" by(rule slice_kind_in_slice)
    with ‹preds (slice_kinds S (a#as)) s› ‹kind a = (Q)⇩√› 
      ‹slice_kind S a = (P)⇩√› have "pred (kind a) s"
      by(simp add:slice_kinds_def)
    from True ‹sourcenode a = n› ‹sourcenode ax = n›
    have "slice_kind S ax = kind ax" by(fastforce simp:slice_kind_in_slice)
    with ‹preds (slice_kinds S (ax#asx)) s'› ‹kind ax = (Q')⇩√›
      ‹slice_kind S ax = (P')⇩√› have "pred (kind ax) s'" 
      by(simp add:slice_kinds_def)
    with ‹kind ax = (Q')⇩√› have "Q' s'" by simp
    from ‹valid_edge a› ‹sourcenode a = n› have "n -[]→* n"
      by(fastforce intro:empty_path)
    with True ‹sourcenode a = n› have "∀V ∈ Use n. V ∈ rv S n"
      by(fastforce intro:rvI simp:sourcenodes_def)
    with ‹∀V∈rv S n. state_val s V = state_val s' V› ‹sourcenode a = n›
    have "∀V ∈ Use (sourcenode a). state_val s V = state_val s' V" by blast
    with ‹valid_edge a› ‹pred (kind a) s› have "pred (kind a) s'"
      by(rule CFG_edge_Uses_pred_equal)
    with ‹kind a = (Q)⇩√› have "Q s'" by simp
    with ‹Q' s'› ‹∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s)› have False by simp
    thus ?thesis by simp
  next
    case False
    with ‹kind a = (Q)⇩√› ‹slice_kind S a = (P)⇩√›
    have "P = (λs. False) ∨ P = (λs. True)"
      by(fastforce elim:kind_Predicate_notin_slice_slice_kind_Predicate)
    with ‹slice_kind S a = (P)⇩√› ‹preds (slice_kinds S (a#as)) s›
    have "P = (λs. True)" by(fastforce simp:slice_kinds_def)
    from ‹kind ax = (Q')⇩√› ‹slice_kind S ax = (P')⇩√› 
      ‹sourcenode a = n› ‹sourcenode ax = n› False
    have "P' = (λs. False) ∨ P' = (λs. True)"
      by(fastforce elim:kind_Predicate_notin_slice_slice_kind_Predicate)
    with ‹slice_kind S ax = (P')⇩√› ‹preds (slice_kinds S (ax#asx)) s'›
    have "P' = (λs. True)" by(fastforce simp:slice_kinds_def)
    with ‹P = (λs. True)› ‹∀s. (P s ⟶ ¬ P' s) ∧ (P' s ⟶ ¬ P s)›
    have False by blast
    thus ?thesis by simp
  qed
qed



subsection ‹The set ‹WS››

inductive_set WS :: "'node set ⇒ (('node × 'state) × ('node × 'state)) set"
for S :: "'node set"
where WSI:"⟦obs n (backward_slice S) = obs n' (backward_slice S); 
            ∀V ∈ rv S n. state_val s V = state_val s' V;
            valid_node n; valid_node n'⟧
  ⟹ ((n,s),(n',s')) ∈ WS S"


lemma WSD:
  "((n,s),(n',s')) ∈ WS S 
  ⟹ obs n (backward_slice S) = obs n' (backward_slice S) ∧ 
      (∀V ∈ rv S n. state_val s V = state_val s' V) ∧
      valid_node n ∧ valid_node n'"
by(auto elim:WS.cases)


lemma WS_silent_move:
  assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S" and "S,kind ⊢ (n⇩1,s⇩1) -a→⇩τ (n⇩1',s⇩1')"
  and "obs n⇩1' (backward_slice S) ≠ {}" shows "((n⇩1',s⇩1'),(n⇩2,s⇩2)) ∈ WS S"
proof -
  from ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› have "valid_node n⇩1" and "valid_node n⇩2"
    by(auto dest:WSD)
  from ‹S,kind ⊢ (n⇩1,s⇩1) -a→⇩τ (n⇩1',s⇩1')› have "sourcenode a = n⇩1"
    and "targetnode a = n⇩1'" and "transfer (kind a) s⇩1 = s⇩1'"
    and "n⇩1 ∉ backward_slice S" and "valid_edge a" and "pred (kind a) s⇩1"
    by(auto elim:silent_move.cases)
  from ‹targetnode a = n⇩1'› ‹valid_edge a› have "valid_node n⇩1'"
    by(auto simp:valid_node_def)
  have "(∃m. obs n⇩1' (backward_slice S) = {m}) ∨ obs n⇩1' (backward_slice S) = {}"
    by(rule obs_singleton_disj)
  with ‹obs n⇩1' (backward_slice S) ≠ {}› obtain n 
    where "obs n⇩1' (backward_slice S) = {n}" by fastforce
  hence "n ∈ obs n⇩1' (backward_slice S)" by auto
  then obtain as where "n⇩1' -as→* n" 
    and "∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)" 
    and "n ∈ (backward_slice S)" by(erule obsE)
  from ‹n⇩1' -as→* n› ‹valid_edge a› ‹sourcenode a = n⇩1› ‹targetnode a = n⇩1'›
  have "n⇩1 -a#as→* n" by(rule Cons_path)
  moreover
  from ‹∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)› ‹sourcenode a = n⇩1›
    ‹n⇩1 ∉ backward_slice S› 
  have "∀nx ∈ set(sourcenodes (a#as)). nx ∉ (backward_slice S)"
    by(simp add:sourcenodes_def)
  ultimately have "n ∈ obs n⇩1 (backward_slice S)" using ‹n ∈ (backward_slice S)› 
    by(rule obs_elem)
  hence "obs n⇩1 (backward_slice S) = {n}" by(rule obs_singleton_element)
  with ‹obs n⇩1' (backward_slice S) = {n}› 
  have "obs n⇩1 (backward_slice S) = obs n⇩1' (backward_slice S)"
    by simp
  with ‹valid_node n⇩1› ‹valid_node n⇩1'› have "rv S n⇩1 = rv S n⇩1'"
    by(rule closed_eq_obs_eq_rvs)
  from ‹n ∈ obs n⇩1 (backward_slice S)› ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› 
  have "obs n⇩1 (backward_slice S) = obs n⇩2 (backward_slice S)"
    and "∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V"
    by(fastforce dest:WSD)+
  from ‹obs n⇩1 (backward_slice S) = obs n⇩2 (backward_slice S)›
    ‹obs n⇩1 (backward_slice S) = {n}› ‹obs n⇩1' (backward_slice S) = {n}› 
  have "obs n⇩1' (backward_slice S) = obs n⇩2 (backward_slice S)" by simp
  have "∀V ∈ rv S n⇩1'. state_val s⇩1' V = state_val s⇩2 V"
  proof
    fix V assume "V ∈ rv S n⇩1'"
    with ‹rv S n⇩1 = rv S n⇩1'› have "V ∈ rv S n⇩1" by simp
    then obtain as n' where "n⇩1 -as→* n'" and "n' ∈ (backward_slice S)"
      and "V ∈ Use n'" and "∀nx ∈ set(sourcenodes as). V ∉ Def nx"
      by(erule rvE)
    with ‹n⇩1 ∉ backward_slice S› have "V ∉ Def n⇩1"
      by(auto elim:path.cases simp:sourcenodes_def)
    with ‹valid_edge a› ‹sourcenode a = n⇩1› ‹pred (kind a) s⇩1›
    have "state_val (transfer (kind a) s⇩1) V = state_val s⇩1 V"
      by(fastforce intro:CFG_edge_no_Def_equal)
    with ‹transfer (kind a) s⇩1 = s⇩1'› have "state_val s⇩1' V = state_val s⇩1 V" by simp
    from ‹V ∈ rv S n⇩1› ‹∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V›
    have "state_val s⇩1 V = state_val s⇩2 V" by simp
    with ‹state_val s⇩1' V = state_val s⇩1 V› 
    show "state_val s⇩1' V = state_val s⇩2 V" by simp
  qed
  with ‹obs n⇩1' (backward_slice S) = obs n⇩2 (backward_slice S)›
    ‹valid_node n⇩1'› ‹valid_node n⇩2› show ?thesis by(fastforce intro:WSI)
qed


lemma WS_silent_moves:
  "⟦S,f ⊢ (n⇩1,s⇩1) =as⇒⇩τ (n⇩1',s⇩1'); ((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S; f = kind;
    obs n⇩1' (backward_slice S) ≠ {}⟧
  ⟹ ((n⇩1',s⇩1'),(n⇩2,s⇩2)) ∈ WS S"
proof(induct rule:silent_moves.induct)
  case silent_moves_Nil thus ?case by simp
next
  case (silent_moves_Cons S f n s a n' s' as n'' s'')
  note IH = ‹⟦((n',s'),(n⇩2,s⇩2)) ∈ WS S; f = kind; obs n'' (backward_slice S) ≠ {}⟧
             ⟹ ((n'',s''),(n⇩2,s⇩2)) ∈ WS S›
  from ‹S,f ⊢ (n',s') =as⇒⇩τ (n'',s'')› ‹obs n'' (backward_slice S) ≠ {}›
  have "obs n' (backward_slice S) ≠ {}" by(fastforce dest:silent_moves_obs_slice)
  with ‹((n,s),(n⇩2,s⇩2)) ∈ WS S› ‹S,f ⊢ (n,s) -a→⇩τ (n',s')› ‹f = kind›
  have "((n',s'),(n⇩2,s⇩2)) ∈ WS S" by -(rule WS_silent_move,simp+)
  from IH[OF this ‹f = kind› ‹obs n'' (backward_slice S) ≠ {}›]
  show ?case .
qed



lemma WS_observable_move:
  assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S" and "S,kind ⊢ (n⇩1,s⇩1) -a→ (n⇩1',s⇩1')"
  obtains as where "((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S a) s⇩2)) ∈ WS S"
  and "S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',transfer (slice_kind S a) s⇩2)"
proof(atomize_elim)
  from ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› have "valid_node n⇩1" by(auto dest:WSD)
  from ‹S,kind ⊢ (n⇩1,s⇩1) -a→ (n⇩1',s⇩1')› have [simp]:"n⇩1 = sourcenode a" 
    and [simp]:"n⇩1' = targetnode a" and "pred (kind a) s⇩1"
    and "transfer (kind a) s⇩1 = s⇩1'" and "n⇩1 ∈ (backward_slice S)" 
    and "valid_edge a" and "pred (kind a) s⇩1"
    by(auto elim:observable_move.cases)
  from  ‹valid_edge a› have "valid_node n⇩1'" by(auto simp:valid_node_def)
  from ‹valid_node n⇩1› ‹n⇩1 ∈ (backward_slice S)› 
  have "obs n⇩1 (backward_slice S) = {n⇩1}" by(rule n_in_obs)
  with ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› have "obs n⇩2 (backward_slice S) = {n⇩1}" 
    and "∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V" by(auto dest:WSD)
  from ‹valid_node n⇩1› have "n⇩1 -[]→* n⇩1" by(rule empty_path)
  with ‹n⇩1 ∈ (backward_slice S)› have "∀V ∈ Use n⇩1. V ∈ rv S n⇩1"
    by(fastforce intro:rvI simp:sourcenodes_def)
  with ‹∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V›
  have "∀V ∈ Use n⇩1. state_val s⇩1 V = state_val s⇩2 V" by blast
  with ‹valid_edge a›  ‹pred (kind a) s⇩1› have "pred (kind a) s⇩2"
    by(fastforce intro:CFG_edge_Uses_pred_equal)
  with ‹n⇩1 ∈ (backward_slice S)› have "pred (slice_kind S a) s⇩2"
    by(simp add:slice_kind_in_slice)
  from ‹n⇩1 ∈ (backward_slice S)› obtain s⇩2' 
    where "transfer (slice_kind S a) s⇩2 = s⇩2'"
    by(simp add:slice_kind_in_slice)
  with ‹pred (slice_kind S a) s⇩2› ‹n⇩1 ∈ (backward_slice S)› ‹valid_edge a› 
  have "S,slice_kind S ⊢ (n⇩1,s⇩2) -a→ (n⇩1',s⇩2')"
    by(fastforce intro:observable_moveI)
  from ‹obs n⇩2 (backward_slice S) = {n⇩1}›
  obtain as where "S,slice_kind S ⊢ (n⇩2,s⇩2) =as⇒⇩τ (n⇩1,s⇩2)"
    by(erule obs_silent_moves)
  with ‹S,slice_kind S ⊢ (n⇩1,s⇩2) -a→ (n⇩1',s⇩2')› 
  have "S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',s⇩2')"
    by -(rule observable_moves_snoc)
  have "∀V ∈ rv S n⇩1'. state_val s⇩1' V = state_val s⇩2' V"
  proof
    fix V assume rv:"V ∈ rv S n⇩1'"
    show "state_val s⇩1' V = state_val s⇩2' V"
    proof(cases "V ∈ Def n⇩1")
      case True
      thus ?thesis
      proof(cases "kind a")
        case (Update f)
        with ‹transfer (kind a) s⇩1 = s⇩1'› have "s⇩1' = f s⇩1" by simp
        from Update[THEN sym] ‹n⇩1 ∈ (backward_slice S)› 
        have "slice_kind S a = ⇑f"
          by(fastforce intro:slice_kind_in_slice)
        with ‹transfer (slice_kind S a) s⇩2 = s⇩2'› have "s⇩2' = f s⇩2" by simp
        from ‹valid_edge a› ‹∀V ∈ Use n⇩1. state_val s⇩1 V = state_val s⇩2 V›
          True Update ‹s⇩1' = f s⇩1› ‹s⇩2' = f s⇩2› show ?thesis
          by(fastforce dest:CFG_edge_transfer_uses_only_Use)
      next
        case (Predicate Q)
        with ‹transfer (kind a) s⇩1 = s⇩1'› have "s⇩1' = s⇩1" by simp
        from Predicate[THEN sym] ‹n⇩1 ∈ (backward_slice S)›
        have "slice_kind S a = (Q)⇩√"
          by(fastforce intro:slice_kind_in_slice)
        with ‹transfer (slice_kind S a) s⇩2 = s⇩2'› have "s⇩2' = s⇩2" by simp
        with ‹valid_edge a› ‹∀V ∈ Use n⇩1. state_val s⇩1 V = state_val s⇩2 V› 
          True Predicate ‹s⇩1' = s⇩1› ‹pred (kind a) s⇩1› ‹pred (kind a) s⇩2›
        show ?thesis by(auto dest:CFG_edge_transfer_uses_only_Use)
      qed
    next
      case False
      with ‹valid_edge a› ‹transfer (kind a) s⇩1 = s⇩1'›[THEN sym] 
        ‹pred (kind a) s⇩1› ‹pred (kind a) s⇩2›
      have "state_val s⇩1' V = state_val s⇩1 V"
        by(fastforce intro:CFG_edge_no_Def_equal)
      have "state_val s⇩2' V = state_val s⇩2 V"
      proof(cases "kind a")
        case (Update f)
        with  ‹n⇩1 ∈ (backward_slice S)› have "slice_kind S a = kind a"
          by(fastforce intro:slice_kind_in_slice)
        with ‹valid_edge a› ‹transfer (slice_kind S a) s⇩2 = s⇩2'›[THEN sym] 
          False ‹pred (kind a) s⇩2›
        show ?thesis by(fastforce intro:CFG_edge_no_Def_equal)
      next
        case (Predicate Q)
        with ‹transfer (slice_kind S a) s⇩2 = s⇩2'› have "s⇩2 = s⇩2'"
          by(cases "slice_kind S a",
            auto split:if_split_asm simp:slice_kind_def Let_def)
        thus ?thesis by simp
      qed
      from rv obtain as' nx where "n⇩1' -as'→* nx" 
        and "nx ∈ (backward_slice S)"
        and "V ∈ Use nx" and "∀nx ∈ set(sourcenodes as'). V ∉ Def nx"
        by(erule rvE)
      from ‹∀nx ∈ set(sourcenodes as'). V ∉ Def nx› False
      have "∀nx ∈ set(sourcenodes (a#as')). V ∉ Def nx"
        by(auto simp:sourcenodes_def)
      from  ‹valid_edge a› ‹n⇩1' -as'→* nx› have "n⇩1 -a#as'→* nx"
        by(fastforce intro:Cons_path)
      with ‹nx ∈ (backward_slice S)› ‹V ∈ Use nx› 
        ‹∀nx ∈ set(sourcenodes (a#as')). V ∉ Def nx›
      have "V ∈ rv S n⇩1" by -(rule rvI)
      with ‹∀V ∈ rv S n⇩1. state_val s⇩1 V = state_val s⇩2 V› 
        ‹state_val s⇩1' V = state_val s⇩1 V› ‹state_val s⇩2' V = state_val s⇩2 V›
      show ?thesis by fastforce
    qed
  qed
  with ‹valid_node n⇩1'› have "((n⇩1',s⇩1'),(n⇩1',s⇩2')) ∈ WS S" by(fastforce intro:WSI)
  with ‹S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',s⇩2')›
    ‹transfer (slice_kind S a) s⇩2 = s⇩2'› 
  show "∃as. ((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S a) s⇩2)) ∈ WS S ∧
    S,slice_kind S ⊢ (n⇩2,s⇩2) =as@[a]⇒ (n⇩1',transfer (slice_kind S a) s⇩2)"
    by blast
qed



definition is_weak_sim :: 
  "(('node × 'state) × ('node × 'state)) set ⇒ 'node set ⇒ bool"
  where "is_weak_sim R S ≡ 
  ∀n⇩1 s⇩1 n⇩2 s⇩2 n⇩1' s⇩1' as. ((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ R ∧ S,kind ⊢ (n⇩1,s⇩1) =as⇒ (n⇩1',s⇩1')
  ⟶ (∃n⇩2' s⇩2' as'. ((n⇩1',s⇩1'),(n⇩2',s⇩2')) ∈ R ∧ 
                      S,slice_kind S ⊢ (n⇩2,s⇩2) =as'⇒ (n⇩2',s⇩2'))"


lemma WS_weak_sim:
  assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S" 
  and "S,kind ⊢ (n⇩1,s⇩1) =as⇒ (n⇩1',s⇩1')"
  shows "((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S (last as)) s⇩2)) ∈ WS S ∧
  (∃as'. S,slice_kind S ⊢ (n⇩2,s⇩2) =as'@[last as]⇒ 
                             (n⇩1',transfer (slice_kind S (last as)) s⇩2))"
proof -
  from ‹S,kind ⊢ (n⇩1,s⇩1) =as⇒ (n⇩1',s⇩1')› obtain a' as' n' s'
    where "S,kind ⊢ (n⇩1,s⇩1) =as'⇒⇩τ (n',s')" 
    and "S,kind ⊢ (n',s') -a'→ (n⇩1',s⇩1')" and "as = as'@[a']"
    by(fastforce elim:observable_moves.cases)
  from ‹S,kind ⊢ (n',s') -a'→ (n⇩1',s⇩1')› have "obs n' (backward_slice S) = {n'}"
    by(fastforce elim:observable_move.cases intro!:n_in_obs)
  hence "obs n' (backward_slice S) ≠ {}" by fast
  with ‹S,kind ⊢ (n⇩1,s⇩1) =as'⇒⇩τ (n',s')› ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› 
  have "((n',s'),(n⇩2,s⇩2)) ∈ WS S"
    by -(rule WS_silent_moves,simp+)
  with ‹S,kind ⊢ (n',s') -a'→ (n⇩1',s⇩1')› obtain asx 
    where "((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S a') s⇩2)) ∈ WS S"
    and "S,slice_kind S ⊢ (n⇩2,s⇩2) =asx@[a']⇒ 
    (n⇩1',transfer (slice_kind S a') s⇩2)"
    by(fastforce elim:WS_observable_move)
  with ‹as = as'@[a']› show
    "((n⇩1',s⇩1'),(n⇩1',transfer (slice_kind S (last as)) s⇩2)) ∈ WS S ∧
    (∃as'. S,slice_kind S ⊢ (n⇩2,s⇩2) =as'@[last as]⇒ 
           (n⇩1',transfer (slice_kind S (last as)) s⇩2))" by simp blast
qed

text ‹The following lemma states the correctness of static intraprocedural slicing:\\
  the simulation ‹WS S› is a desired weak simulation›

theorem WS_is_weak_sim:"is_weak_sim (WS S) S"
by(fastforce dest:WS_weak_sim simp:is_weak_sim_def)


subsection ‹@{term "n -as→* n'"} and transitive closure of 
  @{term "S,f ⊢ (n,s) =as⇒⇩τ (n',s')"}›

inductive trans_observable_moves :: 
  "'node set ⇒ ('edge ⇒ 'state edge_kind) ⇒ 'node ⇒ 'state ⇒ 'edge list ⇒ 
  'node ⇒ 'state ⇒ bool" (‹_,_ ⊢ '(_,_') =_⇒* '(_,_')› [51,50,0,0,50,0,0] 51) 

where tom_Nil:
  "S,f ⊢ (n,s) =[]⇒* (n,s)"

| tom_Cons:
  "⟦S,f ⊢ (n,s) =as⇒ (n',s'); S,f ⊢ (n',s') =as'⇒* (n'',s'')⟧
  ⟹ S,f ⊢ (n,s) =(last as)#as'⇒* (n'',s'')"


definition slice_edges :: "'node set ⇒ 'edge list ⇒ 'edge list"
  where "slice_edges S as ≡ [a ← as. sourcenode a ∈ backward_slice S]"


lemma silent_moves_no_slice_edges:
  "S,f ⊢ (n,s) =as⇒⇩τ (n',s') ⟹ slice_edges S as = []"
by(induct rule:silent_moves.induct,auto elim:silent_move.cases simp:slice_edges_def)


lemma observable_moves_last_slice_edges:
  "S,f ⊢ (n,s) =as⇒ (n',s') ⟹ slice_edges S as = [last as]"
by(induct rule:observable_moves.induct,
   fastforce dest:silent_moves_no_slice_edges elim:observable_move.cases 
            simp:slice_edges_def)


lemma slice_edges_no_nodes_in_slice:
  "slice_edges S as = [] 
  ⟹ ∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)"
proof(induct as)
  case Nil thus ?case by(simp add:slice_edges_def sourcenodes_def)
next
  case (Cons a' as')
  note IH = ‹slice_edges S as' = [] ⟹
    ∀nx∈set (sourcenodes as'). nx ∉ backward_slice S›
  from ‹slice_edges S (a'#as') = []› have "slice_edges S as' = []"
    and "sourcenode a' ∉ backward_slice S"
    by(auto simp:slice_edges_def split:if_split_asm)
  from IH[OF ‹slice_edges S as' = []›] ‹sourcenode a' ∉ backward_slice S›
  show ?case by(simp add:sourcenodes_def)
qed



lemma sliced_path_determ:
  "⟦n -as→* n'; n -as'→* n'; slice_edges S as = slice_edges S as';
    preds (slice_kinds S as) s; preds (slice_kinds S as') s'; n' ∈ S;
    ∀V ∈ rv S n. state_val s V = state_val s' V⟧ ⟹ as = as'"
proof(induct arbitrary:as' s s' rule:path.induct)
  case (empty_path n)
  from ‹slice_edges S [] = slice_edges S as'› 
  have "∀nx ∈ set(sourcenodes as'). nx ∉ (backward_slice S)"
    by(fastforce intro!:slice_edges_no_nodes_in_slice simp:slice_edges_def)
  with ‹n -as'→* n› show ?case
  proof(induct nx≡"n" as' nx'≡"n" rule:path.induct)
    case (Cons_path n'' as a)
    from ‹valid_node n› ‹n ∈ S› have "n ∈ backward_slice S" by(rule refl)
    with ‹∀nx∈set (sourcenodes (a # as)). nx ∉ backward_slice S› 
      ‹sourcenode a = n›
    have False by(simp add:sourcenodes_def)
    thus ?case by simp
  qed simp
next
  case (Cons_path n'' as n' a n)
  note IH = ‹⋀as' s s'. ⟦n'' -as'→* n'; slice_edges S as = slice_edges S as';
    preds (slice_kinds S as) s; preds (slice_kinds S as') s'; n' ∈ S;
    ∀V∈rv S n''. state_val s V = state_val s' V⟧ ⟹ as = as'›
  show ?case
  proof(cases as')
    case Nil
    with ‹n -as'→* n'› have "n = n'" by fastforce
    from Nil ‹slice_edges S (a#as) = slice_edges S as'› ‹sourcenode a = n›
    have "n ∉ backward_slice S" by(fastforce simp:slice_edges_def)
    from ‹valid_edge a› ‹sourcenode a = n› ‹n = n'› ‹n' ∈ S›
    have "n ∈ backward_slice S" by(fastforce intro:refl)
    with ‹n = n'› ‹n ∉ backward_slice S› have False by simp
    thus ?thesis by simp
  next
    case (Cons ax asx)
    with ‹n -as'→* n'› have "n = sourcenode ax" and "valid_edge ax" 
      and "targetnode ax -asx→* n'" by(auto elim:path_split_Cons)
    show ?thesis
    proof(cases "targetnode ax = n''")
      case True
      with ‹targetnode ax -asx→* n'› have "n'' -asx→* n'" by simp
      from ‹valid_edge ax› ‹valid_edge a› ‹n = sourcenode ax› ‹sourcenode a = n›
        True ‹targetnode a = n''› have "ax = a" by(fastforce intro:edge_det)
      from ‹slice_edges S (a#as) = slice_edges S as'› Cons 
        ‹n = sourcenode ax› ‹sourcenode a = n›
      have "slice_edges S as = slice_edges S asx"
        by(cases "n ∈ backward_slice S")(auto simp:slice_edges_def)
      from ‹preds (slice_kinds S (a#as)) s› 
      have preds1:"preds (slice_kinds S as) (transfer (slice_kind S a) s)"
        by(simp add:slice_kinds_def)
      from ‹preds (slice_kinds S as') s'› Cons ‹ax = a›
      have preds2:"preds (slice_kinds S asx) (transfer (slice_kind S a) s')"
        by(simp add:slice_kinds_def)
      from ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''›
        ‹preds (slice_kinds S (a#as)) s› ‹preds (slice_kinds S as') s'›
        ‹ax = a› Cons ‹∀V∈rv S n. state_val s V = state_val s' V›
      have "∀V∈rv S n''. state_val (transfer (slice_kind S a) s) V =
                          state_val (transfer (slice_kind S a) s') V"
        by -(rule rv_edge_slice_kinds,auto)
      from IH[OF ‹n'' -asx→* n'› ‹slice_edges S as = slice_edges S asx›
        preds1 preds2 ‹n' ∈ S› this] Cons ‹ax = a› show ?thesis by simp
    next
      case False
      with ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = n› ‹n = sourcenode ax›
        ‹targetnode a = n''› ‹preds (slice_kinds S (a#as)) s›
        ‹preds (slice_kinds S as') s'› Cons
        ‹∀V∈rv S n. state_val s V = state_val s' V›
      have False by -(erule rv_branching_edges_slice_kinds_False,auto)
      thus ?thesis by simp
    qed
  qed
qed



lemma path_trans_observable_moves:
  assumes "n -as→* n'" and "preds (kinds as) s" and "transfers (kinds as) s = s'"
  obtains n'' s'' as' as'' where "S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')"
  and "S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',s')" 
  and "slice_edges S as = slice_edges S as''" and "n -as''@as'→* n'"
proof(atomize_elim)
  from ‹n -as→* n'› ‹preds (kinds as) s› ‹transfers (kinds as) s = s'›
  show "∃n'' s'' as' as''. 
    S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'') ∧
    S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',s') ∧ slice_edges S as = slice_edges S as'' ∧
    n -as''@as'→* n'"
  proof(induct arbitrary:s rule:path.induct)
    case (empty_path n)
    from ‹transfers (kinds []) s = s'› have "s = s'" by(simp add:kinds_def)
    have "S,kind ⊢ (n,s) =[]⇒* (n,s)" by(rule tom_Nil)
    have "S,kind ⊢ (n,s) =[]⇒⇩τ (n,s)" by(rule silent_moves_Nil)
    with ‹S,kind ⊢ (n,s) =[]⇒* (n,s)› ‹s = s'› ‹valid_node n›
    show ?case
      apply(rule_tac x="n" in exI)
      apply(rule_tac x="s" in exI)
      apply(rule_tac x="[]" in exI)
      apply(rule_tac x="[]" in exI)
      by(fastforce intro:path.empty_path simp:slice_edges_def)
  next
    case (Cons_path n'' as n' a n)
    note IH = ‹⋀s. ⟦preds (kinds as) s; transfers (kinds as) s = s'⟧
      ⟹ ∃nx s'' as' as''. S,kind ⊢ (n'',s) =slice_edges S as⇒* (nx,s'') ∧
            S,kind ⊢ (nx,s'') =as'⇒⇩τ (n',s') ∧ 
            slice_edges S as = slice_edges S as'' ∧ n'' -as''@as'→* n'›
    from ‹preds (kinds (a#as)) s› ‹transfers (kinds (a#as)) s = s'›
    have "preds (kinds as) (transfer (kind a) s)" 
      "transfers (kinds as) (transfer (kind a) s) = s'" by(simp_all add:kinds_def)
    from IH[OF this] obtain nx sx asx asx'
      where "S,kind ⊢ (n'',transfer (kind a) s) =slice_edges S as⇒* (nx,sx)"
      and "S,kind ⊢ (nx,sx) =asx⇒⇩τ (n',s')"
      and "slice_edges S as = slice_edges S asx'"
      and "n'' -asx'@asx→* n'"
      by clarsimp
    from ‹preds (kinds (a#as)) s› have "pred (kind a) s" by(simp add:kinds_def)
    show ?case
    proof(cases "n ∈ backward_slice S")
      case True
      with ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹pred (kind a) s›
      have "S,kind ⊢ (n,s) -a→ (n'',transfer (kind a) s)"
        by(fastforce intro:observable_moveI)
      hence "S,kind ⊢ (n,s) =[]@[a]⇒ (n'',transfer (kind a) s)"
        by(fastforce intro:observable_moves_snoc silent_moves_Nil)
      with ‹S,kind ⊢ (n'',transfer (kind a) s) =slice_edges S as⇒* (nx,sx)›
      have "S,kind ⊢ (n,s) =a#slice_edges S as⇒* (nx,sx)"
        by(fastforce dest:tom_Cons)
      with ‹S,kind ⊢ (nx,sx) =asx⇒⇩τ (n',s')›
        ‹slice_edges S as = slice_edges S asx'› ‹n'' -asx'@asx→* n'›
        ‹sourcenode a = n› ‹valid_edge a› ‹targetnode a = n''› True
      show ?thesis
        apply(rule_tac x="nx" in exI)
        apply(rule_tac x="sx" in exI)
        apply(rule_tac x="asx" in exI)
        apply(rule_tac x="a#asx'" in exI)
        by(auto intro:path.Cons_path simp:slice_edges_def)
    next
      case False
      with ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''› ‹pred (kind a) s›
      have "S,kind ⊢ (n,s) -a→⇩τ (n'',transfer (kind a) s)"
        by(fastforce intro:silent_moveI)
      from ‹S,kind ⊢ (n'',transfer (kind a) s) =slice_edges S as⇒* (nx,sx)›
      obtain f s'' asx'' where "S,f ⊢ (n'',s'') =asx''⇒* (nx,sx)"
        and "f = kind" and "s'' = transfer (kind a) s" 
        and "asx'' = slice_edges S as" by simp
      from ‹S,f ⊢ (n'',s'') =asx''⇒* (nx,sx)› ‹f = kind›
        ‹asx'' = slice_edges S as› ‹s'' = transfer (kind a) s›
        ‹S,kind ⊢ (n,s) -a→⇩τ (n'',transfer (kind a) s)› 
        ‹S,kind ⊢ (nx,sx) =asx⇒⇩τ (n',s')› ‹slice_edges S as = slice_edges S asx'›
        ‹n'' -asx'@asx→* n'› False
      show ?thesis
      proof(induct rule:trans_observable_moves.induct)
        case (tom_Nil S f ni si)
        have "S,kind ⊢ (n,s) =[]⇒* (n,s)" by(rule trans_observable_moves.tom_Nil)
        from ‹S,kind ⊢ (ni,si) =asx⇒⇩τ (n',s')›
          ‹S,kind ⊢ (n,s) -a→⇩τ (ni,transfer (kind a) s)› 
          ‹si = transfer (kind a) s›
        have "S,kind ⊢ (n,s) =a#asx⇒⇩τ (n',s')"
          by(fastforce intro:silent_moves_Cons)
        with ‹valid_edge a› ‹sourcenode a = n›
        have "n -a#asx→* n'" by(fastforce dest:silent_moves_preds_transfers_path)
        with ‹sourcenode a = n› ‹valid_edge a› ‹targetnode a = n''›
          ‹[] = slice_edges S as› ‹n ∉ backward_slice S›
          ‹S,kind ⊢ (n,s) =a#asx⇒⇩τ (n',s')›
        show ?case
          apply(rule_tac x="n" in exI)
          apply(rule_tac x="s" in exI)
          apply(rule_tac x="a#asx" in exI)
          apply(rule_tac x="[]" in exI)
          by(fastforce simp:slice_edges_def intro:trans_observable_moves.tom_Nil)
      next
        case (tom_Cons S f ni si asi ni' si' asi' n'' s'')
        from ‹S,f ⊢ (ni,si) =asi⇒ (ni',si')› have "asi ≠ []"
          by(fastforce dest:observable_move_notempty)
        from ‹S,kind ⊢ (n,s) -a→⇩τ (ni,transfer (kind a) s)›
        have "valid_edge a" and "sourcenode a = n" and "targetnode a = ni"
          by(auto elim:silent_move.cases)
        from ‹S,kind ⊢ (n,s) -a→⇩τ (ni,transfer (kind a) s)› ‹f = kind›
          ‹si = transfer (kind a) s› ‹S,f ⊢ (ni,si) =asi⇒ (ni',si')›
        have "S,f ⊢ (n,s) =a#asi⇒ (ni',si')"
          by(fastforce intro:silent_move_observable_moves)
        with ‹S,f ⊢ (ni',si') =asi'⇒* (n'',s'')›
        have "S,f ⊢ (n,s) =(last (a#asi))#asi'⇒* (n'',s'')"
          by -(rule trans_observable_moves.tom_Cons)
        with ‹f = kind› ‹last asi # asi' = slice_edges S as› ‹n ∉ backward_slice S›
          ‹S,kind ⊢ (n'',s'') =asx⇒⇩τ (n',s')›  ‹sourcenode a = n› ‹asi ≠ []›
          ‹ni -asx'@asx→* n'› ‹slice_edges S as = slice_edges S asx'›
          ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = ni›
        show ?case
          apply(rule_tac x="n''" in exI)
          apply(rule_tac x="s''" in exI)
          apply(rule_tac x="asx" in exI)
          apply(rule_tac x="a#asx'" in exI)
          by(auto intro:path.Cons_path simp:slice_edges_def)
      qed
    qed
  qed
qed


lemma WS_weak_sim_trans:
  assumes "((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S"
  and "S,kind ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')" and "as ≠ []"
  shows "((n⇩1',s⇩1'),(n⇩1',transfers (slice_kinds S as) s⇩2)) ∈ WS S ∧ 
         S,slice_kind S ⊢ (n⇩2,s⇩2) =as⇒* (n⇩1',transfers (slice_kinds S as) s⇩2)"
proof -
  obtain f where "f = kind" by simp
  with ‹S,kind ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')› 
  have "S,f ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')" by simp
  from ‹S,f ⊢ (n⇩1,s⇩1) =as⇒* (n⇩1',s⇩1')› ‹((n⇩1,s⇩1),(n⇩2,s⇩2)) ∈ WS S› ‹as ≠ []› ‹f = kind›
  show "((n⇩1',s⇩1'),(n⇩1',transfers (slice_kinds S as) s⇩2)) ∈ WS S ∧
    S,slice_kind S ⊢ (n⇩2,s⇩2) =as⇒* (n⇩1',transfers (slice_kinds S as) s⇩2)"
  proof(induct arbitrary:n⇩2 s⇩2 rule:trans_observable_moves.induct)
    case tom_Nil thus ?case by simp
  next
    case (tom_Cons S f n s as n' s' as' n'' s'')
    note IH = ‹⋀n⇩2 s⇩2. ⟦((n',s'),(n⇩2,s⇩2)) ∈ WS S; as' ≠ []; f = kind⟧
      ⟹ ((n'',s''),(n'',transfers (slice_kinds S as') s⇩2)) ∈ WS S ∧
      S,slice_kind S ⊢ (n⇩2,s⇩2) =as'⇒* (n'',transfers (slice_kinds S as') s⇩2)›
    from ‹S,f ⊢ (n,s) =as⇒ (n',s')›
    obtain asx ax nx sx where "S,f ⊢ (n,s) =asx⇒⇩τ (nx,sx)"
      and "S,f ⊢ (nx,sx) -ax→ (n',s')" and "as = asx@[ax]"
      by(fastforce elim:observable_moves.cases)
    from ‹S,f ⊢ (nx,sx) -ax→ (n',s')› have "obs nx (backward_slice S) = {nx}"
      by(fastforce intro!:n_in_obs elim:observable_move.cases)
    with ‹S,f ⊢ (n,s) =asx⇒⇩τ (nx,sx)› ‹((n,s),(n⇩2,s⇩2)) ∈ WS S› ‹f = kind›
    have "((nx,sx),(n⇩2,s⇩2)) ∈ WS S" by(fastforce intro:WS_silent_moves)
    with ‹S,f ⊢ (nx,sx) -ax→ (n',s')› ‹f = kind›
    obtain asx' where "((n',s'),(n',transfer (slice_kind S ax) s⇩2)) ∈ WS S"
      and "S,slice_kind S ⊢ (n⇩2,s⇩2) =asx'@[ax]⇒ 
      (n',transfer (slice_kind S ax) s⇩2)"
      by(fastforce elim:WS_observable_move)
    show ?case
    proof(cases "as' = []")
      case True
      with ‹S,f ⊢ (n',s') =as'⇒* (n'',s'')› have "n' = n'' ∧ s' = s''"
        by(fastforce elim:trans_observable_moves.cases dest:observable_move_notempty)
      from ‹S,slice_kind S ⊢ (n⇩2,s⇩2) =asx'@[ax]⇒ 
                               (n',transfer (slice_kind S ax) s⇩2)›
      have "S,slice_kind S ⊢ (n⇩2,s⇩2) =(last (asx'@[ax]))#[]⇒* 
                               (n',transfer (slice_kind S ax) s⇩2)"
        by(fastforce intro:trans_observable_moves.intros)
      with ‹((n',s'),(n',transfer (slice_kind S ax) s⇩2)) ∈ WS S› ‹as = asx@[ax]›
        ‹n' = n'' ∧ s' = s''› True
      show ?thesis by(fastforce simp:slice_kinds_def)
    next
      case False
      from IH[OF ‹((n',s'),(n',transfer (slice_kind S ax) s⇩2)) ∈ WS S› this 
        ‹f = kind›]
      have "((n'',s''),(n'',transfers (slice_kinds S as') 
        (transfer (slice_kind S ax) s⇩2))) ∈ WS S"
        and "S,slice_kind S ⊢ (n',transfer (slice_kind S ax) s⇩2) 
        =as'⇒* (n'',transfers (slice_kinds S as')
                     (transfer (slice_kind S ax) s⇩2))" by simp_all
      with ‹S,slice_kind S ⊢ (n⇩2,s⇩2) =asx'@[ax]⇒ 
                               (n',transfer (slice_kind S ax) s⇩2)›
      have "S,slice_kind S ⊢ (n⇩2,s⇩2) =(last (asx'@[ax]))#as'⇒* 
        (n'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s⇩2))"
        by(fastforce intro:trans_observable_moves.tom_Cons)
      with ‹((n'',s''),(n'',transfers (slice_kinds S as') 
        (transfer (slice_kind S ax) s⇩2))) ∈ WS S› False ‹as = asx@[ax]›
      show ?thesis by(fastforce simp:slice_kinds_def)
    qed
  qed
qed


lemma transfers_slice_kinds_slice_edges:
  "transfers (slice_kinds S (slice_edges S as)) s = transfers (slice_kinds S as) s"
proof(induct as arbitrary:s)
  case Nil thus ?case by(simp add:slice_kinds_def slice_edges_def)
next
  case (Cons a' as')
  note IH = ‹⋀s. transfers (slice_kinds S (slice_edges S as')) s =
                  transfers (slice_kinds S as') s›
  show ?case
  proof(cases "sourcenode a' ∈ backward_slice S")
    case True
    hence eq:"transfers (slice_kinds S (slice_edges S (a'#as'))) s
            = transfers (slice_kinds S (slice_edges S as')) 
                (transfer (slice_kind S a') s)"
      by(simp add:slice_edges_def slice_kinds_def)
    have "transfers (slice_kinds S (a'#as')) s
        = transfers (slice_kinds S as') (transfer (slice_kind S a') s)"
      by(simp add:slice_kinds_def)
    with eq IH[of "transfer (slice_kind S a') s"] show ?thesis by simp
  next
    case False
    hence eq:"transfers (slice_kinds S (slice_edges S (a'#as'))) s
            = transfers (slice_kinds S (slice_edges S as')) s"
      by(simp add:slice_edges_def slice_kinds_def)
    from False have "transfer (slice_kind S a') s = s"
      by(cases "kind a'",auto simp:slice_kind_def Let_def)
    hence "transfers (slice_kinds S (a'#as')) s
         = transfers (slice_kinds S as') s"
      by(simp add:slice_kinds_def)
    with eq IH[of s] show ?thesis by simp
  qed
qed


lemma trans_observable_moves_preds:
  assumes "S,f ⊢ (n,s) =as⇒* (n',s')" and "valid_node n"
  obtains as' where "preds (map f as') s" and "slice_edges S as' = as"
  and "n -as'→* n'"
proof(atomize_elim)
  from ‹S,f ⊢ (n,s) =as⇒* (n',s')› ‹valid_node n›
  show "∃as'. preds (map f as') s ∧ slice_edges S as' = as ∧ n -as'→* n'"
  proof(induct rule:trans_observable_moves.induct)
    case tom_Nil thus ?case 
      by(rule_tac x="[]" in exI,fastforce intro:empty_path simp:slice_edges_def)
  next
    case (tom_Cons S f n s as n' s' as' n'' s'')
    note IH = ‹valid_node n' 
      ⟹ ∃asx. preds (map f asx) s' ∧ slice_edges S asx = as' ∧ n' -asx→* n''›
    from ‹S,f ⊢ (n,s) =as⇒ (n',s')›
    have "preds (map f as) s" and "transfers (map f as) s = s'"
      and "n -as→* n'"
      by(fastforce dest:observable_moves_preds_transfers_path)+
    from ‹n -as→* n'› have "valid_node n'" by(fastforce dest:path_valid_node)
    from ‹S,f ⊢ (n,s) =as⇒ (n',s')› have "slice_edges S as = [last as]"
      by(rule observable_moves_last_slice_edges)
    from IH[OF ‹valid_node n'›]
    obtain asx where "preds (map f asx) s'" and "slice_edges S asx = as'"
      and "n' -asx→* n''"
      by blast
    from ‹n -as→* n'› ‹n' -asx→* n''› have "n -as@asx→* n''" by(rule path_Append)
    from ‹preds (map f asx) s'› ‹transfers (map f as) s = s'›[THEN sym]
      ‹preds (map f as) s›
    have "preds (map f (as@asx)) s" by(simp add:preds_split)
    with ‹slice_edges S as = [last as]› ‹slice_edges S asx = as'› 
      ‹n -as@asx→* n''› show ?case
      by(rule_tac x="as@asx" in exI,auto simp:slice_edges_def)
  qed
qed



lemma exists_sliced_path_preds:
  assumes "n -as→* n'" and "slice_edges S as = []" and "n' ∈ backward_slice S"
  obtains as' where "n -as'→* n'" and "preds (slice_kinds S as') s"
  and "slice_edges S as' = []"
proof(atomize_elim)
  from ‹slice_edges S as = []›
  have "∀nx ∈ set(sourcenodes as). nx ∉ (backward_slice S)"
    by(rule slice_edges_no_nodes_in_slice)
  with ‹n -as→* n'› ‹n' ∈ backward_slice S› have "n' ∈ obs n (backward_slice S)"
    by -(rule obs_elem)
  hence "obs n (backward_slice S) = {n'}" by(rule obs_singleton_element)
  from ‹n -as→* n'› have "valid_node n" and "valid_node n'"
    by(fastforce dest:path_valid_node)+
  from ‹n -as→* n'› obtain x where "distance n n' x" and "x ≤ length as"
    by(erule every_path_distance)
  from ‹distance n n' x› ‹obs n (backward_slice S) = {n'}›
  show "∃as'. n -as'→* n' ∧ preds (slice_kinds S as') s ∧ 
              slice_edges S as' = []"
  proof(induct x arbitrary:n rule:nat.induct)
    case zero
    from ‹distance n n' 0› have "n = n'" by(fastforce elim:distance.cases)
    with ‹valid_node n'› show ?case
      by(rule_tac x="[]" in exI,
        auto intro:empty_path simp:slice_kinds_def slice_edges_def)
  next
    case (Suc x)
    note IH = ‹⋀n. ⟦distance n n' x; obs n (backward_slice S) = {n'}⟧
      ⟹ ∃as'. n -as'→* n' ∧ preds (slice_kinds S as') s ∧ 
               slice_edges S as' = []›
    from ‹distance n n' (Suc x)› obtain a 
      where "valid_edge a" and "n = sourcenode a" 
      and "distance (targetnode a) n' x"
      and target:"targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
      distance (targetnode a') n' x ∧
      valid_edge a' ∧ targetnode a' = nx)"
      by(auto elim:distance_successor_distance)
    have "n ∉ backward_slice S"
    proof
      assume "n ∈ backward_slice S"
      from ‹valid_edge a› ‹n = sourcenode a› have "valid_node n" by simp
      with ‹n ∈ backward_slice S› have "obs n (backward_slice S) = {n}"
        by -(rule n_in_obs)
      with ‹obs n (backward_slice S) = {n'}› have "n = n'" by simp
      with ‹valid_node n› have "n -[]→* n'" by(fastforce intro:empty_path)
      with ‹distance n n' (Suc x)› show False
        by(fastforce elim:distance.cases)
    qed
    from ‹distance (targetnode a) n' x› ‹n' ∈ backward_slice S›
    obtain m where "m ∈ obs (targetnode a) (backward_slice S)"
      by(fastforce elim:distance.cases path_ex_obs)
    from ‹valid_edge a› ‹n ∉ backward_slice S› ‹n = sourcenode a›
    have "obs (targetnode a) (backward_slice S) ⊆ 
      obs (sourcenode a) (backward_slice S)"
      by -(rule edge_obs_subset,auto)
    with ‹m ∈ obs (targetnode a) (backward_slice S)› ‹n = sourcenode a›
      ‹obs n (backward_slice S) = {n'}›
    have "n' ∈ obs (targetnode a) (backward_slice S)" by auto
    hence "obs (targetnode a) (backward_slice S) = {n'}" 
      by(rule obs_singleton_element)
    from IH[OF ‹distance (targetnode a) n' x› this]
    obtain as where "targetnode a -as→* n'" and "preds (slice_kinds S as) s"
      and "slice_edges S as = []" by blast
    from ‹targetnode a -as→* n'› ‹valid_edge a› ‹n = sourcenode a›
    have "n -a#as→* n'" by(fastforce intro:Cons_path)
    from ‹slice_edges S as = []› ‹n ∉ backward_slice S› ‹n = sourcenode a›
    have "slice_edges S (a#as) = []" by(simp add:slice_edges_def)
    show ?case
    proof(cases "kind a")
      case (Update f)
      with ‹n ∉ backward_slice S› ‹n = sourcenode a› have "slice_kind S a = ⇑id"
        by(fastforce intro:slice_kind_Upd)
      hence "transfer (slice_kind S a) s = s" and "pred (slice_kind S a) s"
        by simp_all
      with ‹preds (slice_kinds S as) s› have "preds (slice_kinds S (a#as)) s"
        by(simp add:slice_kinds_def)
      with ‹n -a#as→* n'› ‹slice_edges S (a#as) = []› show ?thesis
        by blast
    next
      case (Predicate Q)
      with ‹n ∉ backward_slice S› ‹n = sourcenode a› ‹distance n n' (Suc x)›  
        ‹obs n (backward_slice S) = {n'}› ‹distance (targetnode a) n' x›
        ‹targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
        distance (targetnode a') n' x ∧
        valid_edge a' ∧ targetnode a' = nx)›
      have "slice_kind S a = (λs. True)⇩√"
        by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
      hence "transfer (slice_kind S a) s = s" and "pred (slice_kind S a) s"
        by simp_all
      with ‹preds (slice_kinds S as) s› have "preds (slice_kinds S (a#as)) s"
        by(simp add:slice_kinds_def)
      with ‹n -a#as→* n'› ‹slice_edges S (a#as) = []› show ?thesis by blast
    qed
  qed
qed


theorem fundamental_property_of_static_slicing:
  assumes path:"n -as→* n'" and preds:"preds (kinds as) s" and "n' ∈ S"
  obtains as' where "preds (slice_kinds S as') s"
  and "(∀V ∈ Use n'. state_val (transfers (slice_kinds S as') s) V = 
                     state_val (transfers (kinds as) s) V)"
  and "slice_edges S as = slice_edges S as'" and "n -as'→* n'"
proof(atomize_elim)
  from path preds obtain n'' s'' as' as''
    where "S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')"
    and "S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)"
    and "slice_edges S as = slice_edges S as''"
    and "n -as''@as'→* n'"
    by -(erule_tac S="S" in path_trans_observable_moves,auto)
  from path have "valid_node n" and "valid_node n'" 
    by(fastforce dest:path_valid_node)+
  from ‹valid_node n› have "((n,s),(n,s)) ∈ WS S" by(fastforce intro:WSI)
  from ‹valid_node n'› ‹n' ∈ S› have "obs n' (backward_slice S) = {n'}"
    by(fastforce intro!:n_in_obs refl)
  from ‹valid_node n'› have "n'-[]→* n'" by(fastforce intro:empty_path)
  with ‹valid_node n'› ‹n' ∈ S› have "∀V ∈ Use n'. V ∈ rv S n'"
    by(fastforce intro:rvI refl simp:sourcenodes_def)
  show "∃as'. preds (slice_kinds S as') s ∧
    (∀V ∈ Use n'. state_val (transfers (slice_kinds S as') s) V = 
                  state_val (transfers (kinds as) s) V) ∧
    slice_edges S as = slice_edges S as' ∧ n -as'→* n'"
  proof(cases "slice_edges S as = []")
    case True
    hence "preds (slice_kinds S []) s" and "slice_edges S [] = slice_edges S as"
      by(simp_all add:slice_kinds_def slice_edges_def)
    from ‹S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')› True
    have "n = n''" and "s = s''"
      by(fastforce elim:trans_observable_moves.cases)+
    with ‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
    have "S,kind ⊢ (n,s) =as'⇒⇩τ (n',transfers (kinds as) s)" by simp
    with ‹valid_node n› have "n -as'→* n'"
      by(fastforce dest:silent_moves_preds_transfers_path)
    from ‹S,kind ⊢ (n,s) =as'⇒⇩τ (n',transfers (kinds as) s)›
    have "slice_edges S as' = []" by(fastforce dest:silent_moves_no_slice_edges)
    with ‹n -as'→* n'› ‹valid_node n'› ‹n' ∈ S› obtain asx
      where "n -asx→* n'" and "preds (slice_kinds S asx) s"
      and "slice_edges S asx = []"
      by -(erule exists_sliced_path_preds,auto intro:refl)
    from ‹S,kind ⊢ (n,s) =as'⇒⇩τ (n',transfers (kinds as) s)›
      ‹((n,s),(n,s)) ∈ WS S› ‹obs n' (backward_slice S) = {n'}›
    have "((n',transfers (kinds as) s),(n,s)) ∈ WS S"
      by(fastforce intro:WS_silent_moves)
    with True have "∀V ∈ rv S n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S (slice_edges S as)) s) V"
      by(fastforce dest:WSD simp:slice_edges_def slice_kinds_def)
    with ‹∀V ∈ Use n'. V ∈ rv S n'›
    have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S (slice_edges S as)) s) V" by simp
    with ‹slice_edges S asx = []› ‹slice_edges S [] = slice_edges S as›
    have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S (slice_edges S asx)) s) V"
      by(simp add:slice_edges_def)
    hence "∀V ∈ Use n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S asx) s) V"
      by(simp add:transfers_slice_kinds_slice_edges)
    with ‹n -asx→* n'› ‹preds (slice_kinds S asx) s›
      ‹slice_edges S asx = []› ‹slice_edges S [] = slice_edges S as›
    show ?thesis
      by(rule_tac x="asx" in exI,simp add:slice_edges_def)
  next
    case False
    with ‹S,kind ⊢ (n,s) =slice_edges S as⇒* (n'',s'')› ‹((n,s),(n,s)) ∈ WS S›
    have "((n'',s''),(n'',transfers (slice_kinds S (slice_edges S as)) s)) ∈ WS S"
      "S,slice_kind S ⊢ (n,s) =slice_edges S as⇒* 
      (n'',transfers (slice_kinds S (slice_edges S as)) s)"
      by(fastforce dest:WS_weak_sim_trans)+
    from ‹S,slice_kind S ⊢ (n,s) =slice_edges S as⇒* 
                             (n'',transfers (slice_kinds S (slice_edges S as)) s)›
      ‹valid_node n›
    obtain asx where "preds (slice_kinds S asx) s" 
      and "slice_edges S asx = slice_edges S as"
      and "n -asx→* n''"
      by(fastforce elim:trans_observable_moves_preds simp:slice_kinds_def)
    from ‹n -asx→* n''› have "valid_node n''" by(fastforce dest:path_valid_node)
    with ‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
    have "n'' -as'→* n'"
      by(fastforce dest:silent_moves_preds_transfers_path)
    from ‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
    have "slice_edges S as' = []" by(fastforce dest:silent_moves_no_slice_edges)
    with ‹n'' -as'→* n'› ‹valid_node n'› ‹n' ∈ S› obtain asx'
      where "n'' -asx'→* n'" and "slice_edges S asx' = []"
      and "preds (slice_kinds S asx') (transfers (slice_kinds S asx) s)"
      by -(erule exists_sliced_path_preds,auto intro:refl)
    from ‹n -asx→* n''› ‹n'' -asx'→* n'› have "n -asx@asx'→* n'"
      by(rule path_Append)
    from ‹slice_edges S asx = slice_edges S as› ‹slice_edges S asx' = []›
    have "slice_edges S as = slice_edges S (asx@asx')"
      by(auto simp:slice_edges_def)
    from ‹preds (slice_kinds S asx') (transfers (slice_kinds S asx) s)›
      ‹preds (slice_kinds S asx) s›
    have "preds (slice_kinds S (asx@asx')) s" 
      by(simp add:slice_kinds_def preds_split)
    from ‹obs n' (backward_slice S) = {n'}›
      ‹S,kind ⊢ (n'',s'') =as'⇒⇩τ (n',transfers (kinds as) s)›
      ‹((n'',s''),(n'',transfers (slice_kinds S (slice_edges S as)) s)) ∈ WS S›
    have "((n',transfers (kinds as) s),
      (n'',transfers (slice_kinds S (slice_edges S as)) s)) ∈ WS S"
      by(fastforce intro:WS_silent_moves)
    hence "∀V ∈ rv S n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S (slice_edges S as)) s) V"
      by(fastforce dest:WSD)
    with ‹∀V ∈ Use n'. V ∈ rv S n'› ‹slice_edges S asx = slice_edges S as›
    have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S (slice_edges S asx)) s) V"
      by fastforce
    with ‹slice_edges S asx' = []›
    have "∀V ∈ Use n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S (slice_edges S (asx@asx'))) s) V"
      by(auto simp:slice_edges_def)
    hence "∀V ∈ Use n'. state_val (transfers (kinds as) s) V = 
      state_val (transfers (slice_kinds S (asx@asx')) s) V"
      by(simp add:transfers_slice_kinds_slice_edges)
    with ‹preds (slice_kinds S (asx@asx')) s› ‹n -asx@asx'→* n'›
      ‹slice_edges S as = slice_edges S (asx@asx')›
    show ?thesis by simp blast
  qed
qed


end


subsection ‹The fundamental property of (static) slicing related to the semantics›

locale BackwardSlice_wf = 
  BackwardSlice sourcenode targetnode kind valid_edge Entry Def Use state_val 
  backward_slice +
  CFG_semantics_wf sourcenode targetnode kind valid_edge Entry sem identifies
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" (‹'('_Entry'_')›) and Def :: "'node ⇒ 'var set"
  and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
  and backward_slice :: "'node set ⇒ 'node set" 
  and sem :: "'com ⇒ 'state ⇒ 'com ⇒ 'state ⇒ bool" 
    (‹((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))› [0,0,0,0] 81)
  and identifies :: "'node ⇒ 'com ⇒ bool" (‹_ ≜ _› [51, 0] 80)

begin


theorem fundamental_property_of_path_slicing_semantically:
  assumes "n ≜ c" and "⟨c,s⟩ ⇒ ⟨c',s'⟩"
  obtains n' as where "n -as→* n'" and "preds (slice_kinds {n'} as) s" and "n' ≜ c'"
  and "∀V ∈ Use n'. state_val (transfers (slice_kinds {n'} as) s) V = state_val s' V"
proof(atomize_elim)
  from ‹n ≜ c› ‹⟨c,s⟩ ⇒ ⟨c',s'⟩› obtain n' as where "n -as→* n'"
    and "transfers (kinds as) s = s'" and "preds (kinds as) s" and "n' ≜ c'"
    by(fastforce dest:fundamental_property)
  from ‹n -as→* n'› ‹preds (kinds as) s› obtain as'
    where "preds (slice_kinds {n'} as') s"
    and vals:"∀V ∈ Use n'. state_val (transfers (slice_kinds {n'} as') s) V = 
    state_val (transfers (kinds as) s) V" and "n -as'→* n'"
    by -(erule fundamental_property_of_static_slicing,auto)
  from ‹transfers (kinds as) s = s'› vals have "∀V ∈ Use n'.
    state_val (transfers (slice_kinds {n'} as') s) V = state_val s' V"
    by simp
  with ‹preds (slice_kinds {n'} as') s› ‹n -as'→* n'› ‹ n' ≜ c'›
  show "∃as n'. n -as→* n' ∧ preds (slice_kinds {n'} as) s ∧ n' ≜ c' ∧
    (∀V∈Use n'. state_val (transfers (slice_kinds {n'} as) s) V = state_val s' V)"
    by blast
qed


end

end