Theory Slicing.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 "nxset (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'' nxset (sourcenodes as). x  Def nx 
  have "niset (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'. niset (sourcenodes asx'). ni  backward_slice S; 
      n' -asx'→* nx 
         niset (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 niset (sourcenodes (ax'#asx')). ni  backward_slice S
    have all:"niset (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 "niset (sourcenodes asx'). x  Def ni" .
    with niset (sourcenodes as''). x  Def ni
    have "niset (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 niset (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 niset (sourcenodes (asx'@as'')). x  Def ni
    show ?case by(simp add:sourcenodes_def)
  qed
  with niset (sourcenodes as''). x  Def ni 
  have "niset (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 
    niset (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 "Vrv 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 "Vrv 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 Vrv 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 Vrv 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 Vrv 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 Vrv 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 Vrv 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 "Vrv 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 Vrv 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 "((n1,s1),(n2,s2))  WS S" and "S,kind  (n1,s1) -aτ (n1',s1')"
  and "obs n1' (backward_slice S)  {}" shows "((n1',s1'),(n2,s2))  WS S"
proof -
  from ((n1,s1),(n2,s2))  WS S have "valid_node n1" and "valid_node n2"
    by(auto dest:WSD)
  from S,kind  (n1,s1) -aτ (n1',s1') have "sourcenode a = n1"
    and "targetnode a = n1'" and "transfer (kind a) s1 = s1'"
    and "n1  backward_slice S" and "valid_edge a" and "pred (kind a) s1"
    by(auto elim:silent_move.cases)
  from targetnode a = n1' valid_edge a have "valid_node n1'"
    by(auto simp:valid_node_def)
  have "(m. obs n1' (backward_slice S) = {m})  obs n1' (backward_slice S) = {}"
    by(rule obs_singleton_disj)
  with obs n1' (backward_slice S)  {} obtain n 
    where "obs n1' (backward_slice S) = {n}" by fastforce
  hence "n  obs n1' (backward_slice S)" by auto
  then obtain as where "n1' -as→* n" 
    and "nx  set(sourcenodes as). nx  (backward_slice S)" 
    and "n  (backward_slice S)" by(erule obsE)
  from n1' -as→* n valid_edge a sourcenode a = n1 targetnode a = n1'
  have "n1 -a#as→* n" by(rule Cons_path)
  moreover
  from nx  set(sourcenodes as). nx  (backward_slice S) sourcenode a = n1
    n1  backward_slice S 
  have "nx  set(sourcenodes (a#as)). nx  (backward_slice S)"
    by(simp add:sourcenodes_def)
  ultimately have "n  obs n1 (backward_slice S)" using n  (backward_slice S) 
    by(rule obs_elem)
  hence "obs n1 (backward_slice S) = {n}" by(rule obs_singleton_element)
  with obs n1' (backward_slice S) = {n} 
  have "obs n1 (backward_slice S) = obs n1' (backward_slice S)"
    by simp
  with valid_node n1 valid_node n1' have "rv S n1 = rv S n1'"
    by(rule closed_eq_obs_eq_rvs)
  from n  obs n1 (backward_slice S) ((n1,s1),(n2,s2))  WS S 
  have "obs n1 (backward_slice S) = obs n2 (backward_slice S)"
    and "V  rv S n1. state_val s1 V = state_val s2 V"
    by(fastforce dest:WSD)+
  from obs n1 (backward_slice S) = obs n2 (backward_slice S)
    obs n1 (backward_slice S) = {n} obs n1' (backward_slice S) = {n} 
  have "obs n1' (backward_slice S) = obs n2 (backward_slice S)" by simp
  have "V  rv S n1'. state_val s1' V = state_val s2 V"
  proof
    fix V assume "V  rv S n1'"
    with rv S n1 = rv S n1' have "V  rv S n1" by simp
    then obtain as n' where "n1 -as→* n'" and "n'  (backward_slice S)"
      and "V  Use n'" and "nx  set(sourcenodes as). V  Def nx"
      by(erule rvE)
    with n1  backward_slice S have "V  Def n1"
      by(auto elim:path.cases simp:sourcenodes_def)
    with valid_edge a sourcenode a = n1 pred (kind a) s1
    have "state_val (transfer (kind a) s1) V = state_val s1 V"
      by(fastforce intro:CFG_edge_no_Def_equal)
    with transfer (kind a) s1 = s1' have "state_val s1' V = state_val s1 V" by simp
    from V  rv S n1 V  rv S n1. state_val s1 V = state_val s2 V
    have "state_val s1 V = state_val s2 V" by simp
    with state_val s1' V = state_val s1 V 
    show "state_val s1' V = state_val s2 V" by simp
  qed
  with obs n1' (backward_slice S) = obs n2 (backward_slice S)
    valid_node n1' valid_node n2 show ?thesis by(fastforce intro:WSI)
qed


lemma WS_silent_moves:
  "S,f  (n1,s1) =asτ (n1',s1'); ((n1,s1),(n2,s2))  WS S; f = kind;
    obs n1' (backward_slice S)  {}
   ((n1',s1'),(n2,s2))  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'),(n2,s2))  WS S; f = kind; obs n'' (backward_slice S)  {}
              ((n'',s''),(n2,s2))  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),(n2,s2))  WS S S,f  (n,s) -aτ (n',s') f = kind
  have "((n',s'),(n2,s2))  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 "((n1,s1),(n2,s2))  WS S" and "S,kind  (n1,s1) -a (n1',s1')"
  obtains as where "((n1',s1'),(n1',transfer (slice_kind S a) s2))  WS S"
  and "S,slice_kind S  (n2,s2) =as@[a] (n1',transfer (slice_kind S a) s2)"
proof(atomize_elim)
  from ((n1,s1),(n2,s2))  WS S have "valid_node n1" by(auto dest:WSD)
  from S,kind  (n1,s1) -a (n1',s1') have [simp]:"n1 = sourcenode a" 
    and [simp]:"n1' = targetnode a" and "pred (kind a) s1"
    and "transfer (kind a) s1 = s1'" and "n1  (backward_slice S)" 
    and "valid_edge a" and "pred (kind a) s1"
    by(auto elim:observable_move.cases)
  from  valid_edge a have "valid_node n1'" by(auto simp:valid_node_def)
  from valid_node n1 n1  (backward_slice S) 
  have "obs n1 (backward_slice S) = {n1}" by(rule n_in_obs)
  with ((n1,s1),(n2,s2))  WS S have "obs n2 (backward_slice S) = {n1}" 
    and "V  rv S n1. state_val s1 V = state_val s2 V" by(auto dest:WSD)
  from valid_node n1 have "n1 -[]→* n1" by(rule empty_path)
  with n1  (backward_slice S) have "V  Use n1. V  rv S n1"
    by(fastforce intro:rvI simp:sourcenodes_def)
  with V  rv S n1. state_val s1 V = state_val s2 V
  have "V  Use n1. state_val s1 V = state_val s2 V" by blast
  with valid_edge a  pred (kind a) s1 have "pred (kind a) s2"
    by(fastforce intro:CFG_edge_Uses_pred_equal)
  with n1  (backward_slice S) have "pred (slice_kind S a) s2"
    by(simp add:slice_kind_in_slice)
  from n1  (backward_slice S) obtain s2' 
    where "transfer (slice_kind S a) s2 = s2'"
    by(simp add:slice_kind_in_slice)
  with pred (slice_kind S a) s2 n1  (backward_slice S) valid_edge a 
  have "S,slice_kind S  (n1,s2) -a (n1',s2')"
    by(fastforce intro:observable_moveI)
  from obs n2 (backward_slice S) = {n1}
  obtain as where "S,slice_kind S  (n2,s2) =asτ (n1,s2)"
    by(erule obs_silent_moves)
  with S,slice_kind S  (n1,s2) -a (n1',s2') 
  have "S,slice_kind S  (n2,s2) =as@[a] (n1',s2')"
    by -(rule observable_moves_snoc)
  have "V  rv S n1'. state_val s1' V = state_val s2' V"
  proof
    fix V assume rv:"V  rv S n1'"
    show "state_val s1' V = state_val s2' V"
    proof(cases "V  Def n1")
      case True
      thus ?thesis
      proof(cases "kind a")
        case (Update f)
        with transfer (kind a) s1 = s1' have "s1' = f s1" by simp
        from Update[THEN sym] n1  (backward_slice S) 
        have "slice_kind S a = f"
          by(fastforce intro:slice_kind_in_slice)
        with transfer (slice_kind S a) s2 = s2' have "s2' = f s2" by simp
        from valid_edge a V  Use n1. state_val s1 V = state_val s2 V
          True Update s1' = f s1 s2' = f s2 show ?thesis
          by(fastforce dest:CFG_edge_transfer_uses_only_Use)
      next
        case (Predicate Q)
        with transfer (kind a) s1 = s1' have "s1' = s1" by simp
        from Predicate[THEN sym] n1  (backward_slice S)
        have "slice_kind S a = (Q)"
          by(fastforce intro:slice_kind_in_slice)
        with transfer (slice_kind S a) s2 = s2' have "s2' = s2" by simp
        with valid_edge a V  Use n1. state_val s1 V = state_val s2 V 
          True Predicate s1' = s1 pred (kind a) s1 pred (kind a) s2
        show ?thesis by(auto dest:CFG_edge_transfer_uses_only_Use)
      qed
    next
      case False
      with valid_edge a transfer (kind a) s1 = s1'[THEN sym] 
        pred (kind a) s1 pred (kind a) s2
      have "state_val s1' V = state_val s1 V"
        by(fastforce intro:CFG_edge_no_Def_equal)
      have "state_val s2' V = state_val s2 V"
      proof(cases "kind a")
        case (Update f)
        with  n1  (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) s2 = s2'[THEN sym] 
          False pred (kind a) s2
        show ?thesis by(fastforce intro:CFG_edge_no_Def_equal)
      next
        case (Predicate Q)
        with transfer (slice_kind S a) s2 = s2' have "s2 = s2'"
          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 "n1' -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 n1' -as'→* nx have "n1 -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 n1" by -(rule rvI)
      with V  rv S n1. state_val s1 V = state_val s2 V 
        state_val s1' V = state_val s1 V state_val s2' V = state_val s2 V
      show ?thesis by fastforce
    qed
  qed
  with valid_node n1' have "((n1',s1'),(n1',s2'))  WS S" by(fastforce intro:WSI)
  with S,slice_kind S  (n2,s2) =as@[a] (n1',s2')
    transfer (slice_kind S a) s2 = s2' 
  show "as. ((n1',s1'),(n1',transfer (slice_kind S a) s2))  WS S 
    S,slice_kind S  (n2,s2) =as@[a] (n1',transfer (slice_kind S a) s2)"
    by blast
qed



definition is_weak_sim :: 
  "(('node × 'state) × ('node × 'state)) set  'node set  bool"
  where "is_weak_sim R S  
  n1 s1 n2 s2 n1' s1' as. ((n1,s1),(n2,s2))  R  S,kind  (n1,s1) =as (n1',s1')
   (n2' s2' as'. ((n1',s1'),(n2',s2'))  R  
                      S,slice_kind S  (n2,s2) =as' (n2',s2'))"


lemma WS_weak_sim:
  assumes "((n1,s1),(n2,s2))  WS S" 
  and "S,kind  (n1,s1) =as (n1',s1')"
  shows "((n1',s1'),(n1',transfer (slice_kind S (last as)) s2))  WS S 
  (as'. S,slice_kind S  (n2,s2) =as'@[last as] 
                             (n1',transfer (slice_kind S (last as)) s2))"
proof -
  from S,kind  (n1,s1) =as (n1',s1') obtain a' as' n' s'
    where "S,kind  (n1,s1) =as'τ (n',s')" 
    and "S,kind  (n',s') -a' (n1',s1')" and "as = as'@[a']"
    by(fastforce elim:observable_moves.cases)
  from S,kind  (n',s') -a' (n1',s1') 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  (n1,s1) =as'τ (n',s') ((n1,s1),(n2,s2))  WS S 
  have "((n',s'),(n2,s2))  WS S"
    by -(rule WS_silent_moves,simp+)
  with S,kind  (n',s') -a' (n1',s1') obtain asx 
    where "((n1',s1'),(n1',transfer (slice_kind S a') s2))  WS S"
    and "S,slice_kind S  (n2,s2) =asx@[a'] 
    (n1',transfer (slice_kind S a') s2)"
    by(fastforce elim:WS_observable_move)
  with as = as'@[a'] show
    "((n1',s1'),(n1',transfer (slice_kind S (last as)) s2))  WS S 
    (as'. S,slice_kind S  (n2,s2) =as'@[last as] 
           (n1',transfer (slice_kind S (last as)) s2))" 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' = [] 
    nxset (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 nxset (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;
    Vrv 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 Vrv S n. state_val s V = state_val s' V
      have "Vrv 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
        Vrv 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 "((n1,s1),(n2,s2))  WS S"
  and "S,kind  (n1,s1) =as⇒* (n1',s1')" and "as  []"
  shows "((n1',s1'),(n1',transfers (slice_kinds S as) s2))  WS S  
         S,slice_kind S  (n2,s2) =as⇒* (n1',transfers (slice_kinds S as) s2)"
proof -
  obtain f where "f = kind" by simp
  with S,kind  (n1,s1) =as⇒* (n1',s1') 
  have "S,f  (n1,s1) =as⇒* (n1',s1')" by simp
  from S,f  (n1,s1) =as⇒* (n1',s1') ((n1,s1),(n2,s2))  WS S as  [] f = kind
  show "((n1',s1'),(n1',transfers (slice_kinds S as) s2))  WS S 
    S,slice_kind S  (n2,s2) =as⇒* (n1',transfers (slice_kinds S as) s2)"
  proof(induct arbitrary:n2 s2 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 = n2 s2. ((n',s'),(n2,s2))  WS S; as'  []; f = kind
       ((n'',s''),(n'',transfers (slice_kinds S as') s2))  WS S 
      S,slice_kind S  (n2,s2) =as'⇒* (n'',transfers (slice_kinds S as') s2)
    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),(n2,s2))  WS S f = kind
    have "((nx,sx),(n2,s2))  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) s2))  WS S"
      and "S,slice_kind S  (n2,s2) =asx'@[ax] 
      (n',transfer (slice_kind S ax) s2)"
      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  (n2,s2) =asx'@[ax] 
                               (n',transfer (slice_kind S ax) s2)
      have "S,slice_kind S  (n2,s2) =(last (asx'@[ax]))#[]⇒* 
                               (n',transfer (slice_kind S ax) s2)"
        by(fastforce intro:trans_observable_moves.intros)
      with ((n',s'),(n',transfer (slice_kind S ax) s2))  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) s2))  WS S this 
        f = kind]
      have "((n'',s''),(n'',transfers (slice_kinds S as') 
        (transfer (slice_kind S ax) s2)))  WS S"
        and "S,slice_kind S  (n',transfer (slice_kind S ax) s2) 
        =as'⇒* (n'',transfers (slice_kinds S as')
                     (transfer (slice_kind S ax) s2))" by simp_all
      with S,slice_kind S  (n2,s2) =asx'@[ax] 
                               (n',transfer (slice_kind S ax) s2)
      have "S,slice_kind S  (n2,s2) =(last (asx'@[ax]))#as'⇒* 
        (n'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s2))"
        by(fastforce intro:trans_observable_moves.tom_Cons)
      with ((n'',s''),(n'',transfers (slice_kinds S as') 
        (transfer (slice_kind S ax) s2)))  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' 
    (VUse n'. state_val (transfers (slice_kinds {n'} as) s) V = state_val s' V)"
    by blast
qed


end

end