Theory ReturnAndCallNodes

section ‹Return and their corresponding call nodes›

theory ReturnAndCallNodes imports CFG begin

context CFG begin

subsection ‹Defining ‹return_node››

definition return_node :: "'node ⇒ bool"
  where "return_node n ≡ ∃a a'. valid_edge a ∧ n = targetnode a ∧ 
    valid_edge a' ∧ a ∈ get_return_edges a'"


lemma return_node_determines_call_node:
  assumes "return_node n"
  shows "∃!n'. ∃a a'. valid_edge a ∧ n' = sourcenode a ∧ valid_edge a' ∧ 
    a' ∈ get_return_edges a ∧ n = targetnode a'"
proof(rule ex_ex1I)
  from ‹return_node n›
  show "∃n' a a'. valid_edge a ∧ n' = sourcenode a ∧ valid_edge a' ∧ 
    a' ∈ get_return_edges a ∧ n = targetnode a'"
    by(simp add:return_node_def) blast
next
  fix n' nx
  assume "∃a a'. valid_edge a ∧ n' = sourcenode a ∧ valid_edge a' ∧ 
    a' ∈ get_return_edges a ∧ n = targetnode a'"
    and "∃a a'. valid_edge a ∧ nx = sourcenode a ∧ valid_edge a' ∧ 
    a' ∈ get_return_edges a ∧ n = targetnode a'"
  then obtain a a' ax ax' where "valid_edge a" and "n' = sourcenode a"
    and "valid_edge a'" and "a' ∈ get_return_edges a"
    and "n = targetnode a'" and "valid_edge ax" and "nx = sourcenode ax" 
   and "valid_edge ax'" and "ax' ∈ get_return_edges ax"
    and "n = targetnode ax'"
    by blast
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
    by(rule get_return_edges_valid)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain a''
    where intra_edge1:"valid_edge a''" "sourcenode a'' = sourcenode a"
    "targetnode a'' = targetnode a'" "kind a'' = (λcf. False)⇩√"
    by(fastforce dest:call_return_node_edge)
  from ‹valid_edge ax› ‹ax' ∈ get_return_edges ax› obtain ax''
    where intra_edge2:"valid_edge ax''" "sourcenode ax'' = sourcenode ax"
    "targetnode ax'' = targetnode ax'" "kind ax'' = (λcf. False)⇩√"
    by(fastforce dest:call_return_node_edge)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› 
  obtain Q r p fs where "kind a = Q:r↪⇘p⇙fs"
    by(fastforce dest!:only_call_get_return_edges)
  with ‹valid_edge a› ‹a' ∈ get_return_edges a› obtain Q' p f' 
    where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
  with ‹valid_edge a'›
  have "∃!a''. valid_edge a'' ∧ targetnode a'' = targetnode a' ∧ intra_kind(kind a'')"
    by(rule return_only_one_intra_edge)
  with intra_edge1 intra_edge2 ‹n = targetnode a'› ‹n = targetnode ax'›
  have "a'' = ax''" by(fastforce simp:intra_kind_def)
  with ‹sourcenode a'' = sourcenode a› ‹sourcenode ax'' = sourcenode ax›
    ‹n' = sourcenode a› ‹nx = sourcenode ax›
  show "n' = nx" by simp
qed


lemma return_node_THE_call_node:
  "⟦return_node n; valid_edge a; valid_edge a'; a' ∈ get_return_edges a; 
  n = targetnode a'⟧
  ⟹ (THE n'. ∃a a'. valid_edge a ∧ n' = sourcenode a ∧ valid_edge a' ∧ 
  a' ∈ get_return_edges a ∧ n = targetnode a') = sourcenode a"
  by(fastforce intro!:the1_equality return_node_determines_call_node)


subsection ‹Defining call nodes belonging to a certain ‹return_node››

