Theory Observable

header {* \isaheader{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