Theory NonInterferenceInter

theory NonInterferenceInter
imports FundamentalProperty
section ‹HRB Slicing guarantees IFC Noninterference›

theory NonInterferenceInter 
  imports "HRB-Slicing.FundamentalProperty"
begin

subsection ‹Assumptions of this Approach›

text ‹
Classical IFC noninterference, a special case of a noninterference
definition using partial equivalence relations (per)
\cite{SabelfeldS:01}, partitions the variables (i.e.\ locations) into
security levels. Usually, only levels for secret or high, written
‹H›, and public or low, written ‹L›, variables are
used. Basically, a program that is noninterferent has to fulfil one
basic property: executing the program in two different initial states
that may differ in the values of their ‹H›-variables yields two
final states that again only differ in the values of their 
‹H›-variables; thus the values of the ‹H›-variables did not
influence those of the ‹L›-variables.

Every per-based approach makes certain
assumptions: (i) all \mbox{‹H›-variables} are defined at the
beginning of the program, (ii) all ‹L›-variables are observed (or
used in our terms) at the end and (iii) every variable is either
‹H› or ‹L›. This security label is fixed for a variable
and can not be altered during a program run. Thus, we have to extend 
the prerequisites of the slicing framework in \cite{Wasserrab:09} accordingly
in a new locale:

›

locale NonInterferenceInterGraph =
  SDG sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses 
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") 
  and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
  and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list" +
  fixes H :: "'var set"
  fixes L :: "'var set"
  fixes High :: "'node"  ("'('_High'_')")
  fixes Low :: "'node"   ("'('_Low'_')")
  assumes Entry_edge_Exit_or_High:
  "⟦valid_edge a; sourcenode a = (_Entry_)⟧ 
    ⟹ targetnode a = (_Exit_) ∨ targetnode a = (_High_)"
  and High_target_Entry_edge:
  "∃a. valid_edge a ∧ sourcenode a = (_Entry_) ∧ targetnode a = (_High_) ∧
       kind a = (λs. True)"
  and Entry_predecessor_of_High:
  "⟦valid_edge a; targetnode a = (_High_)⟧ ⟹ sourcenode a = (_Entry_)"
  and Exit_edge_Entry_or_Low: "⟦valid_edge a; targetnode a = (_Exit_)⟧ 
    ⟹ sourcenode a = (_Entry_) ∨ sourcenode a = (_Low_)"
  and Low_source_Exit_edge:
  "∃a. valid_edge a ∧ sourcenode a = (_Low_) ∧ targetnode a = (_Exit_) ∧ 
       kind a = (λs. True)"
  and Exit_successor_of_Low:
  "⟦valid_edge a; sourcenode a = (_Low_)⟧ ⟹ targetnode a = (_Exit_)"
  and DefHigh: "Def (_High_) = H" 
  and UseHigh: "Use (_High_) = H"
  and UseLow: "Use (_Low_) = L"
  and HighLowDistinct: "H ∩ L = {}"
  and HighLowUNIV: "H ∪ L = UNIV"

begin

lemma Low_neq_Exit: assumes "L ≠ {}" shows "(_Low_) ≠ (_Exit_)"
proof
  assume "(_Low_) = (_Exit_)"
  have "Use (_Exit_) = {}" by fastforce
  with UseLow ‹L ≠ {}› ‹(_Low_) = (_Exit_)› show False by simp
qed


lemma valid_node_High [simp]:"valid_node (_High_)"
  using High_target_Entry_edge by fastforce

lemma valid_node_Low [simp]:"valid_node (_Low_)"
  using Low_source_Exit_edge by fastforce


lemma get_proc_Low:
  "get_proc (_Low_) = Main"
proof -
  from Low_source_Exit_edge obtain a where "valid_edge a"
    and "sourcenode a = (_Low_)" and "targetnode a = (_Exit_)"
    and "intra_kind (kind a)" by(fastforce simp:intra_kind_def)
  from ‹valid_edge a› ‹intra_kind (kind a)›
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with ‹sourcenode a = (_Low_)› ‹targetnode a = (_Exit_)› get_proc_Exit
  show ?thesis by simp
qed

lemma get_proc_High:
  "get_proc (_High_) = Main"
proof -
  from High_target_Entry_edge obtain a where "valid_edge a"
    and "sourcenode a = (_Entry_)" and "targetnode a = (_High_)"
    and "intra_kind (kind a)" by(fastforce simp:intra_kind_def)
  from ‹valid_edge a› ‹intra_kind (kind a)›
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with ‹sourcenode a = (_Entry_)› ‹targetnode a = (_High_)› get_proc_Entry
  show ?thesis by simp
qed



lemma Entry_path_High_path:
  assumes "(_Entry_) -as→* n" and "inner_node n"
  obtains a' as' where "as = a'#as'" and "(_High_) -as'→* n" 
  and "kind a' = (λs. True)"
