Theory SCDObservable

section ‹Observable sets w.r.t.\ standard control dependence›

theory SCDObservable imports Observable HRBSlice begin

context SDG begin

lemma matched_bracket_assms_variant:
  assumes "n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V'→⇘in⇙ n⇩2" and "matched n⇩2 ns' n⇩3" 
  and "n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4"
  and "call_of_return_node (parent_node n⇩4) (parent_node n⇩1)"
  obtains a a' where "valid_edge a" and "a' ∈ get_return_edges a"
  and "sourcenode a = parent_node n⇩1" and "targetnode a = parent_node n⇩2"
  and "sourcenode a' = parent_node n⇩3" and "targetnode a' = parent_node n⇩4"
proof(atomize_elim)
  from ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V'→⇘in⇙ n⇩2› obtain a Q r fs where "valid_edge a" 
    and "kind a = Q:r↪⇘p⇙fs" and "parent_node n⇩1 = sourcenode a"
    and "parent_node n⇩2 = targetnode a"
    by(fastforce elim:SDG_edge.cases)
  from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› obtain a' Q' f'
    where "valid_edge a'" and "kind a' = Q'↩⇘p⇙f'"
    and "parent_node n⇩3 = sourcenode a'" and "parent_node n⇩4 = targetnode a'"
    by(fastforce elim:SDG_edge.cases)
  from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
  obtain ax where "valid_edge ax" and "∃Q r fs. kind ax = Q:r↪⇘p⇙fs"
    and "a' ∈ get_return_edges ax"
    by -(drule return_needs_call,fastforce+)
  from ‹valid_edge a› ‹valid_edge ax› ‹kind a = Q:r↪⇘p⇙fs› ‹∃Q r fs. kind ax = Q:r↪⇘p⇙fs›
  have "targetnode a = targetnode ax" by(fastforce dest:same_proc_call_unique_target)
  from ‹valid_edge a'› ‹a' ∈ get_return_edges ax› ‹valid_edge ax›
  have "call_of_return_node (targetnode a') (sourcenode ax)"
    by(fastforce simp:return_node_def call_of_return_node_def)
  with ‹call_of_return_node (parent_node n⇩4) (parent_node n⇩1)› 
    ‹parent_node n⇩4 = targetnode a'›
  have "sourcenode ax = parent_node n⇩1" by fastforce
  with ‹valid_edge ax› ‹a' ∈ get_return_edges ax› ‹targetnode a = targetnode ax›
    ‹parent_node n⇩2 = targetnode a› ‹parent_node n⇩3 = sourcenode a'› 
    ‹parent_node n⇩4 = targetnode a'›
  show "∃a a'. valid_edge a ∧ a' ∈ get_return_edges a ∧
    sourcenode a = parent_node n⇩1 ∧ targetnode a = parent_node n⇩2 ∧
    sourcenode a' = parent_node n⇩3 ∧ targetnode a' = parent_node n⇩4"
    by fastforce
qed

subsection ‹Observable set of standard control dependence is at most a singleton›

definition SDG_to_CFG_set :: "'node SDG_node set ⇒ 'node set" (‹⌊_⌋⇘CFG⇙›)
  where "⌊S⌋⇘CFG⇙ ≡ {m. CFG_node m ∈ S}"


lemma [intro]:"∀n ∈ S. valid_SDG_node n ⟹ ∀n ∈ ⌊S⌋⇘CFG⇙. valid_node n"
  by(fastforce simp:SDG_to_CFG_set_def)


lemma Exit_HRB_Slice:
  assumes "n ∈ ⌊HRB_slice {CFG_node (_Exit_)}⌋⇘CFG⇙" shows "n = (_Exit_)"
