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'  (nxset (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 nxset (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