proof(atomize_elim)
  from ‹(_Entry_) -as→* n› ‹inner_node n›
  show "∃a' as'. as = a'#as' ∧ (_High_) -as'→* n ∧ kind a' = (λs. True)"
  proof(induct n'"(_Entry_)" as n rule:path.induct)
    case (Cons_path n'' as n' a)
    from ‹n'' -as→* n'› ‹inner_node n'› have "n'' ≠ (_Exit_)" 
      by(fastforce simp:inner_node_def)
    with ‹valid_edge a› ‹sourcenode a = (_Entry_)› ‹targetnode a = n''›
    have "n'' = (_High_)" by -(drule Entry_edge_Exit_or_High,auto)
    from High_target_Entry_edge
    obtain a' where "valid_edge a'" and "sourcenode a' = (_Entry_)"
      and "targetnode a' = (_High_)" and "kind a' = (λs. True)"
      by blast
    with ‹valid_edge a› ‹sourcenode a = (_Entry_)› ‹targetnode a = n''›
      ‹n'' = (_High_)›
    have "a = a'" by(auto dest:edge_det)
    with ‹n'' -as→* n'› ‹n'' = (_High_)› ‹kind a' = (λs. True) show ?case by blast
  qed fastforce
qed


lemma Exit_path_Low_path:
  assumes "n -as→* (_Exit_)" and "inner_node n"
  obtains a' as' where "as = as'@[a']" and "n -as'→* (_Low_)"
  and "kind a' = (λs. True)"
proof(atomize_elim)
  from ‹n -as→* (_Exit_)›
  show "∃as' a'. as = as'@[a'] ∧ n -as'→* (_Low_) ∧ kind a' = (λs. True)"
  proof(induct as rule:rev_induct)
    case Nil
    with ‹inner_node n› show ?case by fastforce
  next
    case (snoc a' as')
    from ‹n -as'@[a']→* (_Exit_)›
    have "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' = (_Exit_)"
      by(auto elim:path_split_snoc)
    { assume "sourcenode a' = (_Entry_)"
      with ‹n -as'→* sourcenode a'› have "n = (_Entry_)"
        by(blast intro!:path_Entry_target)
      with ‹inner_node n› have False by(simp add:inner_node_def) }
    with ‹valid_edge a'› ‹targetnode a' = (_Exit_)› have "sourcenode a' = (_Low_)"
      by(blast dest!:Exit_edge_Entry_or_Low)
    from Low_source_Exit_edge
    obtain ax where "valid_edge ax" and "sourcenode ax = (_Low_)"
      and "targetnode ax = (_Exit_)" and "kind ax = (λs. True)"
      by blast
    with ‹valid_edge a'› ‹targetnode a' = (_Exit_)› ‹sourcenode a' = (_Low_)›
    have "a' = ax" by(fastforce intro:edge_det)
    with ‹n -as'→* sourcenode a'› ‹sourcenode a' = (_Low_)› ‹kind ax = (λs. True)
    show ?case by blast
  qed
qed


lemma not_Low_High: "V ∉ L ⟹ V ∈ H"
  using HighLowUNIV
  by fastforce

lemma not_High_Low: "V ∉ H ⟹ V ∈ L"
  using HighLowUNIV
  by fastforce


subsection ‹Low Equivalence›

text ‹
In classical noninterference, an external observer can only see public values,
in our case the ‹L›-variables. If two states agree in the values of all 
‹L›-variables, these states are indistinguishable for him. 
\emph{Low equivalence} groups those states in an equivalence class using 
the relation ‹≈L›:
›

definition lowEquivalence :: "('var ⇀ 'val) list ⇒ ('var ⇀ 'val) list ⇒ bool" 
(infixl "≈L" 50)
  where "s ≈L s' ≡ ∀V ∈ L. hd s V = hd s' V"

text ‹The following lemmas connect low equivalent states with
relevant variables as necessary in the correctness proof for slicing.›

lemma relevant_vars_Entry:
  assumes "V ∈ rv S (CFG_node (_Entry_))" and "(_High_) ∉ ⌊HRB_slice S⌋CFG"
  shows "V ∈ L"
proof -
  from ‹V ∈ rv S (CFG_node (_Entry_))› obtain as n' 
    where "(_Entry_) -as→ι* parent_node n'" 
    and "n' ∈ HRB_slice S" and "V ∈ UseSDG n'"
    and "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as) 
          ⟶ V ∉ DefSDG n''" by(fastforce elim:rvE)
  from ‹(_Entry_) -as→ι* parent_node n'› have "valid_node (parent_node n')"
    by(fastforce intro:path_valid_node simp:intra_path_def)
  thus ?thesis
  proof(cases "parent_node n'" rule:valid_node_cases)
    case Entry
    with ‹V ∈ UseSDG n'› have False
      by -(drule SDG_Use_parent_Use,simp add:Entry_empty)
    thus ?thesis by simp
  next
    case Exit
    with ‹V ∈ UseSDG n'› have False
      by -(drule SDG_Use_parent_Use,simp add:Exit_empty)
    thus ?thesis by simp
  next
    case inner
    with ‹(_Entry_) -as→ι* parent_node n'› obtain a' as' where "as = a'#as'"
      and "(_High_) -as'→ι* parent_node n'"
      by(fastforce elim:Entry_path_High_path simp:intra_path_def)
    from ‹(_Entry_) -as→ι* parent_node n'› ‹as = a'#as'›
    have "sourcenode a' = (_Entry_)" by(fastforce elim:path.cases simp:intra_path_def)
    show ?thesis
    proof(cases "as' = []")
      case True
      with ‹(_High_) -as'→ι* parent_node n'› have "parent_node n' = (_High_)"
        by(fastforce simp:intra_path_def)
      with ‹n' ∈ HRB_slice S› ‹(_High_) ∉ ⌊HRB_slice S⌋CFG
      have False 
        by(fastforce dest:valid_SDG_node_in_slice_parent_node_in_slice 
                    simp:SDG_to_CFG_set_def)
      thus ?thesis by simp
    next
      case False
      with ‹(_High_) -as'→ι* parent_node n'› have "hd (sourcenodes as') = (_High_)"
        by(fastforce intro:path_sourcenode simp:intra_path_def)
      from False have "hd (sourcenodes as') ∈ set (sourcenodes as')"
        by(fastforce intro:hd_in_set simp:sourcenodes_def)
      with ‹as = a'#as'› have "hd (sourcenodes as') ∈ set (sourcenodes as)"
        by(simp add:sourcenodes_def)
      from ‹hd (sourcenodes as') = (_High_)›
      have "valid_node (hd (sourcenodes as'))" by simp
      have "valid_SDG_node (CFG_node (_High_))" by simp
      with ‹hd (sourcenodes as') = (_High_)›
        ‹hd (sourcenodes as') ∈ set (sourcenodes as)›
        ‹∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as) 
        ⟶ V ∉ DefSDG n''›
      have "V ∉ Def (_High_)"
        by(fastforce dest:CFG_Def_SDG_Def[OF ‹valid_node (hd (sourcenodes as'))›])
      hence "V ∉ H" by(simp add:DefHigh)
      thus ?thesis by(rule not_High_Low)
    qed
  qed
qed



lemma lowEquivalence_relevant_nodes_Entry:
  assumes "s ≈L s'" and "(_High_) ∉ ⌊HRB_slice S⌋CFG"
  shows "∀V ∈ rv S (CFG_node (_Entry_)). hd s V = hd s' V"
proof
  fix V assume "V ∈ rv S (CFG_node (_Entry_))"
  with ‹(_High_) ∉ ⌊HRB_slice S⌋CFG have "V ∈ L" by -(rule relevant_vars_Entry)
  with ‹s ≈L s'› show "hd s V = hd s' V" by(simp add:lowEquivalence_def)
qed


subsection ‹The Correctness Proofs›

text ‹
In the following, we present two correctness proofs that slicing
guarantees IFC noninterference. In both theorems, ‹CFG_node
(_High_) ∉ HRB_slice S›, where ‹CFG_node (_Low_) ∈ S›, makes
sure that no high variable (which are all defined in ‹(_High_)›)
can influence a low variable (which are all used in ‹(_Low_)›).


First, a theorem regarding ‹(_Entry_) -as→* (_Exit_)› paths in the 
control flow graph (CFG), which agree to a complete program execution:›


lemma slpa_rv_Low_Use_Low:
  assumes "CFG_node (_Low_) ∈ S"
  shows "⟦same_level_path_aux cs as; upd_cs cs as = []; same_level_path_aux cs as';
    ∀c ∈ set cs. valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
   ∀i < length cs. ∀V ∈ rv S (CFG_node (sourcenode (cs!i))). 
    fst (s!Suc i) V = fst (s'!Suc i) V; ∀i < Suc (length cs). snd (s!i) = snd (s'!i);
   ∀V ∈ rv S (CFG_node m). state_val s V = state_val s' V;
   preds (slice_kinds S as) s; preds (slice_kinds S as') s';
   length s = Suc (length cs); length s' = Suc (length cs)⟧
   ⟹ ∀V ∈ Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
                      state_val (transfers(slice_kinds S as') s') V"
proof(induct arbitrary:m as' s s' rule:slpa_induct)
  case (slpa_empty cs)
  from ‹m -[]→* (_Low_)› have "m = (_Low_)" by fastforce
  from ‹m -[]→* (_Low_)› have "valid_node m"
    by(rule path_valid_node)+
  { fix V assume "V ∈ Use (_Low_)"
    moreover
    from ‹valid_node m› ‹m = (_Low_)› have "(_Low_) -[]→ι* (_Low_)"
      by(fastforce intro:empty_path simp:intra_path_def)
    moreover
    from ‹valid_node m› ‹m = (_Low_)› ‹CFG_node (_Low_) ∈ S›
    have "CFG_node (_Low_) ∈ HRB_slice S"
      by(fastforce intro:HRB_slice_refl)
    ultimately have "V ∈ rv S (CFG_node m)" 
      using ‹m = (_Low_)›
      by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def) }
  hence "∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)" by simp
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    from ‹m -as'→* (_Low_)› ‹m = (_Low_)› have "as' = []"
    proof(induct m as' m'"(_Low_)" rule:path.induct)
      case (Cons_path m'' as a m)
      from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)›
      have "targetnode a = (_Exit_)" by -(rule Exit_successor_of_Low,simp+)
      with ‹targetnode a = m''› ‹m'' -as→* (_Low_)›
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?case by simp
    qed simp
    with ‹∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)›
      ‹∀V ∈ rv S (CFG_node m). state_val s V = state_val s' V› Nil
    show ?thesis by(auto simp:slice_kinds_def)
  qed
next
  case (slpa_intra cs a as)
  note IH = ‹⋀m as' s s'. ⟦upd_cs cs as = []; same_level_path_aux cs as'; 
    ∀a∈set cs. valid_edge a; m -as→* (_Low_); m -as'→* (_Low_);
    ∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V; 
    ∀i<Suc (length cs). snd (s ! i) = snd (s' ! i);
    ∀V∈rv S (CFG_node m). state_val s V = state_val s' V;
    preds (slice_kinds S as) s; preds (slice_kinds S as') s';
    length s = Suc (length cs); length s' = Suc (length cs)⟧
    ⟹ ∀V∈Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
    state_val (transfers(slice_kinds S as') s') V›
  note rvs = ‹∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V›
  from ‹m -a # as→* (_Low_)› have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with ‹m -as'→* (_Low_)› have "m = (_Low_)" by fastforce
      with ‹valid_edge a› ‹sourcenode a = m› have "targetnode a = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)› 
        ‹targetnode a = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)› 
        ‹targetnode a' = (_Exit_)›
      have "a = a'" by(fastforce dest:edge_det)
      with ‹kind a' = (λs. True) have "kind a = (λs. True)" by simp
      with ‹targetnode a = (_Exit_)› ‹targetnode a -as→* (_Low_)›
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax asx)
      with ‹m -as'→* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
        and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
      from ‹preds (slice_kinds S (a # as)) s›
      obtain cf cfs where [simp]:"s = cf#cfs" by(cases s)(auto simp:slice_kinds_def)
      from ‹preds (slice_kinds S as') s'› ‹as' = ax # asx› 
      obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
        by(cases s')(auto simp:slice_kinds_def)
      have "intra_kind (kind ax)"
      proof(cases "kind ax" rule:edge_kind_cases)
        case (Call Q r p fs)
        have False
        proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋CFG")
          case True
          with ‹intra_kind (kind a)› have "slice_kind S a = kind a"
            by -(rule slice_intra_kind_in_slice)
          from ‹valid_edge ax› ‹kind ax = Q:r↪pfs›
          have unique:"∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode ax ∧ 
            intra_kind(kind a')" by(rule call_only_one_intra_edge)
          from ‹valid_edge ax› ‹kind ax = Q:r↪pfs› obtain x 
            where "x ∈ get_return_edges ax" by(fastforce dest:get_return_edge_call)
          with ‹valid_edge ax› obtain a' where "valid_edge a'" 
            and "sourcenode a' = sourcenode ax" and "kind a' = (λcf. False)"
            by(fastforce dest:call_return_node_edge)
          with ‹valid_edge a› ‹sourcenode a = m› ‹sourcenode ax = m›
            ‹intra_kind (kind a)› unique
          have "a' = a" by(fastforce simp:intra_kind_def)
          with ‹kind a' = (λcf. False) ‹slice_kind S a = kind a›
            ‹preds (slice_kinds S (a#as)) s›
          have False by(cases s)(auto simp:slice_kinds_def)
          thus ?thesis by simp
        next
          case False
          with ‹kind ax = Q:r↪pfs› ‹sourcenode a = m› ‹sourcenode ax = m›
          have "slice_kind S ax = (λcf. False):r↪pfs"
            by(fastforce intro:slice_kind_Call)
          with ‹as' = ax # asx› ‹preds (slice_kinds S as') s'›
          have False by(cases s')(auto simp:slice_kinds_def)
          thus ?thesis by simp
        qed
        thus ?thesis by simp
      next
        case (Return Q p f)
        from ‹valid_edge ax› ‹kind ax = Q↩pf› ‹valid_edge a› ‹intra_kind (kind a)›
          ‹sourcenode a = m› ‹sourcenode ax = m›
        have False by -(drule return_edges_only,auto simp:intra_kind_def)
        thus ?thesis by simp
      qed simp
      with ‹same_level_path_aux cs as'› ‹as' = ax#asx›
      have "same_level_path_aux cs asx" by(fastforce simp:intra_kind_def)
      show ?thesis
      proof(cases "targetnode a = targetnode ax")
        case True
        with ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = m› ‹sourcenode ax = m›
        have "a = ax" by(fastforce intro:edge_det)
        with ‹valid_edge a› ‹intra_kind (kind a)› ‹sourcenode a = m›
          ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
          ‹preds (slice_kinds S (a # as)) s›
          ‹preds (slice_kinds S as') s'› ‹as' = ax # asx›
        have rv:"∀V∈rv S (CFG_node (targetnode a)). 
          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 ‹upd_cs cs (a # as) = []› ‹intra_kind (kind a)›
        have "upd_cs cs as = []" by(fastforce simp:intra_kind_def)
        from ‹targetnode ax -asx→* (_Low_)› ‹a = ax›
        have "targetnode a -asx→* (_Low_)" by simp
        from ‹valid_edge a› ‹intra_kind (kind a)›
        obtain cfx 
          where cfx:"transfer (slice_kind S a) s = cfx#cfs ∧ snd cfx = snd cf"
          apply(cases cf)
          apply(cases "sourcenode a ∈ ⌊HRB_slice S⌋CFG") apply auto
          apply(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
          apply(auto simp:intra_kind_def)
          apply(drule slice_kind_Upd) apply auto 
          by(erule kind_Predicate_notin_slice_slice_kind_Predicate) auto
        from ‹valid_edge a› ‹intra_kind (kind a)›
        obtain cfx' 
          where cfx':"transfer (slice_kind S a) s' = cfx'#cfs' ∧ snd cfx' = snd cf'"
          apply(cases cf')
          apply(cases "sourcenode a ∈ ⌊HRB_slice S⌋CFG") apply auto
          apply(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
          apply(auto simp:intra_kind_def)
          apply(drule slice_kind_Upd) apply auto 
          by(erule kind_Predicate_notin_slice_slice_kind_Predicate) auto
        with cfx ‹∀i < Suc (length cs). snd (s!i) = snd (s'!i)›
        have snds:"∀i<Suc(length cs).
          snd (transfer (slice_kind S a) s ! i) = 
          snd (transfer (slice_kind S a) s' ! i)" 
          by auto(case_tac i,auto)
        from rvs cfx cfx' have rvs':"∀i<length cs.
          ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
          fst (transfer (slice_kind S a) s ! Suc i) V =
          fst (transfer (slice_kind S a) s' ! Suc i) V"
          by fastforce
        from ‹preds (slice_kinds S (a # as)) s›
        have "preds (slice_kinds S as) 
          (transfer (slice_kind S a) s)" by(simp add:slice_kinds_def)
        moreover
        from ‹preds (slice_kinds S as') s'› ‹as' = ax # asx› ‹a = ax›
        have "preds (slice_kinds S asx) (transfer (slice_kind S a) s')" 
          by(simp add:slice_kinds_def)
        moreover
        from ‹valid_edge a› ‹intra_kind (kind a)›
        have "length (transfer (slice_kind S a) s) = length s"
          by(cases "sourcenode a ∈ ⌊HRB_slice S⌋CFG")
        (auto dest:slice_intra_kind_in_slice slice_kind_Upd
          elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)
        with ‹length s = Suc (length cs)›
        have "length (transfer (slice_kind S a) s) = Suc (length cs)"
          by simp
        moreover
        from ‹a = ax› ‹valid_edge a› ‹intra_kind (kind a)›
        have "length (transfer (slice_kind S a) s') = length s'"
          by(cases "sourcenode ax ∈ ⌊HRB_slice S⌋CFG")
        (auto dest:slice_intra_kind_in_slice slice_kind_Upd
          elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)
        with ‹length s' = Suc (length cs)›
        have "length (transfer (slice_kind S a) s') = Suc (length cs)"
          by simp
        moreover
        from IH[OF ‹upd_cs cs as = []› ‹same_level_path_aux cs asx› 
          ‹∀c∈set cs. valid_edge c› ‹targetnode a -as→* (_Low_)› 
          ‹targetnode a -asx→* (_Low_)› rvs' snds rv calculation]
          ‹as' = ax # asx› ‹a = ax›
        show ?thesis by(simp add:slice_kinds_def)
      next
        case False
        from ‹∀i < Suc(length cs). snd (s!i) = snd (s'!i)›
        have "snd (hd s) = snd (hd s')" by(erule_tac x="0" in allE) fastforce
        with ‹valid_edge a› ‹valid_edge ax› ‹sourcenode a = m›
          ‹sourcenode ax = m› ‹as' = ax # asx› False
          ‹intra_kind (kind a)› ‹intra_kind (kind ax)›
          ‹preds (slice_kinds S (a # as)) s›
          ‹preds (slice_kinds S as') s'›
          ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
          ‹length s = Suc (length cs)› ‹length s' = Suc (length cs)›
        have False by(fastforce intro!:rv_branching_edges_slice_kinds_False[of a ax])
        thus ?thesis by simp
      qed
    qed
  qed
next
  case (slpa_Call cs a as Q r p fs)
  note IH = ‹⋀m as' s s'. 
    ⟦upd_cs (a # cs) as = []; same_level_path_aux (a # cs) as';
    ∀c∈set (a # cs). valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
    ∀i<length (a # cs). ∀V∈rv S (CFG_node (sourcenode ((a # cs) ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V;
    ∀i<Suc (length (a # cs)). snd (s ! i) = snd (s' ! i);
    ∀V∈rv S (CFG_node m). state_val s V = state_val s' V;
    preds (slice_kinds S as) s; preds (slice_kinds S as') s';
    length s = Suc (length (a # cs)); length s' = Suc (length (a # cs))⟧
    ⟹ ∀V∈Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
    state_val (transfers(slice_kinds S as') s') V›
  note rvs = ‹∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V›
  from ‹m -a # as→* (_Low_)› have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
  from ‹∀c∈set cs. valid_edge c› ‹valid_edge a›
  have "∀c∈set (a # cs). valid_edge c" by simp
  show ?case
   proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with ‹m -as'→* (_Low_)› have "m = (_Low_)" by fastforce
      with ‹valid_edge a› ‹sourcenode a = m› have "targetnode a = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)› 
        ‹targetnode a = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)› 
        ‹targetnode a' = (_Exit_)›
      have "a = a'" by(fastforce dest:edge_det)
      with ‹kind a' = (λs. True) have "kind a = (λs. True)" by simp
      with ‹targetnode a = (_Exit_)› ‹targetnode a -as→* (_Low_)›
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax asx)
      with ‹m -as'→* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
        and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
      from ‹preds (slice_kinds S (a # as)) s›
      obtain cf cfs where [simp]:"s = cf#cfs" by(cases s)(auto simp:slice_kinds_def)
      from ‹preds (slice_kinds S as') s'› ‹as' = ax # asx› 
      obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
        by(cases s')(auto simp:slice_kinds_def)
      have "∃Q r p fs. kind ax = Q:r↪pfs"
      proof(cases "kind ax" rule:edge_kind_cases)
        case Intra
        have False
        proof(cases "sourcenode ax ∈ ⌊HRB_slice S⌋CFG")
          case True
          with ‹intra_kind (kind ax)› 
          have "slice_kind S ax = kind ax"
            by -(rule slice_intra_kind_in_slice)
          from ‹valid_edge a› ‹kind a = Q:r↪pfs›
          have unique:"∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧ 
            intra_kind(kind a')" by(rule call_only_one_intra_edge)
          from ‹valid_edge a› ‹kind a = Q:r↪pfs› obtain x 
            where "x ∈ get_return_edges a" by(fastforce dest:get_return_edge_call)
          with ‹valid_edge a› obtain a' where "valid_edge a'" 
            and "sourcenode a' = sourcenode a" and "kind a' = (λcf. False)"
            by(fastforce dest:call_return_node_edge)
          with ‹valid_edge ax› ‹sourcenode ax = m› ‹sourcenode a = m›
            ‹intra_kind (kind ax)› unique
          have "a' = ax" by(fastforce simp:intra_kind_def)
          with ‹kind a' = (λcf. False) 
            ‹slice_kind S ax = kind ax› ‹as' = ax # asx›
            ‹preds (slice_kinds S as') s'›
          have False by(simp add:slice_kinds_def)
          thus ?thesis by simp
        next
          case False
          with ‹kind a = Q:r↪pfs› ‹sourcenode ax = m› ‹sourcenode a = m›
          have "slice_kind S a = (λcf. False):r↪pfs"
            by(fastforce intro:slice_kind_Call)
          with ‹preds (slice_kinds S (a # as)) s›
          have False by(simp add:slice_kinds_def)
          thus ?thesis by simp
        qed
        thus ?thesis by simp
      next
        case (Return Q' p' f')
        from ‹valid_edge ax› ‹kind ax = Q'↩p'f'› ‹valid_edge a› ‹kind a = Q:r↪pfs›
          ‹sourcenode a = m› ‹sourcenode ax = m›
        have False by -(drule return_edges_only,auto)
        thus ?thesis by simp
      qed simp
      have "sourcenode a ∈ ⌊HRB_slice S⌋CFG"
      proof(rule ccontr)
        assume "sourcenode a ∉ ⌊HRB_slice S⌋CFG"
        from this ‹kind a = Q:r↪pfs›
        have "slice_kind S a = (λcf. False):r↪pfs"
          by(rule slice_kind_Call)
        with ‹preds (slice_kinds S (a # as)) s›
        show False by(simp add:slice_kinds_def)
      qed
      with ‹preds (slice_kinds S (a # as)) s› ‹kind a = Q:r↪pfs›
      have "pred (kind a) s" 
        by(fastforce dest:slice_kind_Call_in_slice simp:slice_kinds_def)
      from ‹sourcenode a ∈ ⌊HRB_slice S⌋CFG
        ‹sourcenode a = m› ‹sourcenode ax = m›
      have "sourcenode ax ∈ ⌊HRB_slice S⌋CFG" by simp
      with ‹as' = ax # asx› ‹preds (slice_kinds S as') s'› 
        ‹∃Q r p fs. kind ax = Q:r↪pfs›
      have "pred (kind ax) s'"
        by(fastforce dest:slice_kind_Call_in_slice simp:slice_kinds_def)
      { fix V assume "V ∈ Use (sourcenode a)"
        from ‹valid_edge a› have "sourcenode a -[]→ι* sourcenode a"
          by(fastforce intro:empty_path simp:intra_path_def)
        with ‹sourcenode a ∈ ⌊HRB_slice S⌋CFG
          ‹valid_edge a› ‹V ∈ Use (sourcenode a)›
        have "V ∈ rv S (CFG_node (sourcenode a))"
          by(auto intro!:rvI CFG_Use_SDG_Use simp:SDG_to_CFG_set_def sourcenodes_def) }
      with ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
        ‹sourcenode a = m›
      have Use:"∀V ∈ Use (sourcenode a). state_val s V = state_val s' V" by simp
      from ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)›
      have "snd (hd s) = snd (hd s')"  by fastforce
      with ‹valid_edge a› ‹kind a = Q:r↪pfs› ‹valid_edge ax›
        ‹∃Q r p fs. kind ax = Q:r↪pfs› ‹sourcenode a = m› ‹sourcenode ax = m›
        ‹pred (kind a) s› ‹pred (kind ax) s'› Use ‹length s = Suc (length cs)›
        ‹length s' = Suc (length cs)›
      have [simp]:"ax = a" by(fastforce intro!:CFG_equal_Use_equal_call)
      from ‹same_level_path_aux cs as'› ‹as' = ax#asx› ‹kind a = Q:r↪pfs›
        ‹∃Q r p fs. kind ax = Q:r↪pfs›
      have "same_level_path_aux (a # cs) asx" by simp
      from ‹targetnode ax -asx→* (_Low_)› have "targetnode a -asx→* (_Low_)" by simp
      from ‹kind a = Q:r↪pfs› ‹upd_cs cs (a # as) = []› 
      have "upd_cs (a # cs) as = []" by simp
      from ‹sourcenode a ∈ ⌊HRB_slice S⌋CFG ‹kind a = Q:r↪pfs›
      have slice_kind:"slice_kind S a = 
        Q:r↪p(cspp (targetnode a) (HRB_slice S) fs)"
        by(rule slice_kind_Call_in_slice)
      from ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)› slice_kind
      have snds:"∀i<Suc (length (a # cs)).
        snd (transfer (slice_kind S a) s ! i) =
        snd (transfer (slice_kind S a) s' ! i)"
        by auto(case_tac i,auto)
      from ‹valid_edge a› ‹kind a = Q:r↪pfs› obtain ins outs 
        where "(p,ins,outs) ∈ set procs" by(fastforce dest!:callee_in_procs)
      with ‹valid_edge a› ‹kind a = Q:r↪pfs›
      have "length (ParamUses (sourcenode a)) = length ins"
        by(fastforce intro:ParamUses_call_source_length)
      with ‹valid_edge a›
      have "∀i < length ins. ∀V ∈ (ParamUses (sourcenode a))!i. V ∈ Use (sourcenode a)"
        by(fastforce intro:ParamUses_in_Use)
      with ‹∀V ∈ Use (sourcenode a). state_val s V = state_val s' V›
      have "∀i < length ins. ∀V ∈ (ParamUses (sourcenode a))!i. 
        state_val s V = state_val s' V"
        by fastforce
      with ‹valid_edge a› ‹kind a = Q:r↪pfs› ‹(p,ins,outs) ∈ set procs›
        ‹pred (kind a) s› ‹pred (kind ax) s'›
      have "∀i < length ins. (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"
        by(fastforce intro!:CFG_call_edge_params)
      from ‹valid_edge a› ‹kind a = Q:r↪pfs› ‹(p,ins,outs) ∈ set procs›
      have "length fs = length ins" by(rule CFG_call_edge_length)
      { fix i assume "i < length fs"
        with ‹length fs = length ins› have "i < length ins" by simp
        from ‹i < length fs› have "(params fs (fst cf))!i = (fs!i) (fst cf)"
          by(rule params_nth)
        moreover
        from ‹i < length fs› have "(params fs (fst cf'))!i = (fs!i) (fst cf')"
          by(rule params_nth)
        ultimately have "(fs!i) (fst (hd s)) = (fs!i) (fst (hd s'))"
          using ‹i < length ins›
            ‹∀i < length ins. (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i›
          by simp }
      hence "∀i < length fs. (fs ! i) (fst cf) = (fs ! i) (fst cf')" by simp
      { fix i assume "i < length fs"
        with ‹∀i < length fs. (fs ! i) (fst cf) = (fs ! i) (fst cf')›
        have "(fs ! i) (fst cf) = (fs ! i) (fst cf')" by simp
        have "((csppa (targetnode a) (HRB_slice S) 0 fs)!i)(fst cf) =
          ((csppa (targetnode a) (HRB_slice S) 0 fs)!i)(fst cf')"
        proof(cases "Formal_in(targetnode a,i + 0) ∈  HRB_slice S")
          case True
          with ‹i < length fs› 
          have "(csppa (targetnode a) (HRB_slice S) 0 fs)!i = fs!i"
            by(rule csppa_Formal_in_in_slice)
          with ‹(fs ! i) (fst cf) = (fs ! i) (fst cf')› show ?thesis by simp
        next
          case False
          with ‹i < length fs› 
          have "(csppa (targetnode a) (HRB_slice S) 0 fs)!i = Map.empty"
            by(rule csppa_Formal_in_notin_slice)
          thus ?thesis by simp
        qed }
      hence eq:"∀i < length fs.
        ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf) =
        ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf')"
        by(simp add:cspp_def)
      { fix i assume "i < length fs"
        hence "(params (cspp (targetnode a) (HRB_slice S) fs)
          (fst cf))!i =
          ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf)"
          by(fastforce intro:params_nth)
        moreover
        from ‹i < length fs›
        have "(params (cspp (targetnode a) (HRB_slice S) fs)
          (fst cf'))!i =
          ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf')"
          by(fastforce intro:params_nth)
        ultimately 
        have "(params (cspp (targetnode a) (HRB_slice S) fs)
          (fst cf))!i =
          (params (cspp (targetnode a) (HRB_slice S) fs)(fst cf'))!i"
          using eq ‹i < length fs› by simp }
      hence "params (cspp (targetnode a) (HRB_slice S) fs)(fst cf) =
        params (cspp (targetnode a) (HRB_slice S) fs)(fst cf')"
        by(simp add:list_eq_iff_nth_eq)
      with slice_kind ‹(p,ins,outs) ∈ set procs›
      obtain cfx where [simp]:
        "transfer (slice_kind S a) (cf#cfs) = cfx#cf#cfs"
        "transfer (slice_kind S a) (cf'#cfs') = cfx#cf'#cfs'"
        by auto
      hence rv:"∀V∈rv S (CFG_node (targetnode a)).
        state_val (transfer (slice_kind S a) s) V = 
        state_val (transfer (slice_kind S a) s') V" by simp
      from rvs ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V› 
        ‹sourcenode a = m›
      have rvs':"∀i<length (a # cs). 
        ∀V∈rv S (CFG_node (sourcenode ((a # cs) ! i))).
        fst ((transfer (slice_kind S a) s) ! Suc i) V = 
        fst ((transfer (slice_kind S a) s') ! Suc i) V"
        by auto(case_tac i,auto)
      from ‹preds (slice_kinds S (a # as)) s›
      have "preds (slice_kinds S as)
        (transfer (slice_kind S a) s)" by(simp add:slice_kinds_def)
      moreover
      from ‹preds (slice_kinds S as') s'› ‹as' = ax#asx›
      have "preds (slice_kinds S asx)
        (transfer (slice_kind S a) s')" by(simp add:slice_kinds_def)
      moreover
      from ‹length s = Suc (length cs)›
      have "length (transfer (slice_kind S a) s) = 
        Suc (length (a # cs))" by simp
      moreover
      from ‹length s' = Suc (length cs)›
      have "length (transfer (slice_kind S a) s') = 
        Suc (length (a # cs))" by simp
      moreover
      from IH[OF ‹upd_cs (a # cs) as = []› ‹same_level_path_aux (a # cs) asx›
        ‹∀c∈set (a # cs). valid_edge c› ‹targetnode a -as→* (_Low_)›
        ‹targetnode a -asx→* (_Low_)› rvs' snds rv calculation] ‹as' = ax#asx›
      show ?thesis by(simp add:slice_kinds_def)
    qed
  qed
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = ‹⋀m as' s s'. ⟦upd_cs cs' as = []; same_level_path_aux cs' as'; 
    ∀c∈set cs'. valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
    ∀i<length cs'. ∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V; 
    ∀i<Suc (length cs'). snd (s ! i) = snd (s' ! i);
    ∀V∈rv S (CFG_node m). state_val s V = state_val s' V;
    preds (slice_kinds S as) s; preds (slice_kinds S as') s';
    length s = Suc (length cs'); length s' = Suc (length cs')⟧
    ⟹ ∀V∈Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
                       state_val (transfers(slice_kinds S as') s') V›
  note rvs = ‹ ∀i<length cs. ∀V∈rv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V›
  from ‹m -a # as→* (_Low_)› have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
  from ‹∀c∈set cs. valid_edge c› ‹cs = c' # cs'›
  have "valid_edge c'" and "∀c∈set cs'. valid_edge c" by simp_all
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with ‹m -as'→* (_Low_)› have "m = (_Low_)" by fastforce
      with ‹valid_edge a› ‹sourcenode a = m› have "targetnode a = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)› 
        ‹targetnode a = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)› 
        ‹targetnode a' = (_Exit_)›
      have "a = a'" by(fastforce dest:edge_det)
      with ‹kind a' = (λs. True) have "kind a = (λs. True)" by simp
      with ‹targetnode a = (_Exit_)› ‹targetnode a -as→* (_Low_)›
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax asx)
      with ‹m -as'→* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
        and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
      from ‹valid_edge a› ‹valid_edge ax› ‹kind a = Q↩pf›
        ‹sourcenode a = m› ‹sourcenode ax = m›
      have "∃Q f. kind ax = Q↩pf" by(auto dest:return_edges_only)
      with ‹same_level_path_aux cs as'› ‹as' = ax#asx› ‹cs = c' # cs'›
      have "ax ∈ get_return_edges c'" and "same_level_path_aux cs' asx" by auto
      from ‹valid_edge c'› ‹ax ∈ get_return_edges c'› ‹a ∈ get_return_edges c'›
      have [simp]:"ax = a" by(rule get_return_edges_unique)
      from ‹targetnode ax -asx→* (_Low_)› have "targetnode a -asx→* (_Low_)" by simp
      from ‹upd_cs cs (a # as) = []› ‹kind a = Q↩pf› ‹cs = c' # cs'›
        ‹a ∈ get_return_edges c'›
      have "upd_cs cs' as = []" by simp
      from ‹length s = Suc (length cs)› ‹cs = c' # cs'›
      obtain cf cfx cfs where "s = cf#cfx#cfs"
        by(cases s,auto,case_tac list,fastforce+)
      from ‹length s' = Suc (length cs)› ‹cs = c' # cs'›
      obtain cf' cfx' cfs' where "s' = cf'#cfx'#cfs'"
        by(cases s',auto,case_tac list,fastforce+)
      from rvs ‹cs = c' # cs'› ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
      have rvs1:"∀i<length cs'. 
        ∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
        fst ((cfx#cfs) ! Suc i) V = fst ((cfx'#cfs') ! Suc i) V"
        and "∀V∈rv S (CFG_node (sourcenode c')). 
        (fst cfx) V = (fst cfx') V"
        by auto
      from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
      obtain Qx rx px fsx where "kind c' = Qx:rx↪pxfsx"
        by(fastforce dest!:only_call_get_return_edges)
      have "∀V ∈ rv S (CFG_node (targetnode a)).
        V ∈ rv S (CFG_node (sourcenode c'))"
      proof
        fix V assume "V ∈ rv S (CFG_node (targetnode a))"
        from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
        obtain a' where edge:"valid_edge a'" "sourcenode a' = sourcenode c'"
          "targetnode a' = targetnode a" "intra_kind (kind a')"
          by -(drule call_return_node_edge,auto simp:intra_kind_def)
        from ‹V ∈ rv S (CFG_node (targetnode a))›
        obtain as n' where "targetnode a -as→ι* parent_node n'"
          and "n' ∈ HRB_slice S" and "V ∈ UseSDG n'"
          and all:"∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes as) 
          ⟶ V ∉ DefSDG n''" by(fastforce elim:rvE)
        from ‹targetnode a -as→ι* parent_node n'› edge
        have "sourcenode c' -a'#as→ι* parent_node n'"
          by(fastforce intro:Cons_path simp:intra_path_def)
        from ‹valid_edge c'› ‹kind c' = Qx:rx↪pxfsx› have "Def (sourcenode c') = {}"
          by(rule call_source_Def_empty)
        hence "∀n''. valid_SDG_node n'' ∧ parent_node n'' = sourcenode c'
          ⟶ V ∉ DefSDG n''" by(fastforce dest:SDG_Def_parent_Def)
        with all ‹sourcenode a' = sourcenode c'›
        have "∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (a'#as)) 
          ⟶ V ∉ DefSDG n''" by(fastforce simp:sourcenodes_def)
        with ‹sourcenode c' -a'#as→ι* parent_node n'› 
          ‹n' ∈ HRB_slice S› ‹V ∈ UseSDG n'›
        show "V ∈ rv S (CFG_node (sourcenode c'))"
          by(fastforce intro:rvI)
      qed
      show ?thesis
      proof(cases "sourcenode a ∈ ⌊HRB_slice S⌋CFG")
        case True
        from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
        have "get_proc (targetnode c') = get_proc (sourcenode a)"
          by -(drule intra_proc_additional_edge,
            auto dest:get_proc_intra simp:intra_kind_def)
        moreover
        from ‹valid_edge c'› ‹kind c' = Qx:rx↪pxfsx›
        have "get_proc (targetnode c') = px" by(rule get_proc_call)
        moreover
        from ‹valid_edge a› ‹kind a = Q↩pf›
        have "get_proc (sourcenode a) = p" by(rule get_proc_return)
        ultimately have [simp]:"px = p" by simp
        from ‹valid_edge c'› ‹kind c' = Qx:rx↪pxfsx›
        obtain ins outs where "(p,ins,outs) ∈ set procs"
          by(fastforce dest!:callee_in_procs)
        with ‹sourcenode a ∈ ⌊HRB_slice S⌋CFG
          ‹valid_edge a› ‹kind a = Q↩pf›
        have slice_kind:"slice_kind S a = 
          Q↩p(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
          by(rule slice_kind_Return_in_slice)
        with ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
        have sx:"transfer (slice_kind S a) s = 
          (rspp (targetnode a) (HRB_slice S) outs (fst cfx) (fst cf),
          snd cfx)#cfs"
          and sx':"transfer (slice_kind S a) s' = 
          (rspp (targetnode a) (HRB_slice S) outs (fst cfx') (fst cf'),
          snd cfx')#cfs'"
          by simp_all
        with rvs1 have rvs':"∀i<length cs'. 
          ∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
          fst ((transfer (slice_kind S a) s) ! Suc i) V = 
          fst ((transfer (slice_kind S a) s') ! Suc i) V"
          by fastforce
        from slice_kind ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)› ‹cs = c' # cs'›
          ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
        have snds:"∀i<Suc (length cs').
          snd (transfer (slice_kind S a) s ! i) =
          snd (transfer (slice_kind S a) s' ! i)"
          apply auto apply(case_tac i) apply auto
          by(erule_tac x="Suc (Suc nat)" in allE) auto
        have "∀V∈rv S (CFG_node (targetnode a)).
          (rspp (targetnode a) (HRB_slice S) outs 
          (fst cfx) (fst cf)) V =
          (rspp (targetnode a) (HRB_slice S) outs 
          (fst cfx') (fst cf')) V"
        proof
          fix V assume "V ∈ rv S (CFG_node (targetnode a))"
          show "(rspp (targetnode a) (HRB_slice S) outs 
            (fst cfx) (fst cf)) V =
            (rspp (targetnode a) (HRB_slice S) outs 
            (fst cfx') (fst cf')) V"
          proof(cases "V ∈ set (ParamDefs (targetnode a))")
            case True
            then obtain i where "i < length (ParamDefs (targetnode a))"
              and "(ParamDefs (targetnode a))!i = V"
              by(fastforce simp:in_set_conv_nth)
            from ‹valid_edge a› ‹kind a = Q↩pf› ‹(p,ins,outs) ∈ set procs›
            have "length(ParamDefs (targetnode a)) = length outs"
              by(fastforce intro:ParamDefs_return_target_length)
            show ?thesis
            proof(cases "Actual_out(targetnode a,i) ∈ HRB_slice S")
              case True
              with ‹i < length (ParamDefs (targetnode a))› ‹valid_edge a›
                ‹length(ParamDefs (targetnode a)) = length outs›
                ‹(ParamDefs (targetnode a))!i = V›[THEN sym]
              have rspp_eq:"(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx) (fst cf)) V = 
                (fst cf)(outs!i)"
                "(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx') (fst cf')) V = 
                (fst cf')(outs!i)"
                by(auto intro:rspp_Actual_out_in_slice)
              from ‹valid_edge a› ‹kind a = Q↩pf› ‹(p,ins,outs) ∈ set procs›
              have "∀V ∈ set outs. V ∈ Use (sourcenode a)" by(fastforce dest:outs_in_Use)
              have "∀V ∈ Use (sourcenode a). V ∈ rv S (CFG_node m)"
              proof
                fix V assume "V ∈ Use (sourcenode a)"
                from ‹valid_edge a› ‹sourcenode a = m›
                have "parent_node (CFG_node m) -[]→ι* parent_node (CFG_node m)"
                  by(fastforce intro:empty_path simp:intra_path_def)
                with ‹sourcenode a ∈ ⌊HRB_slice S⌋CFG 
                  ‹V ∈ Use (sourcenode a)› ‹sourcenode a = m› ‹valid_edge a›
                show "V ∈ rv S (CFG_node m)"
                  by -(rule rvI,
                    auto intro!:CFG_Use_SDG_Use simp:SDG_to_CFG_set_def sourcenodes_def)
              qed
              with ‹∀V ∈ set outs. V ∈ Use (sourcenode a)›
              have "∀V ∈ set outs. V ∈ rv S (CFG_node m)" by simp
              with ‹∀V∈rv S (CFG_node m). state_val s V = state_val s' V›
                ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
              have "∀V ∈ set outs. (fst cf) V = (fst cf') V" by simp
              with ‹i < length (ParamDefs (targetnode a))›
                ‹length(ParamDefs (targetnode a)) = length outs›
              have "(fst cf)(outs!i) = (fst cf')(outs!i)" by fastforce
              with rspp_eq show ?thesis by simp
            next
              case False
              with ‹i < length (ParamDefs (targetnode a))› ‹valid_edge a›
                ‹length(ParamDefs (targetnode a)) = length outs›
                ‹(ParamDefs (targetnode a))!i = V›[THEN sym]
              have rspp_eq:"(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx) (fst cf)) V = 
                (fst cfx)((ParamDefs (targetnode a))!i)"
                "(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx') (fst cf')) V = 
                (fst cfx')((ParamDefs (targetnode a))!i)"
                by(auto intro:rspp_Actual_out_notin_slice)
              from ‹∀V∈rv S (CFG_node (sourcenode c')). 
                (fst cfx) V = (fst cfx') V›
                ‹V ∈ rv S (CFG_node (targetnode a))›
                ‹∀V ∈ rv S (CFG_node (targetnode a)).
                V ∈ rv S (CFG_node (sourcenode c'))›
                ‹(ParamDefs (targetnode a))!i = V›[THEN sym]
              have "(fst cfx) (ParamDefs (targetnode a) ! i) =
                (fst cfx') (ParamDefs (targetnode a) ! i)" by fastforce
              with rspp_eq show ?thesis by fastforce
            qed
          next
            case False
            with ‹∀V∈rv S (CFG_node (sourcenode c')). 
              (fst cfx) V = (fst cfx') V›
              ‹V ∈ rv S (CFG_node (targetnode a))›
              ‹∀V ∈ rv S (CFG_node (targetnode a)).
              V ∈ rv S (CFG_node (sourcenode c'))›
            show ?thesis by(fastforce simp:rspp_def map_merge_def)
          qed
        qed
        with sx sx'
        have rv':"∀V∈rv S (CFG_node (targetnode a)).
          state_val (transfer (slice_kind S a) s) V =
          state_val (transfer (slice_kind S a) s') V"
          by fastforce
        from ‹preds (slice_kinds S (a # as)) s›
        have "preds (slice_kinds S as) 
          (transfer (slice_kind S a) s)"
          by(simp add:slice_kinds_def)
        moreover
        from ‹preds (slice_kinds S as') s'› ‹as' = ax#asx›
        have "preds (slice_kinds S asx) 
          (transfer (slice_kind S a) s')"
          by(simp add:slice_kinds_def)
        moreover
        from ‹length s = Suc (length cs)› ‹cs = c' # cs'› sx
        have "length (transfer (slice_kind S a) s) = Suc (length cs')"
          by(simp,simp add:‹s = cf#cfx#cfs›)
        moreover
        from ‹length s' = Suc (length cs)› ‹cs = c' # cs'› sx'
        have "length (transfer (slice_kind S a) s') = Suc (length cs')"
          by(simp,simp add:‹s' = cf'#cfx'#cfs'›)
        moreover
        from IH[OF ‹upd_cs cs' as = []› ‹same_level_path_aux cs' asx› 
          ‹∀c∈set cs'. valid_edge c› ‹targetnode a -as→* (_Low_)› 
          ‹targetnode a -asx→* (_Low_)› rvs' snds rv' calculation] ‹as' = ax#asx›
        show ?thesis by(simp add:slice_kinds_def)
      next
        case False
        from this ‹kind a = Q↩pf›
        have slice_kind:"slice_kind S a = (λcf. True)↩p(λcf cf'. cf')"
          by(rule slice_kind_Return)
        with ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
        have [simp]:"transfer (slice_kind S a) s = cfx#cfs"
          "transfer (slice_kind S a) s' = cfx'#cfs'" by simp_all
        from slice_kind ‹∀i<Suc (length cs). snd (s ! i) = snd (s' ! i)› 
          ‹cs = c' # cs'› ‹s = cf#cfx#cfs› ‹s' = cf'#cfx'#cfs'›
        have snds:"∀i<Suc (length cs').
          snd (transfer (slice_kind S a) s ! i) =
          snd (transfer (slice_kind S a) s' ! i)" by fastforce
        from rvs1 have rvs':"∀i<length cs'. 
          ∀V∈rv S (CFG_node (sourcenode (cs' ! i))).
          fst ((transfer (slice_kind S a) s) ! Suc i) V = 
          fst ((transfer (slice_kind S a) s') ! Suc i) V"
          by fastforce
        from ‹∀V ∈ rv S (CFG_node (targetnode a)).
          V ∈ rv S (CFG_node (sourcenode c'))›
          ‹∀V∈rv S (CFG_node (sourcenode c')). 
          (fst cfx) V = (fst cfx') V›
        have rv':"∀V∈rv S (CFG_node (targetnode a)).
          state_val (transfer (slice_kind S a) s) V =
          state_val (transfer (slice_kind S a) s') V" by simp
        from ‹preds (slice_kinds S (a # as)) s›
        have "preds (slice_kinds S as) 
          (transfer (slice_kind S a) s)"
          by(simp add:slice_kinds_def)
        moreover
        from ‹preds (slice_kinds S as') s'› ‹as' = ax#asx›
        have "preds (slice_kinds S asx) 
          (transfer (slice_kind S a) s')"
          by(simp add:slice_kinds_def)
        moreover
        from ‹length s = Suc (length cs)› ‹cs = c' # cs'›
        have "length (transfer (slice_kind S a) s) = Suc (length cs')"
          by(simp,simp add:‹s = cf#cfx#cfs›)
        moreover
        from ‹length s' = Suc (length cs)› ‹cs = c' # cs'›
        have "length (transfer (slice_kind S a) s') = Suc (length cs')"
          by(simp,simp add:‹s' = cf'#cfx'#cfs'›)
        moreover
        from IH[OF ‹upd_cs cs' as = []› ‹same_level_path_aux cs' asx› 
          ‹∀c∈set cs'. valid_edge c› ‹targetnode a -as→* (_Low_)› 
          ‹targetnode a -asx→* (_Low_)› rvs' snds rv' calculation] ‹as' = ax#asx›
        show ?thesis by(simp add:slice_kinds_def)
      qed
    qed
  qed
qed


lemma rv_Low_Use_Low:
  assumes "m -as→* (_Low_)" and "m -as'→* (_Low_)" and "get_proc m = Main"
  and "∀V ∈ rv S (CFG_node m). cf V = cf' V"
  and "preds (slice_kinds S as) [(cf,undefined)]"
  and "preds (slice_kinds S as') [(cf',undefined)]"
  and "CFG_node (_Low_) ∈ S"
  shows "∀V ∈ Use (_Low_). 
    state_val (transfers(slice_kinds S as) [(cf,undefined)]) V =
    state_val (transfers(slice_kinds S as') [(cf',undefined)]) V"
proof(cases as)
  case Nil
  with ‹m -as→* (_Low_)› have "valid_node m" and "m = (_Low_)" 
    by(auto intro:path_valid_node simp:vp_def)
  { fix V assume "V ∈ Use (_Low_)"
    moreover
    from ‹valid_node m› ‹m = (_Low_)› have "(_Low_) -[]→ι* (_Low_)"
      by(fastforce intro:empty_path simp:intra_path_def)
    moreover
    from ‹valid_node m› ‹m = (_Low_)› ‹CFG_node (_Low_) ∈ S›
    have "CFG_node (_Low_) ∈ HRB_slice S"
      by(fastforce intro:HRB_slice_refl)
    ultimately have "V ∈ rv S (CFG_node m)" using ‹m = (_Low_)›
      by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def) }
  hence "∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)" by simp
  show ?thesis
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    from ‹m -as'→* (_Low_)› have "m -as'→* (_Low_)" by(simp add:vp_def)
    from ‹m -as'→* (_Low_)› ‹m = (_Low_)› have "as' = []"
    proof(induct m as' m'"(_Low_)" rule:path.induct)
      case (Cons_path m'' as a m)
      from ‹valid_edge a› ‹sourcenode a = m› ‹m = (_Low_)›
      have "targetnode a = (_Exit_)" by -(rule Exit_successor_of_Low,simp+)
      with ‹targetnode a = m''› ‹m'' -as→* (_Low_)›
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?case by simp
    qed simp
    with Nil ‹∀V ∈ rv S (CFG_node m). cf V = cf' V›
      ‹∀V ∈ Use (_Low_). V ∈ rv S (CFG_node m)›
    show ?thesis by(fastforce simp:slice_kinds_def)
  qed
next
  case (Cons ax asx)
  with ‹m -as→* (_Low_)› have "sourcenode ax = m" and "valid_edge ax"
    and "targetnode ax -asx→* (_Low_)"
    by(auto elim:path_split_Cons simp:vp_def)
  show ?thesis
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with ‹m -as'→* (_Low_)› have "m = (_Low_)" by(fastforce simp:vp_def)
      with ‹valid_edge ax› ‹sourcenode ax = m› have "targetnode ax = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from ‹valid_edge ax› ‹sourcenode ax = m› ‹m = (_Low_)› 
        ‹targetnode ax = (_Exit_)› ‹valid_edge a'› ‹sourcenode a' = (_Low_)› 
        ‹targetnode a' = (_Exit_)›
      have "ax = a'" by(fastforce dest:edge_det)
      with ‹kind a' = (λs. True) have "kind ax = (λs. True)" by simp
      with ‹targetnode ax = (_Exit_)› ‹targetnode ax -asx→* (_Low_)›
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax' asx')
      from ‹m -as→* (_Low_)› have "valid_path_aux [] as" and "m -as→* (_Low_)"
        by(simp_all add:vp_def valid_path_def)
      from this ‹as = ax#asx› ‹get_proc m = Main›
      have "same_level_path_aux [] as ∧ upd_cs [] as = []"
        by -(rule vpa_Main_slpa[of _ _ m "(_Low_)"],
        (fastforce intro!:get_proc_Low simp:valid_call_list_def)+)
      hence "same_level_path_aux [] as" and "upd_cs [] as = []" by simp_all
      from ‹m -as'→* (_Low_)› have "valid_path_aux [] as'" and "m -as'→* (_Low_)"
        by(simp_all add:vp_def valid_path_def)
      from this ‹as' = ax'#asx'› ‹get_proc m = Main›
      have "same_level_path_aux [] as' ∧ upd_cs [] as' = []"
        by -(rule vpa_Main_slpa[of _ _ m "(_Low_)"],
        (fastforce intro!:get_proc_Low simp:valid_call_list_def)+)
      hence "same_level_path_aux [] as'" by simp
      from ‹same_level_path_aux [] as› ‹upd_cs [] as = []›
        ‹same_level_path_aux [] as'› ‹m -as→* (_Low_)› ‹m -as'→* (_Low_)›
        ‹∀V ∈ rv S (CFG_node m). cf V = cf' V› ‹CFG_node (_Low_) ∈ S›
        ‹preds (slice_kinds S as) [(cf,undefined)]›
        ‹preds (slice_kinds S as') [(cf',undefined)]›
      show ?thesis by -(erule slpa_rv_Low_Use_Low,auto)
    qed
  qed
qed



lemma nonInterference_path_to_Low:
  assumes "[cf] ≈L [cf']" and "(_High_) ∉ ⌊HRB_slice S⌋CFG"
  and "CFG_node (_Low_) ∈ S"
  and "(_Entry_) -as→* (_Low_)" and "preds (kinds as) [(cf,undefined)]"
  and "(_Entry_) -as'→* (_Low_)" and "preds (kinds as') [(cf',undefined)]"
  shows "map fst (transfers (kinds as) [(cf,undefined)]) ≈L 
         map fst (transfers (kinds as') [(cf',undefined)])"
proof -
  from ‹(_Entry_) -as→* (_Low_)› ‹preds (kinds as) [(cf,undefined)]›
    ‹CFG_node (_Low_) ∈ S›
  obtain asx where "preds (slice_kinds S asx) [(cf,undefined)]"
    and "∀V ∈ Use (_Low_). 
    state_val (transfers (slice_kinds S asx) [(cf,undefined)]) V = 
    state_val (transfers (kinds as) [(cf,undefined)]) V"
    and "slice_edges S [] as = slice_edges S [] asx"
    and "transfers (kinds as) [(cf,undefined)] ≠ []"
    and "(_Entry_) -asx→* (_Low_)" 
    by(erule fundamental_property_of_static_slicing)
  from ‹(_Entry_) -as'→* (_Low_)› ‹preds (kinds as') [(cf',undefined)]›
    ‹CFG_node (_Low_) ∈ S›
  obtain asx' where "preds (slice_kinds S asx') [(cf',undefined)]"
    and "∀V ∈ Use (_Low_). 
    state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V = 
    state_val (transfers(kinds as') [(cf',undefined)]) V"
    and "slice_edges S [] as' = 
    slice_edges S [] asx'"
    and "transfers (kinds as') [(cf',undefined)] ≠ []"
    and "(_Entry_) -asx'→* (_Low_)"
    by(erule fundamental_property_of_static_slicing)
  from ‹[cf] ≈L [cf']› ‹(_High_) ∉ ⌊HRB_slice S⌋CFG
  have "∀V ∈ rv S (CFG_node (_Entry_)). cf V = cf' V" 
    by(fastforce dest:lowEquivalence_relevant_nodes_Entry)
  with ‹(_Entry_) -asx →*(_Low_)› ‹(_Entry_) -asx'→* (_Low_)›
    ‹CFG_node (_Low_) ∈ S› ‹preds (slice_kinds S asx) [(cf,undefined)]›
    ‹preds (slice_kinds S asx') [(cf',undefined)]›
  have "∀V ∈ Use (_Low_). 
    state_val (transfers(slice_kinds S asx) [(cf,undefined)]) V =
    state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V"
    by -(rule rv_Low_Use_Low,auto intro:get_proc_Entry)
  with ‹∀V ∈ Use (_Low_). 
    state_val (transfers (slice_kinds S asx) [(cf,undefined)]) V = 
    state_val (transfers (kinds as) [(cf,undefined)]) V›
    ‹∀V ∈ Use (_Low_). 
    state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V = 
    state_val (transfers(kinds as') [(cf',undefined)]) V›
    ‹transfers (kinds as) [(cf,undefined)] ≠ []› 
    ‹transfers (kinds as') [(cf',undefined)] ≠ []›
  show ?thesis by(fastforce simp:lowEquivalence_def UseLow neq_Nil_conv)
qed


theorem nonInterference_path:
  assumes "[cf] ≈L [cf']" and "(_High_) ∉ ⌊HRB_slice S⌋CFG"
  and "CFG_node (_Low_) ∈ S"
  and "(_Entry_) -as→* (_Exit_)" and "preds (kinds as) [(cf,undefined)]"
  and "(_Entry_) -as'→* (_Exit_)" and "preds (kinds as') [(cf',undefined)]"
  shows "map fst (transfers (kinds as) [(cf,undefined)]) ≈L 
  map fst (transfers (kinds as') [(cf',undefined)])"
proof -
  from ‹(_Entry_) -as→* (_Exit_)› obtain x xs where "as = x#xs"
    and "(_Entry_) = sourcenode x" and "valid_edge x" 
    and "targetnode x -xs→* (_Exit_)"
    apply(cases "as = []")
     apply(clarsimp simp:vp_def,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
    by(fastforce elim:path_split_Cons simp:vp_def)
  from ‹(_Entry_) -as→* (_Exit_)› have "valid_path as" by(simp add:vp_def)
  from ‹valid_edge x› have "valid_node (targetnode x)" by simp
  hence "inner_node (targetnode x)"
  proof(cases rule:valid_node_cases)
    case Entry
    with ‹valid_edge x› have False by(rule Entry_target)
    thus ?thesis by simp
  next
    case Exit
    with ‹targetnode x -xs→* (_Exit_)› have "xs = []"
      by -(drule path_Exit_source,auto)
    from Entry_Exit_edge obtain z where "valid_edge z"
      and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
      and "kind z = (λs. False)" by blast
    from ‹valid_edge x› ‹valid_edge z› ‹(_Entry_) = sourcenode x› 
      ‹sourcenode z = (_Entry_)› Exit ‹targetnode z = (_Exit_)›
    have "x = z" by(fastforce intro:edge_det)
    with ‹preds (kinds as) [(cf,undefined)]› ‹as = x#xs› ‹xs = []›
      ‹kind z = (λs. False) 
    have False by(simp add:kinds_def)
    thus ?thesis by simp
  qed simp
  with ‹targetnode x -xs→* (_Exit_)› obtain x' xs' where "xs = xs'@[x']"
    and "targetnode x -xs'→* (_Low_)" and "kind x' = (λs. True)"
    by(fastforce elim:Exit_path_Low_path)
  with ‹(_Entry_) = sourcenode x› ‹valid_edge x›
  have "(_Entry_) -x#xs'→* (_Low_)" by(fastforce intro:Cons_path)
  from ‹valid_path as› ‹as = x#xs› ‹xs = xs'@[x']›
  have "valid_path (x#xs')"
    by(simp add:valid_path_def del:valid_path_aux.simps)
      (rule valid_path_aux_split,simp)
  with ‹(_Entry_) -x#xs'→* (_Low_)› have "(_Entry_) -x#xs'→* (_Low_)"
    by(simp add:vp_def)
  from ‹as = x#xs› ‹xs = xs'@[x']› have "as = (x#xs')@[x']" by simp
  with ‹preds (kinds as) [(cf,undefined)]› 
  have "preds (kinds (x#xs')) [(cf,undefined)]"
    by(simp add:kinds_def preds_split)
  from ‹(_Entry_) -as'→* (_Exit_)› obtain y ys where "as' = y#ys"
    and "(_Entry_) = sourcenode y" and "valid_edge y" 
    and "targetnode y -ys→* (_Exit_)"
    apply(cases "as' = []")
     apply(clarsimp simp:vp_def,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
    by(fastforce elim:path_split_Cons simp:vp_def)
  from ‹(_Entry_) -as'→* (_Exit_)› have "valid_path as'" by(simp add:vp_def)
  from ‹valid_edge y› have "valid_node (targetnode y)" by simp
  hence "inner_node (targetnode y)"
  proof(cases rule:valid_node_cases)
    case Entry
    with ‹valid_edge y› have False by(rule Entry_target)
    thus ?thesis by simp
  next
    case Exit
    with ‹targetnode y -ys→* (_Exit_)› have "ys = []"
      by -(drule path_Exit_source,auto)
    from Entry_Exit_edge obtain z where "valid_edge z"
      and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
      and "kind z = (λs. False)" by blast
    from ‹valid_edge y› ‹valid_edge z› ‹(_Entry_) = sourcenode y› 
      ‹sourcenode z = (_Entry_)› Exit ‹targetnode z = (_Exit_)›
    have "y = z" by(fastforce intro:edge_det)
    with ‹preds (kinds as') [(cf',undefined)]› ‹as' = y#ys› ‹ys = []›
      ‹kind z = (λs. False) 
    have False by(simp add:kinds_def)
    thus ?thesis by simp
  qed simp
  with ‹targetnode y -ys→* (_Exit_)› obtain y' ys' where "ys = ys'@[y']"
    and "targetnode y -ys'→* (_Low_)" and "kind y' = (λs. True)"
    by(fastforce elim:Exit_path_Low_path)
  with ‹(_Entry_) = sourcenode y› ‹valid_edge y›
  have "(_Entry_) -y#ys'→* (_Low_)" by(fastforce intro:Cons_path)
  from ‹valid_path as'› ‹as' = y#ys› ‹ys = ys'@[y']›
  have "valid_path (y#ys')"
    by(simp add:valid_path_def del:valid_path_aux.simps)
      (rule valid_path_aux_split,simp)
  with ‹(_Entry_) -y#ys'→* (_Low_)› have "(_Entry_) -y#ys'→* (_Low_)"
    by(simp add:vp_def)
  from ‹as' = y#ys› ‹ys = ys'@[y']› have "as' = (y#ys')@[y']" by simp
  with ‹preds (kinds as') [(cf',undefined)]› 
  have "preds (kinds (y#ys')) [(cf',undefined)]"
    by(simp add:kinds_def preds_split)
  from ‹[cf] ≈L [cf']› ‹(_High_) ∉ ⌊HRB_slice S⌋CFG ‹CFG_node (_Low_) ∈ S›
    ‹(_Entry_) -x#xs'→* (_Low_)› ‹preds (kinds (x#xs')) [(cf,undefined)]›
    ‹(_Entry_) -y#ys'→* (_Low_)› ‹preds (kinds (y#ys')) [(cf',undefined)]›
  have "map fst (transfers (kinds (x#xs')) [(cf,undefined)]) ≈L 
    map fst (transfers (kinds (y#ys')) [(cf',undefined)])"
    by(rule nonInterference_path_to_Low)
  with ‹as = x#xs› ‹xs = xs'@[x']› ‹kind x' = (λs. True)
    ‹as' = y#ys› ‹ys = ys'@[y']› ‹kind y' = (λs. True)
  show ?thesis
    apply(cases "transfers (map kind xs') (transfer (kind x) [(cf,undefined)])")
    apply (auto simp add:kinds_def transfers_split)
    by((cases "transfers (map kind ys') (transfer (kind y) [(cf',undefined)])"),
       (auto simp add:kinds_def transfers_split))+
qed


end

text ‹The second theorem assumes that we have a operational semantics,
whose evaluations are written ‹⟨c,s⟩ ⇒ ⟨c',s'⟩› and which conforms 
to the CFG. The correctness theorem then states that if no high variable
influenced a low variable and the initial states were low equivalent, the
reulting states are again low equivalent:›


locale NonInterferenceInter = 
  NonInterferenceInterGraph sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses 
    H L High Low +
  SemanticsProperty sourcenode targetnode kind valid_edge Entry get_proc
    get_return_edges procs Main Exit Def Use ParamDefs ParamUses sem identifies
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") 
  and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
  and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list"
  and sem :: "'com ⇒ ('var ⇀ 'val) list ⇒ 'com ⇒ ('var ⇀ 'val) list ⇒ bool" 
    ("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
  and identifies :: "'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51,0] 80)
  and H :: "'var set" and L :: "'var set" 
  and High :: "'node"  ("'('_High'_')") and Low :: "'node" ("'('_Low'_')") +
  fixes final :: "'com ⇒ bool"
  assumes final_edge_Low: "⟦final c; n ≜ c⟧ 
    ⟹ ∃a. valid_edge a ∧ sourcenode a = n ∧ targetnode a = (_Low_) ∧ kind a = ⇑id"
begin


text‹The following theorem needs the explicit edge from ‹(_High_)›
  to ‹n›. An approach using a ‹init› predicate for initial statements,
  being reachable from ‹(_High_)› via a ‹(λs. True)› edge,
  does not work as the same statement could be identified by several nodes, some
  initial, some not. E.g., in the program \texttt{while (True) Skip;;Skip}
  two nodes identify this inital statement: the initial node and the node
  within the loop (because of loop unrolling).›

theorem nonInterference:
  assumes "[cf1] ≈L [cf2]" and "(_High_) ∉ ⌊HRB_slice S⌋CFG"
  and "CFG_node (_Low_) ∈ S"
  and "valid_edge a" and "sourcenode a = (_High_)" and "targetnode a = n" 
  and "kind a = (λs. True)" and "n ≜ c" and "final c'"
  and "⟨c,[cf1]⟩ ⇒ ⟨c',s1⟩" and "⟨c,[cf2]⟩ ⇒ ⟨c',s2⟩"
  shows "s1L s2"
proof -
  from High_target_Entry_edge obtain ax where "valid_edge ax"
    and "sourcenode ax = (_Entry_)" and "targetnode ax = (_High_)"
    and "kind ax = (λs. True)" by blast
  from ‹n ≜ c› ‹⟨c,[cf1]⟩ ⇒ ⟨c',s1⟩›
  obtain n1 as1 cfs1 where "n -as1* n1" and "n1 ≜ c'"
    and "preds (kinds as1) [(cf1,undefined)]" 
    and "transfers (kinds as1) [(cf1,undefined)] = cfs1" and "map fst cfs1 = s1"
    by(fastforce dest:fundamental_property)
  from ‹n -as1* n1 ‹valid_edge a› ‹sourcenode a = (_High_)› ‹targetnode a = n›
    ‹kind a = (λs. True)
  have "(_High_) -a#as1* n1" by(fastforce intro:Cons_path simp:vp_def valid_path_def)
  from ‹final c'› ‹n1 ≜ c'›
  obtain a1 where "valid_edge a1" and "sourcenode a1 = n1" 
    and "targetnode a1 = (_Low_)" and "kind a1 = ⇑id" by(fastforce dest:final_edge_Low)
  hence "n1 -[a1]→* (_Low_)" by(fastforce intro:path_edge)
  with ‹(_High_) -a#as1* n1 have "(_High_) -(a#as1)@[a1]→* (_Low_)"
    by(fastforce intro!:path_Append simp:vp_def)
  with ‹valid_edge ax› ‹sourcenode ax = (_Entry_)› ‹targetnode ax = (_High_)›
  have "(_Entry_) -ax#((a#as1)@[a1])→* (_Low_)" by -(rule Cons_path)
  moreover
  from ‹(_High_) -a#as1* n1 have "valid_path_aux [] (a#as1)"
    by(simp add:vp_def valid_path_def)
  with ‹kind a1 = ⇑id› have "valid_path_aux [] ((a#as1)@[a1])"
    by(fastforce intro:valid_path_aux_Append)
  with ‹kind ax = (λs. True) have "valid_path_aux [] (ax#((a#as1)@[a1]))"
    by simp
  ultimately have "(_Entry_) -ax#((a#as1)@[a1])→* (_Low_)"
    by(simp add:vp_def valid_path_def)
  from ‹valid_edge a› ‹kind a = (λs. True) ‹sourcenode a = (_High_)›
    ‹targetnode a = n›
  have "get_proc n = get_proc (_High_)"
    by(fastforce dest:get_proc_intra simp:intra_kind_def)
  with get_proc_High have "get_proc n = Main" by simp
  from ‹valid_edge a1 ‹sourcenode a1 = n1 ‹targetnode a1 = (_Low_)› ‹kind a1 = ⇑id›
  have "get_proc n1 = get_proc (_Low_)"
    by(fastforce dest:get_proc_intra simp:intra_kind_def)
  with get_proc_Low have "get_proc n1 = Main" by simp
  from ‹n -as1* n1 have "n -as1sl* n1"
    by(cases as1)
      (auto dest!:vpa_Main_slpa intro:‹get_proc n1 = Main› ‹get_proc n = Main›
             simp:vp_def valid_path_def valid_call_list_def slp_def 
                  same_level_path_def simp del:valid_path_aux.simps)
  then obtain cfx r where cfx:"transfers (map kind as1) [(cf1,undefined)] = [(cfx,r)]"
    by(fastforce elim:slp_callstack_length_equal simp:kinds_def)
  from ‹kind ax = (λs. True) ‹kind a = (λs. True) 
    ‹preds (kinds as1) [(cf1,undefined)]› ‹kind a1 = ⇑id› cfx 
  have "preds (kinds (ax#((a#as1)@[a1]))) [(cf1,undefined)]"
    by(auto simp:kinds_def preds_split)
  from ‹n ≜ c› ‹⟨c,[cf2]⟩ ⇒ ⟨c',s2⟩›
  obtain n2 as2 cfs2 where "n -as2* n2" and "n2 ≜ c'"
    and "preds (kinds as2) [(cf2,undefined)]" 
    and "transfers (kinds as2) [(cf2,undefined)] = cfs2" and "map fst cfs2 = s2"
    by(fastforce dest:fundamental_property)
  from ‹n -as2* n2 ‹valid_edge a› ‹sourcenode a = (_High_)› ‹targetnode a = n›
    ‹kind a = (λs. True)
  have "(_High_) -a#as2* n2" by(fastforce intro:Cons_path simp:vp_def valid_path_def)
  from ‹final c'› ‹n2 ≜ c'›
  obtain a2 where "valid_edge a2" and "sourcenode a2 = n2" 
    and "targetnode a2 = (_Low_)" and "kind a2 = ⇑id" by(fastforce dest:final_edge_Low)
  hence "n2 -[a2]→* (_Low_)" by(fastforce intro:path_edge)
  with ‹(_High_) -a#as2* n2 have "(_High_) -(a#as2)@[a2]→* (_Low_)"
    by(fastforce intro!:path_Append simp:vp_def)
  with ‹valid_edge ax› ‹sourcenode ax = (_Entry_)› ‹targetnode ax = (_High_)›
  have "(_Entry_) -ax#((a#as2)@[a2])→* (_Low_)" by -(rule Cons_path)
  moreover
  from ‹(_High_) -a#as2* n2 have "valid_path_aux [] (a#as2)"
    by(simp add:vp_def valid_path_def)
  with ‹kind a2 = ⇑id› have "valid_path_aux [] ((a#as2)@[a2])"
    by(fastforce intro:valid_path_aux_Append)
  with ‹kind ax = (λs. True) have "valid_path_aux [] (ax#((a#as2)@[a2]))"
    by simp
  ultimately have "(_Entry_) -ax#((a#as2)@[a2])→* (_Low_)"
    by(simp add:vp_def valid_path_def)
  from ‹valid_edge a› ‹kind a = (λs. True) ‹sourcenode a = (_High_)›
    ‹targetnode a = n›
  have "get_proc n = get_proc (_High_)"
    by(fastforce dest:get_proc_intra simp:intra_kind_def)
  with get_proc_High have "get_proc n = Main" by simp
  from ‹valid_edge a2 ‹sourcenode a2 = n2 ‹targetnode a2 = (_Low_)› ‹kind a2 = ⇑id›
  have "get_proc n2 = get_proc (_Low_)"
    by(fastforce dest:get_proc_intra simp:intra_kind_def)
  with get_proc_Low have "get_proc n2 = Main" by simp
  from ‹n -as2* n2 have "n -as2sl* n2"
    by(cases as2)
      (auto dest!:vpa_Main_slpa intro:‹get_proc n2 = Main› ‹get_proc n = Main›
             simp:vp_def valid_path_def valid_call_list_def slp_def 
                  same_level_path_def simp del:valid_path_aux.simps)
  then obtain cfx' r' 
    where cfx':"transfers (map kind as2) [(cf2,undefined)] = [(cfx',r')]"
    by(fastforce elim:slp_callstack_length_equal simp:kinds_def)
  from ‹kind ax = (λs. True) ‹kind a = (λs. True) 
    ‹preds (kinds as2) [(cf2,undefined)]› ‹kind a2 = ⇑id› cfx' 
  have "preds (kinds (ax#((a#as2)@[a2]))) [(cf2,undefined)]"
    by(auto simp:kinds_def preds_split)
  from ‹[cf1] ≈L [cf2]› ‹(_High_) ∉ ⌊HRB_slice S⌋CFG ‹CFG_node (_Low_) ∈ S›
    ‹(_Entry_) -ax#((a#as1)@[a1])→* (_Low_)› 
    ‹preds (kinds (ax#((a#as1)@[a1]))) [(cf1,undefined)]›
    ‹(_Entry_) -ax#((a#as2)@[a2])→* (_Low_)› 
    ‹preds (kinds (ax#((a#as2)@[a2]))) [(cf2,undefined)]›
  have "map fst (transfers (kinds (ax#((a#as1)@[a1]))) [(cf1,undefined)]) ≈L 
        map fst (transfers (kinds (ax#((a#as2)@[a2]))) [(cf2,undefined)])"
    by(rule nonInterference_path_to_Low)
  with ‹kind ax = (λs. True) ‹kind a = (λs. True) ‹kind a1 = ⇑id› ‹kind a2 = ⇑id›
    ‹transfers (kinds as1) [(cf1,undefined)] = cfs1 ‹map fst cfs1 = s1
    ‹transfers (kinds as2) [(cf2,undefined)] = cfs2 ‹map fst cfs2 = s2
  show ?thesis by(cases s1)(cases s2,(fastforce simp:kinds_def transfers_split)+)+
qed


end

end