definition call_of_return_node :: "'node ⇒ 'node ⇒ bool"
  where "call_of_return_node n n' ≡ ∃a a'. return_node n ∧ 
  valid_edge a ∧ n' = sourcenode a ∧ valid_edge a' ∧
  a' ∈ get_return_edges a ∧ n = targetnode a'"


lemma return_node_call_of_return_node:
  "return_node n ⟹ ∃!n'. call_of_return_node n n'"
  by -(frule return_node_determines_call_node,unfold call_of_return_node_def,simp)


lemma call_of_return_nodes_det [dest]:
  assumes "call_of_return_node n n'" and "call_of_return_node n n''"
  shows "n' = n''"
proof -
  from ‹call_of_return_node n n'› have "return_node n" 
    by(simp add:call_of_return_node_def)
  hence "∃!n'. call_of_return_node n n'" by(rule return_node_call_of_return_node)
  with ‹call_of_return_node n n'› ‹call_of_return_node n n''›
  show ?thesis by auto
qed



lemma get_return_edges_call_of_return_nodes:
  "⟦valid_call_list cs m; valid_return_list rs m;
    ∀i < length rs. rs!i ∈ get_return_edges (cs!i); length rs = length cs⟧
  ⟹ ∀i<length cs. call_of_return_node (targetnodes rs!i) (sourcenode (cs!i))"
proof(induct cs arbitrary:m rs)
  case Nil thus ?case by fastforce
next
  case (Cons c' cs')
  note IH = ‹⋀m rs. ⟦valid_call_list cs' m; valid_return_list rs m;
    ∀i<length rs. rs ! i ∈ get_return_edges (cs' ! i); length rs = length cs'⟧
    ⟹ ∀i<length cs'. call_of_return_node (targetnodes rs ! i) (sourcenode (cs'!i))›
  from ‹length rs = length (c' # cs')› obtain r' rs' where "rs = r' # rs'"
    and "length rs' = length cs'" by(cases rs) auto
  with ‹∀i<length rs. rs ! i ∈ get_return_edges ((c' # cs') ! i)›
  have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
    and "r' ∈ get_return_edges c'" by auto
  from ‹valid_call_list (c'#cs') m› have "valid_edge c'"
    by(fastforce simp:valid_call_list_def)
  from this ‹r' ∈ get_return_edges c'›
  have "get_proc (sourcenode c') = get_proc (targetnode r')"
    by(rule get_proc_get_return_edge)
  from ‹valid_call_list (c'#cs') m›
  have "valid_call_list cs' (sourcenode c')"
    apply(clarsimp simp:valid_call_list_def)
    apply(hypsubst_thin)
    apply(erule_tac x="c'#cs'" in allE) apply clarsimp
    by(case_tac cs')(auto simp:sourcenodes_def)
  from ‹valid_return_list rs m› ‹rs = r' # rs'› 
    ‹get_proc (sourcenode c') = get_proc (targetnode r')›
  have "valid_return_list rs' (sourcenode c')"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="r'#cs'" in allE) apply clarsimp
    by(case_tac cs')(auto simp:targetnodes_def)
  from IH[OF ‹valid_call_list cs' (sourcenode c')› 
    ‹valid_return_list rs' (sourcenode c')›
    ‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)› ‹length rs' = length cs'›]
  have all:"∀i<length cs'.
    call_of_return_node (targetnodes rs' ! i) (sourcenode (cs' ! i))" .
  from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› have "valid_edge r'" 
    by(rule get_return_edges_valid)
  from ‹valid_edge r'› ‹valid_edge c'› ‹r' ∈ get_return_edges c'›
  have "return_node (targetnode r')" by(fastforce simp:return_node_def)
  with ‹valid_edge c'› ‹r' ∈ get_return_edges c'› ‹valid_edge r'›
  have "call_of_return_node (targetnode r') (sourcenode c')"
    by(simp add:call_of_return_node_def) blast
  with all ‹rs = r' # rs'› show ?case
    by auto(case_tac i,auto simp:targetnodes_def)
qed


end

end