proof -
  from ‹n ∈ ⌊HRB_slice {CFG_node (_Exit_)}⌋⇘CFG⇙› 
  have "CFG_node n ∈ HRB_slice {CFG_node (_Exit_)}"
    by(simp add:SDG_to_CFG_set_def)
  thus ?thesis
  proof(induct "CFG_node n" rule:HRB_slice_cases)
    case (phase1 nx)
    from ‹nx ∈ {CFG_node (_Exit_)}› have "nx = CFG_node (_Exit_)" by simp
    with ‹CFG_node n ∈ sum_SDG_slice1 nx›
    have "CFG_node n = CFG_node (_Exit_) ∨ 
      (∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
      by(induct rule:sum_SDG_slice1.induct) auto
    then show ?thesis by(fastforce dest:Exit_no_sum_SDG_edge_target)
  next
    case (phase2 nx n' n'' p)
    from ‹nx ∈ {CFG_node (_Exit_)}› have "nx = CFG_node (_Exit_)" by simp
    with ‹n' ∈ sum_SDG_slice1 nx›
    have "n' = CFG_node (_Exit_) ∨ 
      (∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
      by(induct rule:sum_SDG_slice1.induct) auto
    hence "n' = CFG_node (_Exit_)" by(fastforce dest:Exit_no_sum_SDG_edge_target)
    with ‹CFG_node n ∈ sum_SDG_slice2 n'›
    have "CFG_node n = CFG_node (_Exit_) ∨ 
      (∃n Vopt popt b. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)))"
      by(induct rule:sum_SDG_slice2.induct) auto
    then show ?thesis by(fastforce dest:Exit_no_sum_SDG_edge_target)
  qed
qed


lemma Exit_in_obs_intra_slice_node:
  assumes "(_Exit_) ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙"
  shows "CFG_node (_Exit_) ∈ S"
proof -
  let ?S' = "⌊HRB_slice S⌋⇘CFG⇙"
  from ‹(_Exit_) ∈ obs_intra n' ?S'› obtain as where "n' -as→⇩ι* (_Exit_)"
    and "∀nx ∈ set(sourcenodes as). nx ∉ ?S'" and "(_Exit_) ∈ ?S'"
    by(erule obs_intraE)
  from ‹(_Exit_) ∈ ?S'› 
  have "CFG_node (_Exit_) ∈ HRB_slice S" by(simp add:SDG_to_CFG_set_def)
  thus ?thesis
  proof(induct "CFG_node (_Exit_)" rule:HRB_slice_cases)
    case (phase1 nx)
    thus ?case
      by(induct "CFG_node (_Exit_)" rule:sum_SDG_slice1.induct,
        auto dest:Exit_no_sum_SDG_edge_source)
  next
    case (phase2 nx n' n'' p)
    from ‹CFG_node (_Exit_) ∈ sum_SDG_slice2 n'› ‹n' ∈ sum_SDG_slice1 nx› ‹nx ∈ S›
    show ?case
      apply(induct n≡"CFG_node (_Exit_)" rule:sum_SDG_slice2.induct)
      apply(auto dest:Exit_no_sum_SDG_edge_source)
      apply(hypsubst_thin)
      apply(induct n≡"CFG_node (_Exit_)" rule:sum_SDG_slice1.induct)
      apply(auto dest:Exit_no_sum_SDG_edge_source)
      done
  qed
qed


lemma obs_intra_postdominate:
  assumes "n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙" and "¬ method_exit n"
  shows "n postdominates n'"
proof(rule ccontr)
  assume "¬ n postdominates n'"
  from ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› have "valid_node n" 
    by(fastforce dest:in_obs_intra_valid)
  with ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› ‹¬ method_exit n› have "n postdominates n"
    by(fastforce intro:postdominate_refl)
  from ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› obtain as where "n' -as→⇩ι* n"
    and all_notinS:"∀n' ∈ set(sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    and "n ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(erule obs_intraE)
  from ‹n postdominates n› ‹¬ n postdominates n'› ‹n' -as→⇩ι* n›
  obtain as' a as'' where [simp]:"as = as'@a#as''"
    and "valid_edge a" and "¬ n postdominates (sourcenode a)"
    and "n postdominates (targetnode a)"  and "intra_kind (kind a)"
    by(fastforce elim!:postdominate_path_branch simp:intra_path_def)
  from ‹n' -as→⇩ι* n› have "sourcenode a -a#as''→⇩ι* n"
    by(fastforce elim:path_split intro:Cons_path simp:intra_path_def)
  with ‹¬ n postdominates (sourcenode a)› ‹valid_edge a› ‹valid_node n› 
  obtain asx pex where "sourcenode a -asx→⇩ι* pex" and "method_exit pex" 
    and "n ∉ set(sourcenodes asx)" by(fastforce simp:postdominate_def)
  have "asx ≠ []"
  proof
    assume "asx = []"
    with ‹sourcenode a -asx→⇩ι* pex› have "sourcenode a = pex" 
      by(fastforce simp:intra_path_def)
    from ‹method_exit pex› show False
    proof(rule method_exit_cases)
      assume "pex = (_Exit_)"
      with ‹sourcenode a = pex› have "sourcenode a = (_Exit_)" by simp
      with ‹valid_edge a› show False by(rule Exit_source)
    next
      fix a' Q f p
      assume "pex = sourcenode a'" and "valid_edge a'" and "kind a' = Q↩⇘p⇙f"
      from ‹valid_edge a'› ‹kind a' = Q↩⇘p⇙f› ‹valid_edge a› ‹intra_kind (kind a)›
        ‹sourcenode a = pex› ‹pex = sourcenode a'›
      show False by(fastforce dest:return_edges_only simp:intra_kind_def)
    qed
  qed
  then obtain ax asx' where [simp]:"asx = ax#asx'" by(cases asx) auto
  with ‹sourcenode a -asx→⇩ι* pex› have "sourcenode a -ax#asx'→* pex"
    by(simp add:intra_path_def)
  hence "valid_edge ax" and [simp]:"sourcenode a = sourcenode ax"
    and "targetnode ax -asx'→* pex" by(auto elim:path_split_Cons)
  with ‹sourcenode a -asx→⇩ι* pex› have "targetnode ax -asx'→⇩ι* pex"
    by(simp add:intra_path_def)
  with ‹valid_edge ax› ‹n ∉ set(sourcenodes asx)› ‹method_exit pex›
  have "¬ n postdominates targetnode ax"
    by(fastforce simp:postdominate_def sourcenodes_def)
  from ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› all_notinS 
  have "n ∉ set (sourcenodes (a#as''))"
    by(fastforce elim:obs_intra.cases simp:sourcenodes_def)
  from ‹sourcenode a -asx→⇩ι* pex› have "intra_kind (kind ax)"
    by(simp add:intra_path_def)
  with ‹sourcenode a -a#as''→⇩ι* n› ‹n postdominates (targetnode a)› 
    ‹¬ n postdominates targetnode ax› ‹valid_edge ax› 
    ‹n ∉ set (sourcenodes (a#as''))› ‹intra_kind (kind a)›
  have "(sourcenode a) controls n"
    by(fastforce simp:control_dependence_def)
  hence "CFG_node (sourcenode a) s⟶⇘cd⇙ CFG_node n"
    by(fastforce intro:sum_SDG_cdep_edge)
  with ‹n ∈ obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙› have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    by(auto elim!:obs_intraE combine_SDG_slices.cases 
            intro:combine_SDG_slices.intros sum_SDG_slice1.intros 
                  sum_SDG_slice2.intros simp:HRB_slice_def SDG_to_CFG_set_def)
  with all_notinS show False by(simp add:sourcenodes_def)
qed



lemma obs_intra_singleton_disj: 
  assumes "valid_node n"
  shows "(∃m. obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}) ∨ 
         obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {}"
proof(rule ccontr)
  assume "¬ ((∃m. obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}) ∨ 
             obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {})"
  hence "∃nx nx'. nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ∧ 
    nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ∧ nx ≠ nx'" by auto
  then obtain nx nx' where "nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙" 
    and "nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙" and "nx ≠ nx'" by auto
  from ‹nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› obtain as where "n -as→⇩ι* nx" 
    and all:"∀n' ∈ set(sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙" 
    and "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙" 
    by(erule obs_intraE)
  from ‹n -as→⇩ι* nx› have "n -as→* nx" and "∀a ∈ set as. intra_kind (kind a)"
    by(simp_all add:intra_path_def)
  hence "valid_node nx" by(fastforce dest:path_valid_node)
  with ‹nx ∈ ⌊HRB_slice S⌋⇘CFG⇙› have "obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}" 
    by -(rule n_in_obs_intra)
  with ‹n -as→* nx› ‹nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› 
    ‹nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ nx'› have "as ≠ []" 
    by(fastforce elim:path.cases simp:intra_path_def)
  with ‹n -as→* nx› ‹nx ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› 
    ‹nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ nx'› 
    ‹obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}› ‹∀a ∈ set as. intra_kind (kind a)› all
  have "∃a as' as''. n -as'→⇩ι* sourcenode a ∧ targetnode a -as''→⇩ι* nx ∧
                     valid_edge a ∧ as = as'@a#as'' ∧ intra_kind (kind a) ∧
                     obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx} ∧ 
                    (¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨ 
                       obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}))"
  proof(induct arbitrary:nx' rule:path.induct)
    case (Cons_path n'' as n' a n)
    note IH = ‹⋀nx'. ⟦n' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙; 
                       nx' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙; n' ≠ nx'; 
                       obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'};
                       ∀a∈set as. intra_kind (kind a);
                       ∀n'∈set (sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙; as ≠ []⟧
      ⟹ ∃a as' as''. n'' -as'→⇩ι* sourcenode a ∧ targetnode a -as''→⇩ι* n' ∧
        valid_edge a ∧ as = as'@a#as'' ∧ intra_kind (kind a) ∧
        obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {n'} ∧
        (¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨ 
           obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {}))›
    note more_than_one = ‹n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙›
      ‹nx' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙› ‹n' ≠ nx'›
    from ‹∀a∈set (a#as). intra_kind (kind a)›
    have "∀a∈set as. intra_kind (kind a)" and "intra_kind (kind a)" by simp_all
    from ‹∀n'∈set (sourcenodes (a#as)). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
    have all:"∀n'∈set (sourcenodes as). n' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
      by(simp add:sourcenodes_def)
    show ?case
    proof(cases "as = []")
      case True
      with ‹n'' -as→* n'› have [simp]:"n'' = n'" by(fastforce elim:path.cases)
      from more_than_one ‹sourcenode a = n›
      have "¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨ 
               obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {})"
        by auto
      with ‹targetnode a = n''› ‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}›
        ‹sourcenode a = n› True ‹valid_edge a› ‹intra_kind (kind a)› 
      show ?thesis
        apply(rule_tac x="a" in exI)
        apply(rule_tac x="[]" in exI)
        apply(rule_tac x="[]" in exI)
        by(auto intro:empty_path simp:intra_path_def)
    next
      case False
      from ‹n'' -as→* n'› ‹∀a∈set (a # as). intra_kind (kind a)›
      have "n'' -as→⇩ι* n'" by(simp add:intra_path_def)
      with all 
      have subset:"obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ ⊆ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙"
        by -(rule path_obs_intra_subset)
      thus ?thesis
      proof(cases "obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙")
        case True
        with ‹n'' -as→⇩ι* n'› ‹valid_edge a› ‹sourcenode a = n› ‹targetnode a = n''›
          ‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}› ‹intra_kind (kind a)› more_than_one
        show ?thesis
          apply(rule_tac x="a" in exI)
          apply(rule_tac x="[]" in exI)
          apply(rule_tac x="as" in exI)
          by(fastforce intro:empty_path simp:intra_path_def)
      next
        case False
        with subset
        have "obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ ⊂ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙" by simp
        with ‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}› 
        obtain ni where "n' ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙"
          and "ni ∈ obs_intra n'' ⌊HRB_slice S⌋⇘CFG⇙" and "n' ≠ ni" by auto
        from IH[OF this ‹obs_intra n' ⌊HRB_slice S⌋⇘CFG⇙ = {n'}› 
          ‹∀a∈set as. intra_kind (kind a)› all ‹as ≠ []›] obtain a' as' as''
          where "n'' -as'→⇩ι* sourcenode a'" 
          and hyps:"targetnode a' -as''→⇩ι* n'" "valid_edge a'" "as = as'@a'#as''" 
            "intra_kind (kind a')" "obs_intra (targetnode a') ⌊HRB_slice S⌋⇘CFG⇙ = {n'}"
            "¬ (∃m. obs_intra (sourcenode a') ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨ 
                                obs_intra (sourcenode a') ⌊HRB_slice S⌋⇘CFG⇙ = {})"
          by blast
        from ‹n'' -as'→⇩ι* sourcenode a'› ‹valid_edge a› ‹sourcenode a = n› 
          ‹targetnode a = n''› ‹intra_kind (kind a)› ‹intra_kind (kind a')›
        have "n -a#as'→⇩ι* sourcenode a'"
          by(fastforce intro:path.Cons_path simp:intra_path_def)
        with hyps show ?thesis
          apply(rule_tac x="a'" in exI)
          apply(rule_tac x="a#as'" in exI)
          apply(rule_tac x="as''" in exI)
          by fastforce
      qed
    qed
  qed simp
  then obtain a as' as'' where "valid_edge a" and "intra_kind (kind a)"
    and "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}"
    and more_than_one:"¬ (∃m. obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m} ∨ 
                         obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {})"
    by blast
  have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
  proof(rule ccontr)
    assume "¬ sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    hence "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙" by simp
    with ‹valid_edge a›
    have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
      by(fastforce intro!:n_in_obs_intra)
    with more_than_one show False by simp
  qed
  with ‹valid_edge a› ‹intra_kind (kind a)›
  have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆ 
        obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
    by(rule edge_obs_intra_subset)
  with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}› 
  have "nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" by simp
  with more_than_one obtain m 
    where "m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙" and "nx ≠ m" by auto
  from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› have "valid_node m" 
    by(fastforce dest:in_obs_intra_valid)
  from ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}› have "valid_node nx"
    by(fastforce dest:in_obs_intra_valid)
  show False
  proof(cases "m postdominates (sourcenode a)")
    case True
    with ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
      ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
    have "m postdominates nx"
      by(fastforce intro:postdominate_inner_path_targetnode elim:obs_intraE)
    with ‹nx ≠ m› have "¬ nx postdominates m" by(fastforce dest:postdominate_antisym)
    with ‹valid_node nx› ‹valid_node m› obtain asx pex where "m -asx→⇩ι* pex"
      and "method_exit pex" and "nx ∉ set(sourcenodes asx)"
      by(fastforce simp:postdominate_def)
    have "¬ nx postdominates (sourcenode a)"
    proof
      assume "nx postdominates sourcenode a"
      from ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
        ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
      obtain asx' where "sourcenode a -asx'→⇩ι* m" and "nx ∉ set(sourcenodes asx')"
        by(fastforce elim:obs_intraE)
      with ‹m -asx→⇩ι* pex› have "sourcenode a -asx'@asx→⇩ι* pex"
        by(fastforce intro:path_Append simp:intra_path_def)
      with ‹nx ∉ set(sourcenodes asx)› ‹nx ∉ set(sourcenodes asx')› 
        ‹nx postdominates sourcenode a› ‹method_exit pex› show False
        by(fastforce simp:sourcenodes_def postdominate_def)
    qed
    show False
    proof(cases "method_exit nx")
      case True
      from ‹m postdominates nx› obtain xs where "nx -xs→⇩ι* m"
        by -(erule postdominate_implies_inner_path)
      with True have "nx = m"
        by(fastforce dest!:method_exit_inner_path simp:intra_path_def)
      with ‹nx ≠ m› show False by simp
    next
      case False
      with ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
      have "nx postdominates sourcenode a" by(rule obs_intra_postdominate)
      with ‹¬ nx postdominates (sourcenode a)› show False by simp
    qed
  next
    case False
    show False
    proof(cases "method_exit m")
      case True
      from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
        ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
      obtain xs where "sourcenode a -xs→⇩ι* m" and "nx ∉ set(sourcenodes xs)"
        by(fastforce elim:obs_intraE)
      obtain x' xs' where [simp]:"xs = x'#xs'"
      proof(cases xs)
        case Nil
        with ‹sourcenode a -xs→⇩ι* m› have [simp]:"sourcenode a = m"
          by(fastforce simp:intra_path_def)
        with ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› 
        have "m ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(metis obs_intraE)
        with ‹valid_node m› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
          by(rule n_in_obs_intra)
        with ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ m› have False
          by fastforce
        thus ?thesis by simp
      qed blast
      from ‹sourcenode a -xs→⇩ι* m› have "sourcenode a = sourcenode x'" 
        and "valid_edge x'" and "targetnode x' -xs'→⇩ι* m"
        and "intra_kind (kind x')"
        by(auto elim:path_split_Cons simp:intra_path_def)
      from ‹targetnode x' -xs'→⇩ι* m› ‹nx ∉ set(sourcenodes xs)› ‹valid_edge x'› 
        ‹valid_node m› True
      have "¬ nx postdominates (targetnode x')" 
        by(fastforce simp:postdominate_def sourcenodes_def)
      show False
      proof(cases "method_exit nx")
        case True
        from ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
          ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
        have "get_proc m = get_proc nx"
          by(fastforce elim:obs_intraE dest:intra_path_get_procs)
        with ‹method_exit m› ‹method_exit nx› have "m = nx"
          by(rule method_exit_unique)
        with ‹nx ≠ m› show False by simp
      next 
        case False
        with ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}›
        have "nx postdominates (targetnode a)"
          by(fastforce intro:obs_intra_postdominate)
        from ‹obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {nx}›
        obtain ys where "targetnode a -ys→⇩ι* nx" 
          and "∀nx' ∈ set(sourcenodes ys). nx' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
          and "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙" by(fastforce elim:obs_intraE)
        hence "nx ∉ set(sourcenodes ys)"by fastforce
        have "sourcenode a ≠ nx"
        proof
          assume "sourcenode a = nx"
          from ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
          have "nx ∈ ⌊HRB_slice S⌋⇘CFG⇙" by -(erule obs_intraE)
          with ‹valid_node nx›
          have "obs_intra nx ⌊HRB_slice S⌋⇘CFG⇙ = {nx}" by -(erule n_in_obs_intra)
          with ‹sourcenode a = nx› ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› 
            ‹nx ≠ m› show False by fastforce
        qed
        with ‹nx ∉ set(sourcenodes ys)› have "nx ∉ set(sourcenodes (a#ys))"
          by(fastforce simp:sourcenodes_def)
        from ‹valid_edge a› ‹targetnode a -ys→⇩ι* nx› ‹intra_kind (kind a)›
        have "sourcenode a -a#ys→⇩ι* nx"
          by(fastforce intro:Cons_path simp:intra_path_def)
        from ‹sourcenode a -a#ys→⇩ι* nx› ‹nx ∉ set(sourcenodes (a#ys))›
          ‹intra_kind (kind a)› ‹nx postdominates (targetnode a)›
          ‹valid_edge x'› ‹intra_kind (kind x')› ‹¬ nx postdominates (targetnode x')›
          ‹sourcenode a = sourcenode x'›
        have "(sourcenode a) controls nx"
          by(fastforce simp:control_dependence_def)
        hence "CFG_node (sourcenode a) ⟶⇘cd⇙ CFG_node nx" 
          by(fastforce intro:SDG_cdep_edge)
        with ‹nx ∈ ⌊HRB_slice S⌋⇘CFG⇙› have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
          by(fastforce elim!:combine_SDG_slices.cases
                       dest:SDG_edge_sum_SDG_edge cdep_slice1 cdep_slice2 
                      intro:combine_SDG_slices.intros
                       simp:HRB_slice_def SDG_to_CFG_set_def)
        with ‹valid_edge a› 
        have "obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙ = {sourcenode a}"
          by(fastforce intro!:n_in_obs_intra)
        with ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
          ‹nx ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹nx ≠ m›
        show False by simp
      qed
    next
      case False
      with ‹m ∈ obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙›
      have "m postdominates (sourcenode a)" by(rule obs_intra_postdominate)
      with ‹¬ m postdominates (sourcenode a)› show False by simp
    qed
  qed
qed



lemma obs_intra_finite:"valid_node n ⟹ finite (obs_intra n ⌊HRB_slice S⌋⇘CFG⇙)"
by(fastforce dest:obs_intra_singleton_disj[of _ S])

lemma obs_intra_singleton:"valid_node n ⟹ card (obs_intra n ⌊HRB_slice S⌋⇘CFG⇙) ≤ 1"
by(fastforce dest:obs_intra_singleton_disj[of _ S])


lemma obs_intra_singleton_element:
  "m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ⟹ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
apply -
apply(frule in_obs_intra_valid)
apply(drule obs_intra_singleton_disj) apply auto
done


lemma obs_intra_the_element: 
  "m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ ⟹ (THE m. m ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙) = m"
by(fastforce dest:obs_intra_singleton_element)


lemma obs_singleton_element:
  assumes "ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙" and "∀n ∈ set (tl ns). return_node n"
  shows "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {ms}"
proof -
  from ‹ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙› ‹∀n ∈ set (tl ns). return_node n›
  obtain nsx n nsx' n' where "ns = nsx@n#nsx'" and "ms = n'#nsx'"
    and split:"n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙"
    "∀nx ∈ set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    "∀xs x xs'. nsx = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
    ⟶ (∃x'' ∈ set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧ 
                                   nx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
    by(erule obsE)
  from ‹n' ∈ obs_intra n ⌊HRB_slice S⌋⇘CFG⇙›
  have "obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {n'}"
    by(fastforce intro!:obs_intra_singleton_element)
  { fix xs assume "xs ≠ ms" and "xs ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙"
    from ‹xs ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙› ‹∀n ∈ set (tl ns). return_node n›
    obtain zs z zs' z' where "ns = zs@z#zs'" and "xs = z'#zs'"
      and "z' ∈ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙"
      and "∀z' ∈ set zs'. ∃nx'. call_of_return_node z' nx' ∧ nx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      and "∀xs x xs'. zs = xs@x#xs' ∧ obs_intra x ⌊HRB_slice S⌋⇘CFG⇙ ≠ {}
      ⟶ (∃x'' ∈ set (xs'@[z]). ∃nx. call_of_return_node x'' nx ∧ 
                                     nx ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
      by(erule obsE)
    with ‹ns = nsx@n#nsx'› split
    have "nsx = zs ∧ n = z ∧ nsx' = zs'"
      by -(rule obs_split_det[of _ _ _ _ _ _ "⌊HRB_slice S⌋⇘CFG⇙"],fastforce+)
    with ‹obs_intra n ⌊HRB_slice S⌋⇘CFG⇙ = {n'}› ‹z' ∈ obs_intra z ⌊HRB_slice S⌋⇘CFG⇙›
    have "z' = n'" by simp
    with ‹xs ≠ ms› ‹ms = n'#nsx'› ‹xs = z'#zs'› ‹nsx = zs ∧ n = z ∧ nsx' = zs'›
    have False by simp }
  with ‹ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙› show ?thesis by fastforce
qed


lemma obs_finite:"∀n ∈ set (tl ns). return_node n 
  ⟹ finite (obs ns ⌊HRB_slice S⌋⇘CFG⇙)"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])

lemma obs_singleton:"∀n ∈ set (tl ns). return_node n 
  ⟹ card (obs ns ⌊HRB_slice S⌋⇘CFG⇙) ≤ 1"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])

lemma obs_the_element: 
  "⟦ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙; ∀n ∈ set (tl ns). return_node n⟧ 
  ⟹ (THE ms. ms ∈ obs ns ⌊HRB_slice S⌋⇘CFG⇙) = ms"
by(cases "obs ns ⌊HRB_slice S⌋⇘CFG⇙ = {}",auto dest:obs_singleton_element[of _ _ S])
  

end

end