Theory Observable

section ‹Observable Sets of Nodes›

theory Observable imports ReturnAndCallNodes begin

context CFG begin


subsection ‹Intraprocedural observable sets›

inductive_set obs_intra :: "'node ⇒ 'node set ⇒ 'node set" 
for n::"'node" and S::"'node set"
where obs_intra_elem:
  "⟦n -as→⇩ι* n'; ∀nx ∈ set(sourcenodes as). nx ∉ S; n' ∈ S⟧ ⟹ n' ∈ obs_intra n S"


lemma obs_intraE:
  assumes "n' ∈ obs_intra n S"
  obtains as where "n -as→⇩ι* n'" and "∀nx ∈ set(sourcenodes as). nx ∉ S" and "n' ∈ S"
  using ‹n' ∈ obs_intra n S›
  by(fastforce elim:obs_intra.cases)


lemma n_in_obs_intra:
  assumes "valid_node n" and "n ∈ S" shows "obs_intra n S = {n}"
proof -
  from ‹valid_node n› have "n -[]→* n" by(rule empty_path)
  hence "n -[]→⇩ι* n" by(simp add:intra_path_def)
  with ‹n ∈ S› have "n ∈ obs_intra n S" 
    by(fastforce elim:obs_intra_elem simp:sourcenodes_def)
  { fix n' assume "n' ∈ obs_intra n S"
    have "n' = n"
    proof(rule ccontr)
      assume "n' ≠ n"
      from ‹n' ∈ obs_intra n S› obtain as where "n -as→⇩ι* n'"
        and "∀nx ∈ set(sourcenodes as). nx ∉ S"
        and "n' ∈ S" by(fastforce elim:obs_intra.cases)
      from ‹n -as→⇩ι* n'› have "n -as→* n'" by(simp add:intra_path_def)
      from this ‹∀nx ∈ set(sourcenodes as). nx ∉ S› ‹n' ≠ n› ‹n ∈ S›
      show False
      proof(induct rule:path.induct)
        case (Cons_path n'' as n' a n)
        from ‹∀nx∈set (sourcenodes (a#as)). nx ∉ S› ‹sourcenode a = n›
        have "n ∉ S" by(simp add:sourcenodes_def)
        with ‹n ∈ S› show False by simp
      qed simp
    qed }
  with ‹n ∈ obs_intra n S› show ?thesis by fastforce
qed


lemma in_obs_intra_valid:
  assumes "n' ∈ obs_intra n S" shows "valid_node n" and "valid_node n'"
  using ‹n' ∈ obs_intra n S›
  by(auto elim!:obs_intraE intro:path_valid_node simp:intra_path_def)


lemma edge_obs_intra_subset:
  assumes "valid_edge a" and "intra_kind (kind a)" and "sourcenode a ∉ S"
  shows "obs_intra (targetnode a) S ⊆ obs_intra (sourcenode a) S"
proof
  fix n assume "n ∈ obs_intra (targetnode a) S"
  then obtain as where "targetnode a -as→⇩ι* n" 
    and all:"∀nx ∈ set(sourcenodes as). nx ∉ S" and "n ∈ S" by(erule obs_intraE)
  from ‹valid_edge a› ‹intra_kind (kind a)› ‹targetnode a -as→⇩ι* n›
  have "sourcenode a -[a]@as→⇩ι* n" by(fastforce intro:Cons_path simp:intra_path_def)
  moreover
  from all ‹sourcenode a ∉ S› have "∀nx ∈ set(sourcenodes (a#as)). nx ∉ S"
    by(simp add:sourcenodes_def)
  ultimately show "n ∈ obs_intra (sourcenode a) S" using ‹n ∈ S›
    by(fastforce intro:obs_intra_elem)
qed


lemma path_obs_intra_subset:
  assumes "n -as→⇩ι* n'" and "∀n' ∈ set(sourcenodes as). n' ∉ S"
  shows "obs_intra n' S ⊆ obs_intra n S"
proof -
  from ‹n -as→⇩ι* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind (kind a)"
    by(simp_all add:intra_path_def)
  from this ‹∀n' ∈ set(sourcenodes as). n' ∉ S› show ?thesis
  proof(induct rule:path.induct)
    case (Cons_path n'' as n' a n)
    note IH = ‹⟦∀a∈set as. intra_kind (kind a); ∀n'∈set (sourcenodes as). n' ∉ S⟧
      ⟹ obs_intra n' S ⊆ obs_intra n'' S›
    from ‹∀n'∈set (sourcenodes (a#as)). n' ∉ S› 
    have all:"∀n'∈set (sourcenodes as). n' ∉ S" and "sourcenode a ∉ S"
      by(simp_all add:sourcenodes_def)
    from ‹∀a ∈ set (a#as). intra_kind (kind a)›
    have "intra_kind (kind a)" and "∀a ∈ set as. intra_kind (kind a)"
      by(simp_all add:intra_path_def)
    from IH[OF ‹∀a ∈ set as. intra_kind (kind a)› all]
    have "obs_intra n' S ⊆ obs_intra n'' S" .
    from ‹valid_edge a› ‹intra_kind (kind a)› ‹targetnode a = n''›
      ‹sourcenode a = n› ‹sourcenode a ∉ S›
    have "obs_intra n'' S ⊆ obs_intra n S" by(fastforce dest:edge_obs_intra_subset)
    with ‹obs_intra n' S ⊆ obs_intra n'' S› show ?case by fastforce
  qed simp
qed


lemma path_ex_obs_intra:
  assumes "n -as→⇩ι* n'" and "n' ∈ S"
  obtains m where "m ∈ obs_intra n S"
proof(atomize_elim)
  show "∃m. m ∈ obs_intra n S"
  proof(cases "∀nx ∈ set(sourcenodes as). nx ∉ S")
    case True
    with ‹n -as→⇩ι* n'› ‹n' ∈ S› have "n' ∈ obs_intra n S" by -(rule obs_intra_elem)
    thus ?thesis by fastforce
  next
    case False
    hence "∃nx ∈ set(sourcenodes as). nx ∈ S" by fastforce
    then obtain nx ns ns' where "sourcenodes as = ns@nx#ns'"
      and "nx ∈ S" and "∀n' ∈ set ns. n' ∉ S"
      by(fastforce elim!:split_list_first_propE)
    from ‹sourcenodes as = ns@nx#ns'› obtain as' a as'' 
      where "ns = sourcenodes as'"
      and "as = as'@a#as''" and "sourcenode a = nx"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    with ‹n -as→⇩ι* n'› have "n -as'→⇩ι* nx"
      by(fastforce dest:path_split simp:intra_path_def)
    with ‹nx ∈ S› ‹∀n' ∈ set ns. n' ∉ S› ‹ns = sourcenodes as'› 
    have "nx ∈ obs_intra n S" by(fastforce intro:obs_intra_elem)
    thus ?thesis by fastforce
  qed
qed


subsection ‹Interprocedural observable sets restricted to the slice›


fun obs :: "'node list ⇒ 'node set ⇒ 'node list set" 
  where "obs [] S = {}"
  | "obs (n#ns) S = (let S' = obs_intra n S in 
  (if (S' = {} ∨ (∃n' ∈ set ns. ∃nx. call_of_return_node n' nx ∧ nx ∉ S)) 
   then obs ns S else (λnx. nx#ns) ` S'))"


lemma obsI:
  assumes "n' ∈ obs_intra n S"
  and "∀nx ∈ set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
  shows "⟦ns = nsx@n#nsx'; ∀xs x xs'. nsx = xs@x#xs' ∧ obs_intra x S ≠ {}
     ⟶ (∃x'' ∈ set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)⟧
  ⟹ n'#nsx' ∈ obs ns S"
proof(induct ns arbitrary:nsx)
case (Cons x xs)
  note IH = ‹⋀nsx. ⟦xs = nsx@n#nsx'; 
    ∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
    (∃x''∈set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)⟧
    ⟹ n'#nsx' ∈ obs xs S›
  note nsx = ‹∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
    (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)›
  show ?case
  proof(cases nsx)
    case Nil
    with ‹x#xs = nsx@n#nsx'› have "n = x" and "xs = nsx'" by simp_all
    with ‹n' ∈ obs_intra n S›
      ‹∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S›
    show ?thesis by(fastforce simp:Let_def)
  next
    case (Cons z zs)
    with ‹x#xs = nsx@n#nsx'› have [simp]:"x = z" "xs = zs@n#nsx'" by simp_all
    from nsx Cons
    have "∀xs x xs'. zs = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
      (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
      by clarsimp(erule_tac x="z#xs" in allE,auto)
    from IH[OF ‹xs = zs@n#nsx'› this] have "n'#nsx' ∈ obs xs S" by simp
    show ?thesis
    proof(cases "obs_intra z S = {}")
      case True
      with Cons ‹n'#nsx' ∈ obs xs S› show ?thesis by(simp add:Let_def)
    next
      case False
      from nsx Cons
      have "obs_intra z S ≠ {} ⟶
        (∃x''∈set (zs @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
        by clarsimp
      with False have "∃x''∈set (zs @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S"
        by simp
      with ‹xs = zs@n#nsx'› 
      have "∃n' ∈ set xs. ∃nx. call_of_return_node n' nx ∧ nx ∉ S" by fastforce
      with Cons ‹n'#nsx' ∈ obs xs S› show ?thesis by(simp add:Let_def)
    qed
  qed
qed simp



lemma obsE [consumes 2]:
  assumes "ns' ∈ obs ns S" and "∀n ∈ set (tl ns). return_node n"
  obtains nsx n nsx' n' where "ns = nsx@n#nsx'" and "ns' = n'#nsx'" 
  and "n' ∈ obs_intra n S" 
  and "∀nx ∈ set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
  and "∀xs x xs'. nsx = xs@x#xs' ∧ obs_intra x S ≠ {}
  ⟶ (∃x'' ∈ set (xs'@[n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
proof(atomize_elim)
  from ‹ns' ∈ obs ns S› ‹∀n ∈ set (tl ns). return_node n›
  show "∃nsx n nsx' n'. ns = nsx @ n # nsx' ∧ ns' = n' # nsx' ∧
    n' ∈ obs_intra n S ∧ (∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S) ∧
    (∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
    (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S))"
  proof(induct ns)
    case Nil thus ?case by simp
  next
    case (Cons nx ns'')
    note IH = ‹⟦ns' ∈ obs ns'' S; ∀a∈set (tl ns''). return_node a⟧
      ⟹ ∃nsx n nsx' n'. ns'' = nsx @ n # nsx' ∧ ns' = n' # nsx' ∧
      n' ∈ obs_intra n S ∧ 
      (∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S) ∧
      (∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
         (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S))›
    from ‹∀a∈set (tl (nx # ns'')). return_node a› have "∀n ∈ set ns''. return_node n"
      by simp
    show ?case
    proof(cases ns'')
      case Nil
      with ‹ns' ∈ obs (nx#ns'') S› obtain x where "ns' = [x]" and "x ∈ obs_intra nx S"
        by(auto simp:Let_def split:if_split_asm)
      with Nil show ?thesis by fastforce
    next
      case Cons
      with ‹∀n ∈ set ns''. return_node n› have "∀a∈set (tl ns''). return_node a"
        by simp
      show ?thesis
      proof(cases "∃n' ∈ set ns''. ∃nx'. call_of_return_node n' nx' ∧ nx' ∉ S")
        case True
        with ‹ns' ∈ obs (nx#ns'') S› have "ns' ∈ obs ns'' S" by simp
        from IH[OF this ‹∀a∈set (tl ns''). return_node a›]
        obtain nsx n nsx' n' where split:"ns'' = nsx @ n # nsx'"
          "ns' = n' # nsx'" "n' ∈ obs_intra n S"
          "∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
          and imp:"∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
          (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
          by blast
        from True ‹ns'' = nsx @ n # nsx'›
          ‹∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S›
        have "(∃nx'. call_of_return_node n nx' ∧ nx' ∉ S) ∨
          (∃n'∈set nsx. ∃nx'. call_of_return_node n' nx' ∧ nx' ∉ S)" by fastforce
        thus ?thesis
        proof
          assume "∃nx'. call_of_return_node n nx' ∧ nx' ∉ S"
          with split show ?thesis by clarsimp
        next
          assume "∃n'∈set nsx. ∃nx'. call_of_return_node n' nx' ∧ nx' ∉ S"
          with imp have "∀xs x xs'. nx#nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
          (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
            apply clarsimp apply(case_tac xs) apply auto
            by(erule_tac x="list" in allE,auto)+
          with split Cons show ?thesis by auto
        qed
      next
        case False
        hence "∀n'∈set ns''. ∀nx'. call_of_return_node n' nx' ⟶ nx' ∈ S" by simp
        show ?thesis
        proof(cases "obs_intra nx S = {}")
          case True
          with ‹ns' ∈ obs (nx#ns'') S› have "ns' ∈ obs ns'' S" by simp
          from IH[OF this ‹∀a∈set (tl ns''). return_node a›]
          obtain nsx n nsx' n' where split:"ns'' = nsx @ n # nsx'"
            "ns' = n' # nsx'" "n' ∈ obs_intra n S"
            "∀nx∈set nsx'. ∃nx'. call_of_return_node nx nx' ∧ nx' ∈ S"
            and imp:"∀xs x xs'. nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
            (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
            by blast
          from True imp Cons 
          have "∀xs x xs'. nx#nsx = xs @ x # xs' ∧ obs_intra x S ≠ {} ⟶
            (∃x''∈set (xs' @ [n]). ∃nx. call_of_return_node x'' nx ∧ nx ∉ S)"
            by clarsimp (hypsubst_thin,case_tac xs,clarsimp+,erule_tac x="list" in allE,auto)
          with split Cons show ?thesis by auto
        next
          case False
          with ‹∀n'∈set ns''. ∀nx'. call_of_return_node n' nx' ⟶ nx' ∈ S›
            ‹ns' ∈ obs (nx # ns'') S›
          obtain nx'' where "ns' = nx''#ns''" and "nx'' ∈ obs_intra nx S"
          by(fastforce simp:Let_def split:if_split_asm)
          { fix n' assume "n'∈set ns''"
            with ‹∀n ∈ set ns''. return_node n› have "return_node n'" by simp
            hence "∃!n''. call_of_return_node n' n''" 
              by(rule return_node_call_of_return_node)
            from ‹n'∈set ns''› 
              ‹∀n'∈set ns''. ∀nx'. call_of_return_node n' nx' ⟶ nx' ∈ S›
            have "∀nx'. call_of_return_node n' nx' ⟶ nx' ∈ S" by simp
            with ‹∃!n''. call_of_return_node n' n''› 
            have "∃n''. call_of_return_node n' n'' ∧ n'' ∈ S" by fastforce }
          with ‹ns' = nx''#ns''› ‹nx'' ∈ obs_intra nx S› show ?thesis by fastforce
        qed
      qed
    qed
  qed
qed



lemma obs_split_det:
  assumes "xs@x#xs' = ys@y#ys'" 
  and "obs_intra x S ≠ {}" 
  and "∀x' ∈ set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S"
  and "∀zs z zs'. xs = zs@z#zs' ∧ obs_intra z S ≠ {}
  ⟶ (∃z'' ∈ set (zs'@[x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S)"
  and "obs_intra y S ≠ {}" 
  and "∀y' ∈ set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S"
  and "∀zs z zs'. ys = zs@z#zs' ∧ obs_intra z S ≠ {}
  ⟶ (∃z'' ∈ set (zs'@[y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)"
  shows "xs = ys ∧ x = y ∧ xs' = ys'"
using assms
proof(induct xs arbitrary:ys)
  case Nil
  note impy = ‹∀zs z zs'. ys = zs@z#zs' ∧ obs_intra z S ≠ {}
    ⟶ (∃z'' ∈ set (zs'@[y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)›
  show ?case
  proof(cases "ys = []")
    case True
    with Nil ‹[]@x#xs' = ys@y#ys'› show ?thesis by simp
  next
    case False
    with ‹[] @ x # xs' = ys @ y # ys'› 
    obtain zs where "x#zs = ys" and "xs' = zs@y#ys'" by(auto simp:Cons_eq_append_conv)
    from ‹x#zs = ys› ‹obs_intra x S ≠ {}› impy 
    have "∃z'' ∈ set (zs@[y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S"
      by blast
    with ‹xs' = zs@y#ys'› ‹∀x' ∈ set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S›
    have False by fastforce
    thus ?thesis by simp
  qed
next
  case (Cons w ws)
  note IH = ‹⋀ys. ⟦ws @ x # xs' = ys @ y # ys'; obs_intra x S ≠ {};
    ∀x'∈set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S;
    ∀zs z zs'. ws = zs @ z # zs' ∧ obs_intra z S ≠ {} ⟶
      (∃z''∈set (zs' @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S);
    obs_intra y S ≠ {}; ∀y'∈set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S;
    ∀zs z zs'. ys = zs @ z # zs' ∧ obs_intra z S ≠ {} ⟶
      (∃z''∈set (zs' @ [y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)⟧    
    ⟹ ws = ys ∧ x = y ∧ xs' = ys'›
  note impw = ‹∀zs z zs'. w # ws = zs @ z # zs' ∧ obs_intra z S ≠ {} ⟶
    (∃z''∈set (zs' @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S)›
  note impy = ‹∀zs z zs'. ys = zs @ z # zs' ∧ obs_intra z S ≠ {} ⟶
    (∃z''∈set (zs' @ [y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)›
  show ?case
  proof(cases ys)
    case Nil
    with ‹(w#ws) @ x # xs' = ys @ y # ys'› have "y = w" and "ys' = ws @ x # xs'"
      by simp_all
    from ‹y = w› ‹obs_intra y S ≠ {}› impw
    have "∃z''∈set (ws @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S" by blast
    with ‹ys' = ws @ x # xs'› 
      ‹∀y'∈set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S›
    have False by fastforce
    thus ?thesis by simp
  next
    case (Cons w' ws')
    with ‹(w # ws) @ x # xs' = ys @ y # ys'› have "w = w'"
      and "ws @ x # xs' = ws' @ y # ys'" by simp_all
    from impw have imp1:"∀zs z zs'. ws = zs @ z # zs' ∧ obs_intra z S ≠ {} ⟶
      (∃z''∈set (zs' @ [x]). ∃nx. call_of_return_node z'' nx ∧ nx ∉ S)"
      by clarsimp(erule_tac x="w#zs" in allE,clarsimp)
    from Cons impy have imp2:"∀zs z zs'. ws' = zs @ z # zs' ∧ obs_intra z S ≠ {} ⟶
      (∃z''∈set (zs' @ [y]). ∃ny. call_of_return_node z'' ny ∧ ny ∉ S)"
      by clarsimp(erule_tac x="w'#zs" in allE,clarsimp)
    from IH[OF ‹ws @ x # xs' = ws' @ y # ys'› ‹obs_intra x S ≠ {}›
      ‹∀x'∈set xs'. ∃x''. call_of_return_node x' x'' ∧ x'' ∈ S› imp1
      ‹obs_intra y S ≠ {}› ‹∀y'∈set ys'. ∃y''. call_of_return_node y' y'' ∧ y'' ∈ S› 
      imp2]
    have "ws = ws' ∧ x = y ∧ xs' = ys'" .
    with ‹w = w'› Cons show ?thesis by simp
  qed
qed


lemma in_obs_valid:
  assumes "ns' ∈ obs ns S" and "∀n ∈ set ns. valid_node n"
  shows "∀n ∈ set ns'. valid_node n"
  using ‹ns' ∈ obs ns S› ‹∀n ∈ set ns. valid_node n›
  by(induct ns)(auto intro:in_obs_intra_valid simp:Let_def split:if_split_asm)



end

end