Theory Observable

section ‹Observable Sets of Nodes›

theory Observable imports "../Basic/CFG" begin

context CFG begin

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


lemma obsE:
  assumes "n' ∈ obs n S"
  obtains as where "n -as→* n'" and "∀nx ∈ set(sourcenodes as). nx ∉ S"
  and "n' ∈ S"
proof(atomize_elim)
  from ‹n' ∈ obs n S› 
  have "∃as. n -as→* n' ∧ (∀nx ∈ set(sourcenodes as). nx ∉ S) ∧ n' ∈ S"
    by(auto elim:obs.cases)
  thus "∃as. n -as→* n' ∧ (∀nx∈set (sourcenodes as). nx ∉ S) ∧ n' ∈ S" by blast
qed


lemma n_in_obs:
  assumes "valid_node n" and "n ∈ S" shows "obs n S = {n}"
proof -
  from ‹valid_node n› have "n -[]→* n" by(rule empty_path)
  with ‹n ∈ S› have "n ∈ obs n S" by(fastforce elim:obs_elem simp:sourcenodes_def)
  { fix n' assume "n' ∈ obs n S"
    have "n' = n"
    proof(rule ccontr)
      assume "n' ≠ n"
      from ‹n' ∈ obs n S› obtain as where "n -as→* n'"
        and "∀nx ∈ set(sourcenodes as). nx ∉ S"
        and "n' ∈ S" by(erule obsE)
      from ‹n -as→* n'› ‹∀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 n S› show ?thesis by fastforce
qed


lemma in_obs_valid:
  assumes "n' ∈ obs n S" shows "valid_node n" and "valid_node n'"
  using ‹n' ∈ obs n S›
  by(auto elim:obsE intro:path_valid_node)


lemma edge_obs_subset:
  assumes"valid_edge a" and "sourcenode a ∉ S"
  shows "obs (targetnode a) S ⊆ obs (sourcenode a) S"
proof
  fix n assume "n ∈ obs (targetnode a) S"
  then obtain as where "targetnode a -as→* n" 
    and all:"∀nx ∈ set(sourcenodes as). nx ∉ S" and "n ∈ S" by(erule obsE)
  from ‹valid_edge a› ‹targetnode a -as→* n›
  have "sourcenode a -a#as→* n" by(fastforce intro:Cons_path)
  moreover
  from all ‹sourcenode a ∉ S› have "∀nx ∈ set(sourcenodes (a#as)). nx ∉ S"
    by(simp add:sourcenodes_def)
  ultimately show "n ∈ obs (sourcenode a) S" using ‹n ∈ S›
    by(rule obs_elem)
qed


lemma path_obs_subset:
  "⟦n -as→* n'; ∀n' ∈ set(sourcenodes as). n' ∉ S⟧
  ⟹ obs n' S ⊆ obs n S"
proof(induct rule:path.induct)
  case (Cons_path n'' as n' a n)
  note IH = ‹∀n'∈set (sourcenodes as). n' ∉ S ⟹ obs n' S ⊆ obs 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 IH[OF all] have "obs n' S ⊆ obs n'' S" .
  from ‹valid_edge a› ‹targetnode a = n''› ‹sourcenode a = n› ‹sourcenode a ∉ S›
  have "obs n'' S ⊆ obs n S" by(fastforce dest:edge_obs_subset)
  with ‹obs n' S ⊆ obs n'' S› show ?case by fastforce
qed simp


lemma path_ex_obs:
  assumes "n -as→* n'" and "n' ∈ S"
  obtains m where "m ∈ obs n S"
proof(atomize_elim)
  show "∃m. m ∈ obs n S"
  proof(cases "∀nx ∈ set(sourcenodes as). nx ∉ S")
    case True
    with ‹n -as→* n'› ‹n' ∈ S› have "n' ∈ obs n S" by -(rule obs_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)
    with ‹nx ∈ S› ‹∀n' ∈ set ns. n' ∉ S› ‹ns = sourcenodes as'› have "nx ∈ obs n S"
      by(fastforce intro:obs_elem)
    thus ?thesis by fastforce
  qed
qed

end

end