Theory 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