Theory Slicing.CFGExit

theory CFGExit imports CFG begin

subsection ‹Adds an exit node to the abstract CFG›

locale CFGExit = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  'state edge_kind" and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')") + 
  fixes Exit::"'node"  ("'('_Exit'_')")
  assumes Exit_source [dest]: "valid_edge a; sourcenode a = (_Exit_)  False"
  and Entry_Exit_edge: "a. valid_edge a  sourcenode a = (_Entry_) 
    targetnode a = (_Exit_)  kind a = (λs. False)"
  
begin

lemma Entry_noteq_Exit [dest]:
  assumes eq:"(_Entry_) = (_Exit_)" shows "False"
proof -
  from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)" 
    and "valid_edge a" by blast
  with eq show False by simp(erule Exit_source)
qed

lemma Exit_noteq_Entry [dest]:"(_Exit_) = (_Entry_)  False"
  by(rule Entry_noteq_Exit[OF sym],simp)


lemma [simp]: "valid_node (_Entry_)"
proof -
  from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)" 
    and "valid_edge a" by blast
  thus ?thesis by(fastforce simp:valid_node_def)
qed

lemma [simp]: "valid_node (_Exit_)"
proof -
  from Entry_Exit_edge obtain a where "targetnode a = (_Exit_)"
    and "valid_edge a" by blast
  thus ?thesis by(fastforce simp:valid_node_def)
qed


definition inner_node :: "'node  bool"
  where inner_node_def: 
  "inner_node n  valid_node n  n  (_Entry_)  n  (_Exit_)"


lemma inner_is_valid:
  "inner_node n  valid_node n"
by(simp add:inner_node_def valid_node_def)

lemma [dest]:
  "inner_node (_Entry_)  False"
by(simp add:inner_node_def)

lemma [dest]:
  "inner_node (_Exit_)  False" 
by(simp add:inner_node_def)

lemma [simp]:"valid_edge a; targetnode a  (_Exit_) 
   inner_node (targetnode a)"
  by(simp add:inner_node_def,rule ccontr,simp,erule Entry_target)

lemma [simp]:"valid_edge a; sourcenode a  (_Entry_)
   inner_node (sourcenode a)"
  by(simp add:inner_node_def,rule ccontr,simp,erule Exit_source)

lemma valid_node_cases [consumes 1, case_names "Entry" "Exit" "inner"]:
  "valid_node n; n = (_Entry_)  Q; n = (_Exit_)  Q;
    inner_node n  Q  Q"
apply(auto simp:valid_node_def)
 apply(case_tac "sourcenode a = (_Entry_)") apply auto
apply(case_tac "targetnode a = (_Exit_)") apply auto
done

lemma path_Exit_source [dest]:
  assumes "(_Exit_) -as→* n'" shows "n' = (_Exit_)" and "as = []"
  using (_Exit_) -as→* n'
proof(induct n"(_Exit_)" as n' rule:path.induct)
  case (Cons_path n'' as n' a)
  from sourcenode a = (_Exit_) valid_edge a have False 
    by -(rule Exit_source,simp_all)
  { case 1 with False show ?case ..
  next
    case 2 with False show ?case ..
  }
qed simp_all

lemma Exit_no_sourcenode[dest]:
  assumes isin:"(_Exit_)  set (sourcenodes as)" and path:"n -as→* n'"
  shows False
proof -
  from isin obtain ns' ns'' where "sourcenodes as = ns'@(_Exit_)#ns''"
    by(auto dest:split_list simp:sourcenodes_def)
  then obtain as' as'' a where "as = as'@a#as''"
    and source:"sourcenode a = (_Exit_)"
    by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
  with path have "valid_edge a" by(fastforce dest:path_split)
  with source show ?thesis by -(erule Exit_source)
qed


end 

end