section ‹Definition of the CFG›

theory PCFG imports ProcState begin

definition Main :: "pname"
  where "Main = ''Main''"

datatype label = Label nat | Entry | Exit

subsection‹The CFG for every procedure›

subsubsection ‹Definition of ‹⊕››

fun label_incr :: "label → nat → label" (‹_ ⊕ _› 60)
where "(Label l) ⊕ i = Label (l + i)"
  | "Entry ⊕ i = Entry"
  | "Exit ⊕ i = Exit"


lemma Exit_label_incr [dest]: "Exit = n ⊕ i ==> n = Exit"
  by(cases n,auto)

lemma label_incr_Exit [dest]: "n ⊕ i = Exit ==> n = Exit"
  by(cases n,auto)

lemma Entry_label_incr [dest]: "Entry = n ⊕ i ==> n = Entry"
  by(cases n,auto)

lemma label_incr_Entry [dest]: "n ⊕ i = Entry ==> n = Entry"
  by(cases n,auto)

lemma label_incr_inj:
  "n ⊕ c = n' ⊕ c ==> n = n'"
by(cases n)(cases n',auto)+

lemma label_incr_simp:"n ⊕ i = m ⊕ (i + j) ==> n = m ⊕ j"
by(cases n,auto,cases m,auto)

lemma label_incr_simp_rev:"m ⊕ (j + i) = n ⊕ i ==> m ⊕ j = n"
by(cases n,auto,cases m,auto)

lemma label_incr_start_Node_smaller:
  "Label l = n ⊕ i ==> n = Label (l - i)"
by(cases n,auto)

lemma label_incr_start_Node_smaller_rev:
  "n ⊕ i = Label l ==> n = Label (l - i)"
by(cases n,auto)


lemma label_incr_ge:"Label l = n ⊕ i ==> l ≥ i"
by(cases n) auto

lemma label_incr_0 [dest]:
  "[Label 0 = n ⊕ i; i > 0] ==> False" 
by(cases n) auto

lemma label_incr_0_rev [dest]:
  "[n ⊕ i = Label 0; i > 0] ==> False" 
by(cases n) auto

subsubsection ‹The edges of the procedure CFG›

text ‹Control flow information in this language is the node, to which we return
 after the calles procedure is finished.›

datatype p_edge_kind = 
  IEdge "(vname,val,pname × label,pname) edge_kind"
| CEdge "pname × expr list × vname list"


type_synonym p_edge = "(label × p_edge_kind × label)"

inductive Proc_CFG :: "cmd → label → p_edge_kind → label → bool"
(‹_ ⊨ _ -_→_p _›)
where

  Proc_CFG_Entry_Exit:
  "prog ⊨ Entry -IEdge (λs. False)_\<surd>→_p Exit"

| Proc_CFG_Entry:
  "prog ⊨ Entry -IEdge (λs. True)_\<surd>→_p Label 0"

| Proc_CFG_Skip: 
  "Skip ⊨ Label 0 -IEdge ⇑id→_p Exit"

| Proc_CFG_LAss: 
  "V:=e ⊨ Label 0 -IEdge ⇑(λcf. update cf V e)→_p Label 1"

| Proc_CFG_LAssSkip:
  "V:=e ⊨ Label 1 -IEdge ⇑id→_p Exit"

| Proc_CFG_SeqFirst:
  "[c₁ ⊨ n -et→_p n'; n' ≠ Exit] ==> c₁;;c₂ ⊨ n -et→_p n'"

| Proc_CFG_SeqConnect: 
  "[c₁ ⊨ n -et→_p Exit; n ≠ Entry] ==> c₁;;c₂ ⊨ n -et→_p Label #:c₁"

| Proc_CFG_SeqSecond: 
  "[c₂ ⊨ n -et→_p n'; n ≠ Entry] ==> c₁;;c₂ ⊨ n ⊕ #:c₁ -et→_p n' ⊕ #:c₁"

| Proc_CFG_CondTrue:
    "if (b) c₁ else c₂ ⊨ Label 0
  -IEdge (λcf. state_check cf b (Some true))_\<surd>→_p Label 1"

| Proc_CFG_CondFalse:
    "if (b) c₁ else c₂ ⊨ Label 0 -IEdge (λcf. state_check cf b (Some false))_\<surd>→_p
                        Label (#:c₁ + 1)"

| Proc_CFG_CondThen:
  "[c₁ ⊨ n -et→_p n'; n ≠ Entry] ==> if (b) c₁ else c₂ ⊨ n ⊕ 1 -et→_p n' ⊕ 1"

| Proc_CFG_CondElse:
  "[c₂ ⊨ n -et→_p n'; n ≠ Entry]
  ==> if (b) c₁ else c₂ ⊨ n ⊕ (#:c₁ + 1) -et→_p n' ⊕ (#:c₁ + 1)"

| Proc_CFG_WhileTrue:
    "while (b) c' ⊨ Label 0 -IEdge (λcf. state_check cf b (Some true))_\<surd>→_p Label 2"

| Proc_CFG_WhileFalse:
    "while (b) c' ⊨ Label 0 -IEdge (λcf. state_check cf b (Some false))_\<surd>→_p Label 1"

| Proc_CFG_WhileFalseSkip:
  "while (b) c' ⊨ Label 1 -IEdge ⇑id→_p Exit"

| Proc_CFG_WhileBody:
  "[c' ⊨ n -et→_p n'; n ≠ Entry; n' ≠ Exit]
  ==> while (b) c' ⊨ n ⊕ 2 -et→_p n' ⊕ 2"

| Proc_CFG_WhileBodyExit:
  "[c' ⊨ n -et→_p Exit; n ≠ Entry] ==> while (b) c' ⊨ n ⊕ 2 -et→_p Label 0"

| Proc_CFG_Call:
  "Call p es rets ⊨ Label 0 -CEdge (p,es,rets)→_p Label 1"

| Proc_CFG_CallSkip:
  "Call p es rets ⊨ Label 1 -IEdge ⇑id→_p Exit"


subsubsection‹Some lemmas about the procedure CFG›

lemma Proc_CFG_Exit_no_sourcenode [dest]:
  "prog ⊨ Exit -et→_p n' ==> False"
by(induct prog n≡"Exit" et n' rule:Proc_CFG.induct,auto)


lemma Proc_CFG_Entry_no_targetnode [dest]:
  "prog ⊨ n -et→_p Entry ==> False"
by(induct prog n et n'≡"Entry" rule:Proc_CFG.induct,auto)


lemma Proc_CFG_IEdge_intra_kind:
  "prog ⊨ n -IEdge et→_p n' ==> intra_kind et"
by(induct prog n x≡"IEdge et" n' rule:Proc_CFG.induct,auto simp:intra_kind_def)


lemma [dest]:"prog ⊨ n -IEdge (Q:r↪fs)→_p n' ==> False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)

lemma [dest]:"prog ⊨ n -IEdge (Q↩f)→_p n' ==> False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)


lemma Proc_CFG_sourcelabel_less_num_nodes:
  "prog ⊨ Label l -et→_p n' ==> l < #:prog"
proof(induct prog "Label l" et n' arbitrary:l rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ et n' c₂ l)
  thus ?case by simp
next
  case (Proc_CFG_SeqConnect c₁ et c₂ l)
  thus ?case by simp
next
  case (Proc_CFG_SeqSecond c₂ n et n' c₁ l) 
  note n = ‹n ⊕ #:c₁ = Label l›
  note IH = ‹∧l. n = Label l ==> l < #:c₂›
  from n obtain l' where l':"n = Label l'" by(cases n) auto
  from IH[OF this] have "l' < #:c₂" .
  with n l' show ?case by simp
next
  case (Proc_CFG_CondThen c₁ n et n' b c₂ l) 
  note n = ‹n ⊕ 1 = Label l›
  note IH = ‹∧l. n = Label l ==> l < #:c₁›
  from n obtain l' where l':"n = Label l'" by(cases n) auto
  from IH[OF this] have "l' < #:c₁" .
  with n l' show ?case by simp
next
  case (Proc_CFG_CondElse c₂ n et n' b c₁ l)
  note n = ‹n ⊕ (#:c₁ + 1) = Label l›
  note IH = ‹∧l. n = Label l ==> l < #:c₂›
  from n obtain l' where l':"n = Label l'" by(cases n) auto
  from IH[OF this] have "l' < #:c₂" .
  with n l' show ?case by simp
next
  case (Proc_CFG_WhileBody c' n et n' b l)
  note n = ‹n ⊕ 2 = Label l›
  note IH = ‹∧l. n = Label l ==> l < #:c'›
  from n obtain l' where l':"n = Label l'" by(cases n) auto
  from IH[OF this] have "l' < #:c'" .
  with n l' show ?case by simp
next
  case (Proc_CFG_WhileBodyExit c' n et b l)
  note n = ‹n ⊕ 2 = Label l›
  note IH = ‹∧l. n = Label l ==> l < #:c'›
  from n obtain l' where l':"n = Label l'" by(cases n) auto
  from IH[OF this] have "l' < #:c'" .
  with n l' show ?case by simp
qed (auto simp:num_inner_nodes_gr_0)


lemma Proc_CFG_targetlabel_less_num_nodes:
  "prog ⊨ n -et→_p Label l ==> l < #:prog"
proof(induct prog n et "Label l" arbitrary:l rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ n et c₂ l)
 thus ?case by simp
next
  case (Proc_CFG_SeqSecond c₂ n et n' c₁ l)
  note n' = ‹n' ⊕ #:c₁ = Label l›
  note IH = ‹∧l. n' = Label l ==> l < #:c₂›
  from n' obtain l' where l':"n' = Label l'" by(cases n') auto
  from IH[OF this] have "l' < #:c₂" .
  with n' l' show ?case by simp
next
  case (Proc_CFG_CondThen c₁ n et n' b c₂ l)
  note n' = ‹n' ⊕ 1 = Label l›
  note IH = ‹∧l. n' = Label l ==> l < #:c₁›
  from n' obtain l' where l':"n' = Label l'" by(cases n') auto
  from IH[OF this] have "l' < #:c₁" .
  with n' l' show ?case by simp
next
  case (Proc_CFG_CondElse c₂ n et n' b c₁ l)
  note n' = ‹n' ⊕ (#:c₁ + 1) = Label l›
  note IH = ‹∧l. n' = Label l ==> l < #:c₂›
  from n' obtain l' where l':"n' = Label l'" by(cases n') auto
  from IH[OF this] have "l' < #:c₂" .
  with n' l' show ?case by simp
next
  case (Proc_CFG_WhileBody c' n et n' b l)
  note n' = ‹n' ⊕ 2 = Label l›
note IH = ‹∧l. n' = Label l ==> l < #:c'›
  from n' obtain l' where l':"n' = Label l'" by(cases n') auto
  from IH[OF this] have "l' < #:c'" .
  with n' l' show ?case by simp
qed (auto simp:num_inner_nodes_gr_0)


lemma Proc_CFG_EntryD:
  "prog ⊨ Entry -et→_p n'
  ==> (n' = Exit ∧ et = IEdge(λs. False)_\<surd>) ∨ (n' = Label 0 ∧ et = IEdge (λs. True)_\<surd>)"
by(induct prog n≡"Entry" et n' rule:Proc_CFG.induct,auto)


lemma Proc_CFG_Exit_edge:
  obtains l et where "prog ⊨ Label l -IEdge et→_p Exit" and "l ≤ #:prog"
proof(atomize_elim)
  show "∃l et. prog ⊨ Label l -IEdge et→_p Exit ∧ l ≤ #:prog"
  proof(induct prog)
    case Skip
    have "Skip ⊨ Label 0 -IEdge ⇑id→_p Exit" by(rule Proc_CFG_Skip)
    thus ?case by fastforce
  next
    case (LAss V e)
    have "V:=e ⊨ Label 1 -IEdge ⇑id→_p Exit" by(rule Proc_CFG_LAssSkip)
    thus ?case by fastforce
  next
    case (Seq c₁ c₂)
    from ‹∃l et. c₂ ⊨ Label l -IEdge et→_p Exit ∧ l ≤ #:c₂›
    obtain l et where "c₂ ⊨ Label l -IEdge et→_p Exit" and "l ≤ #:c₂" by blast
    hence "c₁;;c₂ ⊨ Label l ⊕ #:c₁ -IEdge et→_p Exit ⊕ #:c₁"
      by(fastforce intro:Proc_CFG_SeqSecond)
    with ‹l ≤ #:c₂› show ?case by fastforce
  next
    case (Cond b c₁ c₂)
    from ‹∃l et. c₁ ⊨ Label l -IEdge et→_p Exit ∧ l ≤ #:c₁›
    obtain l et where "c₁ ⊨ Label l -IEdge et→_p Exit" and "l ≤ #:c₁" by blast
    hence "if (b) c₁ else c₂ ⊨ Label l ⊕ 1 -IEdge et→_p Exit ⊕ 1"
      by(fastforce intro:Proc_CFG_CondThen)
    with ‹l ≤ #:c₁› show ?case by fastforce
  next
    case (While b c')
    have "while (b) c' ⊨ Label 1 -IEdge ⇑id→_p Exit" by(rule Proc_CFG_WhileFalseSkip)
    thus ?case by fastforce
  next
    case (Call p es rets)
    have "Call p es rets ⊨ Label 1 -IEdge ⇑id→_p Exit" by(rule Proc_CFG_CallSkip)
    thus ?case by fastforce
  qed
qed


text ‹Lots of lemmas for call edges ‹…››

lemma Proc_CFG_Call_Labels:
  "prog ⊨ n -CEdge (p,es,rets)→_p n' ==> ∃l. n = Label l ∧ n' = Label (Suc l)"
by(induct prog n et≡"CEdge (p,es,rets)" n' rule:Proc_CFG.induct,auto)


lemma Proc_CFG_Call_target_0:
  "prog ⊨ n -CEdge (p,es,rets)→_p Label 0 ==> n = Entry"
by(induct prog n et≡"CEdge (p,es,rets)" n'≡"Label 0" rule:Proc_CFG.induct)
  (auto dest:Proc_CFG_Call_Labels)


lemma Proc_CFG_Call_Intra_edge_not_same_source:
  "[prog ⊨ n -CEdge (p,es,rets)→_p n'; prog ⊨ n -IEdge et→_p n''] ==> False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ n n' c₂)
  note IH = ‹∧n''. c₁ ⊨ n -IEdge et→_p n'' ==> False›
  from ‹c₁;;c₂ ⊨ n -IEdge et→_p n''› ‹c₁ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n' ≠ Exit›
  obtain nx where "c₁ ⊨ n -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG_Entry_Exit Proc_CFG_Entry)
    by(case_tac n)(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c₁ n c₂)
  from ‹c₁ ⊨ n -CEdge (p, es, rets)→_p Exit›
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case (Proc_CFG_SeqSecond c₂ n n' c₁)
  note IH = ‹∧n''. c₂ ⊨ n -IEdge et→_p n'' ==> False›
  from ‹c₁;;c₂ ⊨ n ⊕ #:c₁ -IEdge et→_p n''› ‹c₂ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry›
  obtain nx where "c₂ ⊨ n -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(cases n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n,auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c₁ n n' b c₂)
  note IH = ‹∧n''. c₁ ⊨ n -IEdge et→_p n'' ==> False›
  from ‹if (b) c₁ else c₂ ⊨ n ⊕ 1 -IEdge et→_p n''› ‹c₁ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry›
  obtain nx where "c₁ ⊨ n -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n) apply auto apply(case_tac n) apply auto
    apply(cases n) apply auto
    by(case_tac n)(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c₂ n n' b c₁)
  note IH = ‹∧n''. c₂ ⊨ n -IEdge et→_p n'' ==> False›
  from ‹if (b) c₁ else c₂ ⊨ n ⊕ #:c₁ + 1 -IEdge et→_p n''› ‹c₂ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry›
  obtain nx where "c₂ ⊨ n -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n) apply auto
     apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n,auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = ‹∧n''. c' ⊨ n -IEdge et→_p n'' ==> False›
  from ‹while (b) c' ⊨ n ⊕ 2 -IEdge et→_p n''› ‹c' ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry› ‹n' ≠ Exit›
  obtain nx where "c' ⊨ n -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(drule label_incr_ge[OF sym]) apply simp
     apply(cases n) apply auto apply(case_tac n) apply auto
    by(cases n,auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBodyExit c' n b)
  from ‹c' ⊨ n -CEdge (p, es, rets)→_p Exit›
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case Proc_CFG_Call
  from ‹Call p es rets ⊨ Label 0 -IEdge et→_p n''›
  show ?case by(fastforce elim:Proc_CFG.cases)
qed


lemma Proc_CFG_Call_Intra_edge_not_same_target:
  "[prog ⊨ n -CEdge (p,es,rets)→_p n'; prog ⊨ n'' -IEdge et→_p n'] ==> False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ n n' c₂)
  note IH = ‹∧n''. c₁ ⊨ n'' -IEdge et→_p n' ==> False›
  from ‹c₁;;c₂ ⊨ n'' -IEdge et→_p n'› ‹c₁ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n' ≠ Exit›
  have "c₁ ⊨ n'' -IEdge et→_p n'"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG_Entry dest:Proc_CFG_targetlabel_less_num_nodes) 
    by(case_tac n')(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c₁ n c₂)
  from ‹c₁ ⊨ n -CEdge (p, es, rets)→_p Exit›
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case (Proc_CFG_SeqSecond c₂ n n' c₁)
  note IH = ‹∧n''. c₂ ⊨ n'' -IEdge et→_p n' ==> False›
  from ‹c₁;;c₂ ⊨ n'' -IEdge et→_p n' ⊕ #:c₁› ‹c₂ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry›
  obtain nx where "c₂ ⊨ nx -IEdge et→_p n'"
    apply - apply(erule Proc_CFG.cases,auto)
       apply(fastforce intro:Proc_CFG_Entry_Exit)
      apply(cases n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
     apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
    apply(cases n') apply(auto dest:Proc_CFG_Call_Labels)
    by(case_tac n') auto
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c₁ n n' b c₂)
  note IH = ‹∧n''. c₁ ⊨ n'' -IEdge et→_p n' ==> False›
  from ‹if (b) c₁ else c₂ ⊨ n'' -IEdge et→_p n' ⊕ 1› ‹c₁ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry›
  obtain nx where "c₁ ⊨ nx -IEdge et→_p n'"
    apply - apply(erule Proc_CFG.cases,auto)
        apply(cases n') apply(auto intro:Proc_CFG_Entry_Exit)
       apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
      apply(cases n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
     apply(cases n') apply auto apply(case_tac n') apply auto
    apply(cases n') apply auto
    apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
    by(case_tac n')(auto dest:Proc_CFG_Call_Labels)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c₂ n n' b c₁)
  note IH = ‹∧n''. c₂ ⊨ n'' -IEdge et→_p n' ==> False›
  from ‹if (b) c₁ else c₂ ⊨ n'' -IEdge et→_p n' ⊕ #:c₁ + 1› ‹c₂ ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry›
  obtain nx where "c₂ ⊨ nx -IEdge et→_p n'"
    apply - apply(erule Proc_CFG.cases,auto)
        apply(cases n') apply(auto intro:Proc_CFG_Entry_Exit)
       apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
      apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
     apply(cases n') apply auto
      apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
     apply(case_tac n') apply(auto dest:Proc_CFG_Call_Labels)
    by(cases n',auto,case_tac n',auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = ‹∧n''. c' ⊨ n'' -IEdge et→_p n' ==> False›
  from ‹while (b) c' ⊨ n'' -IEdge et→_p n' ⊕ 2› ‹c' ⊨ n -CEdge (p, es, rets)→_p n'›
    ‹n ≠ Entry› ‹n' ≠ Exit›
  obtain nx where "c' ⊨ nx -IEdge et→_p n'"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
     apply(cases n') apply auto
    by(cases n',auto,case_tac n',auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBodyExit c' n b)
  from ‹c' ⊨ n -CEdge (p, es, rets)→_p Exit›
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case Proc_CFG_Call
  from ‹Call p es rets ⊨ n'' -IEdge et→_p Label 1›
  show ?case by(fastforce elim:Proc_CFG.cases)
qed


lemma Proc_CFG_Call_nodes_eq:
  "[prog ⊨ n -CEdge (p,es,rets)→_p n'; prog ⊨ n -CEdge (p',es',rets')→_p n'']
  ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ n n' c₂)
  note IH = ‹∧n''. c₁ ⊨ n -CEdge (p',es',rets')→_p n''
 ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹c₁;; c₂ ⊨ n -CEdge (p',es',rets')→_p n''› ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'›
  have "c₁ ⊨ n -CEdge (p',es',rets')→_p n''"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(case_tac n,(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)+)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c₁ n c₂)
  from ‹c₁ ⊨ n -CEdge (p,es,rets)→_p Exit› have False
    by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case (Proc_CFG_SeqSecond c₂ n n' c₁)
  note IH = ‹∧n''. c₂ ⊨ n -CEdge (p',es',rets')→_p n''
 ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹c₁;;c₂ ⊨ n ⊕ #:c₁ -CEdge (p',es',rets')→_p n''› ‹n ≠ Entry›
  obtain nx where edge:"c₂ ⊨ n -CEdge (p',es',rets')→_p nx" and nx:"nx ⊕ #:c₁ = n''"
    apply - apply(erule Proc_CFG.cases,auto)
    by(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes label_incr_inj)+
  from edge have "n' = nx ∧ p = p' ∧ es = es' ∧ rets = rets'" by (rule IH)
  with nx show ?case by auto
next
  case (Proc_CFG_CondThen c₁ n n' b c₂)
  note IH = ‹∧n''. c₁ ⊨ n -CEdge (p',es',rets')→_p n''
 ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹if (b) c₁ else c₂ ⊨ n ⊕ 1 -CEdge (p',es',rets')→_p n''›
  obtain nx where "c₁ ⊨ n -CEdge (p',es',rets')→_p nx ∧ nx ⊕ 1 = n''"
  proof(rule Proc_CFG.cases)
    fix c₂' nx etx nx' bx c₁'
    assume "if (b) c₁ else c₂ = if (bx) c₁' else c₂'"
      and "n ⊕ 1 = nx ⊕ #:c₁' + 1" and "nx ≠ Entry"
    with ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'› obtain l where "n = Label l" and "l ≥ #:c₁"
      by(cases n,auto,cases nx,auto)
    with ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'› have False
      by(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c₁ ⊨ n -CEdge (p',es',rets')→_p nx" 
    and nx:"nx ⊕ 1 = n''" by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_CondElse c₂ n n' b c₁)
  note IH = ‹∧n''. c₂ ⊨ n -CEdge (p',es',rets')→_p n''
 ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹if (b) c₁ else c₂ ⊨ n ⊕ #:c₁ + 1 -CEdge (p',es',rets')→_p n''›
  obtain nx where "c₂ ⊨ n -CEdge (p',es',rets')→_p nx ∧ nx ⊕ #:c₁ + 1 = n''"
  proof(rule Proc_CFG.cases)
    fix c₁' nx etx nx' bx c₂'
    assume ifs:"if (b) c₁ else c₂ = if (bx) c₁' else c₂'"
      and "n ⊕ #:c₁ + 1 = nx ⊕ 1" and "nx ≠ Entry"
      and edge:"c₁' ⊨ nx -etx→_p nx'"
    then obtain l where "nx = Label l" and "l ≥ #:c₁"
      by(cases n,auto,cases nx,auto)
    with edge ifs have False
      by(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c₂ ⊨ n -CEdge (p',es',rets')→_p nx"
    and nx:"nx ⊕ #:c₁ + 1 = n''"
    by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = ‹∧n''. c' ⊨ n -CEdge (p',es',rets')→_p n''
 ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹while (b) c' ⊨ n ⊕ 2 -CEdge (p',es',rets')→_p n''›
  obtain nx where "c' ⊨ n -CEdge (p',es',rets')→_p nx ∧ nx ⊕ 2 = n''"
    by(rule Proc_CFG.cases,auto dest:label_incr_inj Proc_CFG_Call_Labels)
  then obtain nx where edge:"c' ⊨ n -CEdge (p',es',rets')→_p nx" 
    and nx:"nx ⊕ 2 = n''" by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_WhileBodyExit c' n b)
  from ‹c' ⊨ n -CEdge (p,es,rets)→_p Exit› have False
    by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case Proc_CFG_Call
  from ‹Call p es rets ⊨ Label 0 -CEdge (p',es',rets')→_p n''›
  have "p = p' ∧ es = es' ∧ rets = rets' ∧ n'' = Label 1"
    by(auto elim:Proc_CFG.cases)
  then show ?case by simp
qed


lemma Proc_CFG_Call_nodes_eq':
  "[prog ⊨ n -CEdge (p,es,rets)→_p n'; prog ⊨ n'' -CEdge (p',es',rets')→_p n']
  ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ n n' c₂)
  note IH = ‹∧n''. c₁ ⊨ n'' -CEdge (p',es',rets')→_p n'
 ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹c₁;;c₂ ⊨ n'' -CEdge (p',es',rets')→_p n'› ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'›
  have "c₁ ⊨ n'' -CEdge (p',es',rets')→_p n'"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(case_tac n',auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c₁ n c₂)
  from ‹c₁ ⊨ n -CEdge (p,es,rets)→_p Exit› have False
    by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case (Proc_CFG_SeqSecond c₂ n n' c₁)
  note IH = ‹∧n''. c₂ ⊨ n'' -CEdge (p',es',rets')→_p n'
 ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹c₁;;c₂ ⊨ n'' -CEdge (p',es',rets')→_p n' ⊕ #:c₁›
  obtain nx where edge:"c₂ ⊨ nx -CEdge (p',es',rets')→_p n'" and nx:"nx ⊕ #:c₁ = n''"
    apply - apply(erule Proc_CFG.cases,auto)
    by(cases n',
       auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels 
                 label_incr_inj)
  from edge have "n = nx ∧ p = p' ∧ es = es' ∧ rets = rets'" by (rule IH)
  with nx show ?case by auto
next
  case (Proc_CFG_CondThen c₁ n n' b c₂)
  note IH = ‹∧n''. c₁ ⊨ n'' -CEdge (p',es',rets')→_p n'
 ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹if (b) c₁ else c₂ ⊨ n'' -CEdge (p',es',rets')→_p n' ⊕ 1›
  obtain nx where "c₁ ⊨ nx -CEdge (p',es',rets')→_p n' ∧ nx ⊕ 1 = n''"
  proof(cases)
    case (Proc_CFG_CondElse nx nx')
    from ‹n' ⊕ 1 = nx' ⊕ #:c₁ + 1›
      ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'›
    obtain l where "n' = Label l" and "l ≥ #:c₁"
      by(cases n', auto dest:Proc_CFG_Call_Labels,cases nx',auto)
    with ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'› have False
      by(fastforce dest:Proc_CFG_targetlabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c₁ ⊨ nx -CEdge (p',es',rets')→_p n'" 
    and nx:"nx ⊕ 1 = n''"
    by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_CondElse c₂ n n' b c₁)
  note IH = ‹∧n''. c₂ ⊨ n'' -CEdge (p',es',rets')→_p n'
 ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹if (b) c₁ else c₂ ⊨ n'' -CEdge (p',es',rets')→_p n' ⊕ #:c₁ + 1›
  obtain nx where "c₂ ⊨ nx -CEdge (p',es',rets')→_p n' ∧ nx ⊕ #:c₁ + 1 = n''"
  proof(cases)
    case (Proc_CFG_CondThen nx nx')
    from ‹n' ⊕ #:c₁ + 1 = nx' ⊕ 1›
      ‹c₁ ⊨ nx -CEdge (p',es',rets')→_p nx'›
    obtain l where "nx' = Label l" and "l ≥ #:c₁"
      by(cases n',auto,cases nx',auto dest:Proc_CFG_Call_Labels)
    with ‹c₁ ⊨ nx -CEdge (p',es',rets')→_p nx'›
    have False by(fastforce dest:Proc_CFG_targetlabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c₂ ⊨ nx -CEdge (p',es',rets')→_p n'" 
    and nx:"nx ⊕ #:c₁ + 1 = n''"
    by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = ‹∧n''. c' ⊨ n'' -CEdge (p',es',rets')→_p n'
 ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
  from ‹while (b) c' ⊨ n'' -CEdge (p',es',rets')→_p n' ⊕ 2›
  obtain nx where edge:"c' ⊨ nx -CEdge (p',es',rets')→_p n'" and nx:"nx ⊕ 2 = n''"
    by(rule Proc_CFG.cases,auto dest:label_incr_inj)
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_WhileBodyExit c' n b)
  from ‹c' ⊨ n -CEdge (p,es,rets)→_p Exit›
  have False by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case Proc_CFG_Call
  from ‹Call p es rets ⊨ n'' -CEdge (p',es',rets')→_p Label 1›
  have "p = p' ∧ es = es' ∧ rets = rets' ∧ n'' = Label 0"
    by(auto elim:Proc_CFG.cases)
  then show ?case by simp
qed


lemma Proc_CFG_Call_targetnode_no_Call_sourcenode:
  "[prog ⊨ n -CEdge (p,es,rets)→_p n'; prog ⊨ n' -CEdge (p',es',rets')→_p n'']
  ==> False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ n n' c₂)
  note IH = ‹∧n''. c₁ ⊨ n' -CEdge (p', es', rets')→_p n'' ==> False›
  from ‹c₁;; c₂ ⊨ n' -CEdge (p',es',rets')→_p n''› ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'›
  have "c₁ ⊨ n' -CEdge (p',es',rets')→_p n''"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c₁ n c₂)
  from ‹c₁ ⊨ n -CEdge (p,es,rets)→_p Exit› have False
    by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case (Proc_CFG_SeqSecond c₂ n n' c₁)
  note IH = ‹∧n''. c₂ ⊨ n' -CEdge (p', es', rets')→_p n'' ==> False›
  from ‹c₁;; c₂ ⊨ n' ⊕ #:c₁ -CEdge (p', es', rets')→_p n''› ‹c₂ ⊨ n -CEdge (p,es,rets)→_p n'›
  obtain nx where "c₂ ⊨ n' -CEdge (p',es',rets')→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c₁ n n' b c₂)
  note IH = ‹∧n''. c₁ ⊨ n' -CEdge (p',es',rets')→_p n'' ==> False›
  from ‹if (b) c₁ else c₂ ⊨ n' ⊕ 1 -CEdge (p', es', rets')→_p n''› ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'›
  obtain nx where "c₁ ⊨ n' -CEdge (p',es',rets')→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n') apply auto apply(case_tac n) apply auto
    apply(cases n') apply auto
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c₂ n n' b c₁)
  note IH = ‹∧n''. c₂ ⊨ n' -CEdge (p',es',rets')→_p n'' ==> False›
  from ‹if (b) c₁ else c₂ ⊨ n' ⊕ #:c₁ + 1 -CEdge (p', es', rets')→_p n''›
    ‹c₂ ⊨ n -CEdge (p,es,rets)→_p n'›
  obtain nx where "c₂ ⊨ n' -CEdge (p',es',rets')→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n') apply auto
     apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = ‹∧n''. c' ⊨ n' -CEdge (p',es',rets')→_p n'' ==> False›
  from ‹while (b) c' ⊨ n' ⊕ 2 -CEdge (p', es', rets')→_p n''› ‹c' ⊨ n -CEdge (p,es,rets)→_p n'›
  obtain nx where "c' ⊨ n' -CEdge (p',es',rets')→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
    by(cases n',auto,case_tac n,auto)+
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBodyExit c' n b)
  from ‹c' ⊨ n -CEdge (p, es, rets)→_p Exit›
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case Proc_CFG_Call
  from ‹Call p es rets ⊨ Label 1 -CEdge (p', es', rets')→_p n''›
  show ?case by(fastforce elim:Proc_CFG.cases)
qed


lemma Proc_CFG_Call_follows_id_edge:
  "[prog ⊨ n -CEdge (p,es,rets)→_p n'; prog ⊨ n' -IEdge et→_p n''] ==> et = ⇑id"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c₁ n n' c₂)
  note IH = ‹∧n''. c₁ ⊨ n' -IEdge et→_p n'' ==> et = ⇑id›
  from ‹c₁;;c₂ ⊨ n' -IEdge et→_p n''› ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'› ‹n' ≠ Exit›
  obtain nx where "c₁ ⊨ n' -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c₁ n c₂)
  from ‹c₁ ⊨ n -CEdge (p, es, rets)→_p Exit›
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case (Proc_CFG_SeqSecond c₂ n n' c₁)
  note IH = ‹∧n''. c₂ ⊨ n' -IEdge et→_p n'' ==> et = ⇑id›
  from ‹c₁;;c₂ ⊨ n' ⊕ #:c₁ -IEdge et→_p n''› ‹c₂ ⊨ n -CEdge (p,es,rets)→_p n'›
  obtain nx where "c₂ ⊨ n' -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c₁ n n' b c₂)
  note IH = ‹∧n''. c₁ ⊨ n' -IEdge et→_p n'' ==> et = ⇑id›
  from ‹if (b) c₁ else c₂ ⊨ n' ⊕ 1 -IEdge et→_p n''› ‹c₁ ⊨ n -CEdge (p,es,rets)→_p n'›
    ‹n ≠ Entry›
  obtain nx where "c₁ ⊨ n' -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n') apply auto apply(case_tac n) apply auto
    apply(cases n') apply auto
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c₂ n n' b c₁)
  note IH = ‹∧n''. c₂ ⊨ n' -IEdge et→_p n'' ==> et = ⇑id›
  from ‹if (b) c₁ else c₂ ⊨ n' ⊕ #:c₁ + 1 -IEdge et→_p n''› ‹c₂ ⊨ n -CEdge (p,es,rets)→_p n'›
  obtain nx where "c₂ ⊨ n' -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n') apply auto
     apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = ‹∧n''. c' ⊨ n' -IEdge et→_p n'' ==> et = ⇑id›
  from ‹while (b) c' ⊨ n' ⊕ 2 -IEdge et→_p n''› ‹c' ⊨ n -CEdge (p,es,rets)→_p n'›
  obtain nx where "c' ⊨ n' -IEdge et→_p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply auto
     apply(cases n') apply auto apply(case_tac n) apply auto
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBodyExit c' n et' b)
  from ‹c' ⊨ n -CEdge (p, es, rets)→_p Exit›
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case Proc_CFG_Call
  from ‹Call p es rets ⊨ Label 1 -IEdge et→_p n''› show ?case
    by(fastforce elim:Proc_CFG.cases)
qed


lemma Proc_CFG_edge_det:
  "[prog ⊨ n -et→_p n'; prog ⊨ n -et'→_p n'] ==> et = et'"
proof(induct rule:Proc_CFG.induct)
  case Proc_CFG_Entry_Exit thus ?case by(fastforce dest:Proc_CFG_EntryD)
next
  case Proc_CFG_Entry thus ?case by(fastforce dest:Proc_CFG_EntryD)
next
  case Proc_CFG_Skip thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_LAss thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_LAssSkip thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case (Proc_CFG_SeqFirst c₁ n et n' c₂)
  note edge = ‹c₁ ⊨ n -et→_p n'›
  note IH = ‹c₁ ⊨ n -et'→_p n' ==> et = et'›
  from edge ‹n' ≠ Exit› obtain l where l:"n' = Label l" by (cases n') auto
  with edge have "l < #:c₁" by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
  with ‹c₁;;c₂ ⊨ n -et'→_p n'› l have "c₁ ⊨ n -et'→_p n'"
    by(fastforce elim:Proc_CFG.cases intro:Proc_CFG.intros dest:label_incr_ge)
  from IH[OF this] show ?case .
next
  case (Proc_CFG_SeqConnect c₁ n et c₂)
  note edge = ‹c₁ ⊨ n -et→_p Exit›
  note IH = ‹c₁ ⊨ n -et'→_p Exit ==> et = et'›
  from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c₁" by(fastforce intro: Proc_CFG_sourcelabel_less_num_nodes)
  with ‹c₁;;c₂ ⊨ n -et'→_p Label #:c₁› l have "c₁ ⊨ n -et'→_p Exit"
    by(fastforce elim:Proc_CFG.cases 
                dest:Proc_CFG_targetlabel_less_num_nodes label_incr_ge)
  from IH[OF this] show ?case .
next
  case (Proc_CFG_SeqSecond c₂ n et n' c₁)
  note edge = ‹c₂ ⊨ n -et→_p n'›
  note IH = ‹c₂ ⊨ n -et'→_p n' ==> et = et'›
  from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c₂" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  with ‹c₁;;c₂ ⊨ n ⊕ #:c₁ -et'→_p n' ⊕ #:c₁› l have "c₂ ⊨ n -et'→_p n'"
    by -(erule Proc_CFG.cases,
    (fastforce dest:Proc_CFG_sourcelabel_less_num_nodes label_incr_ge
              dest!:label_incr_inj)+)
  from IH[OF this] show ?case .
next
  case Proc_CFG_CondTrue thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_CondFalse thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case (Proc_CFG_CondThen c₁ n et n' b c₂)
  note edge = ‹c₁ ⊨ n -et→_p n'›
  note IH = ‹c₁ ⊨ n -et'→_p n' ==> et = et'›
  from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c₁" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  with ‹if (b) c₁ else c₂ ⊨ n ⊕ 1 -et'→_p n' ⊕ 1› l have "c₁ ⊨ n -et'→_p n'"
    by -(erule Proc_CFG.cases,(fastforce dest:label_incr_ge label_incr_inj)+)
  from IH[OF this] show ?case .
next
  case (Proc_CFG_CondElse c₂ n et n' b c₁)
  note edge = ‹c₂ ⊨ n -et→_p n'›
  note IH = ‹c₂ ⊨ n -et'→_p n' ==> et = et'›
  from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c₂" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  with ‹if (b) c₁ else c₂ ⊨ n ⊕ (#:c₁ + 1) -et'→_p n' ⊕ (#:c₁ + 1)› l 
  have "c₂ ⊨ n -et'→_p n'"
    by -(erule Proc_CFG.cases,(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes 
                             label_incr_inj label_incr_ge label_incr_simp_rev)+)
  from IH[OF this] show ?case .
next
  case Proc_CFG_WhileTrue thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_WhileFalse thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_WhileFalseSkip thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case (Proc_CFG_WhileBody c' n et n' b)
  note edge = ‹c' ⊨ n -et→_p n'›
  note IH = ‹c' ⊨ n -et'→_p n' ==> et = et'›
  from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
  with edge have less:"l < #:c'" 
    by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  from edge ‹n' ≠ Exit› obtain l' where l':"n' = Label l'" by (cases n') auto
  with edge have "l' < #:c'" by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
  with ‹while (b) c' ⊨ n ⊕ 2 -et'→_p n' ⊕ 2› l less l' have "c' ⊨ n -et'→_p n'"
    by(fastforce elim:Proc_CFG.cases dest:label_incr_start_Node_smaller)
  from IH[OF this] show ?case .
next
  case (Proc_CFG_WhileBodyExit c' n et b)
  note edge = ‹c' ⊨ n -et→_p Exit›
  note IH = ‹c' ⊨ n -et'→_p Exit ==> et = et'›
  from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  with ‹while (b) c' ⊨ n ⊕ 2 -et'→_p Label 0› l have "c' ⊨ n -et'→_p Exit"
    by -(erule Proc_CFG.cases,auto dest:label_incr_start_Node_smaller)
  from IH[OF this] show ?case .
next
  case Proc_CFG_Call thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_CallSkip thus ?case by(fastforce elim:Proc_CFG.cases)
qed


lemma WCFG_deterministic:
  "[prog ⊨ n₁ -et₁→_p n₁'; prog ⊨ n₂ -et₂→_p n₂'; n₁ = n₂; n₁' ≠ n₂']
  ==> ∃Q Q'. et₁ = IEdge (Q)_\<surd> ∧ et₂ = IEdge (Q')_\<surd> ∧
            (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
proof(induct arbitrary:n₂ n₂' rule:Proc_CFG.induct)
  case (Proc_CFG_Entry_Exit prog)
  from ‹prog ⊨ n₂ -et₂→_p n₂'› ‹Entry = n₂› ‹Exit ≠ n₂'›
  have "et₂ = IEdge (λs. True)_\<surd>" by(fastforce dest:Proc_CFG_EntryD)
  thus ?case by simp
next
  case (Proc_CFG_Entry prog)
  from ‹prog ⊨ n₂ -et₂→_p n₂'› ‹Entry = n₂› ‹Label 0 ≠ n₂'›
  have "et₂ = IEdge (λs. False)_\<surd>" by(fastforce dest:Proc_CFG_EntryD)
  thus ?case by simp
next
  case Proc_CFG_Skip
  from ‹Skip ⊨ n₂ -et₂→_p n₂'› ‹Label 0 = n₂› ‹Exit ≠ n₂'›
  have False by(fastforce elim:Proc_CFG.cases)
  thus ?case by simp
next
  case (Proc_CFG_LAss V e)
  from ‹V:=e ⊨ n₂ -et₂→_p n₂'› ‹Label 0 = n₂› ‹Label 1 ≠ n₂'›
  have False by -(erule Proc_CFG.cases,auto)
  thus ?case by simp
next
  case (Proc_CFG_LAssSkip V e)
  from ‹V:=e ⊨ n₂ -et₂→_p n₂'› ‹Label 1 = n₂› ‹Exit ≠ n₂'›
  have False by -(erule Proc_CFG.cases,auto)
  thus ?case by simp
next
  case (Proc_CFG_SeqFirst c₁ n et n' c₂)
  note IH = ‹∧n₂ n₂'. [c₁ ⊨ n₂ -et₂→_p n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = IEdge (Q)_\√ ∧ et₂ = IEdge (Q')_\√ ∧
 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹c₁;;c₂ ⊨ n₂ -et₂→_p n₂'› ‹c₁ ⊨ n -et→_p n'› ‹n = n₂› ‹n' ≠ n₂'›
  have "c₁ ⊨ n₂ -et₂→_p n₂' ∨ (c₁ ⊨ n₂ -et₂→_p Exit ∧ n₂' = Label #:c₁)"
    apply hypsubst_thin apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
    by(case_tac n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)+
  thus ?case
  proof
    assume "c₁ ⊨ n₂ -et₂→_p n₂'"
    from IH[OF this ‹n = n₂› ‹n' ≠ n₂'›] show ?case .
  next
    assume "c₁ ⊨ n₂ -et₂→_p Exit ∧ n₂' = Label #:c₁"
    hence edge:"c₁ ⊨ n₂ -et₂→_p Exit" and n2':"n₂' = Label #:c₁" by simp_all
    from IH[OF edge ‹n = n₂› ‹n' ≠ Exit›] show ?case .
  qed
next
  case (Proc_CFG_SeqConnect c₁ n et c₂)
  note IH = ‹∧n₂ n₂'. [c₁ ⊨ n₂ -et₂→_p n₂'; n = n₂; Exit ≠ n₂']
 ==> ∃Q Q'. et = IEdge (Q)_\√ ∧ et₂ = IEdge (Q')_\√ ∧
 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹c₁;;c₂ ⊨ n₂ -et₂→_p n₂'› ‹c₁ ⊨ n -et→_p Exit› ‹n = n₂› ‹n ≠ Entry›
    ‹Label #:c₁ ≠ n₂'› have "c₁ ⊨ n₂ -et₂→_p n₂' ∧ Exit ≠ n₂'"
    apply hypsubst_thin apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
    by(case_tac n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)+
  from IH[OF this[THEN conjunct1] ‹n = n₂› this[THEN conjunct2]]
  show ?case .
next
  case (Proc_CFG_SeqSecond c₂ n et n' c₁)
  note IH = ‹∧n₂ n₂'. [c₂ ⊨ n₂ -et₂→_p n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = IEdge (Q)_\√ ∧ et₂ = IEdge (Q')_\√ ∧
 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹c₁;;c₂ ⊨ n₂ -et₂→_p n₂'› ‹c₂ ⊨ n -et→_p n'› ‹n ⊕ #:c₁ = n₂›
    ‹n' ⊕ #:c₁ ≠ n₂'› ‹n ≠ Entry›
  obtain nx where "c₂ ⊨ n -et₂→_p nx ∧ nx ⊕ #:c₁ = n₂'"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
      apply(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(fastforce dest:label_incr_inj)
  with ‹n' ⊕ #:c₁ ≠ n₂'› have edge:"c₂ ⊨ n -et₂→_p nx" and neq:"n' ≠ nx"
    by auto
  from IH[OF edge _ neq] show ?case by simp
next
  case (Proc_CFG_CondTrue b c₁ c₂)
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→_p n₂'› ‹Label 0 = n₂› ‹Label 1 ≠ n₂'›
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_CondFalse b c₁ c₂)
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→_p n₂'› ‹Label 0 = n₂› ‹Label (#:c₁ + 1) ≠ n₂'›
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_CondThen c₁ n et n' b c₂)
  note IH = ‹∧n₂ n₂'. [c₁ ⊨ n₂ -et₂→_p n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = IEdge (Q)_\√ ∧ et₂ = IEdge (Q')_\√ ∧
 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→_p n₂'› ‹c₁ ⊨ n -et→_p n'› ‹n ≠ Entry›
    ‹n ⊕ 1 = n₂› ‹n' ⊕ 1 ≠ n₂'›
  obtain nx where "c₁ ⊨ n -et₂→_p nx ∧ n' ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros simp del:One_nat_def)
     apply(drule label_incr_inj) apply(auto simp del:One_nat_def)
    apply(drule label_incr_simp_rev[OF sym])
    by(case_tac na,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (Proc_CFG_CondElse c₂ n et n' b c₁)
  note IH = ‹∧n₂ n₂'. [c₂ ⊨ n₂ -et₂→_p n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = IEdge (Q)_\√ ∧ et₂ = IEdge (Q')_\√ ∧
 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→_p n₂'› ‹c₂ ⊨ n -et→_p n'› ‹n ≠ Entry›
    ‹n ⊕ #:c₁ + 1 = n₂› ‹n' ⊕ #:c₁ + 1 ≠ n₂'›
  obtain nx where "c₂ ⊨ n -et₂→_p nx ∧ n' ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros simp del:One_nat_def)
     apply(drule label_incr_simp_rev)
     apply(case_tac na,auto,cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (Proc_CFG_WhileTrue b c')
  from ‹while (b) c' ⊨ n₂ -et₂→_p n₂'› ‹Label 0 = n₂› ‹Label 2 ≠ n₂'›
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_WhileFalse b c')
  from ‹while (b) c' ⊨ n₂ -et₂→_p n₂'› ‹Label 0 = n₂› ‹Label 1 ≠ n₂'›
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_WhileFalseSkip b c')
  from ‹while (b) c' ⊨ n₂ -et₂→_p n₂'› ‹Label 1 = n₂› ‹Exit ≠ n₂'›
  show ?case by -(erule Proc_CFG.cases,auto dest:label_incr_ge)
next
  case (Proc_CFG_WhileBody c' n et n' b)
  note IH = ‹∧n₂ n₂'. [c' ⊨ n₂ -et₂→_p n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = IEdge (Q)_\√ ∧ et₂ = IEdge (Q')_\√ ∧
 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹while (b) c' ⊨ n₂ -et₂→_p n₂'› ‹c' ⊨ n -et→_p n'› ‹n ≠ Entry›
    ‹n' ≠ Exit› ‹n ⊕ 2 = n₂› ‹n' ⊕ 2 ≠ n₂'›
  obtain nx where "c' ⊨ n -et₂→_p nx ∧ n' ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
      apply(fastforce dest:label_incr_ge[OF sym])
     apply(fastforce dest:label_incr_inj)
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (Proc_CFG_WhileBodyExit c' n et b)
  note IH = ‹∧n₂ n₂'. [c' ⊨ n₂ -et₂→_p n₂'; n = n₂; Exit ≠ n₂']
 ==> ∃Q Q'. et = IEdge (Q)_\√ ∧ et₂ = IEdge (Q')_\√ ∧
 (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹while (b) c' ⊨ n₂ -et₂→_p n₂'› ‹c' ⊨ n -et→_p Exit› ‹n ≠ Entry›
    ‹n ⊕ 2 = n₂› ‹Label 0 ≠ n₂'›
  obtain nx where "c' ⊨ n -et₂→_p nx ∧ Exit ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
     apply(fastforce dest:label_incr_ge[OF sym])
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case Proc_CFG_Call thus ?case by -(erule Proc_CFG.cases,auto)
next
  case Proc_CFG_CallSkip thus ?case by -(erule Proc_CFG.cases,auto)
qed


subsection ‹And now: the interprocedural CFG›

subsubsection ‹Statements containing calls›

text ‹A procedure is a tuple composed of its name, its input and output variables
 and its method body›

type_synonym proc = "(pname × vname list × vname list × cmd)"
type_synonym procs = "proc list"


text ‹‹containsCall› guarantees that a call to procedure p is in
 a certain statement.›

declare conj_cong[fundef_cong]

function containsCall :: 
  "procs → cmd → pname list → pname → bool"
where "containsCall procs Skip ps p ⟷ False"
  | "containsCall procs (V:=e) ps p ⟷ False"
  | "containsCall procs (c₁;;c₂) ps p ⟷
       containsCall procs c₁ ps p ∨ containsCall procs c₂ ps p"
  | "containsCall procs (if (b) c₁ else c₂) ps p ⟷
       containsCall procs c₁ ps p ∨ containsCall procs c₂ ps p"
  | "containsCall procs (while (b) c) ps p ⟷
       containsCall procs c ps p"
  | "containsCall procs (Call q es' rets') ps p ⟷ p = q ∧ ps = [] ∨
       (∃ins outs c ps'. ps = q#ps' ∧ (q,ins,outs,c) ∈ set procs ∧
                     containsCall procs c ps' p)"
by pat_completeness auto
termination containsCall
by(relation "measures [λ(procs,c,ps,p). length ps,
  λ(procs,c,ps,p). size c]") auto


lemmas containsCall_induct[case_names Skip LAss Seq Cond While Call] = 
  containsCall.induct


lemma containsCallcases: 
  "containsCall procs prog ps p
  ==> ps = [] ∧ containsCall procs prog ps p ∨
  (∃q ins outs c ps'. ps = ps'@[q] ∧ (q,ins,outs,c) ∈ set procs ∧
  containsCall procs c [] p ∧ containsCall procs prog ps' q)"
proof(induct procs prog ps p rule:containsCall_induct)
  case (Call procs q es' rets' ps p)
  note IH = ‹∧x y z ps'. [ps = q#ps'; (q,x,y,z) ∈ set procs;
 containsCall procs z ps' p]
 ==> ps' = [] ∧ containsCall procs z ps' p ∨
 (∃qx ins outs c psx. ps' = psx@[qx] ∧ (qx,ins,outs,c) ∈ set procs ∧
 containsCall procs c [] p ∧
 containsCall procs z psx qx)›
  from ‹containsCall procs (Call q es' rets') ps p›
  have "p = q ∧ ps = [] ∨
    (∃ins outs c ps'. ps = q#ps' ∧ (q,ins,outs,c) ∈ set procs ∧
                  containsCall procs c ps' p)" by simp
  thus ?case
  proof
    assume assms:"p = q ∧ ps = []"
    hence "containsCall procs (Call q es' rets') ps p" by simp
    with assms show ?thesis by simp
  next
    assume "∃ins outs c ps'. ps = q#ps' ∧ (q,ins,outs,c) ∈ set procs ∧
      containsCall procs c ps' p"
    then obtain ins outs c ps' where "ps = q#ps'" and "(q,ins,outs,c) ∈ set procs"
      and "containsCall procs c ps' p" by blast
    from IH[OF this] have "ps' = [] ∧ containsCall procs c ps' p ∨
      (∃qx insx outsx cx psx.
         ps' = psx @ [qx] ∧ (qx,insx,outsx,cx) ∈ set procs ∧
         containsCall procs cx [] p ∧ containsCall procs c psx qx)" .
    thus ?thesis
    proof
      assume assms:"ps' = [] ∧ containsCall procs c ps' p"
      have "containsCall procs (Call q es' rets') [] q" by simp
      with assms ‹ps = q#ps'› ‹(q,ins,outs,c) ∈ set procs› show ?thesis by fastforce
    next
      assume "∃qx insx outsx cx psx.
        ps' = psx@[qx] ∧ (qx,insx,outsx,cx) ∈ set procs ∧
        containsCall procs cx [] p ∧ containsCall procs c psx qx"
      then obtain qx insx outsx cx psx
        where "ps' = psx@[qx]" and "(qx,insx,outsx,cx) ∈ set procs"
        and "containsCall procs cx [] p"
        and "containsCall procs c psx qx" by blast
      from ‹(q,ins,outs,c) ∈ set procs› ‹containsCall procs c psx qx›
      have "containsCall procs (Call q es' rets') (q#psx) qx" by fastforce
      with ‹ps' = psx@[qx]› ‹ps = q#ps'› ‹(qx,insx,outsx,cx) ∈ set procs›
        ‹containsCall procs cx [] p› show ?thesis by fastforce
    qed
  qed
qed auto



lemma containsCallE:
  "[containsCall procs prog ps p;
    [ps = []; containsCall procs prog ps p] ==> P procs prog ps p;
    ∧q ins outs c es' rets' ps'. [ps = ps'@[q]; (q,ins,outs,c) ∈ set procs;
      containsCall procs c [] p; containsCall procs prog ps' q]
     ==> P procs prog ps p] ==> P procs prog ps p"
  by(auto dest:containsCallcases)


lemma containsCall_in_proc: 
  "[containsCall procs prog qs q; (q,ins,outs,c) ∈ set procs;
  containsCall procs c [] p]
  ==> containsCall procs prog (qs@[q]) p"
proof(induct procs prog qs q rule:containsCall_induct)
  case (Call procs qx esx retsx ps p')
  note IH = ‹∧x y z psx. [ps = qx#psx; (qx,x,y,z) ∈ set procs;
 containsCall procs z psx p'; (p',ins,outs,c) ∈ set procs;
 containsCall procs c [] p] ==> containsCall procs z (psx@[p']) p›
  from ‹containsCall procs (Call qx esx retsx) ps p'›
  have "p' = qx ∧ ps = [] ∨
    (∃insx outsx cx psx. ps = qx#psx ∧ (qx,insx,outsx,cx) ∈ set procs ∧
    containsCall procs cx psx p')" by simp
  thus ?case
  proof
    assume assms:"p' = qx ∧ ps = []"
    with ‹(p', ins, outs, c) ∈ set procs› ‹containsCall procs c [] p›
    have "containsCall procs (Call qx esx retsx) [p'] p" by fastforce
    with assms show ?thesis by simp
  next
    assume "∃insx outsx cx psx. ps = qx#psx ∧ (qx,insx,outsx,cx) ∈ set procs ∧
      containsCall procs cx psx p'"
    then obtain insx outsx cx psx where "ps = qx#psx" 
      and "(qx,insx,outsx,cx) ∈ set procs"
      and "containsCall procs cx psx p'" by blast
    from IH[OF this ‹(p', ins, outs, c) ∈ set procs›
      ‹containsCall procs c [] p›] 
    have "containsCall procs cx (psx @ [p']) p" .
    with ‹ps = qx#psx› ‹(qx,insx,outsx,cx) ∈ set procs›
    show ?thesis by fastforce
  qed
qed auto
    

lemma containsCall_indirection:
  "[containsCall procs prog qs q; containsCall procs c ps p;
  (q,ins,outs,c) ∈ set procs]
  ==> containsCall procs prog (qs@q#ps) p"
proof(induct procs prog qs q rule:containsCall_induct)
  case (Call procs px esx retsx ps' p')
  note IH = ‹∧x y z psx. [ps' = px # psx; (px, x, y, z) ∈ set procs;
 containsCall procs z psx p'; containsCall procs c ps p;
 (p', ins, outs, c) ∈ set procs]
 ==> containsCall procs z (psx @ p' # ps) p›
  from ‹containsCall procs (Call px esx retsx) ps' p'›
  have "p' = px ∧ ps' = [] ∨
    (∃insx outsx cx psx. ps' = px#psx ∧ (px,insx,outsx,cx) ∈ set procs ∧
    containsCall procs cx psx p')" by simp
  thus ?case
  proof
    assume "p' = px ∧ ps' = []"
    with ‹containsCall procs c ps p› ‹(p', ins, outs, c) ∈ set procs›
    show ?thesis by fastforce
  next
    assume "∃insx outsx cx psx. ps' = px#psx ∧ (px,insx,outsx,cx) ∈ set procs ∧
      containsCall procs cx psx p'"
    then obtain insx outsx cx psx where "ps' = px#psx" 
      and "(px,insx,outsx,cx) ∈ set procs"
      and "containsCall procs cx psx p'" by blast
    from IH[OF this ‹containsCall procs c ps p›
      ‹(p', ins, outs, c) ∈ set procs›] 
    have "containsCall procs cx (psx @ p' # ps) p" .
    with ‹ps' = px#psx› ‹(px,insx,outsx,cx) ∈ set procs›
    show ?thesis by fastforce
  qed
qed auto


lemma Proc_CFG_Call_containsCall:
  "prog ⊨ n -CEdge (p,es,rets)→_p n' ==> containsCall procs prog [] p"
by(induct prog n et≡"CEdge (p,es,rets)" n' rule:Proc_CFG.induct,auto)


lemma containsCall_empty_Proc_CFG_Call_edge: 
  assumes "containsCall procs prog [] p"
  obtains l es rets l' where "prog ⊨ Label l -CEdge (p,es,rets)→_p Label l'"
proof(atomize_elim)
  from ‹containsCall procs prog [] p›
  show "∃l es rets l'. prog ⊨ Label l -CEdge (p,es,rets)→_p Label l'"
  proof(induct procs prog ps≡"[]::pname list" p rule:containsCall_induct)
    case Seq thus ?case
      by auto(fastforce dest:Proc_CFG_SeqFirst,fastforce dest:Proc_CFG_SeqSecond)
  next
    case Cond thus ?case
      by auto(fastforce dest:Proc_CFG_CondThen,fastforce dest:Proc_CFG_CondElse)
  next
    case While thus ?case by(fastforce dest:Proc_CFG_WhileBody)
  next
    case Call thus ?case by(fastforce intro:Proc_CFG_Call)
  qed auto
qed


subsubsection‹The edges of the combined CFG›

type_synonym node = "(pname × label)"
type_synonym edge = "(node × (vname,val,node,pname) edge_kind × node)"

fun get_proc :: "node → pname"
  where "get_proc (p,l) = p"


inductive PCFG :: 
  "cmd → procs → node → (vname,val,node,pname) edge_kind → node → bool" 
(‹_,_ ⊨ _ -_→ _› [51,51,0,0,0] 81)
for prog::cmd and procs::procs
where

  Main:
  "prog ⊨ n -IEdge et→_p n' ==> prog,procs ⊨ (Main,n) -et→ (Main,n')"

| Proc:
  "[(p,ins,outs,c) ∈ set procs; c ⊨ n -IEdge et→_p n';
    containsCall procs prog ps p]
  ==> prog,procs ⊨ (p,n) -et→ (p,n')"


| MainCall:
  "[prog ⊨ Label l -CEdge (p,es,rets)→_p n'; (p,ins,outs,c) ∈ set procs]
  ==> prog,procs ⊨ (Main,Label l)
                  -(λs. True):(Main,n')↪map (λe cf. interpret e cf) es→ (p,Entry)"

| ProcCall:
  "[(p,ins,outs,c) ∈ set procs; c ⊨ Label l -CEdge (p',es',rets')→_p Label l';
    (p',ins',outs',c') ∈ set procs; containsCall procs prog ps p]
  ==> prog,procs ⊨ (p,Label l)
               -(λs. True):(p,Label l')↪_'map (λe cf. interpret e cf) es'→ (p',Entry)"

| MainReturn:
  "[prog ⊨ Label l -CEdge (p,es,rets)→_p Label l'; (p,ins,outs,c) ∈ set procs]
  ==> prog,procs ⊨ (p,Exit) -(λcf. snd cf = (Main,Label l'))↩
       (λcf cf'. cf'(rets [:=] map cf outs))→ (Main,Label l')"

| ProcReturn:
  "[(p,ins,outs,c) ∈ set procs; c ⊨ Label l -CEdge (p',es',rets')→_p Label l';
   (p',ins',outs',c') ∈ set procs; containsCall procs prog ps p]
  ==> prog,procs ⊨ (p',Exit) -(λcf. snd cf = (p,Label l'))↩_'
       (λcf cf'. cf'(rets' [:=] map cf outs'))→ (p,Label l')"

| MainCallReturn:
  "prog ⊨ n -CEdge (p,es,rets)→_p n'
  ==> prog,procs ⊨ (Main,n) -(λs. False)_\<surd>→ (Main,n')"

| ProcCallReturn:
  "[(p,ins,outs,c) ∈ set procs; c ⊨ n -CEdge (p',es',rets')→_p n';
    containsCall procs prog ps p]
  ==> prog,procs ⊨ (p,n) -(λs. False)_\<surd>→ (p,n')"


end